1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     smt_eq_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 "util/tptr.h"
23 
24 namespace smt {
25 
26     /**
27        \brief Proof like object used to track dependencies of equality propagation.
28        The idea is to reduce the cost of dependency tracking for the most common
29        justifications used during equality propagation: (asserted equality & congruence).
30     */
31     class eq_justification {
32         void * m_data;
33     public:
34         enum kind {
35             AXIOM,           //!< no justification, it is only used when proof generation is disabled
36             CONGRUENCE,
37             EQUATION,        //!< asserted equation
38             JUSTIFICATION    //!< fallback
39         };
40 
eq_justification()41         explicit eq_justification():
42             m_data(reinterpret_cast<void*>(static_cast<size_t>(AXIOM))) {
43         }
44 
45         /**
46            \brief Create a justification for the congruence rule.
47            If commutativity == true, then it means it is a combined justification: commutativity + congruence.
48         */
eq_justification(bool commutativity)49         explicit eq_justification(bool commutativity):
50             m_data(BOXTAGINT(void*, static_cast<unsigned>(commutativity), CONGRUENCE)) {
51         }
52 
eq_justification(literal l)53         explicit eq_justification(literal l):
54             m_data(BOXTAGINT(void*, l.index(), EQUATION)) {
55         }
56 
eq_justification(justification * js)57         explicit eq_justification(justification * js):
58             m_data(TAG(void*, js, JUSTIFICATION)) {
59         }
60 
get_kind()61         kind get_kind() const {
62             return static_cast<kind>(GET_TAG(m_data));
63         }
64 
get_literal()65         literal get_literal() const { SASSERT(get_kind() == EQUATION); return to_literal(UNBOXINT(m_data)); }
66 
get_justification()67         justification * get_justification() const { SASSERT(get_kind() == JUSTIFICATION); return UNTAG(justification*, m_data); }
68 
used_commutativity()69         bool used_commutativity() const { SASSERT(get_kind() == CONGRUENCE); return UNBOXINT(m_data) != 0; }
70 
mk_axiom()71         static eq_justification mk_axiom() {
72             return eq_justification();
73         }
74 
75         static eq_justification mk_cg(bool comm = false) {
76             return eq_justification(comm);
77         }
78     };
79 
80     const eq_justification null_eq_justification(static_cast<justification*>(nullptr));
81 };
82 
83 
84