在 C++ 中使用 Z3 API 的分段错误

Question

我有一个项目生成了很大的 SMT-LIB v2 字符串形式的问题，它通过将问题写入文件然后通过 exec() 调用求解器来解决这些问题。我正在尝试通过 API 集成 Z3 来解决它，因为问题本质上是增量的，因此求解器的学习将在调用之间使用。

我面临的问题是：

当我使用函数断言某事时出现段错误 'z3_assert_str' 如下所示。
跟踪文件总是空的，似乎配置参数不工作或设置不正确。

我已经尝试使用 Z3 4.4.0 和主干，直接来自 github。

我做错了什么？

以下是 class 中的重要部分：

foo.h

在这个 class 中，我维护了两个向量（v_symbols 和 v_func_decl）来跟踪我在问题中插入的内容，这样我就可以调用 "Z3_parse_smtlib2_string"

// attributes of foo.h
z3::config * cfg;
z3::context * c;
z3::solver * s;

std::vector<Z3_symbol> v_symbols;
std::vector<Z3_func_decl> v_func_decl;

// main z3 interaction function
void z3_assert_str(std::string s);

foo.cpp

// in the class constructor, I initialize the 
// z3 structures as follows
cfg = new z3::config(); 
cfg->set("trace", true);
cfg->set("trace_file_name", "z3.log");
c = new z3::context(*cfg);
s = new z3::solver(*c);

// then I keep adding integer vars
expr foobar = c->int_const(obj.c_str());
v_symbols.push_back(foobar.decl().name());
v_func_decl.push_back(foobar.decl());  

// and Uninterpreted Functions (UF)
func_decl f = c->function(f_name.c_str(), sort_vec, z3_int_sort);
v_symbols.push_back(f.name());
v_func_decl.push_back(f);

// and finally the funcion that asserts a smtlib2 string
void encodingUFVisitorZ3::z3_assert_str(std::string constraint) {
    try {
        Z3_ast ast = Z3_parse_smtlib2_string(*c,constraint.c_str(),
                0, 0, 0,
                v_symbols.size(),
                &v_symbols[0],
                &v_func_decl[0]);

        z3::expr constr = to_expr(*c, ast);
        s->add(constr);
    } catch (z3::exception ex) {
        std::cout << "failed: " << ex << "\n";
    }
}

段错误

Program received signal SIGSEGV, Segmentation fault.
0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
372     bool is_right_associative() const { return m_right_assoc; }
(gdb) bt
#0  0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
#1  0x00007ffff730d7b5 in func_decl::is_right_associative (this=0xa623d8) at ../src/ast/ast.h:591
#2  0x00007ffff730375b in ast_manager::mk_app (this=0x8a4058, decl=0xa623d8, num_args=2, args=0xa6d9a0) at ../src/ast/ast.cpp:2046
#3  0x00007ffff703da03 in cmd_context::mk_app (this=0x7fffffffd2e0, s=..., num_args=2, args=0xa6d9a0, num_indices=0, indices=0x0, range=0x0, result=...) at ../src/cmd_context/cmd_context.cpp:998
#4  0x00007ffff701cfb3 in smt2::parser::pop_app_frame (this=0x7fffffffca80, fr=0x8c1bc0) at ../src/parsers/smt2/smt2parser.cpp:1526
#5  0x00007ffff701eafc in smt2::parser::pop_expr_frame (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1663
#6  0x00007ffff701edd3 in smt2::parser::parse_expr (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1696
#7  0x00007ffff7020910 in smt2::parser::parse_assert (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1957
#8  0x00007ffff7022ca5 in smt2::parser::parse_cmd (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2319
#9  0x00007ffff7023cb6 in smt2::parser::operator() (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2470
#10 0x00007ffff7012df1 in parse_smt2_commands (ctx=..., is=..., interactive=false, ps=...) at ../src/parsers/smt2/smt2parser.cpp:2519
#11 0x00007ffff68de38b in parse_smtlib2_stream (exec=false, c=0x8a3148, is=..., num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:272
#12 0x00007ffff68de664 in Z3_parse_smtlib2_string (c=0x8a3148, str=0xa63758 "(assert (= (at plane1 0) city1))", num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:294
#13 0x0000000000529e38 in encodingUFVisitorZ3::z3_assert_str (this=0x8a2220, constraint=...) at encodingUFVisitorZ3.cpp:308
#14 0x0000000000527f4b in encodingUFVisitorZ3::assertInitialState (this=0x8a2220) at encodingUFVisitorZ3.cpp:118
#15 0x000000000052977d in encodingUFVisitorZ3::solve (this=0x8a2220) at encodingUFVisitorZ3.cpp:238
#16 0x0000000000479854 in PDDLProblem::solve (this=0x84c590) at PDDLProblem.cpp:687
#17 0x000000000053afd1 in main (argc=9, argv=0x7fffffffe018) at main.cpp:203

Answer 1

问题出在我创建的 expr 和 func_decl 对象的所有权概念上。正如我使用的其他求解器所发生的那样，一旦你将对象赋予上下文，我假设上下文获得了对象的所有权，所以我可以忘记它。 z3 似乎不是这样。

在 C++ 中使用 Z3 API 的分段错误

Segmentation fault using the Z3 API with C++

c++

z3

c++11

foo.h

foo.cpp

段错误