diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 997ee971e..c0799c061 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -213,8 +213,8 @@ namespace sat { m_status.push_back(st); m_proof.push_back(&c); if (st == status::deleted) { - del_watch(c, c[0]); - del_watch(c, c[1]); + if (n > 0) del_watch(c, c[0]); + if (n > 1) del_watch(c, c[1]); return; } unsigned num_watch = 0; @@ -338,8 +338,9 @@ namespace sat { for (unsigned i = num_units; i < m_units.size(); ++i) { m_assignment[m_units[i].var()] = l_undef; } - m_units.resize(num_units); + m_units.shrink(num_units); bool ok = m_inconsistent; + IF_VERBOSE(9, verbose_stream() << "is-drup " << m_inconsistent << "\n"); m_inconsistent = false; return ok; @@ -583,6 +584,7 @@ namespace sat { } } void drat::add(literal l, bool learned) { + TRACE("sat", tout << "add: " << l << " " << (learned?"l":"t") << "\n";); declare(l); status st = get_status(learned); if (m_out) dump(1, &l, st); @@ -590,6 +592,7 @@ namespace sat { if (m_check) append(l, st); } void drat::add(literal l1, literal l2, bool learned) { + TRACE("sat", tout << "add: " << l1 << " " << l2 << " " << (learned?"l":"t") << "\n";); declare(l1); declare(l2); literal ls[2] = {l1, l2}; diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index ce2080f8c..77a5f973d 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -113,7 +113,7 @@ namespace sat { s.m_params.set_sym("phase", symbol("random")); } m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]); - m_solvers[i]->copy(s); + m_solvers[i]->copy(s, true); m_solvers[i]->set_par(this, i); push_child(m_solvers[i]->rlimit()); } @@ -235,7 +235,7 @@ namespace sat { // there could be multiple local search engines running at the same time. IF_VERBOSE(1, verbose_stream() << "(sat-parallel refresh :from " << m_num_clauses << " :to " << s.m_clauses.size() << ")\n";); m_solver_copy = alloc(solver, s.m_params, s.rlimit()); - m_solver_copy->copy(s); + m_solver_copy->copy(s, true); m_num_clauses = s.m_clauses.size(); } } @@ -292,7 +292,7 @@ namespace sat { { m_consumer_ready = true; if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) { - s.copy(*m_solver_copy); + s.copy(*m_solver_copy, true); copied = true; m_num_clauses = s.m_clauses.size(); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4354d91ea..4c5a8ac3d 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -95,7 +95,7 @@ namespace sat { if (ext) ext->set_solver(this); } - void solver::copy(solver const & src) { + void solver::copy(solver const & src, bool copy_learned) { pop_to_base_level(); del_clauses(m_clauses); del_clauses(m_learned); @@ -192,7 +192,7 @@ namespace sat { // copy high quality lemmas unsigned num_learned = 0; for (clause* c : src.m_learned) { - if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) { + if (copy_learned || c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) { buffer.reset(); for (literal l : *c) buffer.push_back(l); clause* c1 = mk_clause_core(buffer.size(), buffer.c_ptr(), true); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c8261397a..379a786d5 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -210,7 +210,7 @@ namespace sat { \pre the model converter of src and this must be empty */ - void copy(solver const & src); + void copy(solver const & src, bool copy_learned = false); // ----------------------- // diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index f020fd2ab..b9adba7cf 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -60,7 +60,7 @@ struct goal2sat::imp { sat::solver_core & m_solver; atom2bool_var & m_map; dep2asm_map & m_dep2asm; - sat::bool_var m_true; + sat::literal m_true; bool m_ite_extra; unsigned long long m_max_memory; expr_ref_vector m_trail; @@ -81,13 +81,14 @@ struct goal2sat::imp { m_default_external(default_external), m_is_lemma(false) { updt_params(p); - m_true = sat::null_bool_var; + m_true = sat::null_literal; } void updt_params(params_ref const & p) { m_ite_extra = p.get_bool("ite_extra", true); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_xor_solver = p.get_bool("xor_solver", false); + if (m_xor_solver) ensure_extension(); } void throw_op_not_handled(std::string const& s) { @@ -117,11 +118,11 @@ struct goal2sat::imp { m_solver.add_clause(num, lits, m_is_lemma); } - sat::bool_var mk_true() { - if (m_true == sat::null_bool_var) { + sat::literal mk_true() { + if (m_true == sat::null_literal) { // create fake variable to represent true; - m_true = m_solver.add_var(false); - mk_clause(sat::literal(m_true, false)); // v is true + m_true = sat::literal(m_solver.add_var(false), false); + mk_clause(m_true); // v is true } return m_true; } @@ -132,10 +133,10 @@ struct goal2sat::imp { sat::bool_var v = m_map.to_bool_var(t); if (v == sat::null_bool_var) { if (m.is_true(t)) { - l = sat::literal(mk_true(), sign); + l = sign ? ~mk_true() : mk_true(); } else if (m.is_false(t)) { - l = sat::literal(mk_true(), !sign); + l = sign ? mk_true() : ~mk_true(); } else { bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);