CODEWITHSUNDEEP
z3smt
Dingbao Xie
Dingbao Xie

Reputation: 736

Is this file compliant with the SMT2.0 standard?

Click to see the file

Is this file compliant with the SMT2.0 standard? At least, z3 can accpet it. By the way, what's the difference between 'declare-const' and 'declare-fun'? For example, in order to declare a Bool variable I can write declare-const a Bool or declare-fun a() Bool.

Upvotes: 1

Views: 283

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

I am unable to locate the file you mention in the post, but to answer your question about declare-const:

(declare-const a Bool)

means the same as 

(declare-fun a () Bool)

declare-const is not part of standard SMT-LIB2. It is a command added to Z3 for the convenience of entering SMT-LIB2 benchmarks manually. You can always use declare-fun instead to be compatible across solvers.

While Z3 can process SMT-LIB2 compliant files. On the other hand, there are several other extensions in Z3's input format that are not part of SMT-LIB2 standard. To mention some:

  • declare-datatypes. Declaration of algebraic datatypes is a Z3 specific extension.

  • tactics and solvers. Creation, composition and application of tactics is specific to Z3.

  • declare-rel, declare-var, rule, query. These commands are used by the fixedpoint solver for the convenience of entering benchmarks as Horn formulas.

Upvotes: 1

Related Questions