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 中编码。