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