2 つの expr_vector A、B があり、それらの要素を比較しようとしています。
if(strcmp(A[i].ToString(),B[i].ToString()) == 1)
エラー 'class z3::expr' には 'ToString' という名前のメンバーがありません。これはオーバーライド文字列 ToString ( ) で見つかります。
または、2 つの expr_vector の変数を比較する方法を教えてください。変数 q1 などは、<expr>それぞれベクトル A と B にあります。
質問で提供したリンクは Z3 C# (.Net) API 用であり、質問は C++ API を使用していることを示唆しています (expr_vectorは Z3 C++ API のクラスです)。
aとbが等しいかどうか、aとが であるかどうかをテストするにbはz3::expr、 を使用する必要がありますeq(a, b)。関数はのeq単なるラッパーでZ3_is_eq_astあり、で定義されていますz3++.h
friend bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }