diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 2422f3fd1..32456445c 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -126,7 +126,7 @@ namespace dd { * Example: 2^4*x + 2 is non-zero for every x. */ - bool pdd_manager::is_non_zero(PDD p) { + bool pdd_manager::is_never_zero(PDD p) { if (is_val(p)) return !is_zero(p); if (m_semantics != mod2N_e) diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 28d273966..79ee3cb5b 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -206,7 +206,7 @@ namespace dd { inline bool is_one(PDD p) const { return p == one_pdd; } inline bool is_val(PDD p) const { return m_nodes[p].is_val(); } inline bool is_internal(PDD p) const { return m_nodes[p].is_internal(); } - bool is_non_zero(PDD p); + bool is_never_zero(PDD p); inline unsigned level(PDD p) const { return m_nodes[p].m_level; } inline unsigned var(PDD p) const { return m_level2var[level(p)]; } inline PDD lo(PDD p) const { return m_nodes[p].m_lo; } @@ -343,7 +343,7 @@ namespace dd { bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_binary() const { return m.is_binary(root); } bool is_monomial() const { return m.is_monomial(root); } - bool is_non_zero() const { return m.is_non_zero(root); } + bool is_never_zero() const { return m.is_never_zero(root); } bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); } pdd operator-() const { return m.minus(*this); } diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp index 219f6eca6..c7258205b 100644 --- a/src/math/polysat/polysat.cpp +++ b/src/math/polysat/polysat.cpp @@ -73,20 +73,18 @@ namespace polysat { return l_undef; } - struct solver::t_del_var : public trail { solver& s; t_del_var(solver& s): s(s) {} void undo() override { s.del_var(); } }; - solver::solver(trail_stack& s, reslimit& lim): m_trail(s), m_lim(lim), m_bdd(1000), - m_dep_manager(m_value_manager, m_alloc), - m_conflict_dep(nullptr, m_dep_manager), + m_dm(m_value_manager, m_alloc), + m_conflict_dep(nullptr, m_dm), m_free_vars(m_activity) { } @@ -108,7 +106,7 @@ namespace polysat { m_value.push_back(rational::zero()); m_justification.push_back(justification::unassigned()); m_viable.push_back(m_bdd.mk_true()); - m_vdeps.push_back(m_dep_manager.mk_empty()); + m_vdeps.push_back(m_dm.mk_empty()); m_cjust.push_back(constraints()); m_watch.push_back(ptr_vector()); m_activity.push_back(0); @@ -134,7 +132,7 @@ namespace polysat { } void solver::add_eq(pdd const& p, unsigned dep) { - p_dependency_ref d(mk_dep(dep), m_dep_manager); + p_dependency_ref d(mk_dep(dep), m_dm); constraint* c = constraint::eq(m_level, p, d); m_constraints.push_back(c); add_watch(*c); @@ -178,7 +176,7 @@ namespace polysat { if (!dep) return; m_trail.push(vector_value_trail(m_vdeps, var)); - m_vdeps[var] = m_dep_manager.mk_join(m_vdeps[var], dep); + m_vdeps[var] = m_dm.mk_join(m_vdeps[var], dep); } bool solver::can_propagate() { @@ -232,15 +230,11 @@ namespace polysat { } } - vector> sub; - for (auto w : vars) - if (is_assigned(w)) - sub.push_back(std::make_pair(w, m_value[w])); - auto p = c.p().subst_val(sub); + auto p = c.p().subst_val(m_sub); if (p.is_zero()) return false; - if (p.is_non_zero()) { + if (p.is_never_zero()) { // we could tag constraint to allow early substitution before // swapping watch variable in case we can detect conflict earlier. set_conflict(c); @@ -266,7 +260,7 @@ namespace polysat { VERIFY(a.mult_inverse(sz, inv_a)); rational val = mod(inv_a * -b, rational::power_of_two(sz)); m_cjust[other_var].push_back(&c); - propagate(other_var, val, justification::propagation(m_level)); + propagate(other_var, val, c); return false; } @@ -277,12 +271,11 @@ namespace polysat { return false; } - void solver::propagate(unsigned var, rational const& val, justification const& j) { - SASSERT(j.is_propagation()); + void solver::propagate(unsigned var, rational const& val, constraint& c) { if (is_viable(var, val)) - assign_core(var, val, j); + assign_core(var, val, justification::propagation(m_level)); else - set_conflict(*m_cjust[var].back()); + set_conflict(c); } void solver::push_level() { @@ -312,9 +305,8 @@ namespace polysat { */ void solver::pop_assignment() { while (!m_search.empty() && m_justification[m_search.back()].level() > m_level) { - auto v = m_search.back(); undo_var(m_search.back()); - m_search.pop_back(); + pop_search(); } } @@ -322,7 +314,18 @@ namespace polysat { m_justification[v] = justification::unassigned(); m_free_vars.unassign_var_eh(v); m_cjust[v].reset(); - m_viable[v] = m_bdd.mk_true(); + m_viable[v] = m_bdd.mk_true(); // TBD does not work with external bit-assignments + } + + void solver::pop_search() { + m_search.pop_back(); + m_sub.pop_back(); + } + + void solver::push_search(unsigned var, rational const& val) { + m_search.push_back(var); + m_value[var] = val; + m_sub.push_back(std::make_pair(var, val)); } void solver::add_watch(constraint& c) { @@ -361,7 +364,7 @@ namespace polysat { unsigned var = m_free_vars.next_var(); switch (find_viable(var, val)) { case l_false: - set_conflict(m_cjust[var]); + set_conflict(var); break; case l_true: assign_core(var, val, justification::propagation(m_level)); @@ -375,15 +378,30 @@ namespace polysat { void solver::assign_core(unsigned var, rational const& val, justification const& j) { SASSERT(is_viable(var, val)); - m_search.push_back(var); - m_value[var] = val; + push_search(var, val); m_justification[var] = j; } + + void solver::set_conflict(constraint& c) { + SASSERT(m_conflict_cs.empty()); + m_conflict_cs.push_back(&c); + m_conflict_dep = nullptr; + } + + void solver::set_conflict(unsigned v) { + SASSERT(m_conflict_cs.empty()); + m_conflict_cs.append(m_cjust[v]); + m_conflict_dep = m_vdeps[v]; + if (m_cjust[v].empty()) + m_conflict_cs.push_back(nullptr); + } + /** * Conflict resolution. - * - m_conflict are constraints that are infeasible in the current assignment. - * 1. walk m_search from top down until last variable in m_conflict. + * - m_conflict_cs are constraints that are infeasible in the current assignment. + * - m_conflict_dep are dependencies for infeasibility + * 1. walk m_search from top down until last variable in m_conflict_cs. * 2. resolve constraints in m_cjust to isolate lowest degree polynomials * using variable. * Use Olm-Seidl division by powers of 2 to preserve invertibility. @@ -399,12 +417,10 @@ namespace polysat { * */ void solver::resolve_conflict() { + vector ps = init_conflict(); unsigned v = UINT_MAX; unsigned i = m_search.size(); - vector> sub; - for (auto w : m_search) - sub.push_back(std::make_pair(w, m_value[w])); for (; i-- > 0; ) { v = m_search[i]; @@ -422,12 +438,12 @@ namespace polysat { return; } pdd r = resolve(v, ps); - pdd rval = r.subst_val(sub); - if (r.is_val() && rval.is_non_zero()) { + pdd rval = r.subst_val(m_sub); + if (r.is_val() && rval.is_never_zero()) { report_unsat(); return; } - if (!rval.is_non_zero()) { + if (!rval.is_never_zero()) { backtrack(i); return; } @@ -442,28 +458,23 @@ namespace polysat { } vector solver::init_conflict() { - SASSERT(!m_conflict.empty()); + SASSERT(!m_conflict_cs.empty()); + m_conflict_level = 0; vector ps; reset_marks(); - m_conflict_level = 0; - m_conflict_dep = nullptr; - for (auto* c : m_conflict) { + for (auto* c : m_conflict_cs) { + if (!c) + continue; for (auto v : c->vars()) set_mark(v); ps.push_back(c->p()); m_conflict_level = std::max(m_conflict_level, c->level()); - m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep, c->dep()); + m_conflict_dep = m_dm.mk_join(m_conflict_dep, c->dep()); } - m_conflict.reset(); + m_conflict_cs.reset(); return ps; } - /** - * TBD: m_conflict_dep is a justification that m_value[v] is not viable. - * it is currently not yet being accounted for. - * A more general data-structure could be to maintain a p_dependency - * with each variable state. The dependencies are augmented on backtracking. - */ void solver::backtrack(unsigned i) { do { auto v = m_search[i]; @@ -481,16 +492,17 @@ namespace polysat { void solver::report_unsat() { backjump(base_level()); - m_conflict.push_back(nullptr); + SASSERT(m_conflict_cs.empty()); + m_conflict_cs.push_back(nullptr); } void solver::unsat_core(unsigned_vector& deps) { deps.reset(); - for (auto* c : m_conflict) { + for (auto* c : m_conflict_cs) { if (c) - m_conflict_dep = m_dep_manager.mk_join(c->dep(), m_conflict_dep); + m_conflict_dep = m_dm.mk_join(c->dep(), m_conflict_dep); } - m_dep_manager.linearize(m_conflict_dep, deps); + m_dm.linearize(m_conflict_dep, deps); } @@ -520,16 +532,15 @@ namespace polysat { backjump(new_level + 1); while (m_search.back() != v) { undo_var(m_search.back()); - m_search.pop_back(); + pop_search(); } SASSERT(!m_search.empty()); SASSERT(m_search.back() == v); - m_search.pop_back(); + pop_search(); add_non_viable(v, m_value[v]); add_viable_dep(v, m_conflict_dep); m_qhead = m_search.size(); rational value; - m_conflict_dep = nullptr; switch (find_viable(v, value)) { case l_true: assign_core(v, value, justification::propagation(new_level)); @@ -538,7 +549,7 @@ namespace polysat { assign_core(v, value, justification::decision(new_level)); break; case l_false: - set_conflict(m_cjust[v]); + set_conflict(v); break; } } @@ -569,6 +580,7 @@ namespace polysat { auto const& cs = m_cjust[v]; pdd r = isolate(v, ps); auto degree = r.degree(v); + m_conflict_dep = m_dm.mk_join(m_conflict_dep, m_vdeps[v]); while (degree > 0) { for (auto * c : cs) { if (degree >= c->p().degree(v)) { @@ -576,7 +588,7 @@ namespace polysat { // add parity condition to presere falsification degree = r.degree(v); m_conflict_level = std::max(m_conflict_level, c->level()); - m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep.get(), c->dep()); + m_conflict_dep = m_dm.mk_join(m_conflict_dep.get(), c->dep()); } } } @@ -624,6 +636,10 @@ namespace polysat { } std::ostream& solver::display(std::ostream& out) const { + for (auto v : m_search) { + out << "v" << v << " := " << m_value[v] << "\n"; + out << m_viable[v] << "\n"; + } for (auto* c : m_constraints) out << *c << "\n"; for (auto* c : m_redundant) diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h index d17b1ddfe..26086764e 100644 --- a/src/math/polysat/polysat.h +++ b/src/math/polysat/polysat.h @@ -32,6 +32,7 @@ namespace polysat { typedef dd::bdd bdd; const unsigned null_dependency = UINT_MAX; + const unsigned null_var = UINT_MAX; struct dep_value_manager { void inc_ref(unsigned) {} @@ -120,9 +121,10 @@ namespace polysat { dd::bdd_manager m_bdd; dep_value_manager m_value_manager; small_object_allocator m_alloc; - poly_dep_manager m_dep_manager; - p_dependency_ref m_conflict_dep; + poly_dep_manager m_dm; var_queue m_free_vars; + p_dependency_ref m_conflict_dep; + ptr_vector m_conflict_cs; // Per constraint state scoped_ptr_vector m_constraints; @@ -133,7 +135,7 @@ namespace polysat { ptr_vector m_vdeps; // dependencies for viable values vector m_value; // assigned value vector m_justification; // justification for variable assignment - vector m_cjust; // constraints used for justification + vector m_cjust; // constraints justifying variable range. vector m_watch; // watch list datastructure into constraints. unsigned_vector m_activity; vector m_vars; @@ -141,6 +143,8 @@ namespace polysat { // search state that lists assigned variables unsigned_vector m_search; + vector> m_sub; + unsigned m_qhead { 0 }; unsigned m_level { 0 }; @@ -190,6 +194,9 @@ namespace polysat { void pop_assignment(); void pop_constraints(scoped_ptr_vector& cs); + void push_search(unsigned v, rational const& val); + void pop_search(); + void assign_core(unsigned var, rational const& val, justification const& j); bool is_assigned(unsigned var) const { return !m_justification[var].is_unassigned(); } @@ -197,13 +204,13 @@ namespace polysat { void propagate(unsigned v); bool propagate(unsigned v, constraint& c); bool propagate_eq(unsigned v, constraint& c); - void propagate(unsigned var, rational const& val, justification const& j); + void propagate(unsigned var, rational const& val, constraint& c); void erase_watch(unsigned v, constraint& c); void erase_watch(constraint& c); void add_watch(constraint& c); - void set_conflict(constraint& c) { m_conflict.push_back(&c); } - void set_conflict(ptr_vector& cs) { m_conflict.append(cs); } + void set_conflict(constraint& c); + void set_conflict(unsigned v); unsigned_vector m_marks; unsigned m_clock { 0 }; @@ -219,7 +226,7 @@ namespace polysat { bool can_decide() const { return !m_free_vars.empty(); } void decide(); - p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dep_manager.mk_leaf(dep); } + p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); } bool is_conflict() const { return !m_conflict.empty(); } bool at_base_level() const; diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp index b10abb891..a1f4765ea 100644 --- a/src/test/pdd.cpp +++ b/src/test/pdd.cpp @@ -314,12 +314,12 @@ public : std::cout << "sub 2 " << p.subst_val(sub2) << "\n"; std::cout << "sub 3 " << p.subst_val(sub3) << "\n"; - std::cout << "expect 1 " << (2*a + 1).is_non_zero() << "\n"; - std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_non_zero() << "\n"; - std::cout << "expect 0 " << (2*a + 2).is_non_zero() << "\n"; - SASSERT((2*a + 1).is_non_zero()); - SASSERT((2*a + 2*b + 1).is_non_zero()); - SASSERT(!(2*a*b + 3*b + 2).is_non_zero()); + std::cout << "expect 1 " << (2*a + 1).is_never_zero() << "\n"; + std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_never_zero() << "\n"; + std::cout << "expect 0 " << (2*a + 2).is_never_zero() << "\n"; + SASSERT((2*a + 1).is_never_zero()); + SASSERT((2*a + 2*b + 1).is_never_zero()); + SASSERT(!(2*a*b + 3*b + 2).is_never_zero()); } };