1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sat_watched.h 7 8 Abstract: 9 10 Element of the SAT solver watchlist. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2011-05-21. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "sat/sat_types.h" 22 #include "util/vector.h" 23 24 namespace sat { 25 /** 26 A watched element can be: 27 28 1) A literal: for watched binary clauses 29 2) A pair of literals: for watched ternary clauses 30 3) A pair (literal, clause-offset): for watched clauses, where the first element of the pair is a literal of the clause. 31 4) A external constraint-idx: for external constraints. 32 33 For binary clauses: we use a bit to store whether the binary clause was learned or not. 34 35 Remark: there are no clause objects for binary clauses. 36 */ 37 38 class extension; 39 40 class watched { 41 public: 42 enum kind { 43 BINARY = 0, TERNARY, CLAUSE, EXT_CONSTRAINT 44 }; 45 private: 46 size_t m_val1; 47 unsigned m_val2; 48 public: watched(literal l,bool learned)49 watched(literal l, bool learned): 50 m_val1(l.to_uint()), 51 m_val2(static_cast<unsigned>(BINARY) + (static_cast<unsigned>(learned) << 2)) { 52 SASSERT(is_binary_clause()); 53 SASSERT(get_literal() == l); 54 SASSERT(is_learned() == learned); 55 SASSERT(learned || is_binary_non_learned_clause()); 56 } 57 watched(literal l1,literal l2)58 watched(literal l1, literal l2) { 59 SASSERT(l1 != l2); 60 if (l1.index() > l2.index()) 61 std::swap(l1, l2); 62 m_val1 = l1.to_uint(); 63 m_val2 = static_cast<unsigned>(TERNARY) + (l2.to_uint() << 2); 64 SASSERT(is_ternary_clause()); 65 SASSERT(get_literal1() == l1); 66 SASSERT(get_literal2() == l2); 67 } 68 val2()69 unsigned val2() const { return m_val2; } 70 watched(literal blocked_lit,clause_offset cls_off)71 watched(literal blocked_lit, clause_offset cls_off): 72 m_val1(cls_off), 73 m_val2(static_cast<unsigned>(CLAUSE) + (blocked_lit.to_uint() << 2)) { 74 SASSERT(is_clause()); 75 SASSERT(get_blocked_literal() == blocked_lit); 76 SASSERT(get_clause_offset() == cls_off); 77 } 78 watched(ext_constraint_idx cnstr_idx)79 explicit watched(ext_constraint_idx cnstr_idx): 80 m_val1(cnstr_idx), 81 m_val2(static_cast<unsigned>(EXT_CONSTRAINT)) { 82 SASSERT(is_ext_constraint()); 83 SASSERT(get_ext_constraint_idx() == cnstr_idx); 84 } 85 get_kind()86 kind get_kind() const { return static_cast<kind>(m_val2 & 3); } 87 is_binary_clause()88 bool is_binary_clause() const { return get_kind() == BINARY; } get_literal()89 literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(static_cast<unsigned>(m_val1)); } set_literal(literal l)90 void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); } is_learned()91 bool is_learned() const { SASSERT(is_binary_clause()); return ((m_val2 >> 2) & 1) == 1; } 92 is_binary_learned_clause()93 bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); } is_binary_non_learned_clause()94 bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); } 95 set_learned(bool l)96 void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); } 97 is_ternary_clause()98 bool is_ternary_clause() const { return get_kind() == TERNARY; } get_literal1()99 literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast<unsigned>(m_val1)); } get_literal2()100 literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); } 101 is_clause()102 bool is_clause() const { return get_kind() == CLAUSE; } get_clause_offset()103 clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); } get_blocked_literal()104 literal get_blocked_literal() const { SASSERT(is_clause()); return to_literal(m_val2 >> 2); } set_clause_offset(clause_offset c)105 void set_clause_offset(clause_offset c) { SASSERT(is_clause()); m_val1 = c; } set_blocked_literal(literal l)106 void set_blocked_literal(literal l) { SASSERT(is_clause()); m_val2 = static_cast<unsigned>(CLAUSE) + (l.to_uint() << 2); } set_clause(literal blocked_lit,clause_offset cls_off)107 void set_clause(literal blocked_lit, clause_offset cls_off) { 108 m_val1 = cls_off; 109 m_val2 = static_cast<unsigned>(CLAUSE) + (blocked_lit.to_uint() << 2); 110 } 111 is_ext_constraint()112 bool is_ext_constraint() const { return get_kind() == EXT_CONSTRAINT; } get_ext_constraint_idx()113 ext_constraint_idx get_ext_constraint_idx() const { SASSERT(is_ext_constraint()); return m_val1; } 114 115 bool operator==(watched const & w) const { return m_val1 == w.m_val1 && m_val2 == w.m_val2; } 116 bool operator!=(watched const & w) const { return !operator==(w); } 117 }; 118 119 static_assert(0 <= watched::BINARY && watched::BINARY <= 3, ""); 120 static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, ""); 121 static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, ""); 122 static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, ""); 123 124 struct watched_lt { operatorwatched_lt125 bool operator()(watched const & w1, watched const & w2) const { 126 if (w2.is_binary_clause()) return false; 127 if (w1.is_binary_clause()) return true; 128 if (w2.is_ternary_clause()) return false; 129 if (w1.is_ternary_clause()) return true; 130 return false; 131 } 132 }; 133 134 typedef vector<watched> watch_list; 135 136 watched* find_binary_watch(watch_list & wlist, literal l); 137 watched const* find_binary_watch(watch_list const & wlist, literal l); 138 bool erase_clause_watch(watch_list & wlist, clause_offset c); 139 void erase_ternary_watch(watch_list & wlist, literal l1, literal l2); 140 void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned); 141 142 class clause_allocator; 143 std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext); 144 145 void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist); 146 }; 147 148