使用Z3和SMT-LIB定义具有实数的sqrt函数

2 回答

• 2

  假设您的公式是量化的，那么您可以通过引入新变量和添加约束来隐式定义平方根 . 例如，您可以写：

  (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中使用幂的推理在某种程度上是有限的，所以它实际上取决于你的公式说明这个公式是否将以与关系编码相同的方式处理 .

  回复于 2024-04-20T11:09:25+08:00
• 1

  如果你实际上不需要函数，那么将y定义为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最简单的方法是使用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)
  

  Nikolaj定义函数 is_sqrt 的想法也是一个有趣的想法，并且具有无量词的优点，因此它可以与nlsat（Z3中最强大的非线性求解器）一起使用 .

  回复于 2024-04-20T11:09:25+08:00