[Python Z3 Interface] Retrieve partial/full model even if z3 solver gives status "Unknown"

[lahiri-phdworks]

Intention :

Z3 solver interface exposes a check() function which sometimes returns "unknown" status when invoked on constraints involving quantified expressions. When model() function is called on z3.status with unknown it raises model not available exception. Want to get a partial model out from z3.

Issue :

Using the sexpr() function and adding in the set-options properly, z3 can be used to get a model even for unknown result. I have attached an example below.

Can z3's python API be used to retrieve such a model (bypassing the exception) ?

Python Code & SMT LIB Code

# -*- coding: utf-8 -*-
​
from z3 import *
​
x, y, z = Reals('x y z')
m, n, l = Reals('m n l')
u, v = Ints('u v')
​
S = SolverFor("NRA")
​
S.add(x >= 0)
S.add(y >= 30, z <= 50)
S.add(m >= 5, n >= 5)
S.add(m * x + n * y + l > 300)
​
S.add(ForAll([u, v], Implies(m * u + n * v + l > 300, u + v + z <= 50)))
​
print(S.check())
print(S.sexpr())

below is the stack trace for the run when I call print(S.model()) after print(S.check())

unknown
Traceback (most recent call last):

  File "C:\Python38\Lib\site-packages\z3\z3.py", line 6696, in model
    return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)

  File "C:\Python38\Lib\site-packages\z3\z3core.py", line 3759, in Z3_solver_get_model
    _elems.Check(a0)

  File "C:\Python38\Lib\site-packages\z3\z3core.py", line 1385, in Check
    raise self.Exception(self.get_error_message(ctx, err))

Z3Exception: b'there is no current model'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):

  File "C:\Users\lahir\Documents\GitHub\codersguild\Research\tangram-solve\z3_tryouts.py", line 19, in <module>
    print(S.model())

  File "C:\Python38\Lib\site-packages\z3\z3.py", line 6698, in model
    raise Z3Exception("model is not available")

Z3Exception: model is not available

Equivalent SMT File.

(set-option :print-success true) 
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(set-option :produce-proofs true) ; enable proof generation
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun l () Real)
(assert (>= x 0.0))
(assert (>= y 30.0))
(assert (<= z 50.0))
(assert (>= m 5.0))
(assert (>= n 5.0))
(assert (not (<= (+ (* m x) (* n y) l) 300.0)))
(assert (forall ((u Int) (v Int))
  (let ((a!1 (<= (+ (* m (to_real u)) (* n (to_real v)) l) 300.0)))
    (or (<= (+ (to_real u) (to_real v) z) 50.0) a!1))))
(check-sat)
(get-model)

I now pass it to z3 on the cmd-line

$ z3 example.smt2 

Partial Model Output :

success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
unknown
(model 
  (define-fun z () Real
    20.0)
  (define-fun y () Real
    30.0)
  (define-fun l () Real
    145.0)
  (define-fun x () Real
    0.0)
  (define-fun n () Real
    5.0)
  (define-fun m () Real
    5.0)
)

Any suggestions or code examples regarding the same can be very helpful.

[lahiri-phdworks]

Actually we would be running z3 on a more advanced cases as shown below. Can this issue be related to using NRA with quantification and uninterpreted functions?

# -*- coding: utf-8 -*-

from z3 import *
HYPOTENUSE = 150
BOUND_X = 400
BOUND_Y = 400

LT1_x1, LT1_y1 = Reals('LT1_x1 LT1_y1')
LT1_x2, LT1_y2 = Reals('LT1_x2 LT1_y2')
LT1_u, LT1_v, LT1_m = Reals('LT1_u LT1_v LT1_m')

LT1_a1, LT1_b1, LT1_c1 = Reals('LT1_a1 LT1_b1 LT1_c1')
LT1_a2, LT1_b2, LT1_c2 = Reals('LT1_a2 LT1_b2 LT1_c2')
LT1_a3, LT1_b3, LT1_c3 = Reals('LT1_a3 LT1_b3 LT1_c3')

S = SolverFor("NRA")

S.add((LT1_u - LT1_x1) ** 2 + (LT1_v - LT1_y1) ** 2 == (HYPOTENUSE ** 2)/2)
S.add((LT1_u - LT1_x2) ** 2 + (LT1_v - LT1_y2) ** 2 == (HYPOTENUSE ** 2)/2)
S.add((LT1_x2 - LT1_x1) ** 2 + (LT1_y2 - LT1_y1) ** 2 == HYPOTENUSE ** 2)

