mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 11:51:20 +00:00
Code Activity

Use quick explain for unsat core in Fu Malik algorithm by default

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-15 16:58:42 -08:00
parent 074e851d49
commit c837f62863
3 changed files with 39 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/opt/fu_malik.cpp
View file

@ -123,7 +123,15 @@ namespace opt {
expr_ref_vector ls1(m), ls2(m); expr_ref_vector ls1(m), ls2(m);
ls1.append(mid, literals.c_ptr()); ls1.append(mid, literals.c_ptr());
ls2.append(literals.size()-mid, literals.c_ptr() + mid); ls2.append(literals.size()-mid, literals.c_ptr() + mid);
#if Z3DEBUG
expr_ref_vector ls(m);
ls.append(ls1);
ls.append(ls2);
SASSERT(ls.size() == literals.size());
for (unsigned i = 0; i < literals.size(); ++i) {
SASSERT(ls[i].get() == literals[i].get());
}
#endif
expr_ref_vector as1(m); expr_ref_vector as1(m);
as1.append(assumptions); as1.append(assumptions);
as1.append(ls1); as1.append(ls1);
@ -153,6 +161,7 @@ namespace opt {
ptr_vector<expr> core; ptr_vector<expr> core;
if (m_use_new_bv_solver) { if (m_use_new_bv_solver) {
// Binary search for minimal unsat core
expr_set core_set; expr_set core_set;
expr_ref_vector empty(m); expr_ref_vector empty(m);
quick_explain(empty, assumptions, true, core_set); quick_explain(empty, assumptions, true, core_set);
@ -160,6 +169,24 @@ namespace opt {
for (; it != end; ++it) { for (; it != end; ++it) {
core.push_back(*it); core.push_back(*it);
} }
//// Forward linear search for unsat core
//unsigned i = 0;
//while (s().check_sat(core.size(), core.c_ptr()) != l_false) {
// IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
// core.push_back(assumptions[i].get());
// ++i;
//}
//// Backward linear search for unsat core
//unsigned i = 0;
//core.append(assumptions.size(), assumptions.c_ptr());
//while (!core.empty() && s().check_sat(core.size()-1, core.c_ptr()) == l_false) {
// IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
// core.pop_back();
// ++i;
//}
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";); IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
} }
else { else {
@ -214,7 +241,11 @@ namespace opt {
} }
} }
void set_solver() { void set_solver() {
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
if (opt_s.is_dumping_benchmark())
return;
solver& current_solver = s(); solver& current_solver = s();
goal g(m, true, false); goal g(m, true, false);
unsigned num_assertions = current_solver.get_num_assertions(); unsigned num_assertions = current_solver.get_num_assertions();
@ -223,8 +254,7 @@ namespace opt {
} }
probe *p = mk_is_qfbv_probe(); probe *p = mk_is_qfbv_probe();
bool all_bv = (*p)(g).is_true(); bool all_bv = (*p)(g).is_true();
if (all_bv) { if (all_bv) {
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
smt::context & ctx = opt_s.get_context(); smt::context & ctx = opt_s.get_context();
tactic_ref t = mk_qfbv_tactic(m, ctx.get_params()); tactic_ref t = mk_qfbv_tactic(m, ctx.get_params());
// The new SAT solver hasn't supported unsat core yet // The new SAT solver hasn't supported unsat core yet

4
src/opt/opt_solver.cpp
View file

@ -105,6 +105,10 @@ namespace opt {
static unsigned g_checksat_count = 0; static unsigned g_checksat_count = 0;
bool opt_solver::is_dumping_benchmark() {
return m_is_dump;
}
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
TRACE("opt_solver_na2as", { TRACE("opt_solver_na2as", {
tout << "opt_opt_solver::check_sat_core: " << m_context.size() << "\n"; tout << "opt_opt_solver::check_sat_core: " << m_context.size() << "\n";

1
src/opt/opt_solver.h
View file

@ -79,6 +79,7 @@ namespace opt {
static opt_solver& to_opt(solver& s); static opt_solver& to_opt(solver& s);
void set_interim_stats(statistics & st); void set_interim_stats(statistics & st);
bool is_dumping_benchmark();
class toggle_objective { class toggle_objective {
opt_solver& s; opt_solver& s;