1

With the z3/python web interface, if I ask:

x = Real ('x')
solve(x * x == 2, show=True)

I nicely get:

Problem:
[x·x = 2]
Solution:
[x = -1.4142135623?]

I thought the following smt-lib2 script would have the same solution:

(set-option :produce-models true)
(declare-fun s0 () Real)
(assert (= 2.0 (* s0 s0)))
(check-sat)

Alas, I get unknown with z3 (v3.2).

I suspect the problem is with the non-linear term (* s0 s0), which the python interface somehow doesn't suffer from. Is there a way to code the same in smt-lib2 to get a model?

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
alias
  • 28,120
  • 2
  • 23
  • 40

1 Answers1

1

Try your example with Z3 web interface, I get a result of sat.

Z3 web interface and Z3Py are based on Z3 v4.0, so I think the problem is fixed in the upcoming release.

pad
  • 41,040
  • 7
  • 92
  • 166
  • Quite right! And this is what it returns for the value of s0: ((s0 (root-obj (+ (^ x 2) (- 2)) 1))) I'm curious how the "root-obj" function is interpreted; and how other tools querying Z3 can get a real-number out of it. – alias Apr 03 '12 at 04:42
  • Z3 4.0 uses root-obj to repredent algebraic irrational numbers. It consists of a univariate polynomial and an index. The root-obj above is representing the first root of x^2 - 2, which is -1.41... We can ask the SMT 2.0 to display the results in decimal notation by using '(set-option :pp-decimal true)'. I used decimals by default in z3py because the goal is to reach a crowd that is not used to constraint solving and algebraic number theory. – Leonardo de Moura Apr 05 '12 at 01:55
  • More information about the new nonlinear arithmetic procedure in z3 4.0 can be found here http://research.microsoft.com/apps/pubs/default.aspx?id=159549 – Leonardo de Moura Apr 05 '12 at 01:58
  • Thanks Leonardo. Are there some restrictions regarding mixing and matching of integer coefficients? I noticed that the following works:http://rise4fun.com/Z3Py/xCU, but the integer coefficient version doesn't: http://rise4fun.com/Z3Py/TDA – alias Apr 13 '12 at 04:55
  • 1
    @LeonardodeMoura: Repeating earlier comment, in case it missed your attention: Are there some restrictions regarding mixing and matching of integer coefficients? I noticed that the following works:rise4fun.com/Z3Py/xCU, but the integer coefficient version doesn't: rise4fun.com/Z3Py/TDA – alias Apr 18 '12 at 07:53
  • Z3 uses a collection of solvers. It decides which one to use based on the input. Since nlsat has limited support for integers, it is not automatically selected for mixed integer/real problems. NLSAT treats integers as reals. In a post-processing step, I set a `sat` result to `unknown` if an integer constant is assigned to a real value. BTW, you can force Z3 to use nlsat using tactics: http://rise4fun.com/Z3Py/Z1j. In this example it works, and finds the solution. – Leonardo de Moura Apr 18 '12 at 15:42
  • Note that the option name is (now) pp.decimal, not pp-decimal. So `(set-option :pp.decimal true)`. – Chris Pacejo Mar 26 '21 at 01:10