From ce5c8b3066610119270a7c5d386603c7d94b9930 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Jun 2021 16:19:37 -0700 Subject: [PATCH] rename to some saner name Signed-off-by: Nikolaj Bjorner --- src/math/polysat/constraint.cpp | 6 ++--- src/math/polysat/eq_constraint.cpp | 4 +-- src/math/polysat/solver.cpp | 38 +++++++++-------------------- src/math/polysat/solver.h | 4 +-- src/math/polysat/ule_constraint.cpp | 4 +-- src/math/polysat/viable.h | 30 ++++++++++++----------- 6 files changed, 37 insertions(+), 49 deletions(-) diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 4b7d2ca44..b772ba26d 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -238,9 +238,9 @@ namespace polysat { SASSERT(std::all_of(new_constraints().begin(), new_constraints().end(), [var](constraint* c) { return c->bvar() != var; })); SASSERT(std::all_of(other.new_constraints().begin(), other.new_constraints().end(), [var](constraint* c) { return c->bvar() != var; })); int j = 0; - for (int i = 0; i < m_literals.size(); ++i) - if (m_literals[i].var() != var) - m_literals[j++] = m_literals[i]; + for (auto lit : m_literals) + if (lit.var() != var) + m_literals[j++] = lit; m_literals.shrink(j); for (sat::literal lit : other.literals()) if (lit.var() != var) diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index 3b39c9b81..2ebffb5cb 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -63,11 +63,11 @@ namespace polysat { rational a = q.hi().val(); rational b = q.lo().val(); - s.m_vble.intersect_eq(a, v, b, is_positive()); + s.m_viable.intersect_eq(a, v, b, is_positive()); rational val; - if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) + if (s.m_viable.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 3f7eccd97..e32ed2ee6 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -36,7 +36,7 @@ namespace polysat { solver::solver(reslimit& lim): m_lim(lim), - m_vble(*this), + m_viable(*this), m_dm(m_value_manager, m_alloc), m_linear_solver(*this), m_free_vars(m_activity), @@ -65,7 +65,7 @@ namespace polysat { LOG("Free variables: " << m_free_vars); LOG("Assignment: " << assignments_pp(*this)); if (!m_conflict.empty()) LOG("Conflict: " << m_conflict); - IF_LOGGING(m_vble.log()); + IF_LOGGING(m_viable.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; } @@ -82,7 +82,7 @@ namespace polysat { pvar v = m_value.size(); m_value.push_back(rational::zero()); m_justification.push_back(justification::unassigned()); - m_vble.push(); + m_viable.push(); m_cjust.push_back(constraints()); m_watch.push_back(ptr_vector()); m_activity.push_back(0); @@ -101,7 +101,7 @@ namespace polysat { void solver::del_var() { // TODO also remove v from all learned constraints. pvar v = m_value.size() - 1; - m_vble.pop(); + m_viable.pop(); m_cjust.pop_back(); m_value.pop_back(); m_justification.pop_back(); @@ -118,20 +118,6 @@ namespace polysat { constraint_ref solver::mk_diseq(pdd const& p, unsigned dep) { return m_constraints.eq(m_level, neg_t, p, mk_dep_ref(dep)); -#if 0 - if (p.is_val()) { - // if (!p.is_zero()) - // return nullptr; // TODO: probably better to create a dummy always-true constraint? - // // Use 0 != 0 for a constraint that is always false - // Use p != 0 as evaluable dummy constraint - } - unsigned sz = size(p.var()); - 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 = m_vble.sz2bits(sz).non_zero(); - return m_constraints.viable(m_level, pos_t, slack, non_zero, mk_dep_ref(dep)); -#endif } constraint_ref solver::mk_ule(pdd const& p, pdd const& q, unsigned dep) { @@ -228,7 +214,7 @@ namespace polysat { void solver::propagate(pvar v, rational const& val, constraint& c) { LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c); - if (m_vble.is_viable(v, val)) { + if (m_viable.is_viable(v, val)) { m_free_vars.del_var_eh(v); assign_core(v, val, justification::propagation(m_level)); } @@ -267,7 +253,7 @@ namespace polysat { break; } case trail_instr_t::viable_i: { - m_vble.pop_viable(); + m_viable.pop_viable(); break; } case trail_instr_t::assign_i: { @@ -356,9 +342,9 @@ namespace polysat { void solver::decide(pvar v) { LOG("Decide v" << v); - IF_LOGGING(m_vble.log(v)); + IF_LOGGING(m_viable.log(v)); rational val; - switch (m_vble.find_viable(v, val)) { + switch (m_viable.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) @@ -383,7 +369,7 @@ namespace polysat { else ++m_stats.m_num_propagations; LOG(assignment_pp(*this, v, val) << " by " << j); - SASSERT(m_vble.is_viable(v, val)); + SASSERT(m_viable.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); @@ -469,7 +455,7 @@ namespace polysat { pvar conflict_var = null_var; clause_ref lemma; for (auto v : m_conflict.vars(m_constraints)) - if (!m_vble.has_viable(v)) { + if (!m_viable.has_viable(v)) { SASSERT(conflict_var == null_var || conflict_var == v); // at most one variable can be empty conflict_var = v; } @@ -737,7 +723,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(m_vble.log()); + IF_LOGGING(m_viable.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. @@ -832,7 +818,7 @@ namespace polysat { // TODO: viability restrictions on 'v' must have happened before decision on 'v'. Do we really need to save/restore m_viable here? SASSERT(m_cjust[v] == just); // check this with assertion - m_vble.add_non_viable(v, val); + m_viable.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 4429bba2f..ca8ea652b 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -60,7 +60,7 @@ namespace polysat { typedef ptr_vector constraints; reslimit& m_lim; - viable m_vble; // viable sets per variable + viable m_viable; // viable sets per variable scoped_ptr_vector m_pdd; dep_value_manager m_value_manager; small_object_allocator m_alloc; @@ -118,7 +118,7 @@ namespace polysat { void push_viable(pvar v) { - m_vble.push_viable(v); + m_viable.push_viable(v); } void push_qhead() { diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index ec2538b56..bab634620 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -76,10 +76,10 @@ namespace polysat { if (v != null_var) { s.push_cjust(v, this); - s.m_vble.intersect_ule(v, a, b, c, d, is_positive()); + s.m_viable.intersect_ule(v, a, b, c, d, is_positive()); rational val; - if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) + if (s.m_viable.find_viable(v, val) == dd::find_t::singleton) s.propagate(v, val, *this); return; diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index c893bf051..901f4ee61 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -30,6 +30,15 @@ namespace polysat { vector m_viable; // set of viable values. vector> m_viable_trail; + /** + * Register all values that are not contained in vals as non-viable. + */ + void intersect_viable(pvar v, bdd vals); + + dd::bdd_manager& get_bdd() { return m_bdd; } + dd::fdd const& sz2bits(unsigned sz); + dd::fdd const& var2bits(pvar v); + public: viable(solver& s); @@ -40,6 +49,11 @@ namespace polysat { void pop_viable(); + /** + * update state of viable for pvar v + * based on affine constraints + */ + void intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive); void intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive); @@ -61,15 +75,6 @@ namespace polysat { */ 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. @@ -80,12 +85,9 @@ namespace polysat { * (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); + /** Like log(v) but for all variables */ + void log(); }; }