diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp index 52cd9ae08..95647e0b1 100644 --- a/src/math/dd/dd_bdd.cpp +++ b/src/math/dd/dd_bdd.cpp @@ -1181,14 +1181,14 @@ namespace dd { bdd bddv::all0() const { bdd r = m->mk_true(); - for (unsigned i = size(); i-- > 0; ) + for (unsigned i = 0; i < size() && !r.is_false(); ++i) r &= !m_bits[i]; return r; } bdd bddv::all1() const { bdd r = m->mk_true(); - for (unsigned i = size(); i-- > 0; ) + for (unsigned i = 0; i < size() && !r.is_false(); ++i) r &= m_bits[i]; return r; } diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index f2d774ecc..09dd6f084 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -12,6 +12,7 @@ z3_add_component(polysat solver.cpp ule_constraint.cpp var_constraint.cpp + viable.cpp COMPONENT_DEPENDENCIES util dd diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index d1f0a981c..d0e03dda0 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -63,24 +63,11 @@ namespace polysat { rational a = q.hi().val(); rational b = q.lo().val(); - bddv const& x = s.var2bits(v).var(); - if (b == 0 && a.is_odd()) { - // hacky test optimizing special case. - // general case is compute inverse(a)*-b for equality 2^k*a*x + b == 0 - // then constrain x. - // - s.intersect_viable(v, is_positive() ? x.all0() : !x.all0()); - } - else { - IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << "\n"); - - bddv lhs = a * x + b; - bdd xs = is_positive() ? lhs.all0() : !lhs.all0(); - s.intersect_viable(v, xs); - } + s.m_vble.intersect_eq(a, v, b, is_positive()); + rational val; - if (s.find_viable(v, val) == dd::find_t::singleton) + if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) s.propagate(v, val, *this); return; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 14cbc9061..353cc820a 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -34,6 +34,7 @@ namespace polysat { return *m_pdd[sz]; } +#if 0 dd::fdd const& solver::sz2bits(unsigned sz) { m_bits.reserve(sz + 1); auto* bits = m_bits[sz]; @@ -70,11 +71,14 @@ namespace polysat { return var2bits(v).find_hint(m_viable[v], m_value[v], val); } +#endif + solver::solver(reslimit& lim): m_lim(lim), - m_linear_solver(*this), - m_bdd(1000), + m_vble(*this), + // m_bdd(1000), m_dm(m_value_manager, m_alloc), + m_linear_solver(*this), m_free_vars(m_activity), m_bvars(), m_constraints(m_bvars) { @@ -85,31 +89,6 @@ namespace polysat { m_conflict.reset(); } -#if POLYSAT_LOGGING_ENABLED - void solver::log_viable() { - // only for small problems - if (m_viable.size() < 10) { - for (pvar v = 0; v < m_viable.size(); ++v) { - log_viable(v); - } - } - } - - void solver::log_viable(pvar v) { - if (size(v) <= 5) { - vector xs; - for (rational x = rational::zero(); x < rational::power_of_two(size(v)); x += 1) { - if (is_viable(v, x)) { - xs.push_back(x); - } - } - LOG("Viable for pvar " << v << ": " << xs); - } else { - LOG("Viable for pvar " << v << ": "); - } - } -#endif - bool solver::should_search() { return m_lim.inc() && @@ -126,7 +105,7 @@ namespace polysat { LOG("Free variables: " << m_free_vars); LOG("Assignment: " << assignments_pp(*this)); if (!m_conflict.empty()) LOG("Conflict: " << m_conflict); - IF_LOGGING(log_viable()); + IF_LOGGING(m_vble.log()); if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; } else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; } @@ -140,10 +119,10 @@ namespace polysat { } unsigned solver::add_var(unsigned sz) { - pvar v = m_viable.size(); + pvar v = m_value.size(); m_value.push_back(rational::zero()); m_justification.push_back(justification::unassigned()); - m_viable.push_back(m_bdd.mk_true()); + m_vble.push(); m_cjust.push_back(constraints()); m_watch.push_back(ptr_vector()); m_activity.push_back(0); @@ -161,8 +140,8 @@ namespace polysat { void solver::del_var() { // TODO also remove v from all learned constraints. - pvar v = m_viable.size() - 1; - m_viable.pop_back(); + pvar v = m_value.size() - 1; + m_vble.pop(); m_cjust.pop_back(); m_value.pop_back(); m_justification.pop_back(); @@ -189,7 +168,7 @@ namespace polysat { auto slack = add_var(sz); auto q = p + var(slack); add_eq(q, dep); // TODO: 'dep' now refers to two constraints; this is not yet supported - auto non_zero = sz2bits(sz).non_zero(); + auto non_zero = m_vble.sz2bits(sz).non_zero(); return m_constraints.viable(m_level, pos_t, slack, non_zero, mk_dep_ref(dep)); } @@ -287,7 +266,7 @@ namespace polysat { void solver::propagate(pvar v, rational const& val, constraint& c) { LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c); - if (is_viable(v, val)) { + if (m_vble.is_viable(v, val)) { m_free_vars.del_var_eh(v); assign_core(v, val, justification::propagation(m_level)); } @@ -326,10 +305,7 @@ namespace polysat { break; } case trail_instr_t::viable_i: { - auto p = m_viable_trail.back(); - LOG_V("Undo viable_i"); - m_viable[p.first] = p.second; - m_viable_trail.pop_back(); + m_vble.pop_viable(); break; } case trail_instr_t::assign_i: { @@ -418,9 +394,9 @@ namespace polysat { void solver::decide(pvar v) { LOG("Decide v" << v); - IF_LOGGING(log_viable(v)); + IF_LOGGING(m_vble.log(v)); rational val; - switch (find_viable(v, val)) { + switch (m_vble.find_viable(v, val)) { case dd::find_t::empty: // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing) // (fail here in debug mode so we notice if we miss some) @@ -445,7 +421,7 @@ namespace polysat { else ++m_stats.m_num_propagations; LOG(assignment_pp(*this, v, val) << " by " << j); - SASSERT(is_viable(v, val)); + SASSERT(m_vble.is_viable(v, val)); SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; })); m_value[v] = val; m_search.push_assignment(v, val); @@ -531,7 +507,7 @@ namespace polysat { pvar conflict_var = null_var; clause_ref lemma; for (auto v : m_conflict.vars(m_constraints)) - if (!has_viable(v)) { + if (!m_vble.has_viable(v)) { SASSERT(conflict_var == null_var || conflict_var == v); // at most one variable can be empty conflict_var = v; } @@ -799,7 +775,7 @@ namespace polysat { // Guess a literal from the given clause; returns the guessed constraint sat::literal solver::decide_bool(clause& lemma) { LOG_H3("Guessing literal in lemma: " << lemma); - IF_LOGGING(log_viable()); + IF_LOGGING(m_vble.log()); LOG("Boolean assignment: " << m_bvars); // To make a guess, we need to find an unassigned literal that is not false in the current model. @@ -887,20 +863,14 @@ namespace polysat { rational val = m_value[v]; LOG_H3("Reverting decision: pvar " << v << " := " << val); SASSERT(m_justification[v].is_decision()); - bdd viable = m_viable[v]; constraints just(m_cjust[v]); backjump(m_justification[v].level()-1); // Since decision "v -> val" caused a conflict, we may keep all // viability restrictions on v and additionally exclude val. // TODO: viability restrictions on 'v' must have happened before decision on 'v'. Do we really need to save/restore m_viable here? - SASSERT(m_viable[v] == viable); // check this with assertion SASSERT(m_cjust[v] == just); // check this with assertion - // push_viable(v); - // m_viable[v] = viable; - // for (unsigned i = m_cjust[v].size(); i < just.size(); ++i) - // push_cjust(v, just[i]); - add_non_viable(v, val); + m_vble.add_non_viable(v, val); auto confl = std::move(m_conflict); m_conflict.reset(); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 5a884148b..4429bba2f 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -28,6 +28,7 @@ Author: #include "math/polysat/linear_solver.h" #include "math/polysat/search_state.h" #include "math/polysat/trail.h" +#include "math/polysat/viable.h" #include "math/polysat/log.h" namespace polysat { @@ -52,15 +53,15 @@ namespace polysat { friend class conflict_explainer; friend class forbidden_intervals; friend class linear_solver; + friend class viable; friend class assignment_pp; friend class assignments_pp; typedef ptr_vector constraints; reslimit& m_lim; - dd::bdd_manager m_bdd; + viable m_vble; // viable sets per variable scoped_ptr_vector m_pdd; - scoped_ptr_vector m_bits; dep_value_manager m_value_manager; small_object_allocator m_alloc; poly_dep_manager m_dm; @@ -85,7 +86,6 @@ namespace polysat { svector m_disjunctive_lemma; // Per variable information - vector m_viable; // set of viable values. vector m_value; // assigned value vector m_justification; // justification for variable assignment vector m_cjust; // constraints justifying variable range. @@ -110,7 +110,6 @@ namespace polysat { svector m_trail; unsigned_vector m_qhead_trail; - vector> m_viable_trail; unsigned_vector m_cjust_trail; ptr_vector m_activate_trail; @@ -119,8 +118,7 @@ namespace polysat { void push_viable(pvar v) { - m_trail.push_back(trail_instr_t::viable_i); - m_viable_trail.push_back(std::make_pair(v, m_viable[v])); + m_vble.push_viable(v); } void push_qhead() { @@ -144,43 +142,6 @@ namespace polysat { unsigned size(pvar v) const { return m_size[v]; } - /** - * Check whether variable v has any viable values left according to m_viable. - */ - bool has_viable(pvar v); - - /** - * check if value is viable according to m_viable. - */ - bool is_viable(pvar v, rational const& val); - - /** - * register that val is non-viable for var. - */ - void add_non_viable(pvar v, rational const& val); - - /** - * Register all values that are not contained in vals as non-viable. - */ - void intersect_viable(pvar v, bdd vals); - - /** - * Add dependency for variable viable range. - */ - void add_viable_dep(pvar v, p_dependency* dep); - - /** - * Find a next viable value for variable. - */ - dd::find_t find_viable(pvar v, rational & val); - - /** Log all viable values for the given variable. - * (Inefficient, but useful for debugging small instances.) - */ - void log_viable(pvar v); - /** Like log_viable but for all variables */ - void log_viable(); - /** * undo trail operations for backtracking. * Each struct is a subclass of trail and implements undo(). @@ -188,10 +149,7 @@ namespace polysat { void del_var(); - dd::bdd_manager& get_bdd() { return m_bdd; } dd::pdd_manager& sz2pdd(unsigned sz); - dd::fdd const& sz2bits(unsigned sz); - dd::fdd const& var2bits(pvar v) { return sz2bits(size(v)); } void push_level(); void pop_levels(unsigned num_levels); diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index e72c8bd03..5be78e30d 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -74,22 +74,22 @@ namespace polysat { d = q.lo().val(); } if (v != null_var) { - bddv const& x = s.var2bits(v).var(); + bddv const& x = s.m_vble.var2bits(v).var(); s.push_cjust(v, this); // hacky special case if (a == 1 && b == 0 && c == 0 && d == 0) // x <= 0 - s.intersect_viable(v, is_positive() ? x.all0() : !x.all0()); + s.m_vble.intersect_viable(v, is_positive() ? x.all0() : !x.all0()); else { IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << (is_positive() ? " <= " : " > ") << c << "*x + " << d << "\n"); bddv l = a * x + b; bddv r = c * x + d; bdd xs = is_positive() ? (l <= r) : (l > r); - s.intersect_viable(v, xs); + s.m_vble.intersect_viable(v, xs); } rational val; - if (s.find_viable(v, val) == dd::find_t::singleton) { + if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) { s.propagate(v, val, *this); } diff --git a/src/math/polysat/var_constraint.cpp b/src/math/polysat/var_constraint.cpp index cfc5ff739..43ea1ac6a 100644 --- a/src/math/polysat/var_constraint.cpp +++ b/src/math/polysat/var_constraint.cpp @@ -32,15 +32,15 @@ namespace polysat { } bool var_constraint::is_currently_false(solver& s) { - return s.m_viable[m_var].is_false(); + return s.m_vble.is_false(m_var); } bool var_constraint::is_currently_true(solver& s) { - return !s.m_viable[m_var].is_false(); + return !is_currently_false(s); } void var_constraint::narrow(solver& s) { - s.intersect_viable(m_var, m_viable); + s.m_vble.intersect_viable(m_var, m_viable); } } diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp new file mode 100644 index 000000000..c8efc2361 --- /dev/null +++ b/src/math/polysat/viable.cpp @@ -0,0 +1,114 @@ + +#include "math/polysat/viable.h" +#include "math/polysat/solver.h" + +namespace polysat { + + viable::viable(solver& s): + s(s), + m_bdd(1000) + {} + + void viable::push_viable(pvar v) { + s.m_trail.push_back(trail_instr_t::viable_i); + m_viable_trail.push_back(std::make_pair(v, m_viable[v])); + } + + void viable::pop_viable() { + auto p = m_viable_trail.back(); + LOG_V("Undo viable_i"); + m_viable[p.first] = p.second; + m_viable_trail.pop_back(); + } + + // a*v + b == 0 or a*v + b != 0 + void viable::intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive) { + bddv const& x = var2bits(v).var(); + if (b == 0 && a.is_odd()) { + // hacky test optimizing special case. + // general case is compute inverse(a)*-b for equality 2^k*a*x + b == 0 + // then constrain x. + // + intersect_viable(v, is_positive ? x.all0() : !x.all0()); + } + else if (a.is_odd()) { + rational a_inv; + VERIFY(a.mult_inverse(x.size(), a_inv)); + bdd eq = x == mod(a_inv * -b, rational::power_of_two(x.size())); + intersect_viable(v, is_positive ? eq : !eq); + } + else { + IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << "\n"); + + bddv lhs = a * x + b; + bdd xs = is_positive ? lhs.all0() : !lhs.all0(); + intersect_viable(v, xs); + } + } + + bool viable::has_viable(pvar v) { + return !m_viable[v].is_false(); + } + + bool viable::is_viable(pvar v, rational const& val) { + return var2bits(v).contains(m_viable[v], val); + } + + void viable::add_non_viable(pvar v, rational const& val) { + LOG("pvar " << v << " /= " << val); + SASSERT(is_viable(v, val)); + auto const& bits = var2bits(v); + intersect_viable(v, bits.var() != val); + } + + void viable::intersect_viable(pvar v, bdd vals) { + push_viable(v); + m_viable[v] &= vals; + if (m_viable[v].is_false()) + s.set_conflict(v); + } + + dd::find_t viable::find_viable(pvar v, rational & val) { + return var2bits(v).find_hint(m_viable[v], s.m_value[v], val); + } + + dd::fdd const& viable::sz2bits(unsigned sz) { + m_bits.reserve(sz + 1); + auto* bits = m_bits[sz]; + if (!bits) { + m_bits.set(sz, alloc(dd::fdd, m_bdd, sz)); + bits = m_bits[sz]; + } + return *bits; + } + +#if POLYSAT_LOGGING_ENABLED + void viable::log() { + // only for small problems + if (m_viable.size() < 10) { + for (pvar v = 0; v < m_viable.size(); ++v) { + log(v); + } + } + } + + void viable::log(pvar v) { + if (s.size(v) <= 5) { + vector xs; + for (rational x = rational::zero(); x < rational::power_of_two(s.size(v)); x += 1) { + if (is_viable(v, x)) { + xs.push_back(x); + } + } + LOG("Viable for pvar " << v << ": " << xs); + } else { + LOG("Viable for pvar " << v << ": "); + } + } +#endif + + dd::fdd const& viable::var2bits(pvar v) { return sz2bits(s.size(v)); } + + +} + diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h new file mode 100644 index 000000000..3cc1d6fe5 --- /dev/null +++ b/src/math/polysat/viable.h @@ -0,0 +1,91 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + maintain viable domains + + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once + +#include +#include "math/dd/dd_bdd.h" +#include "math/polysat/types.h" + +namespace polysat { + + class solver; + + class viable { + typedef dd::bdd bdd; + solver& s; + dd::bdd_manager m_bdd; + scoped_ptr_vector m_bits; + vector m_viable; // set of viable values. + vector> m_viable_trail; + + public: + viable(solver& s); + + void push() { m_viable.push_back(m_bdd.mk_true()); } + void pop() { m_viable.pop_back(); } + + void push_viable(pvar v); + + void pop_viable(); + + void intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive); + + /** + * Check whether variable v has any viable values left according to m_viable. + */ + bool has_viable(pvar v); + + bool is_false(pvar v) { return m_viable[v].is_false(); } + + /** + * check if value is viable according to m_viable. + */ + bool is_viable(pvar v, rational const& val); + + /** + * register that val is non-viable for var. + */ + void add_non_viable(pvar v, rational const& val); + + /** + * Register all values that are not contained in vals as non-viable. + */ + void intersect_viable(pvar v, bdd vals); + + /** + * Add dependency for variable viable range. + */ + void add_viable_dep(pvar v, p_dependency* dep); + + /** + * Find a next viable value for variable. + */ + dd::find_t find_viable(pvar v, rational & val); + + /** Log all viable values for the given variable. + * (Inefficient, but useful for debugging small instances.) + */ + void log(pvar v); + /** Like log_viable but for all variables */ + void log(); + + dd::bdd_manager& get_bdd() { return m_bdd; } + dd::fdd const& sz2bits(unsigned sz); + dd::fdd const& var2bits(pvar v); + + }; +} + +