z3 - Z3中宏和量词的区别

Question

我想知道以下两个陈述有什么区别 -

声明 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 实现它。

谢谢!

Answer 1

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

(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 的示例(也可在线获取 here):

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用其他表达式替换变量。