Z3 - 如何從給定公式中提取變量？

我正在使用Z3 C++ API（版本4.3.1），我想提取公式的變量（expr類型的對象）。我找到了similar question，但它在Z3py中。我想知道Z3 C/C++ API中是否有方法從expr對象中提取變量。謝謝！Z3 - 如何從給定公式中提取變量？

例如（一些細節省略）：

expr fs = implies(x + y == 0, z * x < 15); 
    std::vector<expr> varlist = get_vars(fs);

varlist然後應包含X，Y，Z。

來源

2014-09-22 cxcfan

發行版中的C++示例（examples/C++/example.cpp）顯示了示例訪問者模式。這是非常簡單的，但會給出這個想法。

我在這裏重複瞭如下：

void visit(expr const & e) { 
if (e.is_app()) { 
    unsigned num = e.num_args(); 
    for (unsigned i = 0; i < num; i++) { 
     visit(e.arg(i)); 
    } 
    // do something 
    // Example: print the visited expression 
    func_decl f = e.decl(); 
    std::cout << "application of " << f.name() << ": " << e << "\n"; 
} 
else if (e.is_quantifier()) { 
    visit(e.body()); 
    // do something 
} 
else { 
    assert(e.is_var()); 
    // do something 
} 
}

參觀者功能可以通過使用以前訪問過的表情，因爲在一般Z3高速緩存使用共享的子表達式得到改善。這與Python示例類似。

希望這會有幫助

來源

2014-09-26 23:50:15

非常感謝，我還有一個問題。我注意到'e.is_app（）'和'e.is_var（）'是兩個不同的分支。但是，變量也是一個應用程序。那麼什麼樣的表達式'e'可以進入'e.is_var（）'分支而不是'e.is_app（）'分支？ – cxcfan 2014-09-28 06:42:19

表達式可以是應用程序，量詞或綁定變量。 e.is_var（）檢查僅對綁定變量成功。 Z3使用綁定變量的索引。所以e.is_app和e.is_var的情況從不重疊。 – 2016-11-28 17:36:25

Z3 - 如何從給定公式中提取變量？

回答

相關問題