Z3 4.0 Z3_parse_smtlib2_string [英] Z3 4.0 Z3_parse_smtlib2_string

问题描述

我通过 C API/JNA/Scala 将 Z3 与 SMT2 一起使用，并且似乎工作得很好.

I am using Z3 with SMT2 via C API/JNA/Scala and seems to work pretty well.

我想尝试增量求解.所以一开始我用 Z3_parse_smtlib2_string 来翻译这个:

I want to try incremental solving. So at first I translate this by using 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 检索模型(如果检查返回可满足，在本例中就是这种情况).目前没有问题.

Then I get back an Z3_ast, put it into a solver via Z3_solver_assert, check it with Z3_solver_check and retrieve a model via Z3_solver_get_model (if the check returned satisfiable, which is the case in this example). So far there is no problem.

但是当我想另外声明一些这样的东西时:

But when I want to assert something additionally like this:

(assert (= x 1))

我在调用 Z3_parse_smtlib2_string 时陷入困境，因为它抱怨 x 是一个未知常量.如果我还添加 declare-fun 到第二个代码段，我会收到无效参数错误.这个变量不应该已经存在于环境中吗?我是否必须设置 Z3_parse_smtlib2_string 的附加参数?我怎样才能从先前解析的公式中得到这些?

I get stuck at the point where Z3_parse_smtlib2_string is called, because it complains, that x is an unknown constant. If I add also add the declare-fun to the second snippet I get an invalid argument error. Shouldn't this variable exist already in the environment? Do I have to set the additional parameters of Z3_parse_smtlib2_string? How can I get those out of the previsously parsed formula?

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

Also using (set-option :global-decls true) did not work as Z3 tells me that this option value cannot be modified after initialization.

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

Does anybody have a clue how to solve this problem?

推荐答案

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

要从第一次解析传递中恢复声明的常量和排序，您可以使用 Z3_get_smtlib_num_decls、Z3_get_smtlib_decl 和类似的排序.

To recover the declared constants and sorts from the first parsing pass, you can use Z3_get_smtlib_num_decls, Z3_get_smtlib_decl and similarly for sorts.

这篇关于Z3 4.0 Z3_parse_smtlib2_string的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！