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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
|
/********************* */
/*! \file theory_uf.h
** \verbatim
** Top contributors (to current version):
** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief This is the interface to TheoryUF implementations
**
** This is the interface to TheoryUF implementations. All
** implementations of TheoryUF should inherit from this class.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__UF__THEORY_UF_H
#define CVC4__THEORY__UF__THEORY_UF_H
#include "context/cdo.h"
#include "expr/node.h"
#include "expr/node_trie.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/proof_checker.h"
#include "theory/uf/symmetry_breaker.h"
#include "theory/uf/theory_uf_rewriter.h"
namespace CVC4 {
namespace theory {
namespace uf {
class CardinalityExtension;
class HoExtension;
class TheoryUF : public Theory {
public:
class NotifyClass : public eq::EqualityEngineNotify {
TheoryUF& d_uf;
public:
NotifyClass(TheoryUF& uf): d_uf(uf) {}
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_uf.propagateLit(predicate);
}
return d_uf.propagateLit(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
bool value) override
{
Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
return d_uf.propagateLit(t1.eqNode(t2));
}
return d_uf.propagateLit(t1.eqNode(t2).notNode());
}
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
{
Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_uf.conflict(t1, t2);
}
void eqNotifyNewClass(TNode t) override
{
Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
d_uf.eqNotifyNewClass(t);
}
void eqNotifyMerge(TNode t1, TNode t2) override
{
Debug("uf-notify") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
<< ")" << std::endl;
d_uf.eqNotifyMerge(t1, t2);
}
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
{
Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
d_uf.eqNotifyDisequal(t1, t2, reason);
}
};/* class TheoryUF::NotifyClass */
private:
/** The notify class */
NotifyClass d_notify;
/** The associated cardinality extension (or nullptr if it does not exist) */
std::unique_ptr<CardinalityExtension> d_thss;
/** the higher-order solver extension (or nullptr if it does not exist) */
std::unique_ptr<HoExtension> d_ho;
/** node for true */
Node d_true;
/**
* Should be called to propagate the literal. We use a node here
* since some of the propagated literals are not kept anywhere.
*/
bool propagateLit(TNode literal);
/**
* Explain why this literal is true by adding assumptions
* with proof (if "pf" is non-NULL).
*/
void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf);
/**
* Explain a literal, with proof (if "pf" is non-NULL).
*/
Node explain(TNode literal, eq::EqProof* pf);
/** All the function terms that the theory has seen */
context::CDList<TNode> d_functionsTerms;
/** Symmetry analyzer */
SymmetryBreaker d_symb;
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
/** called when a new equivalance class is created */
void eqNotifyNewClass(TNode t);
/** called when two equivalance classes have merged */
void eqNotifyMerge(TNode t1, TNode t2);
/** called when two equivalence classes are made disequal */
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
TheoryUF(context::Context* c,
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr,
std::string instanceName = "");
~TheoryUF();
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
* documentation in Theory::needsEqualityEngine.
*/
bool needsEqualityEngine(EeSetupInfo& esi) override;
/** finish initialization */
void finishInit() override;
//--------------------------------- end initialization
//--------------------------------- standard check
/** Post-check, called after the fact queue of the theory is processed. */
void postCheck(Effort level) override;
/** Pre-notify fact, return true if processed. */
bool preNotifyFact(TNode atom,
bool pol,
TNode fact,
bool isPrereg,
bool isInternal) override;
/** Notify fact */
void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
//--------------------------------- end standard check
/** Collect model values in m based on the relevant terms given by termSet */
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
TrustNode expandDefinition(Node node) override;
void preRegisterTerm(TNode term) override;
TrustNode explain(TNode n) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
void presolve() override;
void computeCareGraph() override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
std::string identify() const override { return "THEORY_UF"; }
/** get a pointer to the uf with cardinality */
CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
private:
bool areCareDisequal(TNode x, TNode y);
void addCarePairs(const TNodeTrie* t1,
const TNodeTrie* t2,
unsigned arity,
unsigned depth);
TheoryUfRewriter d_rewriter;
/** Proof rule checker */
UfProofRuleChecker d_ufProofChecker;
/** A (default) theory state object */
TheoryState d_state;
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* CVC4__THEORY__UF__THEORY_UF_H */
|
