Z3 4.0 Z3_parse_smtlib2_string

Question

我正在通过 C API/JNA/Scala 将 Z3 与 SMT2 一起使用，并且似乎运行良好。

我想尝试增量求解。所以起初我使用 Z3_parse_smtlib2_string 来翻译这个：

(declare-fun x () Int)
(assert (>= x 0))
(check-sat)
(get-model)

然后我得到一个 Z3_ast，通过 Z3_solver_assert 将其放入求解器，通过 Z3_solver_check 检查并通过 Z3_solver_get_model 检索模型（如果检查返回令人满意，在本例中就是这种情况）。到目前为止没有任何问题。

但是当我想另外断言这样的事情时：

(assert (= x 1))

我被困在调用 Z3_parse_smtlib2_string 的地方，因为它抱怨说 x 是一个未知常量。如果我将 declare-fun 添加到第二个 sn-p 我会得到一个无效的参数错误。 这个变量不应该已经存在于环境中吗？我必须设置 Z3_parse_smtlib2_string 的附加参数吗？如何从预先解析的公式中取出那些？

同样使用(set-option :global-decls true) 也不起作用，因为 Z3 告诉我这个选项值在初始化后无法修改。

有人知道如何解决这个问题吗？

Answer 1

Z3_parse_smtlib2_string 可以作为现有排序和常量的额外参数列表。因此，第二次调用它时，您可以告诉它您已经知道 x 代表什么。

要从第一个解析过程中恢复声明的常量和排序，您可以使用Z3_get_smtlib_num_decls、Z3_get_smtlib_decl 和类似的排序。