1 /********************* */
2 /*! \file shared_terms_database.h
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Tim King, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 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
16 #include "cvc4_private.h"
20 #include "expr/node.h"
21 #include "theory/theory.h"
22 #include "theory/uf/equality_engine.h"
23 #include "util/statistics_registry.h"
24 #include "context/cdhashset.h"
30 class SharedTermsDatabase
: public context::ContextNotifyObj
{
34 /** A container for a list of shared terms */
35 typedef std::vector
<TNode
> shared_terms_list
;
37 /** The iterator to go through the shared terms list */
38 typedef shared_terms_list::const_iterator shared_terms_iterator
;
42 /** Some statistics */
43 IntStat d_statSharedTerms
;
45 // Needs to be a map from Nodes as after a backtrack they might not exist
46 typedef std::hash_map
<Node
, shared_terms_list
, TNodeHashFunction
> SharedTermsMap
;
48 /** A map from atoms to a list of shared terms */
49 SharedTermsMap d_atomsToTerms
;
51 /** Each time we add a shared term, we add it's parent to this list */
52 std::vector
<TNode
> d_addedSharedTerms
;
54 /** Context-dependent size of the d_addedSharedTerms list */
55 context::CDO
<unsigned> d_addedSharedTermsSize
;
57 /** A map from atoms and subterms to the theories that use it */
58 typedef context::CDHashMap
<std::pair
<Node
, TNode
>, theory::Theory::Set
, TNodePairHashFunction
> SharedTermsTheoriesMap
;
59 SharedTermsTheoriesMap d_termsToTheories
;
61 /** Map from term to theories that have already been notified about the shared term */
62 typedef context::CDHashMap
<TNode
, theory::Theory::Set
, TNodeHashFunction
> AlreadyNotifiedMap
;
63 AlreadyNotifiedMap d_alreadyNotifiedMap
;
65 /** The registered equalities for propagation */
66 typedef context::CDHashSet
<Node
, NodeHashFunction
> RegisteredEqualitiesSet
;
67 RegisteredEqualitiesSet d_registeredEqualities
;
71 /** This method removes all the un-necessary stuff from the maps */
74 // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
75 class EENotifyClass
: public theory::eq::EqualityEngineNotify
{
76 SharedTermsDatabase
& d_sharedTerms
;
78 EENotifyClass(SharedTermsDatabase
& shared
): d_sharedTerms(shared
) {}
79 bool eqNotifyTriggerEquality(TNode equality
, bool value
) {
80 d_sharedTerms
.propagateEquality(equality
, value
);
84 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
89 bool eqNotifyTriggerTermEquality(theory::TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
90 return d_sharedTerms
.propagateSharedEquality(tag
, t1
, t2
, value
);
93 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
94 d_sharedTerms
.conflict(t1
, t2
, true);
97 void eqNotifyNewClass(TNode t
) { }
98 void eqNotifyPreMerge(TNode t1
, TNode t2
) { }
99 void eqNotifyPostMerge(TNode t1
, TNode t2
) { }
100 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) { }
103 /** The notify class for d_equalityEngine */
104 EENotifyClass d_EENotify
;
106 /** Equality engine */
107 theory::eq::EqualityEngine d_equalityEngine
;
110 * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
111 * the theory. Returns false if there is a direct conflict (via rewrite for example).
113 bool propagateSharedEquality(theory::TheoryId theory
, TNode a
, TNode b
, bool value
);
116 * Called from the equality engine when a trigger equality is deduced.
118 bool propagateEquality(TNode equality
, bool polarity
);
121 TheoryEngine
* d_theoryEngine
;
123 /** Are we in conflict */
124 context::CDO
<bool> d_inConflict
;
126 /** Conflicting terms, if any */
127 Node d_conflictLHS
, d_conflictRHS
;
129 /** Polarity of the conflict */
130 bool d_conflictPolarity
;
132 /** Called by the equality engine notify to mark the conflict */
133 void conflict(TNode lhs
, TNode rhs
, bool polarity
) {
135 // Only remember it if we're not already in conflict
139 d_conflictPolarity
= polarity
;
144 * Should be called before any public non-const method in order to
145 * enqueue the conflict to the theory engine.
147 void checkForConflict();
151 SharedTermsDatabase(TheoryEngine
* theoryEngine
, context::Context
* context
);
152 ~SharedTermsDatabase() throw(AssertionException
);
155 * Asserts the equality to the shared terms database,
157 void assertEquality(TNode equality
, bool polarity
, TNode reason
);
160 * Return whether the equality is alreday known to the engine
162 bool isKnown(TNode literal
) const;
165 * Returns an explanation of the propagation that came from the database.
167 Node
explain(TNode literal
) const;
170 * Add an equality to propagate.
172 void addEqualityToPropagate(TNode equality
);
175 * Add a shared term to the database. The shared term is a subterm of the atom and
176 * should be associated with the given theory.
178 void addSharedTerm(TNode atom
, TNode term
, theory::Theory::Set theories
);
181 * Mark that the given theories have been notified of the given shared term.
183 void markNotified(TNode term
, theory::Theory::Set theories
);
186 * Returns true if the atom contains any shared terms, false otherwise.
188 bool hasSharedTerms(TNode atom
) const;
191 * Iterator pointing to the first shared term belonging to the given atom.
193 shared_terms_iterator
begin(TNode atom
) const;
196 * Iterator pointing to the end of the list of shared terms belonging to the given atom.
198 shared_terms_iterator
end(TNode atom
) const;
201 * Get the theories that share the term in a given atom (and have not yet been notified).
203 theory::Theory::Set
getTheoriesToNotify(TNode atom
, TNode term
) const;
206 * Get the theories that share the term and have been notified already.
208 theory::Theory::Set
getNotifiedTheories(TNode term
) const;
211 * Returns true if the term is currently registered as shared with some theory.
213 bool isShared(TNode term
) const {
214 return d_alreadyNotifiedMap
.find(term
) != d_alreadyNotifiedMap
.end();
218 * Returns true if the literal is an (dis-)equality with both sides registered as shared with
221 bool isSharedEquality(TNode literal
) const {
222 TNode atom
= literal
.getKind() == kind::NOT
? literal
[0] : literal
;
223 return atom
.getKind() == kind::EQUAL
&& isShared(atom
[0]) && isShared(atom
[1]);
227 * Returns true if the shared terms a and b are known to be equal.
229 bool areEqual(TNode a
, TNode b
) const;
232 * Retursn true if the shared terms a and b are known to be dis-equal.
234 bool areDisequal(TNode a
, TNode b
) const;
237 * get equality engine
239 theory::eq::EqualityEngine
* getEqualityEngine() { return &d_equalityEngine
; }
244 * This method gets called on backtracks from the context manager.
246 void contextNotifyPop() {