1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sat_justification.h 7 8 Abstract: 9 10 Justifications for SAT assignments 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2011-05-21. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 namespace sat { 22 23 class justification { 24 public: 25 enum kind { NONE = 0, BINARY = 1, TERNARY = 2, CLAUSE = 3, EXT_JUSTIFICATION = 4}; 26 private: 27 unsigned m_level; 28 size_t m_val1; 29 unsigned m_val2; justification(unsigned lvl,ext_justification_idx idx,kind k)30 justification(unsigned lvl, ext_justification_idx idx, kind k):m_level(lvl), m_val1(idx), m_val2(k) {} val1()31 unsigned val1() const { return static_cast<unsigned>(m_val1); } 32 public: justification(unsigned lvl)33 justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {} justification(unsigned lvl,literal l)34 explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {} justification(unsigned lvl,literal l1,literal l2)35 justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {} justification(unsigned lvl,clause_offset cls_off)36 explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {} mk_ext_justification(unsigned lvl,ext_justification_idx idx)37 static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); } 38 level()39 unsigned level() const { return m_level; } 40 get_kind()41 kind get_kind() const { return static_cast<kind>(m_val2 & 7); } 42 is_none()43 bool is_none() const { return m_val2 == NONE; } 44 is_binary_clause()45 bool is_binary_clause() const { return m_val2 == BINARY; } get_literal()46 literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(val1()); } 47 is_ternary_clause()48 bool is_ternary_clause() const { return get_kind() == TERNARY; } get_literal1()49 literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(val1()); } get_literal2()50 literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); } 51 is_clause()52 bool is_clause() const { return m_val2 == CLAUSE; } get_clause_offset()53 clause_offset get_clause_offset() const { return m_val1; } 54 is_ext_justification()55 bool is_ext_justification() const { return m_val2 == EXT_JUSTIFICATION; } get_ext_justification_idx()56 ext_justification_idx get_ext_justification_idx() const { return m_val1; } 57 58 }; 59 60 inline std::ostream & operator<<(std::ostream & out, justification const & j) { 61 switch (j.get_kind()) { 62 case justification::NONE: 63 out << "none"; 64 break; 65 case justification::BINARY: 66 out << "binary " << j.get_literal(); 67 break; 68 case justification::TERNARY: 69 out << "ternary " << j.get_literal1() << " " << j.get_literal2(); 70 break; 71 case justification::CLAUSE: 72 out << "clause"; 73 break; 74 case justification::EXT_JUSTIFICATION: 75 out << "external"; 76 break; 77 } 78 out << " @" << j.level(); 79 return out; 80 } 81 82 }; 83 84