mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

flush gmc for sat-preprocessor model bug #4532

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-26 14:30:48 -07:00
parent e8ef9a85a4
commit ac39ddb43f
3 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_model_converter.h
View file

@ -81,7 +81,7 @@ namespace sat {
private:
vector<entry> m_entries; // entries accumulated during SAT search
unsigned m_exposed_lim; // last entry that was exposed to model converter.
bool_vector m_mark; // literals that are used in asserted clauses.
bool_vector m_mark; // literals that are used in asserted clauses.
solver const* m_solver;
elim_stackv m_elim_stack;

6
src/sat/sat_solver.cpp
View file

@ -91,9 +91,9 @@ namespace sat {
solver::~solver() {
m_ext = nullptr;
SASSERT(m_config.m_num_threads > 1 || check_invariant());
TRACE("sat", tout << "Delete clauses\n";);
CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";);
del_clauses(m_clauses);
TRACE("sat", tout << "Delete learned\n";);
CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";);
del_clauses(m_learned);
dealloc(m_cuber);
m_cuber = nullptr;
@ -1207,6 +1207,7 @@ namespace sat {
propagate(false);
if (check_inconsistent()) return l_false;
if (m_config.m_force_cleanup) do_cleanup(true);
TRACE("sat", display(tout););
if (m_config.m_gc_burst) {
// force gc
@ -1221,6 +1222,7 @@ namespace sat {
if (m_config.m_max_conflicts == 0) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
TRACE("sat", display(tout); m_mc.display(tout););
return l_undef;
}

12
src/sat/tactic/goal2sat.cpp
View file

@ -965,8 +965,10 @@ void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
s.flush(m_smc);
m_var2expr.resize(s.num_vars());
map.mk_var_inv(m_var2expr);
flush_gmc();
}
void sat2goal::mc::flush_gmc() {
sat::literal_vector updates;
m_smc.expand(updates);
@ -1072,14 +1074,15 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
}
expr_ref sat2goal::mc::lit2expr(sat::literal l) {
if (!m_var2expr.get(l.var())) {
sat::bool_var v = l.var();
if (!m_var2expr.get(v)) {
app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
m_var2expr.set(l.var(), aux);
m_var2expr.set(v, aux);
if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
m_gmc->hide(aux->get_decl());
}
VERIFY(m_var2expr.get(l.var()));
expr_ref result(m_var2expr.get(l.var()), m);
VERIFY(m_var2expr.get(v));
expr_ref result(m_var2expr.get(v), m);
if (l.sign()) {
result = m.mk_not(result);
}
@ -1210,7 +1213,6 @@ struct sat2goal::imp {
checkpoint();
r.assert_expr(lit2expr(mc, s.trail_literal(i)));
}
// collect binary clauses
svector<sat::solver::bin_clause> bin_clauses;
s.collect_bin_clauses(bin_clauses, m_learned, false);