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
|
/********************* */
/*! \file congruence_manager.h
** \verbatim
** Top contributors (to current version):
** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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 [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_private.h"
#pragma once
#include "context/cdlist.h"
#include "context/cdmaybe.h"
#include "context/cdo.h"
#include "context/cdtrail_queue.h"
#include "context/context.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/constraint_forward.h"
#include "theory/arith/partial_model.h"
#include "theory/uf/equality_engine.h"
#include "util/dense_map.h"
#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class EqualityInference;
}
namespace arith {
class ArithCongruenceManager {
private:
context::CDRaised d_inConflict;
RaiseEqualityEngineConflict d_raiseConflict;
/**
* The set of ArithVars equivalent to a pair of terms.
* If this is 0 or cannot be 0, this can be signalled.
* The pair of terms for the congruence is stored in watched equalities.
*/
DenseSet d_watchedVariables;
/** d_watchedVariables |-> (= x y) */
ArithVarToNodeMap d_watchedEqualities;
class ArithCongruenceNotify : public eq::EqualityEngineNotify {
private:
ArithCongruenceManager& d_acm;
public:
ArithCongruenceNotify(ArithCongruenceManager& acm);
bool eqNotifyTriggerEquality(TNode equality, bool value) override;
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
bool value) override;
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
void eqNotifyNewClass(TNode t) override;
void eqNotifyPreMerge(TNode t1, TNode t2) override;
void eqNotifyPostMerge(TNode t1, TNode t2) override;
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
};
ArithCongruenceNotify d_notify;
/** module for shostak normalization, d_eqi_counter is how many pending merges in d_eq_infer we have processed */
quantifiers::EqualityInference * d_eq_infer;
context::CDO< unsigned > d_eqi_counter;
Node d_true;
context::CDList<Node> d_keepAlive;
/** 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;
SetupLiteralCallBack d_setupLiteral;
const ArithVariables& d_avariables;
eq::EqualityEngine d_ee;
void raiseConflict(Node conflict);
public:
bool inConflict() const;
bool hasMorePropagations() const;
const Node getNextPropagation();
bool canExplain(TNode n) const;
void setMasterEqualityEngine(eq::EqualityEngine* eq);
private:
Node externalToInternal(TNode n) const;
void pushBack(TNode n);
void pushBack(TNode n, TNode r);
void pushBack(TNode n, TNode r, TNode w);
bool propagate(TNode x);
void explain(TNode literal, std::vector<TNode>& assumptions);
/** This sends a shared term to the uninterpreted equality engine. */
void assertionToEqualityEngine(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);
void eqNotifyNewClass(TNode t);
void eqNotifyPostMerge(TNode t1, TNode t2);
public:
ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
~ArithCongruenceManager();
Node explain(TNode literal);
void explain(TNode lit, NodeBuilder<>& out);
void addWatchedPair(ArithVar s, TNode x, TNode y);
inline bool isWatchedVariable(ArithVar s) const {
return d_watchedVariables.isMember(s);
}
/** Assert an equality. */
void watchedVariableIsZero(ConstraintCP eq);
/** Assert a conjunction from lb and ub. */
void watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub);
/** Assert that the value cannot be zero. */
void watchedVariableCannotBeZero(ConstraintCP c);
/** Assert that the value cannot be zero. */
void watchedVariableCannotBeZero(ConstraintCP c, ConstraintCP d);
/** Assert that the value is congruent to a constant. */
void equalsConstant(ConstraintCP eq);
void equalsConstant(ConstraintCP lb, ConstraintCP ub);
void addSharedTerm(Node x);
/** process inferred equalities based on Shostak normalization */
bool fixpointInfer();
eq::EqualityEngine * getEqualityEngine() { return &d_ee; }
private:
class Statistics {
public:
IntStat d_watchedVariables;
IntStat d_watchedVariableIsZero;
IntStat d_watchedVariableIsNotZero;
IntStat d_equalsConstantCalls;
IntStat d_propagations;
IntStat d_propagateConstraints;
IntStat d_conflicts;
Statistics();
~Statistics();
} d_statistics;
};/* class ArithCongruenceManager */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
|
