Search code examples
z3smt-lib

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)))
Solution

  • 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.)