我正在研究 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。
最佳答案
我找到了通过引入跟踪断言来生成 unsat 核心的解决方案,
- 我们需要将 unsat-core 配置为 true。
我们需要创建 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";
关于c++ - Z3 不饱和核心 : an assumption must be a propositional variable or the negation of one,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40458415/