CODEWITHSUNDEEP
z3smtz3py
user12843894
user12843894

Reputation: 77

How to define un-declared type in Z3 Solver

I'm using SMT Solver Z3 to solve the constraints. for example:

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)

// SAT

However, how if we don't know what is the type of the variable a, is there any way to define un-declared variables and get the expected results of that variable with solving the constraints

Upvotes: 1

Views: 486

Answers (1)

alias
alias

Reputation: 30428

Short answer: No.

SMTLib (the language z3 and many other SMT solvers accept) is a many-sorted first-order logic. This means every variable has to have a known type during its declaration. The type can be one of the base types supported by the language (Int, Real, Bool etc.), or it can be a user-defined type, via the declare-datatype or declare-sort constructs.

See the language definition for details: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

If you're trying to model a "dynamically" typed language (like Lisp, Python, etc.), then the usual trick is to declare a union of types that the variable can belong to, and switch accordingly as you interpret that language. But doing so directly in SMTLib can be rather verbose and error-prone, you're better of using a high-level interface like z3py or any of the high-level language bindings to z3, from Java, C, Haskell, Scala, etc. But in any of these encodings, it'll be up to you to make sure the types are properly stored and changed, the underlying language of SMTLib will remain strongly typed as described in the standard I linked above.

Upvotes: 1

Related Questions