1 /*++
2 Copyright (c) 2020 Microsoft Corporation
3 
4 Module Name:
5 
6     euf_justification.h
7 
8 Abstract:
9 
10     justification structure for euf
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2020-08-23
15 
16 --*/
17 
18 #pragma once
19 
20 namespace euf {
21 
22     class justification {
23         enum class kind_t {
24             axiom_t,
25             congruence_t,
26             external_t
27         };
28         kind_t m_kind;
29         bool   m_comm;
30         void*  m_external;
justification(bool comm)31         justification(bool comm):
32             m_kind(kind_t::congruence_t),
33             m_comm(comm),
34             m_external(nullptr)
35         {}
36 
justification(void * ext)37         justification(void* ext):
38             m_kind(kind_t::external_t),
39             m_comm(false),
40             m_external(ext)
41         {}
42 
43     public:
justification()44         justification():
45             m_kind(kind_t::axiom_t),
46             m_comm(false),
47             m_external(nullptr)
48         {}
49 
axiom()50         static justification axiom() { return justification(); }
congruence(bool c)51         static justification congruence(bool c) { return justification(c); }
external(void * ext)52         static justification external(void* ext) { return justification(ext); }
53 
is_external()54         bool   is_external() const { return m_kind == kind_t::external_t; }
is_congruence()55         bool   is_congruence() const { return m_kind == kind_t::congruence_t; }
is_commutative()56         bool   is_commutative() const { return m_comm; }
57         template <typename T>
ext()58         T*  ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); }
59 
copy(std::function<void * (void *)> & copy_justification)60         justification copy(std::function<void*(void*)>& copy_justification) const {
61             switch (m_kind) {
62             case kind_t::external_t:
63                 return external(copy_justification(m_external));
64             case kind_t::axiom_t:
65                 return axiom();
66             case kind_t::congruence_t:
67                 return congruence(m_comm);
68             default:
69                 UNREACHABLE();
70                 return axiom();
71             }
72         }
73 
display(std::ostream & out,std::function<void (std::ostream &,void *)> const & ext)74         std::ostream& display(std::ostream& out, std::function<void (std::ostream&, void*)> const& ext) const {
75             switch (m_kind) {
76             case kind_t::external_t:
77                 if (ext)
78                     ext(out, m_external);
79                 else
80                     out << "external";
81                 return out;
82             case kind_t::axiom_t:
83                 return out << "axiom";
84             case kind_t::congruence_t:
85                 return out << "congruence";
86             default:
87                 UNREACHABLE();
88                 return out;
89             }
90             return out;
91         }
92     };
93 }
94