Question about define-const

[Jake Vossen]

Hey everyone, I am trying to write my own parser for SMT-LIB2, and am wondering if someone could explain to me what is up with `define-const`?

From my understanding it is not part of the language, but Z3 and CVC4 both seem to accept it. This old post seems to suggest that it is specifically not part of the language: https://cs.nyu.edu/pipermail/smt-lib/2015/000863.html.

So if I was just writing a parser for SMT-LIB 2 - should `(define-const t (_ BitVec 8) (ite p u v))` be something that is valid? Do you think I should parse it anyways even if it is not part of the standard? Is there a list of other things that fall into this bucket of not part of the standard, but implemented by the major solvers?

Let me know what you guys think.

[Clark Barrett]

Hi Jake,

You are correct that define-const is not part of the standard (as opposed to declare-const which is).  In general, you should not have to implement any solver-specific extensions like this, unless you are working with a particular application that targets an extended language.  The SMT-LIB benchmark library, for example, uses only standard-compliant commands.

-Clark

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/1c0d862b-cc16-4e8b-abdf-896f9f4baee4n%40googlegroups.com.

[Jake Vossen]

Clark,

Thank you! I also learned about the benchmarks, which are going to be useful in my testing. 

Have a good one, I appreciate your help.