如何有效地提取Z3中的子公式（謂詞，術語）？

假設我想從BoolExpr的類型給定的約束條件提取所有的子式（謂詞而言）和這裏有兩個例子：如何有效地提取Z3中的子公式（謂詞，術語）？

(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。

來源

2014-09-11 Yu Feng

您可以利用表達式是唯一的事實。您可以將它們插入到有序的字典或散列表中，並使用字典/散列表來檢測您是否已遍歷相同的子表達式。

您還可以利用每個子表達式具有唯一標識符的事實。只要表達式仍然是「活的」，標識符就是唯一的，也就是說，它沒有被垃圾回收。您可以通過維護您追蹤的表達式列表來「固定」（確保表達式不是垃圾回收）表達式。使用方法「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」方法，該方法對於表達式（函數應用程序，量化，綁定變量），排序和函數均使用。因此，您也可以選擇將緩存作爲一組以前看到的表達式來維護，而不是訴諸訪問較低級別的整數標識符。有關更多詳細信息，請參閱AST.java。

來源

2014-09-11 02:00:46

如果我完全控制操作，比如說，連接，分離等，我可以輕鬆地緩存唯一的子表達式。問題來自於我經常調用「ctx-solver-simplify」來縮小它的大小。在簡化過程中，唯一子表達式的數量可能會縮小，我別無選擇，只能遍歷簡化的expr以再次獲取新的唯一子表達式，這是非常低效的。 – 2014-09-11 03:45:19

如何有效地提取Z3中的子公式（謂詞，術語）？

回答

相關問題