Z3 中定义变量和常量的宏

Question

我希望 Z3 中有可以定义变量和常量的宏。我不知道如何使用该语言执行此操作，因此我使用 cpp(c 预处理器)来执行此操作。

例如，我有:

#define CONST(NAME,VALUE) (declare-const NAME Int) (assert (= NAME VALUE))

然后我可以定义常量，例如:

CONST(MIN_AGE, 10)
CONST(MAX_AGE, 140)

有没有办法在语言中做到这一点？

Answer 1

在 SMTLib 中编写这些内容的规范方法是:

(define-fun MIN_AGE () Int  10)
(define-fun MAX_AGE () Int 140)

请注意使用 define-fun 构造而不是 declare-const，后者声明名称并将其与常量值关联。

参见http://smtlib.cs.uiowa.edu/有关该语言的详细信息。特别是这个document标准化求解器的语法和语义。 define-fun 命令在第 62 页上进行了描述。

请注意，SMTLib 并不是真正要“手写”的。更适合机器生成。大多数 SMT 用户将使用更高级别的 API，该 API 将在后台使用 SMT-Lib(或不同的机制)与求解器进行通信。所有主要语言都有可供选择，包括 C/C++/Java/Python/Haskell/O'Caml 等，它们支持的成熟度和功能水平各不相同。我的建议是选择其中一种语言并使用它们的 API，而不是直接在 SMTLib 中编码。