From 625ec18b0fdb8e8122ee8d40056526214480a96c Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 6 Nov 2023 10:39:02 +0100 Subject: [PATCH] Remove unused stuff --- src/math/polysat/viable.cpp | 225 ------------------------------------ src/math/polysat/viable.h | 19 --- 2 files changed, 244 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 24941fad5..c18843d70 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1210,151 +1210,6 @@ namespace { return true; } -#if 0 - bool viable::collect_bit_information(pvar v, bool add_conflict, const vector& cnstr, svector& fixed, vector>& justifications) { - pdd p = s.var(v); - fixed.clear(); - justifications.clear(); - fixed.resize(p.power_of_2(), l_undef); - justifications.resize(p.power_of_2(), vector()); - if (cnstr.empty()) - return true; - - clause_builder builder(s, "bit check"); - uint_set already_added; - vector> postponed; - - auto add_entry = [&builder, &already_added](const signed_constraint& src) { - if (already_added.contains(src.bvar())) - return; - already_added.insert(src.bvar()); - builder.insert_eval(~src); - }; - - auto add_entry_list = [add_entry](const vector& list) { - for (const auto& e : list) - add_entry(e); - }; - - unsigned largest_mask = 0; - - for (unsigned i = 0; i < cnstr.size(); i++) { - const signed_constraint& src = cnstr[i]; - - single_bit bit; - trailing_bits mask; - if (src->is_ule() && - simplify_clause::get_bit(src->to_ule().lhs(), src->to_ule().rhs(), p, bit, src.is_positive()) && p.is_var()) { - lbool prev = fixed[bit.position]; - fixed[bit.position] = bit.positive ? l_true : l_false; - if (prev != l_undef && fixed[bit.position] != prev) { - LOG("Bit conflicting " << src << " with " << justifications[bit.position][0]); - if (add_conflict) { - add_entry_list(justifications[bit.position]); - add_entry(src); - s.set_conflict(*builder.build()); - } - return false; - } - justifications[bit.position].clear(); - justifications[bit.position].push_back(src); - } - else if (src->is_eq() && - simplify_clause::get_lsb(src->to_ule().lhs(), src->to_ule().rhs(), p, mask, src.is_positive()) && p.is_var()) { - if (src.is_positive()) { - for (unsigned i = 0; i < mask.length; i++) { - lbool prev = fixed[i]; - fixed[i] = mask.bits.get_bit(i) ? l_true : l_false; - //verbose_stream() << "Setting bit " << i << " to " << mask.bits.get_bit(i) << " because of parity " << e->src << "\n"; - if (prev != l_undef) { - if (fixed[i] != prev) { - LOG("Positive parity conflicting " << src << " with " << justifications[i][0]); - if (add_conflict) { - add_entry_list(justifications[i]); - add_entry(src); - s.set_conflict(*builder.build()); - } - return false; - } - else { - if (largest_mask < mask.length) { - largest_mask = mask.length; - justifications[i].clear(); - justifications[i].push_back(src); - } - } - } - else { - SASSERT(justifications[i].empty()); - justifications[i].push_back(src); - } - } - } - else - postponed.push_back({ src, mask }); - } - } - - bool_vector removed(postponed.size(), false); - bool changed; - do { - changed = false; - for (unsigned j = 0; j < postponed.size(); j++) { - if (removed[j]) - continue; - const auto& neg = postponed[j]; - unsigned indet = 0; - unsigned last_indet = 0; - unsigned i = 0; - for (; i < neg.second.length; i++) { - if (fixed[i] != l_undef) { - if (fixed[i] != (neg.second.bits.get_bit(i) ? l_true : l_false)) { - removed[j] = true; - break; // this is already satisfied - } - } - else { - indet++; - last_indet = i; - } - } - if (i == neg.second.length) { - if (indet == 0) { - // Already false - LOG("Found conflict with constraint " << neg.first); - if (add_conflict) { - for (unsigned k = 0; k < neg.second.length; k++) - add_entry_list(justifications[k]); - add_entry(neg.first); - s.set_conflict(*builder.build()); - } - return false; - } - else if (indet == 1) { - // Simple BCP - auto& justification = justifications[last_indet]; - SASSERT(justification.empty()); - for (unsigned k = 0; k < neg.second.length; k++) { - if (k != last_indet) { - SASSERT(fixed[k] != l_undef); - for (const auto& just : justifications[k]) - justification.push_back(just); - } - } - justification.push_back(neg.first); - fixed[last_indet] = neg.second.bits.get_bit(last_indet) ? l_false : l_true; - removed[j] = true; - LOG("Applying fast BCP on bit " << last_indet << " from constraint " << neg.first); - changed = true; - } - } - } - } while(changed); - - return true; - } -#endif - bool viable::has_viable(pvar v) { fixed_bits_info fbi; @@ -1868,90 +1723,10 @@ namespace { return true; } -#if 0 - void viable::make_bit_justification(pvar v) { - if (!m_units[v] || m_units[v]->interval.is_full()) - return; - // TODO: Maybe this helps? This prefers justifications from bits - svector fixed; - vector> justifications; - if (!collect_bit_information(v, false, fixed, justifications)) - return; - - entry* first = m_units[v]; - entry* e = first; - vector intervals; - do { - intervals.push_back(e->interval); - e = e->next(); - } - while (e != first); - int additional = 0; - for (unsigned i = 0; i < intervals.size(); i++) { // Try to justify by bits as good as possible - if (intervals[i].hi_val().is_zero()) - additional += refine_bits(v, s.var(v).manager().max_value(), fixed, justifications); - else - additional += refine_bits(v, intervals[i].hi_val() - 1, fixed, justifications); - } - verbose_stream() << "Found " << additional << " intervals\n"; - } - - void viable::get_bit_min_max(pvar v, conflict& core, rational& min, rational& max, vector& justifications_min, vector& justifications_max) { - pdd v_pdd = s.var(v); - min = 0; - max = v_pdd.manager().max_value(); - svector fixed; - vector> justifications; - vector candidates; - for (const auto& c : core) { - if (!c->is_ule()) - continue; - ule_constraint ule = c->to_ule(); - pdd sum = ule.lhs() + ule.rhs(); - if (sum.is_univariate_in(v) && sum.degree(v) == 1) - candidates.push_back(c); - } - - if (candidates.empty() || !collect_bit_information(v, false, candidates, fixed, justifications)) - return; - - for (unsigned i = 0; i < fixed.size(); i++) { - verbose_stream() << (fixed[fixed.size() - 1] == l_true ? '1' : fixed[fixed.size() - 1] == l_false ? '0' : '?'); - } - verbose_stream() << "\n"; - - max = 0; - - for (unsigned i = fixed.size(); i > 0; i--) { - min *= 2; - max *= 2; - lbool val = fixed[i - 1]; - if (val == l_true) { - min++; - max++; - for (auto& add : justifications[i - 1]) - justifications_min.push_back(add); - } - else if (val == l_undef) - max++; - else { - SASSERT(val == l_false); - for (auto& add : justifications[i - 1]) - justifications_max.push_back(add); - } - } - } -#endif - bool viable::resolve_interval(pvar v, conflict& core) { DEBUG_CODE( log(v); ); VERIFY(!has_viable(v)); // does a pass over interval refinement, making sure the intervals actually exist -#if 0 - // Prefer bit information as justifications - make_bit_justification(v); -#endif - entry const* e = m_units[v].get_entries(s.size(v)); // TODO: take other sizes into account // TODO: in the forbidden interval paper, they start with the longest interval. We should also try that at some point. entry const* first = e; diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index e10a846c5..494897949 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -168,9 +168,6 @@ namespace polysat { rational extend_by_bits(pdd const& var, rational const& bounds, fixed_bits_info const& fbi, vector& out_src, vector& out_side_cond) const; bool collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi); -#if 0 - bool collect_bit_information(pvar v, bool add_conflict, const vector& cnstr, svector& fixed, vector>& justifications); -#endif std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const; std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const; @@ -260,22 +257,6 @@ namespace polysat { */ find_t find_viable(pvar v, rational& out_val); - private: - /** - * Find a next viable value for variable. Attempts to find two different values, to distinguish propagation/decision. - * NOTE: out_hi is set to -1 by the fallback solver. - * @return l_true on success, l_false on conflict, l_undef on resource limit - */ - lbool find_viable2(pvar v, rational& out_lo, rational& out_hi); - - lbool find_viable_fallback(pvar v, rational& out_lo, rational& out_hi); - public: - -#if 0 - void make_bit_justification(pvar v); - void get_bit_min_max(pvar v, conflict& core, rational& min, rational& max, vector& justifications_min, vector& justifications_max); -#endif - /** * Retrieve the unsat core for v, * and add the forbidden interval lemma for v (which eliminates v from the unsat core).