z3 - Z3 C ++ APIを使用してsmtlib2文字列を読み取る方法は？

Question

expr指定されたSMTLIB2ファイルからオブジェクトを作成したいと思います。Z3_parse_smtlib_stringCの例で関数を見ることができます。exprクラスにそのラッパーはありますか？

Answer 1

Z3 C++ API は、この機能を expr クラスの一部として明示的に提供していません。ただし、C++ API は C API と一緒に使用できます。つまり、関数Z3_parse_smtlib_string(または ... _file) を使用してこれを実現できます。この関数は を返すことに注意してください。これは、C++ の「世界」に戻るためにオブジェクトにZ3_ast変換する必要があります。expr

簡単な例:

#include <z3++.h>

...

context ctx;
Z3_ast a = Z3_parse_smtlib2_file(ctx, "test.smt2", 0, 0, 0, 0, 0, 0);    
expr e(ctx, a);
std::cout << "Result = " << e << std::endl;

Z3_parse_smtlib2_*関数はエラー チェックを実行しないため、エラーが発生しても例外はスローされません。これは、 への呼び出しによって実現できますcontext::check_error()。