1 /********************* */
2 /*! \file congruence_manager.h
4 ** Original author: Tim King
5 ** Major contributors: Dejan Jovanovic
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
22 #include "theory/arith/arithvar.h"
23 #include "theory/arith/constraint_forward.h"
24 #include "theory/arith/partial_model.h"
26 #include "theory/uf/equality_engine.h"
28 #include "context/cdo.h"
29 #include "context/cdlist.h"
30 #include "context/context.h"
31 #include "context/cdtrail_queue.h"
32 #include "context/cdmaybe.h"
34 #include "util/statistics_registry.h"
35 #include "util/dense_map.h"
41 class ArithCongruenceManager
{
43 context::CDRaised d_inConflict
;
44 RaiseConflict d_raiseConflict
;
47 * The set of ArithVars equivalent to a pair of terms.
48 * If this is 0 or cannot be 0, this can be signalled.
49 * The pair of terms for the congruence is stored in watched equalities.
51 DenseSet d_watchedVariables
;
52 /** d_watchedVariables |-> (= x y) */
53 ArithVarToNodeMap d_watchedEqualities
;
56 class ArithCongruenceNotify
: public eq::EqualityEngineNotify
{
58 ArithCongruenceManager
& d_acm
;
60 ArithCongruenceNotify(ArithCongruenceManager
& acm
): d_acm(acm
) {}
62 bool eqNotifyTriggerEquality(TNode equality
, bool value
) {
63 Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
65 return d_acm
.propagate(equality
);
67 return d_acm
.propagate(equality
.notNode());
71 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
75 bool eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
76 Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1
<< ", " << t2
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
78 return d_acm
.propagate(t1
.eqNode(t2
));
80 return d_acm
.propagate(t1
.eqNode(t2
).notNode());
84 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
85 Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1
<< ", " << t2
<< std::endl
;
86 if (t1
.getKind() == kind::CONST_BOOLEAN
) {
87 d_acm
.propagate(t1
.iffNode(t2
));
89 d_acm
.propagate(t1
.eqNode(t2
));
93 void eqNotifyNewClass(TNode t
) { }
94 void eqNotifyPreMerge(TNode t1
, TNode t2
) { }
95 void eqNotifyPostMerge(TNode t1
, TNode t2
) { }
96 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) { }
98 ArithCongruenceNotify d_notify
;
100 context::CDList
<Node
> d_keepAlive
;
102 /** Store the propagations. */
103 context::CDTrailQueue
<Node
> d_propagatations
;
105 /* This maps the node a theory engine will request on an explain call to
106 * to its corresponding PropUnit.
107 * This is node is potentially both the propagation or
108 * Rewriter::rewrite(propagation).
110 typedef context::CDHashMap
<Node
, size_t, NodeHashFunction
> ExplainMap
;
111 ExplainMap d_explanationMap
;
113 ConstraintDatabase
& d_constraintDatabase
;
114 SetupLiteralCallBack d_setupLiteral
;
116 const ArithVariables
& d_avariables
;
118 eq::EqualityEngine d_ee
;
120 void raiseConflict(Node conflict
){
121 Assert(!inConflict());
122 Debug("arith::conflict") << "difference manager conflict " << conflict
<< std::endl
;
123 d_inConflict
.raise();
124 d_raiseConflict(conflict
);
128 bool inConflict() const{
129 return d_inConflict
.isRaised();
132 bool hasMorePropagations() const {
133 return !d_propagatations
.empty();
136 const Node
getNextPropagation() {
137 Assert(hasMorePropagations());
138 Node prop
= d_propagatations
.front();
139 d_propagatations
.dequeue();
143 bool canExplain(TNode n
) const {
144 return d_explanationMap
.find(n
) != d_explanationMap
.end();
147 void setMasterEqualityEngine(eq::EqualityEngine
* eq
);
150 Node
externalToInternal(TNode n
) const{
151 Assert(canExplain(n
));
152 ExplainMap::const_iterator iter
= d_explanationMap
.find(n
);
153 size_t pos
= (*iter
).second
;
154 return d_propagatations
[pos
];
157 void pushBack(TNode n
){
158 d_explanationMap
.insert(n
, d_propagatations
.size());
159 d_propagatations
.enqueue(n
);
161 ++(d_statistics
.d_propagations
);
164 void pushBack(TNode n
, TNode r
){
165 d_explanationMap
.insert(r
, d_propagatations
.size());
166 d_explanationMap
.insert(n
, d_propagatations
.size());
167 d_propagatations
.enqueue(n
);
169 ++(d_statistics
.d_propagations
);
172 void pushBack(TNode n
, TNode r
, TNode w
){
173 d_explanationMap
.insert(w
, d_propagatations
.size());
174 d_explanationMap
.insert(r
, d_propagatations
.size());
175 d_explanationMap
.insert(n
, d_propagatations
.size());
176 d_propagatations
.enqueue(n
);
178 ++(d_statistics
.d_propagations
);
181 bool propagate(TNode x
);
182 void explain(TNode literal
, std::vector
<TNode
>& assumptions
);
185 /** This sends a shared term to the uninterpreted equality engine. */
186 void assertionToEqualityEngine(bool eq
, ArithVar s
, TNode reason
);
188 /** Dequeues the delay queue and asserts these equalities.*/
189 void enableSharedTerms();
190 void dequeueLiterals();
192 void enqueueIntoNB(const std::set
<TNode
> all
, NodeBuilder
<>& nb
);
194 Node
explainInternal(TNode internal
);
198 ArithCongruenceManager(context::Context
* satContext
, ConstraintDatabase
&, SetupLiteralCallBack
, const ArithVariables
&, RaiseConflict raiseConflict
);
200 Node
explain(TNode literal
);
201 void explain(TNode lit
, NodeBuilder
<>& out
);
203 void addWatchedPair(ArithVar s
, TNode x
, TNode y
);
205 inline bool isWatchedVariable(ArithVar s
) const {
206 return d_watchedVariables
.isMember(s
);
209 /** Assert an equality. */
210 void watchedVariableIsZero(Constraint eq
);
212 /** Assert a conjunction from lb and ub. */
213 void watchedVariableIsZero(Constraint lb
, Constraint ub
);
215 /** Assert that the value cannot be zero. */
216 void watchedVariableCannotBeZero(Constraint c
);
218 /** Assert that the value cannot be zero. */
219 void watchedVariableCannotBeZero(Constraint c
, Constraint d
);
222 /** Assert that the value is congruent to a constant. */
223 void equalsConstant(Constraint eq
);
224 void equalsConstant(Constraint lb
, Constraint ub
);
227 void addSharedTerm(Node x
);
232 IntStat d_watchedVariables
;
233 IntStat d_watchedVariableIsZero
;
234 IntStat d_watchedVariableIsNotZero
;
236 IntStat d_equalsConstantCalls
;
238 IntStat d_propagations
;
239 IntStat d_propagateConstraints
;
246 };/* class ArithCongruenceManager */
248 }/* CVC4::theory::arith namespace */
249 }/* CVC4::theory namespace */
250 }/* CVC4 namespace */