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
223
224
|
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
#include "theory/arith/arithvar.h"
#include "theory/arith/constraint_forward.h"
#include "theory/uf/equality_engine.h"
#include "context/cdo.h"
#include "context/cdlist.h"
#include "context/context.h"
#include "context/cdtrail_queue.h"
#include "util/stats.h"
namespace CVC4 {
namespace theory {
namespace arith {
/**
* This implements a CDMaybe.
* This has either been set in the context or it has not.
* T must have a default constructor and support assignment.
*/
template <class T>
class CDMaybe {
private:
typedef std::pair<bool, T> BoolTPair;
context::CDO<BoolTPair> d_data;
public:
CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T()))
{}
bool isSet() const {
return d_data.get().first;
}
void set(const T& d){
Assert(!isSet());
d_data.set(std::make_pair(true, d));
}
const T& get() const{
Assert(isSet());
return d_data.get().second;
}
};
class DifferenceManager {
private:
CDMaybe<Node> d_conflict;
struct Difference {
bool isSlack;
TNode x;
TNode y;
Difference() : isSlack(false), x(TNode::null()), y(TNode::null()){}
Difference(TNode a, TNode b) : isSlack(true), x(a), y(b) {
Assert(x < y);
}
};
class DifferenceNotifyClass {
private:
DifferenceManager& d_dm;
public:
DifferenceNotifyClass(DifferenceManager& dm): d_dm(dm) {}
bool notify(TNode propagation) {
Debug("arith::differences") << "DifferenceNotifyClass::notify(" << propagation << ")" << std::endl;
// Just forward to dm
return d_dm.propagate(propagation);
}
void notify(TNode t1, TNode t2) {
Debug("arith::differences") << "DifferenceNotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
Node equality = t1.eqNode(t2);
d_dm.propagate(equality);
}
};
std::vector< Difference > d_differences;
struct LiteralsQueueElem {
bool d_eq;
ArithVar d_var;
Node d_reason;
LiteralsQueueElem() : d_eq(false), d_var(ARITHVAR_SENTINEL), d_reason() {}
LiteralsQueueElem(bool eq, ArithVar v, Node n) : d_eq(eq), d_var(v), d_reason(n) {}
};
/** Stores the queue of assertions. This keeps the Node backing the reasons */
context::CDTrailQueue<LiteralsQueueElem> d_literalsQueue;
//PropManager& d_queue;
/** Store the propagations. */
context::CDTrailQueue<Node> d_propagatations;
/* This maps the node a theory engine will request on an explain call to
* to its corresponding PropUnit.
* This is node is potentially both the propagation or Rewriter::rewrite(propagation).
*/
typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap;
ExplainMap d_explanationMap;
ConstraintDatabase& d_constraintDatabase;
TNodeCallBack& d_setupLiteral;
public:
bool inConflict() const{
return d_conflict.isSet();
};
Node conflict() const{
Assert(inConflict());
return d_conflict.get();
}
bool hasMorePropagations() const {
return !d_propagatations.empty();
}
const Node getNextPropagation() {
Assert(hasMorePropagations());
Node prop = d_propagatations.front();
d_propagatations.dequeue();
return prop;
}
bool canExplain(TNode n) const {
return d_explanationMap.find(n) != d_explanationMap.end();
}
private:
Node externalToInternal(TNode n) const{
Assert(canExplain(n));
size_t pos = (*(d_explanationMap.find(n))).second;
return d_propagatations[pos];
}
void pushBack(TNode n){
d_explanationMap.insert(n, d_propagatations.size());
d_propagatations.enqueue(n);
}
void pushBack(TNode n, TNode r){
d_explanationMap.insert(r, d_propagatations.size());
d_explanationMap.insert(n, d_propagatations.size());
d_propagatations.enqueue(n);
}
DifferenceNotifyClass d_notify;
theory::uf::EqualityEngine<DifferenceNotifyClass> d_ee;
bool propagate(TNode x);
void explain(TNode literal, std::vector<TNode>& assumptions);
Node d_false;
/**
* This is set to true when the first shared term is added.
* When this is set to true in the context, d_queue is emptied
* and not used again in the context.
*/
context::CDO<bool> d_hasSharedTerms;
/**
* The generalization of asserting an equality or a disequality.
* If there are shared equalities, this is added to the equality engine.
* Otherwise, this is put on a queue until there is a shared term.
*/
void assertLiteral(bool eq, ArithVar s, TNode reason);
/** This sends a shared term to the uninterpretted equality engine. */
void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
/** Dequeues the delay queue and asserts these equalities.*/
void enableSharedTerms();
void dequeueLiterals();
void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
Node explainInternal(TNode internal);
public:
DifferenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&);
Node explain(TNode literal);
void explain(TNode lit, NodeBuilder<>& out);
void addDifference(ArithVar s, Node x, Node y);
inline bool isDifferenceSlack(ArithVar s) const{
if(s < d_differences.size()){
return d_differences[s].isSlack;
}else{
return false;
}
}
/** Assert an equality. */
void differenceIsZero(Constraint eq);
/** Assert a conjunction from lb and ub. */
void differenceIsZero(Constraint lb, Constraint ub);
/** Assert that the value cannot be zero. */
void differenceCannotBeZero(Constraint c);
void addSharedTerm(Node x);
};/* class DifferenceManager */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H */
|
