java - 如何高效提取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

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

您还可以利用每个子表达式都有一个唯一标识符这一事实。 只要表达式仍然“Activity ”，即尚未被垃圾回收，标识符就是唯一的。当然，您可以通过维护您跟踪的表达式列表来“pinn”(确保表达式不被垃圾收集)表达式。 使用方法“getId”访问唯一标识符。它在 AST.java 中定义 (以及用于 .NET 的 Ast.cs、用于 C 的 z3_api.h 和用于 C++ 的 z++.h)。

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

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

该标识符用于所使用的 AST 对象的“compareTo”方法 对于表达式(函数应用、量化、绑定(bind)变量)、排序和函数。 因此，您还可以选择将缓存维护为一组先前看到的表达式，而无需访问较低级别的整数标识符。 有关更多详细信息，请参阅 AST.java。