z3 C++ API：exprの操作を取得

Question

私はz3をC++ライブラリとして使用しています。 私の現在のプログラミングプロジェクトでは、私はz3を使用して簡素化しているブール方程式を持っています。

私のプロジェクトで単純化された方程式を使用するには、lhs、rhs、および簡略化された方程式の操作が必要です。

例：（< 5 x）は式（X == 3）& &を（3×==）Z3

(= x 3) 

LHS引数内に簡略化される - > X

expression.arg(0) 

rhs引数 - > 3

expression.arg(1) 

操作（=）を取得するにはどうすればよいですか？

1つ以上の引数を持つ任意のexprに操作権が必要ですか？

私はAPIを3時間表示していますが、わかりません。

誰もが正しい方向に私を指すことができますように！ Z3で

おかげ Toebs

Answer 1

「トップ」レベルの演算子を取得するには文字列として、つまり元の "と"の場合、そして簡略化された "="の場合は次を使用できます。

expression.decl().name().str() 

Answer 2

機能アプリケーションは、引数のベクトルと関数の宣言として表現されています。例えば、関数fが引数xとyに適用されたとします。 C++ APIでは、これは、e.num_args()引数、xを有するexprオブジェクトeの形状をとるyはe.arg(0)、e.arg(1)とあるこれらの引数に適用されます。

（彼らは定数関数のアプリケーションであるため、明らかに、これはまた、多くの場合、APIのさまざまな部分にconstと呼ばれる0引数、働いています。）