c++ - s.get_model() の後にモデルから整数を取得する

Question

Z3 の C++ APIでは、次の方法でモデルを検索できます。

model m = s.get_model();

それで：

cout << m.eval(A);

の値を教えてくれますA。

ただし、 expr オブジェクトを返しますが、の値を整数としてプログラムm.eval(A)に格納したいと考えています。Aexpr を int に変換するにはどうすればよいですか?

Answer 1

この正確な質問は以前に出てきました。おそらくこれらは明確にするのに役立ちます：Q1 Q2

Answer 2

C API は、整数である式から整数値を取得するためのメソッドを公開します。最も一般的な API は次のとおりです。

/**
   \brief Return numeral value, as a string of a numeric constant term
   \pre Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST
   def_API('Z3_get_numeral_string', STRING, (_in(CONTEXT), _in(AST)))
*/

Z3_string Z3_API Z3_get_numeral_string(__in Z3_context c, __in Z3_ast a);

string( )を返しますchar*。これにより、bignum (64 ビットに収まらない数値) を返すことができます。
Z3 は、Z3_get_numeral特殊なケース向けに他の一連のバリアントを公開しています。これらは z3_api.h に記載されているか、http ://research.microsoft.com/en-us/um/redmond/projects/z3/code/group__capi.html を参照してください。

Answer 3

Z3py を使用した例

x= Int('x')
s = Solver()
s.add(x + 3 == 5)
print s.check()
m = s.model()
print m
y = (m.evaluate(x))
z = y + 4
print simplify(z)

出力：

sat
[x = 2]
6