Z3對平方根的支持

Question

我一直在搜索z3提供的平方根功能。例如，爲了添加一個關於實數x的約束，即x * x = 2，對它進行編碼的最佳方法是什麼？

我想：

(declare-const x Real) 
(assert (= 2 (* x x))) 
(check-sat) 

結果是未知的。該模型也是不可用的。

但是，我相信應該有一種方法來滿足這一點。我指的是嚴格的擴展版本的smt-lib 2.0語言，而不是python api。

Answer 1

您需要使用非線性求解器。你的例子沒有自動檢測和使用它的原因是因爲常數爲2：這被解析爲一個整數而不是真實的，所以它在技術上是整數和實數的組合理論，而非線性解算器可能只涉及實數，除非你強迫它。要強制其使用，您可以使用check-sat-using和非線性求解qfnra-nlsat（rise4fun鏈接：http://rise4fun.com/Z3/fXDp）：

(declare-const x Real) 

(push) 
(assert (= 2 (* x x))) 
(check-sat-using qfnra-nlsat) ; sat 
(get-model) 
; may have to play with printing options as this is irrational (or this may be a bug) 
; (model 
; (define-fun x() Real 
; (/ 5.0 4.0)) 
;) 
(pop) 

; the reason you need to use check-sat-using is because the 2 gets parsed into an integer; to force it to be a real, use a decimal: 
(push) 
(assert (= 2.0 (* x x))) 

(check-sat) ; sat 
(get-model) 
;(model 
; (define-fun x() Real 
; (root-obj (+ (^ x 2) (- 2)) 1)) 
;) 
(pop) 

對於普通指數（平方根等），你可以使用^爲冪：

; you can also use^for exponentiation  
(push) 
(assert (= 2.0 (^ x 2.0))) 
(check-sat) ; sat 
(get-model) 
; (model 
; (define-fun x() Real 
; (root-obj (+ (^ x 2) (- 2)) 1)) 
;) 
(pop) 

; to represent square root, etc., you may use fractional or decimal exponents 
(push) 
(assert (= 25.0 (^ x 0.5))) ; square root: 2 = sqrt(x) 
(check-sat) ; sat 
(get-model) 
; maybe a bug or have to tune the model printer 
;(model 
; (define-fun x() Real 
; (- 1.0)) 
;) 
(pop) 

(push) 
(assert (= 2.0 (^ x (/ 1.0 3.0)))) 
(check-sat) ; sat 
(get-model) 
;(model 
; (define-fun x() Real 
; 8.0) 
;) 
(pop) 

(push) 
(assert (= 10.0 (^ x 0.2))) 
(check-sat) ; sat 
(get-model) 
;(model 
; (define-fun x() Real 
; 100000.0) 
;) 
(pop) 

這是一個古老的，但相關的職位：z3/python reals

一些印刷問題，例如，如果你需要的十進制近似值，可以通過使用固定：

(set-option :pp.decimal true)