From ca309341c3de0e3762acf663263e9cbc8b69eabb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Oct 2016 22:07:46 -0700 Subject: [PATCH] fixing cancellation code paths for inc_sat_solver Signed-off-by: Nikolaj Bjorner --- .../bit_blaster/bit_blaster_rewriter.cpp | 9 ++++++ .../bit_blaster/bit_blaster_rewriter.h | 1 + src/sat/sat_solver.cpp | 29 ++++++++++++------- src/sat/sat_solver/inc_sat_solver.cpp | 14 ++++++--- .../portfolio/bounded_int2bv_solver.cpp | 3 +- 5 files changed, 41 insertions(+), 15 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index c260178ad..e8d8c4e4b 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -165,6 +165,10 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { m_keyval_lim.push_back(m_keys.size()); } + unsigned get_num_scopes() const { + return m_keyval_lim.size(); + } + void pop(unsigned num_scopes) { if (num_scopes > 0) { SASSERT(num_scopes <= m_keyval_lim.size()); @@ -637,6 +641,7 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl { } void push() { m_cfg.push(); } void pop(unsigned s) { m_cfg.pop(s); } + unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); } }; bit_blaster_rewriter::bit_blaster_rewriter(ast_manager & m, params_ref const & p): @@ -680,3 +685,7 @@ void bit_blaster_rewriter::operator()(expr * e, expr_ref & result, proof_ref & r m_imp->operator()(e, result, result_proof); } +unsigned bit_blaster_rewriter::get_num_scopes() const { + return m_imp->get_num_scopes(); +} + diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h index b23daab3a..8db328ec8 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h @@ -37,6 +37,7 @@ public: void operator()(expr * e, expr_ref & result, proof_ref & result_proof); void push(); void pop(unsigned num_scopes); + unsigned get_num_scopes() const; }; #endif diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 831eb228f..e70a30a5a 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3158,7 +3158,14 @@ namespace sat { init_search(); propagate(false); if (inconsistent()) return l_false; - init_assumptions(asms.size(), asms.c_ptr(), 0, 0); + if (asms.empty()) { + bool_var v = mk_var(true, false); + literal lit(v, false); + init_assumptions(1, &lit, 0, 0); + } + else { + init_assumptions(asms.size(), asms.c_ptr(), 0, 0); + } propagate(false); if (check_inconsistent()) return l_false; @@ -3169,6 +3176,7 @@ namespace sat { checkpoint(); literal_set::iterator it = vars.begin(), end = vars.end(); unsigned num_resolves = 0; + lbool is_sat = l_true; for (; it != end; ++it) { literal lit = *it; if (value(lit) != l_undef) { @@ -3179,8 +3187,10 @@ namespace sat { propagate(false); while (inconsistent()) { if (!resolve_conflict()) { - TRACE("sat", tout << "inconsistent\n";); - return l_false; + TRACE("sat", display(tout << "inconsistent\n");); + m_inconsistent = false; + is_sat = l_undef; + break; } propagate(false); ++num_resolves; @@ -3189,17 +3199,16 @@ namespace sat { break; } } - lbool is_sat; - while (true) { + if (is_sat == l_true) { if (scope_lvl() == 1 && num_resolves > 0) { is_sat = l_undef; - break; } - is_sat = bounded_search(); - if (is_sat == l_undef) { - restart(); + else { + is_sat = bounded_search(); + if (is_sat == l_undef) { + restart(); + } } - break; } if (is_sat == l_false) { TRACE("sat", tout << "unsat\n";); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 592603e53..f5efed726 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -234,6 +234,7 @@ public: } virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { + init_preprocess(); TRACE("sat", tout << assumptions << "\n" << vars << "\n";); sat::literal_vector asms; sat::bool_var_vector bvars; @@ -341,7 +342,7 @@ public: mk_bit_blaster_tactic(m, m_bb_rewriter.get()), //mk_aig_tactic(), using_params(mk_simplify_tactic(m), simp2_p)); - for (unsigned i = 0; i < m_num_scopes; ++i) { + while (m_bb_rewriter->get_num_scopes() < m_num_scopes) { m_bb_rewriter->push(); } m_preprocess->reset(); @@ -364,6 +365,7 @@ private: } catch (tactic_exception & ex) { IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); + TRACE("sat", tout << "exception: " << ex.msg() << "\n";); m_preprocess = 0; m_bb_rewriter = 0; return l_undef; @@ -518,10 +520,14 @@ private: } dep2asm_t dep2asm; goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled - for (; m_fmls_head < m_fmls.size(); ++m_fmls_head) { - g->assert_expr(m_fmls[m_fmls_head].get()); + for (unsigned i = 0 ; i < m_fmls.size(); ++i) { + g->assert_expr(m_fmls[i].get()); } - return internalize_goal(g, dep2asm); + lbool res = internalize_goal(g, dep2asm); + if (res != l_undef) { + m_fmls_head = m_fmls.size(); + } + return res; } void extract_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 688d9403a..f8b2f5325 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -247,8 +247,9 @@ private: expr_ref t(m.mk_const(fbv), m); t = m_bv.mk_bv2int(t); if (!offset.is_zero()) { - t = m_arith.mk_add(t, m_arith.mk_numeral(lo, true)); + t = m_arith.mk_add(t, m_arith.mk_numeral(offset, true)); } + TRACE("pb", tout << lo << " <= " << hi << " offset: " << offset << "\n"; tout << mk_pp(e, m) << " |-> " << t << "\n";); sub.insert(e, t); } else {