1

我正在尝试通过 C API 和 smtlib2 使用 Z3 进行增量求解。不幸的是，在断言一些简单的公式、检查它、获取它的模型、断言一些额外的东西然后再次检查时，我遇到了分段违规。这也发生在没有断言新事物的情况下，即在检查、检索模型和再次检查时。这是重现错误的最小示例：

#include<z3.h>

int main()
{
  Z3_config cfg = Z3_mk_config();
  Z3_context ctx = Z3_mk_context(cfg);
  Z3_ast fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () Int) (assert (= a 0))", 0, 0, 0, 0, 0, 0);
  Z3_solver solver = Z3_mk_solver(ctx);
  Z3_solver_assert(ctx, solver, fs);
  Z3_solver_check(ctx, solver);
  Z3_model m = Z3_solver_get_model(ctx, solver);
  Z3_solver_check(ctx, solver);
  Z3_del_config(cfg);
  return 0;
}

我尝试了两个 Z3 版本（Mac 64 位上的 4.3.1 和 Ubuntu 64 位上的 4.1）。

感谢任何帮助、提示或解决方法 - 也许我只是以错误的方式使用 API？

非常感谢，

伊丽莎白

4

1 回答 1

1

这是使用引用计数的代码版本。当我删除引用计数时它会崩溃。

void main() {
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_ast fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () Int) (assert (= a 0))", 0, 0, 0, 0, 0, 0);
    Z3_inc_ref(ctx, fs);
    Z3_solver solver = Z3_mk_solver(ctx);
    Z3_solver_inc_ref(ctx, solver);
    Z3_solver_assert(ctx, solver, fs);
    Z3_solver_check(ctx, solver);
    Z3_model m = Z3_solver_get_model(ctx, solver);
    Z3_model_inc_ref(ctx, m);
    Z3_solver_check(ctx, solver);


    // work with model

    Z3_solver_dec_ref(ctx, solver);
    Z3_model_dec_ref(ctx, m);
    Z3_dec_ref(ctx, fs);
    Z3_del_config(cfg);
 }

顺便提一句。C++ API 隐藏了所有的引用计数细节。使用起来更方便。

于 2013-04-09T20:03:53.273 回答