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