diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index d1225ced9..eaa088e85 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2504,7 +2504,7 @@ namespace sat { } void ba_solver::remove_constraint(constraint& c, char const* reason) { - TRACE("ba", tout << "remove " << c << " " << reason << "\n";); + TRACE("ba", display(tout << "remove ", c, true) << " " << reason << "\n";); IF_VERBOSE(21, display(verbose_stream() << "remove " << reason << " ", c, true);); nullify_tracking_literal(c); clear_watch(c); @@ -2991,7 +2991,7 @@ namespace sat { init_use_lists(); remove_unused_defs(); set_non_external(); - if (get_config().m_elim_vars) elim_pure(); + if (get_config().m_elim_vars && !s().get_config().m_incremental && !s().tracking_assumptions()) elim_pure(); for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]); for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); unit_strengthen(); @@ -4371,7 +4371,7 @@ namespace sat { SASSERT(c1.index() != c2.index()); if (subsumes(c1, c2, slit)) { if (slit.empty()) { - TRACE("ba", tout << "subsume cardinality\n" << c1.index() << ":" << c1 << "\n" << c2.index() << ":" << c2 << "\n";); + TRACE("ba", tout << "subsume cardinality\n" << c1 << "\n" << c2.index() << ":" << c2 << "\n";); remove_constraint(c2, "subsumed"); ++m_stats.m_num_pb_subsumes; set_non_learned(c1); @@ -4789,13 +4789,14 @@ namespace sat { return out << index2constraint(idx); } - void ba_solver::display(std::ostream& out, constraint const& c, bool values) const { + std::ostream& ba_solver::display(std::ostream& out, constraint const& c, bool values) const { switch (c.tag()) { case card_t: display(out, c.to_card(), values); break; case pb_t: display(out, c.to_pb(), values); break; case xr_t: display(out, c.to_xr(), values); break; default: UNREACHABLE(); break; } + return out; } void ba_solver::collect_statistics(statistics& st) const { diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 56cebe557..cbbd49ebe 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -608,7 +608,7 @@ namespace sat { bool check_model(model const& m) const override; ptr_vector const & constraints() const { return m_constraints; } - void display(std::ostream& out, constraint const& c, bool values) const; + std::ostream& display(std::ostream& out, constraint const& c, bool values) const; bool validate() override; diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 4b0abd3b6..0abb38eae 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -68,7 +68,6 @@ namespace sat { void model_converter::operator()(model & m) const { bool first = false; - TRACE("sat", display(tout);); literal_vector clause; for (unsigned i = m_entries.size(); i-- > m_exposed_lim; ) { entry const& e = m_entries[i]; @@ -86,7 +85,7 @@ namespace sat { // end of clause VERIFY (sat || e.get_kind() != ATE); if (!sat && e.get_kind() != ATE && v0 != null_bool_var) { - VERIFY(legal_to_flip(v0)); + VERIFY(legal_to_flip(v0)); m[v0] = var_sign ? l_false : l_true; } elim_stack* st = e.m_elim_stack[index]; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e781089c1..6dcfd0c75 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -869,7 +869,10 @@ private: return; } TRACE("sat", m_solver.display_model(tout);); - sat::model const & ll_m = m_solver.get_model(); + sat::model ll_m = m_solver.get_model(); + if (m_sat_mc) { + (*m_sat_mc)(ll_m); + } mdl = alloc(model, m); for (sat::bool_var v = 0; v < ll_m.size(); ++v) { expr* n = m_sat_mc->var2expr(v); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 884b533cd..541fbc47b 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1002,43 +1002,11 @@ void sat2goal::mc::get_units(obj_map& units) { } +void sat2goal::mc::operator()(sat::model& md) { + m_smc(md); +} + void sat2goal::mc::operator()(model_ref & md) { - model_evaluator ev(*md); - ev.set_model_completion(false); - - // create a SAT model using md - sat::model sat_md; - expr_ref val(m); - for (expr * atom : m_var2expr) { - if (!atom) { - sat_md.push_back(l_undef); - continue; - } - ev(atom, val); - if (m.is_true(val)) - sat_md.push_back(l_true); - else if (m.is_false(val)) - sat_md.push_back(l_false); - else - sat_md.push_back(l_undef); - } - - // apply SAT model converter - m_smc(sat_md); - - // register value of non-auxiliary boolean variables back into md - unsigned sz = m_var2expr.size(); - for (sat::bool_var v = 0; v < sz; v++) { - app * atom = m_var2expr.get(v); - if (atom && is_uninterp_const(atom)) { - func_decl * d = atom->get_decl(); - lbool new_val = sat_md[v]; - if (new_val == l_true) - md->register_decl(d, m.mk_true()); - else if (new_val == l_false) - md->register_decl(d, m.mk_false()); - } - } // apply externalized model converter if (m_gmc) (*m_gmc)(md); TRACE("sat_mc", tout << "after sat_mc\n"; model_v2_pp(tout, *md);); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 2177ca34d..31e94bd74 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -79,7 +79,7 @@ public: ast_manager& m; sat::model_converter m_smc; generic_model_converter_ref m_gmc; - app_ref_vector m_var2expr; + app_ref_vector m_var2expr; // flushes from m_smc to m_gmc; void flush_gmc(); @@ -88,7 +88,8 @@ public: mc(ast_manager& m); ~mc() override {} // flush model converter from SAT solver to this structure. - void flush_smc(sat::solver_core& s, atom2bool_var const& map); + void flush_smc(sat::solver_core& s, atom2bool_var const& map); + void operator()(sat::model& m); void operator()(model_ref& md) override; void operator()(expr_ref& fml) override; model_converter* translate(ast_translation& translator) override;