Z3py 使用 pow() 函数返回未知方程 [英] Z3py returns unknown for equation using pow() function

问题描述

Z3py 使用 pow() 函数返回以下简单问题的未知数.

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

返回

unknown

显然 x = 0, z = 1 是一个令人满意的解决方案.任何关于改变方程构建方式或修改策略的建议表示赞赏.

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.

推荐答案

可能有些bug，但是下面返回的是x = 0 和 z = 1 的模型>，即使它给未知.假设 Python API 也显示此模型，您可以创建一个简单的 hack 来提取模型并将其添加到断言中进行检查，类似于这如何防止未来模型重用旧模型值:Z3:找到所有满意的模型

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

示例如下(rise4fun 链接:http://rise4fun.com/Z3/dPnI):

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

您可能还对这篇相关文章感兴趣:Z3 对平方根的支持

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

为了完整起见，以下是 Python 中似乎可行的模型提取思想(使用 4.3.3，可能是从不稳定的构建，但可能是不久前的):

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

这给出:

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

这篇关于Z3py 使用 pow() 函数返回未知方程的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！