S.add(LT1_a1 * LT1_a2 + LT1_b1 * LT1_b2 == 0)
S.add(LT1_a3 + LT1_m * LT1_b3 == 0)

S.add(LT1_a1 * LT1_u + LT1_b1 * LT1_v + LT1_c1 == 0)
S.add(LT1_a2 * LT1_u + LT1_b2 * LT1_v + LT1_c2 == 0)

S.add(LT1_u >= 0, LT1_v >= 0)
S.add(LT1_u <= BOUND_X, LT1_v <= BOUND_Y)

S.add(LT1_x1 >= 0, LT1_x2 >= 0)
S.add(LT1_y1 >= 0, LT1_y2 >= 0)

S.add(LT1_b1 != 0)
S.add(LT1_b2 != 0)
S.add(LT1_b3 != 0)

doodle = Function("doodle_function", RealSort(), RealSort(), BoolSort())
covered_by = Function("covers", RealSort(), RealSort(), RealSort())
lt1_area_piece = Function("lt1_area_piece", RealSort(), RealSort(), BoolSort())

x = Int('tx')
y = Int('ty')
S.add(x >= 0, y >= 0, x <= BOUND_X, y <= BOUND_Y)

S.add(ForAll([x, y], lt1_area_piece(x, y) == And(
            (LT1_a1 * x + LT1_b1 * y + LT1_c1)/LT1_b1 > 0, 
            (LT1_a2 * x + LT1_b2 * y + LT1_c2)/LT1_b2 > 0, 
            (LT1_a3 * x + LT1_b3 * y + LT1_c3)/LT1_b3 < 0
        )
    ))

S.add(ForAll([x, y], Implies(lt1_area_piece(x, y), covered_by(x, y) == 3)))

print(S.check())
print(S.sexpr())

[lahiri-phdworks]

This the trial it is taking on the models

(model-del k!0)
(model-add z () Real (ite k!0 50.0 (+ 50.0 1.0)))
(model-del k!1)
(model-add l () Real (- k!1 (+ (* m x) (* n y))))
(model-del k!2)
(model-add x () Real (ite k!2 0.0 (+ 0.0 (- 1.0))))
(model-del k!3)
(model-add y () Real (ite k!3 30.0 (+ 30.0 (- 1.0))))
(model-del k!4)
(model-add m () Real (ite k!4 5.0 (+ 5.0 (- 1.0))))
(model-del k!5)
(model-add n () Real (ite k!5 5.0 (+ 5.0 (- 1.0))))
(model-del k!6)
(model-add k!1 () Real (ite k!6 300.0 (+ 300.0 1.0)))
(model-del k!7)
(model-add k!6 () Bool (not k!7))
(model-add k!2 () Bool true)
(model-add k!3 () Bool true)
(model-add k!0 () Bool true)
(model-add k!4 () Bool true)
(model-add k!5 () Bool true)
(model-add k!7 () Bool true)

[NikolajBjorner]

There isn't any model to give you. The trail you see are instructions that lets z3 transform a model found for a simplified formula into a model of the original formula. It doesn't imply that z3 is able to find a model for the formula. You are using quantifiers and division and non-linear functions. This cocktail isn't playing well with the main solvers that handle NRA. Remove the division whenever possible. For example, if LT1_b1 is never 0, you can just use multiplication for the same checks, e.g. X * Y > 0 instead of X / Y > 0, and even better you can spell out the cases:

X / Y > 0 becomes (X > 0 and Y > 0) or (X < 0 and Y < 0)

[lahiri-phdworks]

Thanks for telling me.

Will this statement also cause issues ? S.add((LT1_u - LT1_x1) ** 2 + (LT1_v - LT1_y1) ** 2 == (HYPOTENUSE ** 2)/2).

[NikolajBjorner]

There are hooks to handle powers and convert them to multiplication for the solvers that only understand multiplication. But it is not comprehensively tested so I had to fix bugs in these scenarios a number of times before based on either fuzz or users.

[lahiri-phdworks]

NRA + functions work well with Z3 actually. It is wonderful. What is failing in my case is the universal quantification over NRA with uninterpreted functions.