10

私はZ3を初めて使用し、こことGoogleで私の質問に対する答えを検索しました。残念ながら、私は成功しませんでした。

Z3 4.0 C / C++APIを使用しています。未定義の関数d：（Int Int）Intを宣言し、いくつかのアサーションを追加して、モデルを計算しました。これまでのところ、それはうまくいきます。

ここで、モデルによって定義された関数dの特定の値、たとえばd（0,0）を抽出したいと思います。次のステートメントは機能しますが、 d（0,0）の関数値（整数）ではなく式を返します。

z3::expr args[] = {c.int_val(0), c.int_val(0)};
z3::expr result = m.eval(d(2, args));

チェック

result.is_int();

trueを返します。

私の（うまくいけばあまり愚かではない）質問は、返された式をC / C ++ intにキャストする方法ですか？

ヘルプは非常にありがたいです。ありがとうございました！

4

1 に答える 1

7

Z3_get_numeral_intはあなたが探しているものです。

文書からの抜粋は次のとおりです。

Z3_bool Z3_get_numeral_int(__in Z3_context c, __in Z3_ast v, __out int * i)

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a 
machine int. Return Z3_TRUE if the call succeeded.

ただし、注意が必要です。Z3の整数は数学的な整数であり、32ビット整数の範囲を簡単に超える可能性があります。その意味で、Z3_get_numeral_stringを使用し、文字列を大きな整数に解析することは、より良いオプションです。

于 2012-07-25T15:07:48.197 に答える