gpt4 book ai didi

java - 如何高效提取Z3中的子公式(谓词、术语)?

转载 作者:行者123 更新时间:2023-12-01 12:33:15 25 4
gpt4 key购买 nike

假设我想从给定的 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。

最佳答案

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

您还可以利用每个子表达式都有一个唯一标识符这一事实。只要表达式仍然“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。

关于java - 如何高效提取Z3中的子公式(谓词、术语)?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25777574/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com