用Z3 API与C++进行故障分割

Question

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

我面临的问题是：

1. 当我使用下面所示的函数'z3_assert_str‘断言某物时，我会得到一个分段错误。
2. 跟踪文件始终是空的，似乎配置参数不工作或设置不正确。

我已经尝试过使用Z3 4.4.0和树干，直接从github。

我做错了什么？

下面是这个类的重要部分：

foo.h

在这个类中，我维护两个向量(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的情况似乎并非如此。