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