diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp index 87fdb53c8..390ab87b7 100644 --- a/src/math/polysat/clause_builder.cpp +++ b/src/math/polysat/clause_builder.cpp @@ -17,8 +17,13 @@ Author: namespace polysat { + static_assert(!std::is_copy_assignable_v); + static_assert(!std::is_copy_constructible_v); + static_assert(std::is_move_assignable_v); + static_assert(std::is_move_constructible_v); + clause_builder::clause_builder(solver& s): - m_solver(s), m_dep(nullptr, s.m_dm) + m_solver(&s), m_dep(nullptr, s.m_dm) {} void clause_builder::reset() { @@ -29,7 +34,6 @@ namespace polysat { } clause_ref clause_builder::build() { - // TODO: here we could set all the levels of the new constraints. so we do not have to compute the max at every use site. clause_ref cl = clause::from_literals(m_level, std::move(m_dep), std::move(m_literals)); m_level = 0; SASSERT(empty()); @@ -37,11 +41,11 @@ namespace polysat { } void clause_builder::add_dependency(p_dependency* d) { - m_dep = m_solver.m_dm.mk_join(m_dep, d); + m_dep = m_solver->m_dm.mk_join(m_dep, d); } - void clause_builder::push_literal(sat::literal lit) { - push(m_solver.m_constraints.lookup(lit)); + void clause_builder::push(sat::literal lit) { + push(m_solver->m_constraints.lookup(lit)); } void clause_builder::push(signed_constraint c) { diff --git a/src/math/polysat/clause_builder.h b/src/math/polysat/clause_builder.h index 84792da3e..f51bfa639 100644 --- a/src/math/polysat/clause_builder.h +++ b/src/math/polysat/clause_builder.h @@ -25,13 +25,17 @@ namespace polysat { // TODO: this is now incorporated in conflict_core class clause_builder { - solver& m_solver; + solver* m_solver; sat::literal_vector m_literals; p_dependency_ref m_dep; unsigned m_level = 0; public: clause_builder(solver& s); + clause_builder(clause_builder const& s) = delete; + clause_builder(clause_builder&& s) = default; + clause_builder& operator=(clause_builder const& s) = delete; + clause_builder& operator=(clause_builder&& s) = default; bool empty() const { return m_literals.empty() && m_dep == nullptr && m_level == 0; } void reset(); @@ -43,15 +47,9 @@ namespace polysat { void add_dependency(p_dependency* d); - /// Add a literal to the clause. - /// Intended to be used for literals representing a constraint that already exists. - void push_literal(sat::literal lit); - + void push(sat::literal lit); void push(signed_constraint c); - /// Add a constraint to the clause that does not yet exist in the solver so far. - // void push_new_constraint(signed_constraint c); - using const_iterator = decltype(m_literals)::const_iterator; const_iterator begin() const { return m_literals.begin(); } const_iterator end() const { return m_literals.end(); } diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp index 642848f65..3648ac299 100644 --- a/src/math/polysat/conflict_core.cpp +++ b/src/math/polysat/conflict_core.cpp @@ -149,10 +149,10 @@ namespace polysat { clause_builder c_lemma(*m_solver); for (auto premise : premises) { handle_saturation_premises(premise); - c_lemma.push_literal(~premise.blit()); + c_lemma.push(~premise.blit()); active_level = std::max(active_level, m_solver->m_bvars.level(premise.blit())); } - c_lemma.push_literal(c.blit()); + c_lemma.push(c.blit()); clause* cl = cm().store(c_lemma.build()); if (cl->size() == 1) c->set_unit_clause(cl); @@ -180,10 +180,10 @@ namespace polysat { pvar v = item.var(); auto c = ~cm().eq(0, m_solver->var(v) - m_solver->m_value[v]); cm().ensure_bvar(c.get()); - lemma.push_literal(c.blit()); + lemma.push(c.blit()); } else { sat::literal lit = item.lit(); - lemma.push_literal(~lit); + lemma.push(~lit); } --todo; } @@ -228,10 +228,12 @@ namespace polysat { } clause_builder conflict_core::build_lemma(unsigned reverted_level) { - if (is_bailout()) - return build_fallback_lemma(reverted_level); - else + if (!is_bailout()) return build_core_lemma(reverted_level); + else if (m_bailout_lemma) + return *std::move(m_bailout_lemma); + else + return build_fallback_lemma(reverted_level); } bool conflict_core::resolve_value(pvar v, vector const& cjust_v) { diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h index d64d2d78b..fea6dc355 100644 --- a/src/math/polysat/conflict_core.h +++ b/src/math/polysat/conflict_core.h @@ -14,6 +14,7 @@ Author: #pragma once #include "math/polysat/constraint.h" #include "math/polysat/clause_builder.h" +#include namespace polysat { @@ -38,6 +39,7 @@ namespace polysat { /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution. */ bool m_bailout = false; + std::optional m_bailout_lemma; solver* m_solver = nullptr; constraint_manager& cm(); @@ -69,6 +71,7 @@ namespace polysat { m_conflict_var = null_var; m_saturation_premises.reset(); m_bailout = false; + m_bailout_lemma.reset(); SASSERT(empty()); } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 14a7a007a..d3ef3f7fe 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -713,7 +713,7 @@ namespace polysat { // - drawback: might have to bail out at boolean resolution // Also: maybe we can skip ~L in some cases? but in that case it shouldn't be marked. // - reason_builder.push_literal(~lit); + reason_builder.push(~lit); } clause_ref reason = reason_builder.build();