CODEWITHSUNDEEP
z3smt-lib
Tilo RC
Tilo RC

Reputation: 15

Can the type of a variable in Z3 be dynamically redefined in a formula?

For example, consider the formula from SymPy's new assumptions:

(x>2) & (y>0) & (Q.integer(y) | (y>10))

The expressions (Q.integer(y) | (y>10)) means that y is an integer or y is greater than 10 (or both). If it's not an integer then it would be a real number. Is there a way to translate this into SMT-LIB format? Or would you simply have to consider the case where Q.integer(y) is true and the case where Q.integer(y) is false?

I tried researching this information online but I couldn't find anything that would provide a way to to do what I asked. I suspect that this isn't possible and after declaring the type of a variable it can not be changed. Something I tried that obviously doesn't work:

(declare-const y Real)
(assert (or (> y 10) (declare-const y Int)))

Upvotes: 0

Views: 89

Answers (1)

alias
alias

Reputation: 30497

SMTLib is a statically typed-language, meaning every-variable has a given sort (i.e., Real/Integer/etc.), and that type is fixed. That is, variables cannot change their type "dynamically."

I suspect what you're trying to say is a little different actually. You want y to not have a fraction under certain conditions. This is how you write that in SMTLib:

(declare-const y Real)

(assert (or (> y 10)
            (exists ((x Int)) (= y (to_real x)))))

The above says either y > 10, or there is an integer that when converted equals y. Given this, you can have:

(assert (= y 2.3))
(check-sat)

which produces:

unsat

OR, you can have:

(assert (= y 3))
(check-sat)

which will be sat.

Having said that, I should add when you mix integers and reals like this, you'll find yourself in the semi-decidable fragment of the combined logic: That is, the solver is likely to say unknown when the constraints get sufficiently complicated. (Another way to put this: There's no decision procedure for mixed integer-real arithmetic, as otherwise you could solve Diophantine equations, which is an undecidable problem.)

Upvotes: 0

Related Questions