c++ - Z3 不饱和核心 : an assumption must be a propositional variable or the negation of one

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. 我们需要将 unsat-core 配置为 true。

2. 我们需要创建 bool 变量来跟踪断言

   Z3_parse_smtlib_string(ctx,
   "(benchmark tst :extrafuns ( (x Int) (y Int)) :formula (> x y) :formula (= x 0) :formula (> y 0) )",
   0, 0, 0,
   0, 0, 0);
   params p(ctx);
   p.set(":unsat-core", true); 
   solver 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";
   else
      std::cout << "UNSAT?!\n";
   expr_vector core = s.unsat_core();
   std::cout << core << "\n";