From 9fc4015c46360058ad4b4fcccc7fee076ca5c74c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Oct 2022 03:57:39 -0700 Subject: [PATCH] remove ternary clause optimization Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured. --- src/sat/sat_cleaner.cpp | 3 - src/sat/sat_drat.cpp | 4 - src/sat/sat_gc.cpp | 24 ---- src/sat/sat_integrity_checker.cpp | 26 ---- src/sat/sat_justification.h | 21 +--- src/sat/sat_proof_trim.cpp | 17 --- src/sat/sat_simplifier.cpp | 3 - src/sat/sat_solver.cpp | 197 ++---------------------------- src/sat/sat_solver.h | 6 - src/sat/sat_types.h | 2 - src/sat/sat_watched.cpp | 33 ----- src/sat/sat_watched.h | 38 +----- src/sat/smt/pb_solver.cpp | 28 ----- 13 files changed, 16 insertions(+), 386 deletions(-) diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index bbdedab86..8da933fb2 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -64,9 +64,6 @@ namespace sat { } TRACE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";); break; -#if ENABLE_TERNARY - case watched::TERNARY: -#endif case watched::CLAUSE: // skip break; diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 306ff2493..46a608151 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -445,10 +445,6 @@ namespace sat { return false; case justification::BINARY: return contains(c, j.get_literal()); -#if ENABLE_TERNARY - case justification::TERNARY: - return contains(c, j.get_literal1(), j.get_literal2()); -#endif case justification::CLAUSE: return contains(s.get_clause(j)); default: diff --git a/src/sat/sat_gc.cpp b/src/sat/sat_gc.cpp index ab9bc8857..a655956db 100644 --- a/src/sat/sat_gc.cpp +++ b/src/sat/sat_gc.cpp @@ -178,33 +178,9 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";); } -#if ENABLE_TERNARY - bool solver::can_delete3(literal l1, literal l2, literal l3) const { - if (value(l1) == l_true && - value(l2) == l_false && - value(l3) == l_false) { - justification const& j = m_justification[l1.var()]; - if (j.is_ternary_clause()) { - watched w1(l2, l3); - watched w2(j.get_literal1(), j.get_literal2()); - return w1 != w2; - } - } - return true; - } -#endif - bool solver::can_delete(clause const & c) const { if (c.on_reinit_stack()) return false; -#if ENABLE_TERNARY - if (c.size() == 3) { - return - can_delete3(c[0],c[1],c[2]) && - can_delete3(c[1],c[0],c[2]) && - can_delete3(c[2],c[0],c[1]); - } -#endif literal l0 = c[0]; if (value(l0) != l_true) return true; diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index a6086d8a7..223e58677 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -26,13 +26,6 @@ namespace sat { integrity_checker::integrity_checker(solver const & _s): s(_s) { } - -#if ENABLE_TERNARY - // for ternary clauses - static bool contains_watched(watch_list const & wlist, literal l1, literal l2) { - return wlist.contains(watched(l1, l2)); - } -#endif // for nary clauses static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) { @@ -65,18 +58,6 @@ namespace sat { if (c.frozen()) return true; -#if ENABLE_TERNARY - if (c.size() == 3) { - CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n"; - tout << "watch_list:\n"; - s.display_watch_list(tout, s.get_wlist(~c[0])); - tout << "\n";); - VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2])); - VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2])); - VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1])); - return true; - } -#endif { if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) { bool on_prop_stack = false; @@ -174,13 +155,6 @@ namespace sat { tout << "\n";); VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l)); break; -#if ENABLE_TERNARY - case watched::TERNARY: - VERIFY(!s.was_eliminated(w.get_literal1().var())); - VERIFY(!s.was_eliminated(w.get_literal2().var())); - VERIFY(w.get_literal1().index() < w.get_literal2().index()); - break; -#endif case watched::CLAUSE: VERIFY(!s.get_clause(w.get_clause_offset()).was_removed()); break; diff --git a/src/sat/sat_justification.h b/src/sat/sat_justification.h index 1fc97a38c..f83173aa7 100644 --- a/src/sat/sat_justification.h +++ b/src/sat/sat_justification.h @@ -22,11 +22,7 @@ namespace sat { class justification { public: - enum kind { NONE = 0, BINARY = 1, -#if ENABLE_TERNARY - TERNARY = 2, -#endif - CLAUSE = 3, EXT_JUSTIFICATION = 4}; + enum kind { NONE = 0, BINARY = 1, CLAUSE = 2, EXT_JUSTIFICATION = 3}; private: unsigned m_level; size_t m_val1; @@ -36,9 +32,7 @@ namespace sat { public: justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {} explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {} -#if ENABLE_TERNARY - justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {} -#endif + explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {} static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); } @@ -51,12 +45,6 @@ namespace sat { bool is_binary_clause() const { return m_val2 == BINARY; } literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(val1()); } -#if ENABLE_TERNARY - bool is_ternary_clause() const { return get_kind() == TERNARY; } - literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(val1()); } - literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); } -#endif - bool is_clause() const { return m_val2 == CLAUSE; } clause_offset get_clause_offset() const { return m_val1; } @@ -73,11 +61,6 @@ namespace sat { case justification::BINARY: out << "binary " << j.get_literal(); break; -#if ENABLE_TERNARY - case justification::TERNARY: - out << "ternary " << j.get_literal1() << " " << j.get_literal2(); - break; -#endif case justification::CLAUSE: out << "clause"; break; diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index 4c4b9ecaf..df55aecd7 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -125,10 +125,6 @@ namespace sat { in_coi |= m_in_coi.contains(lit.index()); else if (js.is_binary_clause()) in_coi = m_in_coi.contains(js.get_literal().index()); -#if ENABLE_TERNARY - else if (js.is_ternary_clause()) - in_coi = m_in_coi.contains(js.get_literal1().index()) || m_in_coi.contains(js.get_literal2().index()); -#endif else UNREACHABLE(); // approach does not work for external justifications @@ -226,12 +222,6 @@ namespace sat { case justification::BINARY: add_dependency(j.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - add_dependency(j.get_literal1()); - add_dependency(j.get_literal2()); - break; -#endif case justification::CLAUSE: for (auto lit : s.get_clause(j)) if (s.value(lit) == l_false) @@ -262,13 +252,6 @@ namespace sat { m_clause.push_back(l); m_clause.push_back(j.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - m_clause.push_back(l); - m_clause.push_back(j.get_literal1()); - m_clause.push_back(j.get_literal2()); - break; -#endif case justification::CLAUSE: s.get_clause(j).mark_used(); IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n"); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b67ef6a2a..9ba536091 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -271,9 +271,6 @@ namespace sat { watch_list::iterator end2 = wlist.end(); for (; it2 != end2; ++it2) { switch (it2->get_kind()) { -#if ENABLE_TERNARY - case watched::TERNARY: -#endif case watched::CLAUSE: // consume break; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 56dcdf0df..eea3a2475 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -448,10 +448,6 @@ namespace sat { if (redundant && m_par) m_par->share_clause(*this, lits[0], lits[1]); return nullptr; -#if ENABLE_TERNARY - case 3: - return mk_ter_clause(lits, st); -#endif default: return mk_nary_clause(num_lits, lits, st); } @@ -545,58 +541,6 @@ namespace sat { m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); } -#if ENABLE_TERNARY - clause * solver::mk_ter_clause(literal * lits, sat::status st) { - VERIFY(ENABLE_TERNARY); - m_stats.m_mk_ter_clause++; - clause * r = alloc_clause(3, lits, st.is_redundant()); - bool reinit = attach_ter_clause(*r, st); - if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r); - if (st.is_redundant()) - m_learned.push_back(r); - else - m_clauses.push_back(r); - for (literal l : *r) { - m_touched[l.var()] = m_touch_index; - } - return r; - } - - bool solver::attach_ter_clause(clause & c, sat::status st) { - VERIFY(ENABLE_TERNARY); - bool reinit = false; - if (m_config.m_drat) m_drat.add(c, st); - TRACE("sat_verbose", tout << c << "\n";); - SASSERT(!c.was_removed()); - m_watches[(~c[0]).index()].push_back(watched(c[1], c[2])); - m_watches[(~c[1]).index()].push_back(watched(c[0], c[2])); - m_watches[(~c[2]).index()].push_back(watched(c[0], c[1])); - if (!at_base_lvl()) - reinit = propagate_ter_clause(c); - return reinit; - } - - bool solver::propagate_ter_clause(clause& c) { - bool reinit = false; - if (value(c[1]) == l_false && value(c[2]) == l_false) { - m_stats.m_ter_propagate++; - assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2])); - reinit = !c.is_learned(); - } - else if (value(c[0]) == l_false && value(c[2]) == l_false) { - m_stats.m_ter_propagate++; - assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2])); - reinit = !c.is_learned(); - } - else if (value(c[0]) == l_false && value(c[1]) == l_false) { - m_stats.m_ter_propagate++; - assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1])); - reinit = !c.is_learned(); - } - return reinit; - } -#endif - clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) { m_stats.m_mk_clause++; clause * r = alloc_clause(num_lits, lits, st.is_redundant()); @@ -663,13 +607,7 @@ namespace sat { void solver::attach_clause(clause & c, bool & reinit) { SASSERT(c.size() > 2); - reinit = false; -#if ENABLE_TERNARY - if (ENABLE_TERNARY && c.size() == 3) - reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted()); - else -#endif - reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack()); + reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack()); } void solver::set_learned(clause& c, bool redundant) { @@ -917,12 +855,6 @@ namespace sat { } void solver::detach_clause(clause& c) { -#if ENABLE_TERNARY - if (c.size() == 3) { - detach_ter_clause(c); - return; - } -#endif detach_nary_clause(c); } @@ -932,14 +864,6 @@ namespace sat { erase_clause_watch(get_wlist(~c[1]), cls_off); } -#if ENABLE_TERNARY - void solver::detach_ter_clause(clause & c) { - erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]); - erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]); - erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]); - } -#endif - // ----------------------- // // Basic @@ -1123,31 +1047,6 @@ namespace sat { *it2 = *it; it2++; break; -#if ENABLE_TERNARY - case watched::TERNARY: { - lbool val1, val2; - l1 = it->get_literal1(); - l2 = it->get_literal2(); - val1 = value(l1); - val2 = value(l2); - if (val1 == l_false && val2 == l_undef) { - m_stats.m_ter_propagate++; - assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l)); - } - else if (val1 == l_undef && val2 == l_false) { - m_stats.m_ter_propagate++; - assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l)); - } - else if (val1 == l_false && val2 == l_false) { - CONFLICT_CLEANUP(); - set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2); - return false; - } - *it2 = *it; - it2++; - break; - } -#endif case watched::CLAUSE: { if (value(it->get_blocked_literal()) == l_true) { TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n"; @@ -2534,12 +2433,6 @@ namespace sat { case justification::BINARY: process_antecedent(~(js.get_literal()), num_marks); break; -#if ENABLE_TERNARY - case justification::TERNARY: - process_antecedent(~(js.get_literal1()), num_marks); - process_antecedent(~(js.get_literal2()), num_marks); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); unsigned i = 0; @@ -2718,13 +2611,6 @@ namespace sat { SASSERT(consequent != null_literal); process_antecedent_for_unsat_core(~(js.get_literal())); break; -#if ENABLE_TERNARY - case justification::TERNARY: - SASSERT(consequent != null_literal); - process_antecedent_for_unsat_core(~(js.get_literal1())); - process_antecedent_for_unsat_core(~(js.get_literal2())); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); unsigned i = 0; @@ -2861,12 +2747,6 @@ namespace sat { case justification::BINARY: level = update_max_level(js.get_literal(), level, unique_max); return level; -#if ENABLE_TERNARY - case justification::TERNARY: - level = update_max_level(js.get_literal1(), level, unique_max); - level = update_max_level(js.get_literal2(), level, unique_max); - return level; -#endif case justification::CLAUSE: for (literal l : get_clause(js)) level = update_max_level(l, level, unique_max); @@ -3218,15 +3098,6 @@ namespace sat { return false; } break; -#if ENABLE_TERNARY - case justification::TERNARY: - if (!process_antecedent_for_minimization(~(js.get_literal1())) || - !process_antecedent_for_minimization(~(js.get_literal2()))) { - reset_unmark(old_size); - return false; - } - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); unsigned i = 0; @@ -3382,12 +3253,6 @@ namespace sat { case justification::BINARY: update_lrb_reasoned(js.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - update_lrb_reasoned(js.get_literal1()); - update_lrb_reasoned(js.get_literal2()); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); for (literal l : c) { @@ -3457,20 +3322,6 @@ namespace sat { unmark_lit(~l2); } } -#if ENABLE_TERNARY - else if (w.is_ternary_clause()) { - literal l2 = w.get_literal1(); - literal l3 = w.get_literal2(); - if (is_marked_lit(l2) && is_marked_lit(~l3) && l0 != ~l3) { - // eliminate ~l3 from lemma because we have the clause l \/ l2 \/ l3 - unmark_lit(~l3); - } - else if (is_marked_lit(~l2) && is_marked_lit(l3) && l0 != ~l2) { - // eliminate ~l2 from lemma because we have the clause l \/ l2 \/ l3 - unmark_lit(~l2); - } - } -#endif else { // May miss some binary/ternary clauses, but that is ok. // I sort the watch lists at every simplification round. @@ -3735,17 +3586,6 @@ namespace sat { } else { clause & c = *(cw.get_clause()); -#if ENABLE_TERNARY - if (ENABLE_TERNARY && c.size() == 3) { - if (propagate_ter_clause(c) && !at_base_lvl()) - m_clauses_to_reinit[j++] = cw; - else if (has_variables_to_reinit(c) && !at_base_lvl()) - m_clauses_to_reinit[j++] = cw; - else - c.set_reinit_stack(false); - continue; - } -#endif detach_clause(c); attach_clause(c, reinit); if (reinit && !at_base_lvl()) @@ -4012,12 +3852,6 @@ namespace sat { case justification::BINARY: out << "binary " << js.get_literal() << "@" << lvl(js.get_literal()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - out << "ternary " << js.get_literal1() << "@" << lvl(js.get_literal1()) << " "; - out << js.get_literal2() << "@" << lvl(js.get_literal2()); - break; -#endif case justification::CLAUSE: { out << "("; bool first = true; @@ -4677,24 +4511,14 @@ namespace sat { if (!check_domain(lit, ~js.get_literal())) return false; s |= m_antecedents.find(js.get_literal().var()); break; -#if ENABLE_TERNARY - case justification::TERNARY: - if (!check_domain(lit, ~js.get_literal1()) || - !check_domain(lit, ~js.get_literal2())) return false; - s |= m_antecedents.find(js.get_literal1().var()); - s |= m_antecedents.find(js.get_literal2().var()); - break; -#endif case justification::CLAUSE: { clause & c = get_clause(js); for (literal l : c) { if (l != lit) { - if (check_domain(lit, ~l) && all_found) { - s |= m_antecedents.find(l.var()); - } - else { - all_found = false; - } + if (check_domain(lit, ~l) && all_found) + s |= m_antecedents.find(l.var()); + else + all_found = false; } } break; @@ -4729,12 +4553,11 @@ namespace sat { bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { index_set s; - if (m_antecedents.contains(lit.var())) { + if (m_antecedents.contains(lit.var())) return true; - } - if (assumptions.contains(lit)) { - s.insert(lit.index()); - } + + if (assumptions.contains(lit)) + s.insert(lit.index()); else { if (!extract_assumptions(lit, s)) { SASSERT(!m_todo_antecedents.empty()); @@ -4806,7 +4629,7 @@ namespace sat { clause_vector const & cs = *(vs[i]); for (clause* cp : cs) { clause & c = *cp; - if (ENABLE_TERNARY && c.size() == 3) + if (c.size() == 3) num_ter++; else num_cls++; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 88c404c7c..2e53e4620 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -305,11 +305,6 @@ namespace sat { void mk_bin_clause(literal l1, literal l2, sat::status st); void mk_bin_clause(literal l1, literal l2, bool learned) { mk_bin_clause(l1, l2, learned ? sat::status::redundant() : sat::status::asserted()); } bool propagate_bin_clause(literal l1, literal l2); -#if ENABLE_TERNARY - clause * mk_ter_clause(literal * lits, status st); - bool attach_ter_clause(clause & c, status st); - bool propagate_ter_clause(clause& c); -#endif clause * mk_nary_clause(unsigned num_lits, literal * lits, status st); bool has_variables_to_reinit(clause const& c) const; bool has_variables_to_reinit(literal l1, literal l2) const; @@ -345,7 +340,6 @@ namespace sat { void detach_bin_clause(literal l1, literal l2, bool learned); void detach_clause(clause & c); void detach_nary_clause(clause & c); - void detach_ter_clause(clause & c); void push_reinit_stack(clause & c); void push_reinit_stack(literal l1, literal l2); diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 7c4e4fb73..4e119a2ae 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -34,8 +34,6 @@ class params_ref; class reslimit; class statistics; -#define ENABLE_TERNARY false - namespace sat { #define SAT_VB_LVL 10 diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp index dedbf45f0..5573212f5 100644 --- a/src/sat/sat_watched.cpp +++ b/src/sat/sat_watched.cpp @@ -71,34 +71,6 @@ namespace sat { VERIFY(found); } -#if ENABLE_TERNARY - void erase_ternary_watch(watch_list& wlist, literal l1, literal l2) { - watched w(l1, l2); - watch_list::iterator it = wlist.begin(), end = wlist.end(); - watch_list::iterator it2 = it; - bool found = false; - for (; it != end; ++it) { - if (!found && w == *it) { - found = true; - } - else { - *it2 = *it; - ++it2; - } - } - wlist.set_end(it2); -#if 0 - VERIFY(found); - for (watched const& w2 : wlist) { - if (w2 == w) { - std::cout << l1 << " " << l2 << "\n"; - } - //VERIFY(w2 != w); - } -#endif - } -#endif - void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) { watch_list::iterator end = wlist.end(); for (; it != end; ++it, ++it2) @@ -120,11 +92,6 @@ namespace sat { if (w.is_learned()) out << "*"; break; -#if ENABLE_TERNARY - case watched::TERNARY: - out << "(" << w.get_literal1() << " " << w.get_literal2() << ")"; - break; -#endif case watched::CLAUSE: out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")"; break; diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 7e88c8c51..6d91434db 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -40,11 +40,7 @@ namespace sat { class watched { public: enum kind { - BINARY = 0, -#if ENABLE_TERNARY - TERNARY, -#endif - CLAUSE, EXT_CONSTRAINT + BINARY = 0, CLAUSE, EXT_CONSTRAINT }; private: size_t m_val1; @@ -59,18 +55,6 @@ namespace sat { SASSERT(learned || is_binary_non_learned_clause()); } -#if ENABLE_TERNARY - watched(literal l1, literal l2) { - SASSERT(l1 != l2); - if (l1.index() > l2.index()) - std::swap(l1, l2); - m_val1 = l1.to_uint(); - m_val2 = static_cast(TERNARY) + (l2.to_uint() << 2); - SASSERT(is_ternary_clause()); - SASSERT(get_literal1() == l1); - SASSERT(get_literal2() == l2); - } -#endif unsigned val2() const { return m_val2; } @@ -101,11 +85,6 @@ namespace sat { void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); } -#if ENABLE_TERNARY - bool is_ternary_clause() const { return get_kind() == TERNARY; } - literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast(m_val1)); } - literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); } -#endif bool is_clause() const { return get_kind() == CLAUSE; } clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast(m_val1); } @@ -124,21 +103,14 @@ namespace sat { bool operator!=(watched const & w) const { return !operator==(w); } }; - static_assert(0 <= watched::BINARY && watched::BINARY <= 3, ""); -#if ENABLE_TERNARY - static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, ""); -#endif - static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, ""); - static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, ""); + static_assert(0 <= watched::BINARY && watched::BINARY <= 2, ""); + static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 2, ""); + static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 2, ""); struct watched_lt { bool operator()(watched const & w1, watched const & w2) const { if (w2.is_binary_clause()) return false; if (w1.is_binary_clause()) return true; -#if ENABLE_TERNARY - if (w2.is_ternary_clause()) return false; - if (w1.is_ternary_clause()) return true; -#endif return false; } }; @@ -148,8 +120,6 @@ namespace sat { watched* find_binary_watch(watch_list & wlist, literal l); watched const* find_binary_watch(watch_list const & wlist, literal l); bool erase_clause_watch(watch_list & wlist, clause_offset c); - void erase_ternary_watch(watch_list & wlist, literal l1, literal l2); - void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned); class clause_allocator; std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext); diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index c3e43bfbe..424b20d4e 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -690,15 +690,6 @@ namespace pb { inc_coeff(consequent, offset); process_antecedent(js.get_literal(), offset); break; -#if ENABLE_TERNARY - case sat::justification::TERNARY: - inc_bound(offset); - SASSERT (consequent != sat::null_literal); - inc_coeff(consequent, offset); - process_antecedent(js.get_literal1(), offset); - process_antecedent(js.get_literal2(), offset); - break; -#endif case sat::justification::CLAUSE: { inc_bound(offset); sat::clause & c = s().get_clause(js); @@ -1019,16 +1010,6 @@ namespace pb { inc_coeff(consequent, 1); process_antecedent(js.get_literal()); break; -#if ENABLE_TERNARY - case sat::justification::TERNARY: - SASSERT(consequent != sat::null_literal); - round_to_one(consequent.var()); - inc_bound(1); - inc_coeff(consequent, 1); - process_antecedent(js.get_literal1()); - process_antecedent(js.get_literal2()); - break; -#endif case sat::justification::CLAUSE: { sat::clause & c = s().get_clause(js); unsigned i = 0; @@ -3476,15 +3457,6 @@ namespace pb { ineq.push(lit, offset); ineq.push(js.get_literal(), offset); break; -#if ENABLE_TERNARY - case sat::justification::TERNARY: - SASSERT(lit != sat::null_literal); - ineq.reset(offset); - ineq.push(lit, offset); - ineq.push(js.get_literal1(), offset); - ineq.push(js.get_literal2(), offset); - break; -#endif case sat::justification::CLAUSE: { ineq.reset(offset); sat::clause & c = s().get_clause(js);