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时崩溃字符串

回答

相关问题