私はZ3を初めて使用しています。Z3のbool変数に値を代入するC api
私はbool型変数aを定義します:
Z3_sort bool_type = Z3_mk_bool_sort(ctx);
Z3_ast a = Z3_mk_const(ctx、Z3_mk_string_symbol(ctx、 "a")、bool_type);
私は別の値をどのように割り当てることができますか?私はZ3_L_TRUEを直接割り当てることができないようです。
提案がありますか?ありがとう!
私はZ3を初めて使用しています。Z3のbool変数に値を代入するC api
私はbool型変数aを定義します:
Z3_sort bool_type = Z3_mk_bool_sort(ctx);
Z3_ast a = Z3_mk_const(ctx、Z3_mk_string_symbol(ctx、 "a")、bool_type);
私は別の値をどのように割り当てることができますか?私はZ3_L_TRUEを直接割り当てることができないようです。
提案がありますか?ありがとう!
私の最初の提案は、C APIの代わりにC++ APIを使用することです。 C APIを使用すると、エラーが発生しやすくなります。 、
https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c
と
https://github.com/Z3Prover/z3/blob/master/examples/c++/example.cpp
あなたがやっているようにあなたは、論理変数の作成例が表示されます。分布は、CおよびC++ APIの両方を使用する例が付属しています論理変数を制約するアサーションを追加することです。 テキストベースのAPIを使用して論理モデリングを理解する方が簡単です。 つまり、SMT-LIB形式を使用して、あなたが意図しているものをモデル化することをお勧めします。 これは、プログラムAPIを使って何をするべきかを推測する方法を提供します。
質問について:論理モデリングには「割り当て」という概念はありません。 あなたは確実に平等を表明することができます。さらに、Z3_L_TRUEは、充足可能性をチェックするときに使用される戻りコード です。メソッドZ3_mk_trueを使用して論理定数 "true"を作成することができます。