2016-07-23 10 views
0

私は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を直接割り当てることができないようです。

提案がありますか?ありがとう!

答えて

1

私の最初の提案は、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"を作成することができます。

関連する問題