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);
問題は、最後から 2 番目のステートメントにあります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でクラッシュが発生しています。私は問題を解決し、アップデートを投稿しようとします。