1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_b_justification.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-19. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "smt/smt_literal.h" 22 #include "smt/smt_clause.h" 23 24 namespace smt { 25 26 /** 27 \brief Proof like object used to track dependencies of boolean propagation. 28 The idea is to reduce the cost of dependency tracking for the most common 29 justifications used during boolean propagation: unit propagation 30 */ 31 class b_justification { 32 void * m_data; 33 public: 34 enum kind { 35 CLAUSE, //!< clause of arbitrary size 36 BIN_CLAUSE, //!< binary clause 37 AXIOM, //!< no justification, it is only use if proof generation is disabled 38 JUSTIFICATION //!< fallback 39 }; 40 b_justification()41 b_justification(): 42 m_data(reinterpret_cast<void*>(static_cast<size_t>(AXIOM))) {} 43 b_justification(clause * c)44 explicit b_justification(clause * c): 45 m_data(TAG(void*, c, CLAUSE)) { 46 } 47 b_justification(literal l)48 explicit b_justification(literal l): 49 m_data(BOXTAGINT(void*, l.index(), BIN_CLAUSE)) { 50 } 51 b_justification(justification * js)52 explicit b_justification(justification * js): 53 m_data(TAG(void*, js, JUSTIFICATION)) { 54 SASSERT(js); 55 } 56 get_kind()57 kind get_kind() const { 58 return static_cast<kind>(GET_TAG(m_data)); 59 } 60 get_clause()61 clause * get_clause() const { 62 SASSERT(get_kind() == CLAUSE); 63 return UNTAG(clause*, m_data); 64 } 65 get_justification()66 justification * get_justification() const { 67 SASSERT(get_kind() == JUSTIFICATION); 68 return UNTAG(justification*, m_data); 69 } 70 get_literal()71 literal get_literal() const { 72 SASSERT(get_kind() == BIN_CLAUSE); 73 return to_literal(UNBOXINT(m_data)); 74 } 75 76 bool operator==(b_justification const & other) const { 77 return m_data == other.m_data; 78 } 79 80 bool operator!=(b_justification const & other) const { 81 return !operator==(other); 82 } 83 mk_axiom()84 static b_justification mk_axiom() { 85 return b_justification(); 86 } 87 }; 88 89 const b_justification null_b_justification(static_cast<clause*>(nullptr)); 90 91 inline std::ostream& operator<<(std::ostream& out, b_justification::kind k) { 92 switch (k) { 93 case b_justification::CLAUSE: return out << "clause"; 94 case b_justification::BIN_CLAUSE: return out << "bin_clause"; 95 case b_justification::AXIOM: return out << "axiom"; 96 case b_justification::JUSTIFICATION: return out << "theory"; 97 } 98 return out; 99 } 100 101 typedef std::pair<literal, b_justification> justified_literal; 102 }; 103 104 105