使用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解算器）。