Z3 API：解析定點SMTLib時崩潰字符串

我想使用Z3的C/C++ API來解析SMTLib2格式（特別是SeaHorn生成的文件）中的定點約束。但是，我的應用程序在解析字符串時崩潰（我正在使用Z3_fixedpoint_from_string方法）。我正在使用的Z3版本是4.5.1 64位版本。Z3 API：解析定點SMTLib時崩潰字符串

我嘗試解析的SMTLib文件找到了Z3二進制文件，我從源文件中編譯，但調用Z3_fixedpoint_from_string時會遇到分段錯誤。我縮小了問題的範圍，直到我認爲這個問題與將關係添加到定點上下文有關。產生我的機器上的賽格故障一個簡單的例子是：

#include "z3.h" 

int main() 
{ 
    Z3_context c = Z3_mk_context(Z3_mk_config()); 
    Z3_fixedpoint f = Z3_mk_fixedpoint(c); 

    Z3_fixedpoint_from_string (c, f, "(declare-rel R())"); 

    Z3_del_context(c); 
}

運行這段代碼Valgrind的報告很多無效的讀取和寫入。所以，這不是API應該如何使用，或者某處存在問題。不幸的是，我找不到任何有關如何以編程方式使用定點引擎的例子。但是，例如調用Z3_fixedpoint_from_string (c, f, "(declare-var x Int)");工作得很好。

順便說一句，其中是Z3_del_fixedpoint()？

來源

2017-03-09 Dan

有沒有這樣的事情作爲一種C/C++語言。你使用哪種語言？ – 2501

該示例使用C API，但我打算混合使用C和C++ API調用。我用g ++ 4.9編譯了這個例子。 – Dan

我現在加了這個以防萬一你和其他人可以使用它。 https://github.com/Z3Prover/z3/commit/509f7409badc0e7834968511ca3c6b6f97fdaed6 –

定點對象「f」是引用計數。調用者負責在創建後立即採取引用計數。使用C++智能指針來控制它更容易，類似於我們如何控制其他對象。 C++ API沒有固定點對象的包裝，因此您必須以其他包裝的風格創建自己的包裝。

代替del_fixedpoint，使用引用計數器。

class fixedpoint : public object { 
    Z3_fixedpoint m_fp; 
public: 
    fixedpoint(context& c):object(c) { mfp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); } 
    ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); } 
    operator Z3_fixedpoint() const { return m_fp; } 

    void from_string(char const* s) { 
     Z3_fixedpoint_from_string (ctx(), m_fp, s); 
    } 

}; 

int main() 
{ 
    context c; 
    fixedpoint f(c); 
    f.from_string("....");  
}

來源

2017-03-10 02:26:30

工程就像一個魅力！謝謝！你們很棒。但爲什麼沒有C++接口到定點設施？ – Dan

Z3 API：解析定點SMTLib時崩潰字符串

回答

相關問題