From bfc0af782051c833f15ff9d6a51959eaec349c2b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Jul 2014 16:35:46 -0700 Subject: [PATCH] testing inc-sat solver Signed-off-by: Nikolaj Bjorner --- src/opt/dual_maxres.cpp | 76 +++++++++++++++-------------- src/opt/inc_sat_solver.cpp | 24 +++++++-- src/opt/mus.cpp | 10 +++- src/sat/sat_solver.cpp | 5 +- src/tactic/arith/card2bv_tactic.cpp | 2 +- 5 files changed, 73 insertions(+), 44 deletions(-) diff --git a/src/opt/dual_maxres.cpp b/src/opt/dual_maxres.cpp index 95834ca1a..5895f0573 100644 --- a/src/opt/dual_maxres.cpp +++ b/src/opt/dual_maxres.cpp @@ -134,7 +134,7 @@ public: case l_undef: break; case l_false: - is_sat = get_cores(soft_compl, cores); + is_sat = get_cores(cores); for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) { is_sat = process_unsat(cores[i]); } @@ -177,57 +177,61 @@ public: // TBD: when the remaining are satisfiable, then extend the // satisfying model to improve upper bound. // - lbool get_cores(ptr_vector& core, vector >& cores) { - // assume 'core' is minimal. + lbool get_cores(vector >& cores) { + // assume m_s is unsat. + lbool is_sat = l_false; expr_ref_vector asms(m); asms.append(m_asms.size(), m_asms.c_ptr()); - remove_soft(core, asms); cores.reset(); - cores.push_back(core); - ptr_vector new_core; - while (true) { - lbool is_sat = m_s->check_sat(asms.size(), asms.c_ptr()); - switch (is_sat) { - case l_false: - new_core.reset(); - m_s->get_unsat_core(new_core); - switch (minimize_core(new_core)) { - case l_false: - return l_false; - case l_true: - cores.push_back(new_core); - remove_soft(new_core, asms); - break; - default: - return l_undef; - } + ptr_vector core; + while (is_sat == l_false) { + core.reset(); + m_s->get_unsat_core(core); + is_sat = minimize_core(core); + if (is_sat != l_true) { break; - case l_true: - TRACE("opt", - tout << "num cores: " << cores.size() << "\n"; - tout << "num satisfying: " << asms.size() << "\n";); - return l_true; - default: - return l_undef; } - } + cores.push_back(core); + break; + // + // TBD: multiple core refinement + // produces unsound results. + // what is a sound variant? + // + remove_soft(core, asms); + is_sat = m_s->check_sat(asms.size(), asms.c_ptr()); + + } + TRACE("opt", + tout << "num cores: " << cores.size() << "\n"; + for (unsigned i = 0; i < cores.size(); ++i) { + for (unsigned j = 0; j < cores[i].size(); ++j) { + tout << mk_pp(cores[i][j], m) << " "; + } + tout << "\n"; + } + tout << "num satisfying: " << asms.size() << "\n";); + + return is_sat; } lbool process_unsat(ptr_vector& core) { expr_ref fml(m); - TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());); SASSERT(!core.empty()); if (core.empty()) { return l_false; } remove_soft(core); rational w = split_soft(core); - TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); + TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr()); + for (unsigned i = 0; i < core.size(); ++i) { + tout << get_weight(core[i]) << " "; + } + tout << "min-weight: " << w << "\n";); max_resolve(core, w); - m_lower += w; + m_lower += w; IF_VERBOSE(1, verbose_stream() << "(opt.dual_max_res [" << m_lower << ":" << m_upper << "])\n";); - return l_true; } @@ -261,9 +265,7 @@ public: switch (is_sat) { case l_false: if (num_true*2 < m_asms.size()) { - soft_compl.reset(); - m_s->get_unsat_core(soft_compl); - return minimize_core(soft_compl); + return l_false; } break; case l_true: diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index 792686f69..506e3227c 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -11,6 +11,7 @@ #include "bit_blaster_tactic.h" #include "simplify_tactic.h" #include "goal2sat.h" +#include "ast_pp.h" // incremental SAT solver. class inc_sat_solver : public solver { @@ -78,11 +79,10 @@ public: for (unsigned i = 0; i < num_assumptions; ++i) { g->assert_expr(assumptions[i], m.mk_leaf(assumptions[i])); } - TRACE("opt", g->display(tout);); + TRACE("opt", g->display_with_dependencies(tout);); m_fmls.reset(); try { (*m_preprocess)(g, result, mc, pc, core); - TRACE("opt", result[0]->display(tout);); } catch (tactic_exception & ex) { IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); @@ -95,7 +95,7 @@ public: return l_undef; } g = result[0]; - TRACE("opt", g->display(tout);); + TRACE("opt", g->display_with_dependencies(tout);); m_goal2sat(*g, m_params, m_solver, m_map, dep2asm); } @@ -185,8 +185,24 @@ private: asm2dep.insert(it->m_value.index(), it->m_key); } sat::literal_vector const& core = m_solver.get_core(); + + TRACE("opt", + dep2asm_t::iterator it = dep2asm.begin(); + dep2asm_t::iterator end = dep2asm.end(); + for (; it != end; ++it) { + tout << mk_pp(it->m_key, m) << " |-> " << it->m_value << "\n"; + } + tout << "core: "; + for (unsigned i = 0; i < core.size(); ++i) { + tout << core[i] << " "; + } + tout << "\n"; + ); + for (unsigned i = 0; i < core.size(); ++i) { - m_core.push_back(asm2dep.find(core[i].index())); + expr* e; + if (asm2dep.find(core[i].index(), e)) + m_core.push_back(e); } } diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 4cfab6376..9ce2dd187 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -129,7 +129,7 @@ struct mus::imp { add_core(core, assumptions); lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr()); assumptions.resize(sz); - switch(is_sat) { + switch (is_sat) { case l_undef: return is_sat; case l_true: @@ -160,6 +160,14 @@ struct mus::imp { break; } } + DEBUG_CODE( + assumptions.reset(); + for (unsigned i = 0; i < mus.size(); ++i) { + assumptions.push_back(m_cls2expr[mus[i]].get()); + } + lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr()); + SASSERT(is_sat == l_false); + ); return l_true; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index bf6d0953f..1d3d3ce71 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2141,6 +2141,9 @@ namespace sat { // void solver::user_push() { + if (m_level.size() == 0) { + return; + } literal lit; if (m_user_scope_literal_pool.empty()) { bool_var new_v = mk_var(true, false); @@ -2183,7 +2186,7 @@ namespace sat { void solver::user_pop(unsigned num_scopes) { pop_to_base_level(); - while (num_scopes > 0) { + while (num_scopes > 0 && !m_user_scope_literals.empty()) { literal lit = m_user_scope_literals.back(); m_user_scope_literal_pool.push_back(lit); m_user_scope_literals.pop_back(); diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 26bea6343..a433dd307 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -198,7 +198,7 @@ public: m_rw1(g->form(idx), new_f1); TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); m_rw2(new_f1, new_f2); - g->update(idx, new_f2); + g->update(idx, new_f2, g->pr(idx), g->dep(idx)); } g->inc_depth();