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