使用Z3的C++ api創建一個長分隔符？

什麼是創建一個可變數量的disjuncts長分歧的首選方法？使用Z3的C++ api創建一個長分隔符？

我的猜測是，這樣的事情應該用expr_vector首先動態push_back所有析取的，然後以某種方式使用Z3_mk_or建立我的脫節是可能的。

但是我怎樣才能從expr_vectorZ3_ast的數組作爲第三個參數Z3_mk_or？

順便說一句，如果創建一個長序列的二元分離而不是單個長n元分解，那麼是否存在任何效率懲罰？

2012-05-30 Juan A. Navarro

我只是在猜測，但這顯然是指Microsoft Research的[Z3項目]（http://research.microsoft.com/en-us/um/redmond/projects/z3/）。 –

Z3 C++ API不支持從expr_vector對象創建n元析取。我同意這是一個有用的功能，我會將它添加到下一個Z3版本中。您可以使用以下代碼模擬此功能。下面的代碼並不完美，因爲它創建了expr_vector的「副本」，但它可以用作臨時解決方法。正如我上面所說，下一個版本將會支持這種操作，並且這個副本將被避免。

#include<vector> 
#include<z3++.h> 
using namespace z3; 

expr mk_or(expr_vector args) { 
    std::vector<Z3_ast> array; 
    for (unsigned i = 0; i < args.size(); i++) 
     array.push_back(args[i]); 
    return to_expr(args.ctx(), Z3_mk_or(args.ctx(), array.size(), &(array[0]))); 
} 

int main() { 
    context  c; 
    expr_vector args(c); 

    args.push_back(c.bool_const("p")); 
    args.push_back(c.bool_const("q")); 
    args.push_back(c.bool_const("r")); 

    std::cout << mk_or(args) << std::endl; 
    return 0; 
}

關於你提到的第二個問題，有沒有顯著的性能損失，如果一個二進制創建的析取而不是一個單一n元一個的長序列。在內部，Z3可以非常有效地在二進制和n-ary格式之間進行轉換。

來源

2012-05-30 20:35:03

謝謝，這或多或少是我已經編碼的解決方法。提供支持時，我會看看將來的版本。 –

使用Z3的C++ api創建一個長分隔符？

回答

相關問題