Get expression using Z3 solver

Question

I am new to Z3 solver and SMTLib2. I want to obtain expressions for each variable in the constraints. Assume, I have this program.

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= x (+ y 1)))
(assert (= z (+ x 10)))
(check-sat)
(get-value (z))

Using get-value, I can obtain the value for z that satisfies all the constraints. But, how can I get the expression for z. Something like z=y+11.

I find that using simplify, I can simplify the constraints but is there anyway to get expression for each variable in the constraints.

Answer 1

Z3 is first and formost an SMT solver; it solves existential problems, i.e., it will only show that there exists a solution, it will not compute a closed form of all solutions.

That said, there are some ways in which at least some results of that form can be obtained, for instance via simplification as mentioned, or perhaps via quantifier elimination if the logic permits it (see for instance Equivalent Quantifier Free Formulas, or Quantifier Elimination - More questions).

If more than one but perhaps not all models are required, look into Z3: finding all satisfying models and search for multiple other questions of similar title.