Z3py使用pow（）函数为方程返回未知数

Question

对于使用pow（）函数的以下简单问题，Z3py返回未知数。

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是一个令人满意的解决方案。任何改变方程式构建方式或修改策略的建议都值得赞赏。

Answer 1

可能有一些错误，但以下返回的模型为x = 0和z = 1，即使它给出未知。假设Python API也显示这个模型，你可以创建一个简单的黑客来提取模型并将其添加到断言来检查，类似于如何防止未来模型重用旧模型值：Z3: finding all satisfying models

下面是示例rise4fun链接：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 support for square root

为了完整起见，这里是在Python的模型提取的想法，似乎工作（使用4.3.3，大概从不稳定的建立，但不久前可能）：

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