1

Z3py returns unknown for the following simple problem using pow() function. 

import z3;

goal = z3.Goal();
goal = z3.Then('purify-arith','nlsat');
solver = goal.solver();

x = z3.Real('x');
solver.add(x <= 1.8);
solver.add(x >= 0);

z = 10**x;
#z = pow(10,x) returns same result

solver.add(z >= 0, z <= 1.8);
print solver.check()

returns

unknown

Obviously x = 0, z = 1 is a satisfactory solution. Any suggestions in changing the way the equations are constructed, or modifying the tactics are appreciated.

Alex Allen
  • 39
  • 7

1 Answers1

2

There may be some bug, but the following returns a model of x = 0 and z = 1, even though it gives unknown. Assuming the Python API also shows this model, you could create a simple hack to extract the model and add it to the assertions to check, similar to how this prevents future models from reusing old model values: Z3: finding all satisfying models

Here's the example (rise4fun link: http://rise4fun.com/Z3/dPnI ): 

(declare-const x Real)
(declare-const z Real)

(assert (>= x 0.0))
(assert (<= x 1.8))
(assert (= z (^ 10.0 x)))
(assert (<= z 1.8))
(assert (>= z 0.0))

(apply (repeat (then purify-arith simplify ctx-simplify ctx-solver-simplify nlsat qfnra-nlsat))) ; gives:
; (goals
;(goal
;  (>= x 0.0)
;  (<= x (/ 9.0 5.0))
;  (<= (^ 10.0 x) (/ 9.0 5.0))
;  (>= (^ 10.0 x) 0.0)
;  :precision precise :depth 44)
;)

; (apply (repeat (then (repeat purify-arith) (repeat simplify) (repeat ctx-simplify) (repeat ctx-solver-simplify)  (repeat nlsat)  (repeat qfnra-nlsat))))

(check-sat) ; unknown
;(check-sat-using qfnra-nlsat) ; unknown

(get-model) ; gives x = 0.0 and z = 1.0 even though unknown from check-sat

; could extract 0 and 1 in python API and check whether it's sat:
(assert (= x 0))
(assert (= z 1))

(check-sat) ; sat

You might also be interested in this related post: Z3 support for square root

For completeness, here's the model extraction idea in Python that seems to work (using 4.3.3, probably a build from unstable, but a while ago likely):

import z3;

print z3.get_version_string();

goal = z3.Goal();
goal = z3.Then('purify-arith','nlsat');
#solver = goal.solver();

solver = z3.Solver();

x = z3.Real('x');
z = z3.Real('z');
solver.add(x <= 1.8);
solver.add(x >= 0);
solver.add(z == 10.0 ** x);

# z = 10**x;
#z = pow(10,x) returns same result

solver.add(z >= 0, z <= 1.8);

print solver

print solver.check()
print solver.model()

m = solver.model()

solver.add(x == m[x])
solver.add(z == m[z])

print solver

print solver.check()

This gives:

D:\>python exponent.py
4.3.3
[x <= 9/5, x >= 0, z == 10**x, z >= 0, z <= 9/5]
unknown
[x = 0, z = 1]
[x <= 9/5,
 x >= 0,
 z == 10**x,
 z >= 0,
 z <= 9/5,
 x == 0,
 z == 1]
sat
Community
  • 1
  • 1
Taylor T. Johnson
  • 2,834
  • 16
  • 17
  • Based on some other odd behavior (e.g., in the square roots) and not being able to find `^` in the SMT-LIB documents, does `^` mean exponentiation? Other things like pow and ** don't seem to be defined. – Taylor T. Johnson May 04 '15 at 21:14
  • Thanks a lot for your help Prof. Johnson. Your answer solved my problem. As a side note, in your SMT code, you used the tactical apply (repeat (then (repeat purify-arith) (repeat simplify) (repeat ctx-simplify) (repeat ctx-solver-simplify) (repeat nlsat) (repeat qfnra-nlsat)))) . Do you recommend that as a "default" tactical for hard non-linear problems? What is your "everyday" tactical setting? Thanks! – Alex Allen May 05 '15 at 22:16
  • Happy to help! I don't think the simplify stuff is helping much: if `qfnra-nlsat` can't solve a nonlinear real (or coerced integer) problem, probably the simplifiers won't help. I had more so included this because it was a little odd a model was found, but the result was unknown (but Z3 has some options for partial model construction and returning the last model checked, it's just interesting it didn't try what the hack is doing to just plug in the model it found and check it, which I hoped the simplifier might try). – Taylor T. Johnson May 06 '15 at 03:27