Z3 unsat核心:假设必须是一个命题变量或一个变量的否定。

Question

我正在研究C++ Z3 unsat核心，

Z3_parse_smtlib_string(ctx,
    "(benchmark tst :extrafuns ((b1 Bool) (b2 Bool) (b3 Bool) (x Int) (y Int)) :formula (=> b1 (> x y)) :formula (=> b2 (= x 0)) :formula (=> b3 (> y 0)))",0, 0, 0,0, 0, 0);
num_formulas = Z3_get_smtlib_num_formulas(ctx); 
std::vector<expr> assumptions;
for (i = 0; i < num_formulas; i++) 
{
    Z3_ast f = Z3_get_smtlib_formula(ctx, i);
    z3::expr e(ctx, f);
    assumptions.push_back(e);
    s.add(e);
}
s.check(3,&assumptions[0]) ;
expr_vector core = s.unsat_core();
std::cout << "size: " << core.size() << "\n";
for (unsigned i = 0; i < core.size(); i++)
{
    std::cout << core[i] << "\n";
}

然而，它提出了一个警告:一个假设必须是一个命题变量，或者是一个变量的否定。此外，返回的unsat核心大小为0。

Answer 1

我通过引入跟踪断言找到了生成unsat核心的解决方案，

1. 我们需要将非卫星核心配置为真。
2. 我们需要创建布尔变量来跟踪断言。 Z3_parse_smtlib_string(ctx，“(基准tst :extrafuns ( (x ) ( y )：公式(> x)：公式(X0)：公式(> y0 )"，”0，0，0，0，0，0，0，0，0，0“；p.set(":unsat-core"，真)；求解器s(ctx)；s.set(p)；num_formulas = Z3_get_smtlib_num_formulas(ctx)；for (i = 0；I< num_formulas；i++) { Z3_ast f= Z3_get_smtlib_formula(ctx，i)；z3::expr e(ctx，f)；std::stringstream qname；qname << "q“<< i；s.add(e，qname.str().c_str())；} if (s.check() == z3::sat) std::cout << s.get_model() << "\n"；cout <<？！\n；expr_vector core = s.unsat_core()；std::cout << core << "\n"；