如何有效地提取Z3中的子公式(谓词、术语)

Question

假设我想从BoolExpr类型的给定约束中提取所有子公式（谓词、术语），这里有两个例子：

(f(x)=2 and f(y)=3) or (f(z)=1 and f(y)=3)
The output should be f(x)=2, f(y)=3 and f(z)=1.
(p and q) or (p or r) and (p and (q or r))
The output should be p, q and r.

一种天真的方法是遍历整个AST并记录所有唯一的子公式。当AST中有一堆冗余节点，并且我们必须频繁地执行这样的提取时，这是令人不快的。我想知道是否有一种干净有效的方法可以做到这一点。

我正在为Z3使用Java API。

Answer 1

您可以利用表达式是唯一的这一事实。您可以将它们插入有序字典或哈希表中，并使用字典/哈希表以检测是否已经遍历了相同的子表达式。

您还可以利用这样一个事实，即每个子表达式都有一个唯一的标识符。只要表达式仍然是"活动的"，也就是说，它没有被垃圾收集，标识符就是唯一的。当然，您可以通过维护您跟踪的表达式列表来"pinn"（确保表达式不是垃圾收集的）表达式。使用方法"getId"访问唯一标识符。它在AST.java中定义（Ast.cs用于.NET，z3_api.h用于C，z++.h用于C++）。

  /**
   * A unique identifier for the AST (unique among all ASTs).
   **/
  public int getId() throws Z3Exception
  {
      return Native.getAstId(getContext().nCtx(), getNativeObject());
  }

然后，一个好的遍历算法会维护一个缓存（从整数标识符到子公式的字典）。在遍历子表达式之前，它会检查缓存中是否已经看到该标识符。

标识符用于所用AST对象的"compareTo"方法对于这两个表达式（函数应用程序、量化、绑定变量）、排序和函数。因此，您也可以选择将缓存维护为一组以前看到的表达式，而不必访问较低级别的整数标识符。有关更多详细信息，请参阅AST.java。