2017-12-31 186 views
1

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

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

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

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

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

答えて

0
  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オブジェクトには、プッシュメソッドとポップメソッドがあります。ソルバーオブジェクトに制約を追加することができます。制約の存続時間は、プッシュ/ポップのネストに従います。制約は、制約が追加されたスコープを削除するポップまで有効です。
+0

ありがとう@Nikola、これは本当に便利です。しかし、第2のポイントについては、定数ではなく制約のスコープについて話しています。これは定数がグローバルであることを意味しますか?再度、感謝します! – Inquirer

関連する問題