使用Z3和SMT-LIB以實數定義sqrt函數

Question

如何以smt-libv2格式編寫sqrt函數。

備註： 要獲得最多兩個值，我找到了一個有用的鏈接：Use Z3 and SMT-LIB to get a maximum of two values。

Answer 1

假設您的公式是免費量化的，那麼您可以通過引入新變量和添加約束來隱式定義平方根。 例如，你可以寫：

(define-fun is_sqrt ((x Real) (y Real)) Bool (= y (* x x))) 

然後 'x' 爲 'Y' 的平方根;如果你只是想非負平方根，則：

(define-fun is_sqrt ((x Real) (y Real)) Bool (and (>= x 0) (= y (* x x)))) 

對於您的斷言每次發生，你有一個平方根，引入一個新的變量，並插上新的變量到那個地方。然後添加斷言

(assert (is_sqrt fresh-variable sub-term)) 

Z3還提供了一個內置的操作符，用於將條件提升爲功率。 你可以用它來得到一個平方根。所以寫的「X」，平方根 你可以寫術語：

(^ x 0.5) 

使用Z3權力的結論是比較有限的，所以這真的取決於你的公式表示，這一提法是否將被處理與關係編碼一樣。

Answer 2

如果你實際上並不需要的功能，那麼最簡單的方式來定義Ÿ爲X平方根是斷言Y * Y = X，即：

; This will cause Z3 to return a decimal answer instead of a root-obj 
(set-option :pp.decimal true) 

; Option 1: inverse of multiplication. This works fine if you don't actually 
; need to define a custom function. This will find y = 1.414... or y = -1.414... 
(declare-fun y() Real) 
(assert (= 2.0 (* y y))) 

; Do this if you want to find the positive root y = 1.414... 
(assert (>= y 0.0)) 

(check-sat) 
(get-value (y)) 
(reset) 

我使用未解釋函數嘗試另一種方法是這樣的：

; Option 2: uninterpreted functions. Unfortunately Z3 seems to always return 
; 'unknown' when sqrt is defined this way. Here we ignore the possibility that 
; x < 0.0; fixing this doesn't help the situation, though. 
(declare-fun sqrt (Real) Real) 
(assert (forall ((x Real)) (= x (* (sqrt x) (sqrt x))))) 
(declare-fun y() Real) 
(assert (= y (sqrt 2.0))) 
(check-sat) 
(reset) 

最後，迄今爲止最容易，如果你正在使用Z3是使用內置的PO如Nikolaj所建議的那樣。您可以根據函數圍繞想法：

; Option 3: built-in power operator. This is not standard SMT-LIB, but works 
; well with Z3. 
(define-fun sqrt ((x Real)) Real (^ x 0.5)) 
(declare-fun y() Real) 
(assert (= y (sqrt 2.0))) 
(check-sat) 
(get-value (y)) 
(reset) 

定義一個函數is_sqrt的尼古拉的想法也是一個有趣的想法，並且具有的優點在於它是量詞免費的，所以它會與nlsat工作（上最強大的非線性Z3解算器）。