Z3 Java APIのシンボルの作成

Question

私はZ3を初めて使用しています。私はZ3 Java APIで定数を取り戻す2つの質問を持っています。

1. 定数の作成はどのように内部的に行われますか？私は最終的に `INTERNALmkStringSymbolは、」私はそのソースを見ることができないネイティブなので、今このラインlong var3 = INTERNALmkStringSymbol(var0, var2);

にvar3で変数を生成Native.mkStringSymbol(var1.nCtx(), var2)を呼び出しpublic StringSymbol mkSymbol(String)まで public BitVecExpr mkBVConst(String, int)を追跡することによって開始したことを理解すること。私はそれがどのように動作するのか不思議です。誰もそれがどのように機能するか知っていますか？そのソースを表示する場所？

2. 私が混乱しているもう一つのことは、APIを使った定数のスコープです。インタラクティブなZ3では、それは一致するプッシュとポップを介して維持されますが、APIを通して、どのようにスコープが定義され、管理されているのかわかりません。

洞察力や指導に感謝します。

Answer 1

1. Z3はオープンソースです。あなたはhttps://github.com/z3prover/z3.gitからソースを表示してダウンロードすることができます。 Z3のシンボルはsrc/util/symbol.hで定義されています。シンボルはLISPアトムに似ていることがわかります。それらはdllの存続期間中存続し、ユニークです。したがって、同じ名前の2つのシンボルは、ポインタが等しくなります。 Java APIは、src/api/z3_api.hで宣言されているC APIを呼び出します。ディレクトリsrc/apiには、シンボルを作成する関数を含むAPI関数が含まれています。 mkBVConstなどの式定数を作成すると、それはポインタ一意の式になります（同じmkBVConstを2回作成すると、アンマネージポインタは等しくなります）。Javaポインタは同じではありませんが、等価性テストはすべてこれの）。
2. Solverオブジェクトには、プッシュメソッドとポップメソッドがあります。ソルバーオブジェクトに制約を追加することができます。制約の存続時間は、プッシュ/ポップのネストに従います。制約は、制約が追加されたスコープを削除するポップまで有効です。