1

我正在从 Z3 版本 3.2 迁移到版本 4.0。但是，之前工作的代码不再直接工作，我正在尝试找出相同的原因。我将整个代码简化为一个非常简单的声明和断言，但它仍然不起作用。代码是 -

long intSort = Z3_mk_int_sort (context);
long periodDeclStr = Z3_mk_string_symbol(context, "period");
long periodVar =  Z3_mk_const(context, periodDeclStr, intSort);

long solver = z3_mk_solver();
long zero = Z3_mk_int (context, 0, intSort);
long eqSt = Z3_mk_eq(context, periodVar, zero);     
Z3_solver_assert (context, solver, eqSt);

问题在于倒数第二个语句Z3_mk_eq()

我收到错误 -

WARNING: invalid function application, sort mismatch on argument at position 2
WARNING: (define = arith arith Bool) applied to: 
period of sort arith
0::Int of sort Int

我的问题如下 -

  1. 如何调试此错误？这仍然适用于 3.2 版，但没有求解器。
  2. 是否有必要仅在将变量添加到上下文后才必须创建求解器？创建求解器后，我可以将变量添加到上下文中吗？或者我必须重新创建求解器？

抱歉，添麻烦了。我正在混合求解器和上下文以将它们传递给求解器。然而，问题仍然没有解决。我在Z3_ast_to_String()API 中遇到了崩溃。我将尝试解决问题并发布更新。

4

2 回答 2

2

Z3 4.0 现在有一个交互日志，可以精确记录 API 交互。应该可以使用此功能来调试 JNI 分层和您发现的错误。使用 Z3_open_log() 打开日志。您应该在创建任何上下文之前打开日志。如果您只想捕获交互的子集，您也可以在任何时候关闭日志 (Z3_close_log())。您可以通过提供后缀“.log”来重播日志并在其上运行 Z3。或者，您可以使用选项 /log 运行 Z3，即“Z3.exe /log”以重播交互。

于 2012-06-03T15:03:49.787 回答
0

你不想Z3_mk_eq(context, id, zero)代替Z3_mk_eq(context, periodDecl, zero)吗？

于 2012-06-02T10:23:58.310 回答