1 /********************* */
2 /*! \file shared_terms_database.cpp
4 ** Original author: dejan
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/shared_terms_database.h"
21 using namespace theory
;
23 SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass
& notify
, context::Context
* context
)
24 : ContextNotifyObj(context
),
26 d_statSharedTerms("theory::shared_terms", 0),
27 d_addedSharedTermsSize(context
, 0),
28 d_termsToTheories(context
),
29 d_alreadyNotifiedMap(context
),
30 d_sharedNotify(notify
),
31 d_termToNotifyList(context
),
33 d_allocatedNLNext(context
, 0),
35 d_equalityEngine(d_EENotify
, context
, "SharedTermsDatabase")
37 StatisticsRegistry::registerStat(&d_statSharedTerms
);
40 SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException
)
42 StatisticsRegistry::unregisterStat(&d_statSharedTerms
);
43 for (unsigned i
= 0; i
< d_allocatedNLSize
; ++i
) {
44 d_allocatedNL
[i
]->deleteSelf();
48 void SharedTermsDatabase::addSharedTerm(TNode atom
, TNode term
, Theory::Set theories
) {
49 Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom
<< ", " << term
<< ", " << Theory::setToString(theories
) << ")" << std::endl
;
51 std::pair
<TNode
, TNode
> search_pair(atom
, term
);
52 SharedTermsTheoriesMap::iterator find
= d_termsToTheories
.find(search_pair
);
53 if (find
== d_termsToTheories
.end()) {
54 // First time for this term and this atom
55 d_atomsToTerms
[atom
].push_back(term
);
56 d_addedSharedTerms
.push_back(atom
);
57 d_addedSharedTermsSize
= d_addedSharedTermsSize
+ 1;
58 d_termsToTheories
[search_pair
] = theories
;
59 if (!d_equalityEngine
.hasTerm(term
)) {
60 d_equalityEngine
.addTriggerTerm(term
);
63 Assert(theories
!= (*find
).second
);
64 d_termsToTheories
[search_pair
] = Theory::setUnion(theories
, (*find
).second
);
68 SharedTermsDatabase::shared_terms_iterator
SharedTermsDatabase::begin(TNode atom
) const {
69 Assert(hasSharedTerms(atom
));
70 return d_atomsToTerms
.find(atom
)->second
.begin();
73 SharedTermsDatabase::shared_terms_iterator
SharedTermsDatabase::end(TNode atom
) const {
74 Assert(hasSharedTerms(atom
));
75 return d_atomsToTerms
.find(atom
)->second
.end();
78 bool SharedTermsDatabase::hasSharedTerms(TNode atom
) const {
79 return d_atomsToTerms
.find(atom
) != d_atomsToTerms
.end();
82 void SharedTermsDatabase::backtrack() {
83 for (int i
= d_addedSharedTerms
.size() - 1, i_end
= (int)d_addedSharedTermsSize
; i
>= i_end
; -- i
) {
84 TNode atom
= d_addedSharedTerms
[i
];
85 shared_terms_list
& list
= d_atomsToTerms
[atom
];
88 d_atomsToTerms
.erase(atom
);
91 d_addedSharedTerms
.resize(d_addedSharedTermsSize
);
94 Theory::Set
SharedTermsDatabase::getTheoriesToNotify(TNode atom
, TNode term
) const {
95 // Get the theories that share this term from this atom
96 std::pair
<TNode
, TNode
> search_pair(atom
, term
);
97 SharedTermsTheoriesMap::iterator find
= d_termsToTheories
.find(search_pair
);
98 Assert(find
!= d_termsToTheories
.end());
100 // Get the theories that were already notified
101 Theory::Set alreadyNotified
= 0;
102 AlreadyNotifiedMap::iterator theoriesFind
= d_alreadyNotifiedMap
.find(term
);
103 if (theoriesFind
!= d_alreadyNotifiedMap
.end()) {
104 alreadyNotified
= (*theoriesFind
).second
;
107 // Return the ones that haven't been notified yet
108 return Theory::setDifference((*find
).second
, alreadyNotified
);
112 Theory::Set
SharedTermsDatabase::getNotifiedTheories(TNode term
) const {
113 // Get the theories that were already notified
114 AlreadyNotifiedMap::iterator theoriesFind
= d_alreadyNotifiedMap
.find(term
);
115 if (theoriesFind
!= d_alreadyNotifiedMap
.end()) {
116 return (*theoriesFind
).second
;
123 SharedTermsDatabase::NotifyList
* SharedTermsDatabase::getNewNotifyList()
126 if (d_allocatedNLSize
== d_allocatedNLNext
) {
127 retval
= new (true) NotifyList(d_context
);
128 d_allocatedNL
.push_back(retval
);
129 d_allocatedNLNext
= ++d_allocatedNLSize
;
132 retval
= d_allocatedNL
[d_allocatedNLNext
];
133 d_allocatedNLNext
= d_allocatedNLNext
+ 1;
135 Assert(retval
->empty());
140 void SharedTermsDatabase::mergeSharedTerms(TNode a
, TNode b
)
142 // Note: a is the new representative
144 NotifyList
* pnlLeft
= NULL
;
145 NotifyList
* pnlRight
= NULL
;
147 TermToNotifyList::iterator it
= d_termToNotifyList
.find(a
);
148 if (it
== d_termToNotifyList
.end()) {
149 pnlLeft
= getNewNotifyList();
150 d_termToNotifyList
[a
] = pnlLeft
;
153 pnlLeft
= (*it
).second
;
155 it
= d_termToNotifyList
.find(b
);
156 if (it
!= d_termToNotifyList
.end()) {
157 pnlRight
= (*it
).second
;
160 // Get theories interested in EC for lhs
161 Theory::Set lhsSet
= getNotifiedTheories(a
);
162 Theory::Set rhsSet
= getNotifiedTheories(b
);
163 NotifyList::iterator nit
;
166 for (TheoryId currentTheory
= THEORY_FIRST
; currentTheory
!= THEORY_LAST
; ++ currentTheory
) {
168 if (Theory::setContains(currentTheory
, rhsSet
)) {
171 else if (pnlRight
!= NULL
&&
172 ((nit
= pnlRight
->end()) != pnlRight
->end())) {
173 right
= (*nit
).second
;
176 // no match for right: continue
180 if (Theory::setContains(currentTheory
, lhsSet
)) {
183 else if ((nit
= pnlLeft
->find(currentTheory
)) != pnlLeft
->end()) {
184 left
= (*nit
).second
;
187 // no match for left: insert right into left
188 (*pnlLeft
)[currentTheory
] = right
;
192 // New shared equality: notify the client
194 // TODO: add propagation of disequalities?
196 // Normalize the equality
197 Node equality
= left
.eqNode(right
);
198 Node normalized
= Rewriter::rewriteEquality(currentTheory
, equality
);
199 if (normalized
.getKind() != kind::CONST_BOOLEAN
|| !normalized
.getConst
<bool>()) {
201 d_sharedNotify
.notify(normalized
, equality
, currentTheory
);
208 void SharedTermsDatabase::markNotified(TNode term
, Theory::Set theories
) {
209 Theory::Set alreadyNotified
= d_alreadyNotifiedMap
[term
];
210 Theory::Set newlyNotified
= Theory::setDifference(theories
, alreadyNotified
);
211 if (newlyNotified
!= 0) {
212 TNode rep
= d_equalityEngine
.getRepresentative(term
);
214 TermToNotifyList::iterator it
= d_termToNotifyList
.find(rep
);
215 Assert(it
!= d_termToNotifyList
.end());
216 NotifyList
* pnl
= (*it
).second
;
217 for (TheoryId theory
= THEORY_FIRST
; theory
!= THEORY_LAST
; ++ theory
) {
218 if (Theory::setContains(theory
, newlyNotified
) &&
219 pnl
->find(theory
) == pnl
->end()) {
220 (*pnl
)[theory
] = term
;
225 d_alreadyNotifiedMap
[term
] = Theory::setUnion(newlyNotified
, alreadyNotified
);
229 bool SharedTermsDatabase::areEqual(TNode a
, TNode b
) {
230 return d_equalityEngine
.areEqual(a
,b
);
234 bool SharedTermsDatabase::areDisequal(TNode a
, TNode b
) {
235 return d_equalityEngine
.areDisequal(a
,b
);
238 void SharedTermsDatabase::processSharedLiteral(TNode literal
, TNode reason
)
240 bool negated
= literal
.getKind() == kind::NOT
;
241 TNode atom
= negated
? literal
[0] : literal
;
243 Assert(!d_equalityEngine
.areDisequal(atom
[0], atom
[1]));
244 d_equalityEngine
.assertEquality(atom
, false, reason
);
245 // !!! need to send this out
248 Assert(!d_equalityEngine
.areEqual(atom
[0], atom
[1]));
249 d_equalityEngine
.assertEquality(atom
, true, reason
);
253 static Node
mkAnd(const std::vector
<TNode
>& conjunctions
) {
254 Assert(conjunctions
.size() > 0);
257 all
.insert(conjunctions
.begin(), conjunctions
.end());
259 if (all
.size() == 1) {
260 // All the same, or just one
261 return conjunctions
[0];
264 NodeBuilder
<> conjunction(kind::AND
);
265 std::set
<TNode
>::const_iterator it
= all
.begin();
266 std::set
<TNode
>::const_iterator it_end
= all
.end();
267 while (it
!= it_end
) {
276 Node
SharedTermsDatabase::explain(TNode literal
)
278 std::vector
<TNode
> assumptions
;
279 if (literal
.getKind() == kind::NOT
) {
280 Assert(literal
[0].getKind() == kind::EQUAL
);
281 d_equalityEngine
.explainEquality(literal
[0][0], literal
[0][1], false, assumptions
);
283 Assert(literal
.getKind() == kind::EQUAL
);
284 d_equalityEngine
.explainEquality(literal
[0], literal
[1], true, assumptions
);
286 return mkAnd(assumptions
);