2

我想知道以下两条语句有什么区别-

声明 1

(define-fun max_integ ((x Int) (y Int)) Int 
  (ite (< x y) y x))

声明 2

(declare-fun max_integ ((Int)(Int)) Int)
(assert (forall ((x Int) (y Int)) (= (max_integ x y) (if (< x y) y x))))

我观察到，当我使用 Statement1 时，我的 z3 约束在 0.03 秒内给了我一个结果。而当我使用 Statement2 时，它没有在 2 分钟内完成，我终止了求解器。我也想知道如何使用 C-API 实现它。

谢谢 ！

4

1 回答 1

3

语句 1 是一个宏。Z3 将用表达式替换每次出现max_integ的ite。它在解析期间执行此操作。在第二个语句中，默认情况下，Z3 不会消除max_integ，并且为了能够返回sat它必须为未解释的符号构建一个解释，该解释max_integ将满足所有x和的量词y。Z3 有一个名为 的选项:macro-finder，它将检测本质上是编码宏的量词，并消除它们。这是一个示例（也可在此处在线获得）：

(set-option :macro-finder true)
(declare-fun max_integ ((Int)(Int)) Int)
(assert (forall ((x Int) (y Int)) (= (max_integ x y) (if (< x y) y x))))
(check-sat)
(get-model)

话虽如此，我们可以通过编写一个给定 Z3 表达式返回新 Z3 表达式的函数，轻松地在编程 API 中模拟宏。这里是一个使用 Python API 的示例（也可以在此处在线获得）：

def max(a, b):
   # The function If builds a Z3 if-then-else expression
   return If(a >= b, a, b)

x, y = Ints('x y')
solve(x == max(x, y), y == max(x, y), x > 0)

另一种选择是使用 C API Z3_substitute_vars：. 这个想法是一个包含自由变量的表达式。自由变量是使用 API 创建的Z3_mk_bound。每个变量代表一个参数。然后，我们用Z3_substitute_vars其他表达式替换变量。

于 2013-04-02T16:00:23.863 回答