1 /********************* */
2 /*! \file shared_terms_database.cpp
4 ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com>
5 ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>
6 ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Clark Barrett <barrett@cs.nyu.edu>
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 ** [[ Add lengthier description here ]]
13 ** \todo document this file
17 #include "theory/shared_terms_database.h"
18 #include "theory/theory_engine.h"
22 using namespace theory
;
24 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine
* theoryEngine
, context::Context
* context
)
25 : ContextNotifyObj(context
)
27 , d_statSharedTerms("theory::shared_terms", 0)
28 , d_addedSharedTermsSize(context
, 0)
29 , d_termsToTheories(context
)
30 , d_alreadyNotifiedMap(context
)
31 , d_registeredEqualities(context
)
33 , d_equalityEngine(d_EENotify
, context
, "SharedTermsDatabase")
34 , d_theoryEngine(theoryEngine
)
35 , d_inConflict(context
, false)
37 StatisticsRegistry::registerStat(&d_statSharedTerms
);
40 SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException
)
42 StatisticsRegistry::unregisterStat(&d_statSharedTerms
);
45 void SharedTermsDatabase::addEqualityToPropagate(TNode equality
) {
46 d_registeredEqualities
.insert(equality
);
47 d_equalityEngine
.addTriggerEquality(equality
);
52 void SharedTermsDatabase::addSharedTerm(TNode atom
, TNode term
, Theory::Set theories
) {
53 Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom
<< ", " << term
<< ", " << Theory::setToString(theories
) << ")" << std::endl
;
55 std::pair
<TNode
, TNode
> search_pair(atom
, term
);
56 SharedTermsTheoriesMap::iterator find
= d_termsToTheories
.find(search_pair
);
57 if (find
== d_termsToTheories
.end()) {
58 // First time for this term and this atom
59 d_atomsToTerms
[atom
].push_back(term
);
60 d_addedSharedTerms
.push_back(atom
);
61 d_addedSharedTermsSize
= d_addedSharedTermsSize
+ 1;
62 d_termsToTheories
[search_pair
] = theories
;
64 Assert(theories
!= (*find
).second
);
65 d_termsToTheories
[search_pair
] = Theory::setUnion(theories
, (*find
).second
);
69 SharedTermsDatabase::shared_terms_iterator
SharedTermsDatabase::begin(TNode atom
) const {
70 Assert(hasSharedTerms(atom
));
71 return d_atomsToTerms
.find(atom
)->second
.begin();
74 SharedTermsDatabase::shared_terms_iterator
SharedTermsDatabase::end(TNode atom
) const {
75 Assert(hasSharedTerms(atom
));
76 return d_atomsToTerms
.find(atom
)->second
.end();
79 bool SharedTermsDatabase::hasSharedTerms(TNode atom
) const {
80 return d_atomsToTerms
.find(atom
) != d_atomsToTerms
.end();
83 void SharedTermsDatabase::backtrack() {
84 for (int i
= d_addedSharedTerms
.size() - 1, i_end
= (int)d_addedSharedTermsSize
; i
>= i_end
; -- i
) {
85 TNode atom
= d_addedSharedTerms
[i
];
86 shared_terms_list
& list
= d_atomsToTerms
[atom
];
89 d_atomsToTerms
.erase(atom
);
92 d_addedSharedTerms
.resize(d_addedSharedTermsSize
);
95 Theory::Set
SharedTermsDatabase::getTheoriesToNotify(TNode atom
, TNode term
) const {
96 // Get the theories that share this term from this atom
97 std::pair
<TNode
, TNode
> search_pair(atom
, term
);
98 SharedTermsTheoriesMap::iterator find
= d_termsToTheories
.find(search_pair
);
99 Assert(find
!= d_termsToTheories
.end());
101 // Get the theories that were already notified
102 Theory::Set alreadyNotified
= 0;
103 AlreadyNotifiedMap::iterator theoriesFind
= d_alreadyNotifiedMap
.find(term
);
104 if (theoriesFind
!= d_alreadyNotifiedMap
.end()) {
105 alreadyNotified
= (*theoriesFind
).second
;
108 // Return the ones that haven't been notified yet
109 return Theory::setDifference((*find
).second
, alreadyNotified
);
113 Theory::Set
SharedTermsDatabase::getNotifiedTheories(TNode term
) const {
114 // Get the theories that were already notified
115 AlreadyNotifiedMap::iterator theoriesFind
= d_alreadyNotifiedMap
.find(term
);
116 if (theoriesFind
!= d_alreadyNotifiedMap
.end()) {
117 return (*theoriesFind
).second
;
123 bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory
, TNode a
, TNode b
, bool value
)
125 Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory
<< a
<< "," << b
<< ", " << (value
? "true" : "false") << ")" << endl
;
132 Node equality
= a
.eqNode(b
);
134 d_theoryEngine
->assertToTheory(equality
, theory
, THEORY_BUILTIN
);
136 d_theoryEngine
->assertToTheory(equality
.notNode(), theory
, THEORY_BUILTIN
);
143 void SharedTermsDatabase::markNotified(TNode term
, Theory::Set theories
) {
145 // Find out if there are any new theories that were notified about this term
146 Theory::Set alreadyNotified
= 0;
147 AlreadyNotifiedMap::iterator theoriesFind
= d_alreadyNotifiedMap
.find(term
);
148 if (theoriesFind
!= d_alreadyNotifiedMap
.end()) {
149 alreadyNotified
= (*theoriesFind
).second
;
151 Theory::Set newlyNotified
= Theory::setDifference(theories
, alreadyNotified
);
153 // If no new theories were notified, we are done
154 if (newlyNotified
== 0) {
158 Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term
<< ")" << endl
;
160 // First update the set of notified theories for this term
161 d_alreadyNotifiedMap
[term
] = Theory::setUnion(newlyNotified
, alreadyNotified
);
163 // Mark the shared terms in the equality engine
164 theory::TheoryId currentTheory
;
165 while ((currentTheory
= Theory::setPop(newlyNotified
)) != THEORY_LAST
) {
166 d_equalityEngine
.addTriggerTerm(term
, currentTheory
);
169 // Check for any conflits
173 bool SharedTermsDatabase::areEqual(TNode a
, TNode b
) const {
174 if (d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
)) {
175 return d_equalityEngine
.areEqual(a
,b
);
177 Assert(d_equalityEngine
.hasTerm(a
) || a
.isConst());
178 Assert(d_equalityEngine
.hasTerm(b
) || b
.isConst());
179 // since one (or both) of them is a constant, and the other is in the equality engine, they are not same
184 bool SharedTermsDatabase::areDisequal(TNode a
, TNode b
) const {
185 if (d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
)) {
186 return d_equalityEngine
.areDisequal(a
,b
,false);
188 Assert(d_equalityEngine
.hasTerm(a
) || a
.isConst());
189 Assert(d_equalityEngine
.hasTerm(b
) || b
.isConst());
190 // one (or both) are in the equality engine
195 void SharedTermsDatabase::assertEquality(TNode equality
, bool polarity
, TNode reason
)
197 Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality
<< ", " << (polarity
? "true" : "false") << ", " << reason
<< ")" << endl
;
198 // Add it to the equality engine
199 d_equalityEngine
.assertEquality(equality
, polarity
, reason
);
200 // Check for conflict
204 bool SharedTermsDatabase::propagateEquality(TNode equality
, bool polarity
) {
206 d_theoryEngine
->propagate(equality
, THEORY_BUILTIN
);
208 d_theoryEngine
->propagate(equality
.notNode(), THEORY_BUILTIN
);
213 static Node
mkAnd(const std::vector
<TNode
>& conjunctions
) {
214 Assert(conjunctions
.size() > 0);
217 all
.insert(conjunctions
.begin(), conjunctions
.end());
219 if (all
.size() == 1) {
220 // All the same, or just one
221 return conjunctions
[0];
224 NodeBuilder
<> conjunction(kind::AND
);
225 std::set
<TNode
>::const_iterator it
= all
.begin();
226 std::set
<TNode
>::const_iterator it_end
= all
.end();
227 while (it
!= it_end
) {
235 void SharedTermsDatabase::checkForConflict() {
237 d_inConflict
= false;
238 std::vector
<TNode
> assumptions
;
239 d_equalityEngine
.explainEquality(d_conflictLHS
, d_conflictRHS
, d_conflictPolarity
, assumptions
);
240 Node conflict
= mkAnd(assumptions
);
241 d_theoryEngine
->conflict(conflict
, THEORY_BUILTIN
);
242 d_conflictLHS
= d_conflictRHS
= Node::null();
246 bool SharedTermsDatabase::isKnown(TNode literal
) const {
247 bool polarity
= literal
.getKind() != kind::NOT
;
248 TNode equality
= polarity
? literal
: literal
[0];
250 return d_equalityEngine
.areEqual(equality
[0], equality
[1]);
252 return d_equalityEngine
.areDisequal(equality
[0], equality
[1], false);
256 Node
SharedTermsDatabase::explain(TNode literal
) const {
257 bool polarity
= literal
.getKind() != kind::NOT
;
258 TNode atom
= polarity
? literal
: literal
[0];
259 Assert(atom
.getKind() == kind::EQUAL
);
260 std::vector
<TNode
> assumptions
;
261 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
262 return mkAnd(assumptions
);