diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index afd7ae905..5f121726a 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -62,6 +62,7 @@ public: proof_converter_ref pc; model_converter_ref mc; expr_dependency_ref core(m); + obj_map dep2asm; if (!m_fmls.empty()) { goal_ref g = alloc(goal, m); @@ -86,7 +87,7 @@ public: } g = result[0]; TRACE("opt", g->display(tout);); - m_goal2sat(*g, m_params, m_solver, m_map); + m_goal2sat(*g, m_params, m_solver, m_map, dep2asm); } lbool r = m_solver.check(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 8e8ab3e71..c357f7a29 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -699,7 +699,11 @@ namespace sat { init_search(); init_assumptions(num_lits, lits); propagate(false); - if (inconsistent()) return l_false; + if (inconsistent()) { + if (tracking_assumptions()) + resolve_conflict(); + return l_false; + } cleanup(); if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) { m_restart_threshold = m_config.m_burst_search; @@ -867,6 +871,7 @@ namespace sat { m_assumptions.push_back(l); mk_clause(1, &l); } + TRACE("sat", display(tout);); } void solver::reinit_assumptions() { @@ -1564,7 +1569,6 @@ namespace sat { literal l = m_trail[idx]; if (is_marked(l.var())) break; - SASSERT(idx > 0); idx--; } diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp index 2df744138..58abc2807 100644 --- a/src/sat/tactic/atom2bool_var.cpp +++ b/src/sat/tactic/atom2bool_var.cpp @@ -90,8 +90,17 @@ struct collect_boolean_interface_proc { template void operator()(T const & g) { unsigned sz = g.size(); + ptr_vector deps; for (unsigned i = 0; i < sz; i++) { process(g.form(i)); + if (g.dep(i)) { + deps.reset(); + m.linearize(g.dep(i), deps); + for (unsigned j = 0; j < deps.size(); ++j) { + quick_for_each_expr(proc, tvisited, deps[j]); + } + + } } } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index bd3f38d3b..7e22fca8b 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -35,6 +35,7 @@ Notes: #include"for_each_expr.h" #include"model_v2_pp.h" #include"tactic.h" +#include"ast_pp.h" struct goal2sat::imp { struct frame { @@ -52,15 +53,19 @@ struct goal2sat::imp { obj_hashtable m_interface_vars; sat::solver & m_solver; atom2bool_var & m_map; + dep2asm_map & m_dep2asm; sat::bool_var m_true; bool m_ite_extra; unsigned long long m_max_memory; volatile bool m_cancel; + expr_ref_vector m_trail; - imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map): + imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm): m(_m), m_solver(s), - m_map(map) { + m_map(map), + m_dep2asm(dep2asm), + m_trail(m) { updt_params(p); m_cancel = false; m_true = sat::null_bool_var; @@ -360,39 +365,55 @@ struct goal2sat::imp { SASSERT(m_result_stack.empty()); } - void add_assumption(expr* d, expr* literal_d) { - + void insert_dep(expr* dep, bool sign) { + expr_ref new_dep(m), fml(m); + if (is_uninterp_const(dep)) { + new_dep = dep; + } + else { + new_dep = m.mk_fresh_const("dep", m.mk_bool_sort()); + m_trail.push_back(new_dep); + m_interface_vars.insert(new_dep); + fml = m.mk_iff(new_dep, dep); + process(fml); + } + convert_atom(new_dep, false, false); + sat::literal lit = m_result_stack.back(); + m_dep2asm.insert(dep, sign?(~lit):lit); + m_result_stack.pop_back(); } - void operator()(goal const & g) { m_interface_vars.reset(); collect_boolean_interface(g, m_interface_vars); unsigned size = g.size(); expr_ref f(m), d_new(m); ptr_vector deps; + expr_ref_vector fmls(m); for (unsigned idx = 0; idx < size; idx++) { f = g.form(idx); + TRACE("sat", tout << "Formula: " << mk_pp(f, m) << "\n";); // Add assumptions. if (g.dep(idx)) { - expr_dependency * dep = g.dep(idx); deps.reset(); - m.linearize(dep, deps); + fmls.reset(); + m.linearize(g.dep(idx), deps); + fmls.push_back(f); for (unsigned i = 0; i < deps.size(); ++i) { expr * d = deps[i]; expr * d1; SASSERT(m.is_bool(d)); - if (is_uninterp_const(d)) { - add_assumption(d, d); - } - else if (m.is_not(d, d1) && is_uninterp_const(d1)) { - add_assumption(d, d); + if (m.is_not(d, d1)) { + insert_dep(d1, true); + fmls.push_back(d1); } else { - // create fresh variable, map back to dependency. - add_assumption(d, d_new); + insert_dep(d, false); + fmls.push_back(m.mk_not(d)); } } + f = m.mk_or(fmls.size(), fmls.c_ptr()); + TRACE("sat", tout << mk_pp(f, m) << "\n";); } process(f); } @@ -465,8 +486,8 @@ struct goal2sat::scoped_set_imp { } }; -void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m) { - imp proc(g.m(), p, t, m); +void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm) { + imp proc(g.m(), p, t, m, dep2asm); scoped_set_imp set(this, &proc); proc(g); } diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 7e38a1ca5..bcc3dd52e 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -41,6 +41,8 @@ class goal2sat { public: goal2sat(); + typedef obj_map dep2asm_map; + static void collect_param_descrs(param_descrs & r); static bool has_unsupported_bool(goal const & s); @@ -55,7 +57,7 @@ public: \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel), an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory). */ - void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m); + void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm); void set_cancel(bool f); }; diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index c7e2ae608..8b575c177 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -52,7 +52,9 @@ class sat_tactic : public tactic { g->elim_redundancies(); atom2bool_var map(m); - m_goal2sat(*g, m_params, m_solver, map); + obj_map dep2asm; + sat::literal_vector assumptions; + m_goal2sat(*g, m_params, m_solver, map, dep2asm); TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n"; atom2bool_var::iterator it = map.begin(); atom2bool_var::iterator end = map.end(); @@ -66,10 +68,21 @@ class sat_tactic : public tactic { CASSERT("sat_solver", m_solver.check_invariant()); IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream());); TRACE("sat_dimacs", m_solver.display_dimacs(tout);); - - lbool r = m_solver.check(); + dep2assumptions(dep2asm, assumptions); + lbool r = m_solver.check(assumptions.size(), assumptions.c_ptr()); if (r == l_false) { - g->assert_expr(m.mk_false(), 0, 0); + expr_dependency * lcore = 0; + if (produce_core) { + sat::literal_vector const& core = m_solver.get_core(); + u_map asm2dep; + mk_asm2dep(dep2asm, asm2dep); + for (unsigned i = 0; i < core.size(); ++i) { + sat::literal lit = core[i]; + expr* dep = asm2dep.find(lit.index()); + lcore = m.mk_join(lcore, m.mk_leaf(dep)); + } + } + g->assert_expr(m.mk_false(), 0, lcore); } else if (r == l_true && !map.interpreted_atoms()) { // register model @@ -115,6 +128,22 @@ class sat_tactic : public tactic { m_sat2goal.set_cancel(f); m_solver.set_cancel(f); } + + void dep2assumptions(obj_map& dep2asm, + sat::literal_vector& assumptions) { + obj_map::iterator it = dep2asm.begin(), end = dep2asm.end(); + for (; it != end; ++it) { + assumptions.push_back(it->m_value); + } + } + + void mk_asm2dep(obj_map& dep2asm, + u_map& lit2asm) { + obj_map::iterator it = dep2asm.begin(), end = dep2asm.end(); + for (; it != end; ++it) { + lit2asm.insert(it->m_value.index(), it->m_key); + } + } }; struct scoped_set_imp { diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 38b318d2f..879c5f212 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -155,7 +155,6 @@ unsigned read_dimacs(char const * file_name) { g_solver = &solver2; sat::literal_vector assumptions; track_clauses(solver, solver2, assumptions, tracking_clauses); - solver2.display(std::cout); r = g_solver->check(assumptions.size(), assumptions.c_ptr()); } else { diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index 8d82d292c..9f1ed8c72 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -289,7 +289,6 @@ struct is_non_qfbv_predicate { return; if (is_uninterp_const(n)) return; - throw found(); } }; diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 3b5c352bb..916ae1386 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -105,7 +105,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti cond(mk_is_qfbv_probe(), cond(mk_is_qfbv_eq_probe(), and_then(mk_bv1_blaster_tactic(m), - using_params(smt, solver_p)), + using_params(sat, solver_p)), and_then(mk_bit_blaster_tactic(m), when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), and_then(using_params(and_then(mk_simplify_tactic(m), @@ -126,7 +126,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { - tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + tactic * new_sat = cond(mk_produce_proofs_probe(), and_then(mk_simplify_tactic(m), mk_smt_tactic()), mk_sat_tactic(m));