從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

回答

相關問題