从Z3版本3.2迁移到版本4.0

我正在从Z3版本3.2迁移到版本4.0。但是，以前工作的代码不再直接使用，我试图找出相同的原因。我将整个代码简化为一个非常简单的声明和断言，但它仍然行不通。该代码是 -从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

我的问题如下 -

如何调试这个错误？这仍然适用于3.2版本，但没有求解器。
仅当我完成向上下文添加变量后，是否必须创建求解器？创建求解器后，我可以向上下文添加变量吗？或者我必须重新创建求解器？

对不起。我正在混合求解器和上下文来将它们传递给解算器。但是，问题仍然存在未解决的问题。我在Z3_ast_to_String() API中发生崩溃。我会尽力解决问题并发布更新。

来源

2012-06-02 Raj

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

来源

2012-06-03 15:03:49

难道你不想要Z3_mk_eq(context, id, zero)而不是Z3_mk_eq(context, periodDecl, zero)？

来源

2012-06-02 10:23:58

对不起...这只是一个错字。我正确地编写了代码。 – Raj

只是为了更新，我上面显示的错误，它对每个执行都会改变。有时会给Int排序，有时候没有排序显示。也许这是因为我使用JNI Library从Java访问Z3？ – Raj

从Z3版本3.2迁移到版本4.0

回答

相关问题