1 /********************* */
2 /*! \file shared_terms_database.h
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Mathias Preiner, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** [[ Add lengthier description here ]]
13 ** \todo document this file
16 #include "cvc4_private.h"
20 #include <unordered_map>
22 #include "context/cdhashset.h"
23 #include "expr/node.h"
24 #include "theory/theory.h"
25 #include "theory/uf/equality_engine.h"
26 #include "util/statistics_registry.h"
32 class SharedTermsDatabase
: public context::ContextNotifyObj
{
36 /** A container for a list of shared terms */
37 typedef std::vector
<TNode
> shared_terms_list
;
39 /** The iterator to go through the shared terms list */
40 typedef shared_terms_list::const_iterator shared_terms_iterator
;
44 /** Some statistics */
45 IntStat d_statSharedTerms
;
47 // Needs to be a map from Nodes as after a backtrack they might not exist
48 typedef std::unordered_map
<Node
, shared_terms_list
, TNodeHashFunction
> SharedTermsMap
;
50 /** A map from atoms to a list of shared terms */
51 SharedTermsMap d_atomsToTerms
;
53 /** Each time we add a shared term, we add it's parent to this list */
54 std::vector
<TNode
> d_addedSharedTerms
;
56 /** Context-dependent size of the d_addedSharedTerms list */
57 context::CDO
<unsigned> d_addedSharedTermsSize
;
59 /** A map from atoms and subterms to the theories that use it */
60 typedef context::CDHashMap
<std::pair
<Node
, TNode
>, theory::Theory::Set
, TNodePairHashFunction
> SharedTermsTheoriesMap
;
61 SharedTermsTheoriesMap d_termsToTheories
;
63 /** Map from term to theories that have already been notified about the shared term */
64 typedef context::CDHashMap
<TNode
, theory::Theory::Set
, TNodeHashFunction
> AlreadyNotifiedMap
;
65 AlreadyNotifiedMap d_alreadyNotifiedMap
;
67 /** The registered equalities for propagation */
68 typedef context::CDHashSet
<Node
, NodeHashFunction
> RegisteredEqualitiesSet
;
69 RegisteredEqualitiesSet d_registeredEqualities
;
73 /** This method removes all the un-necessary stuff from the maps */
76 // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
77 class EENotifyClass
: public theory::eq::EqualityEngineNotify
{
78 SharedTermsDatabase
& d_sharedTerms
;
80 EENotifyClass(SharedTermsDatabase
& shared
): d_sharedTerms(shared
) {}
81 bool eqNotifyTriggerEquality(TNode equality
, bool value
) override
83 d_sharedTerms
.propagateEquality(equality
, value
);
87 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) override
93 bool eqNotifyTriggerTermEquality(theory::TheoryId tag
,
98 return d_sharedTerms
.propagateSharedEquality(tag
, t1
, t2
, value
);
101 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) override
103 d_sharedTerms
.conflict(t1
, t2
, true);
106 void eqNotifyNewClass(TNode t
) override
{}
107 void eqNotifyPreMerge(TNode t1
, TNode t2
) override
{}
108 void eqNotifyPostMerge(TNode t1
, TNode t2
) override
{}
109 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) override
{}
112 /** The notify class for d_equalityEngine */
113 EENotifyClass d_EENotify
;
115 /** Equality engine */
116 theory::eq::EqualityEngine d_equalityEngine
;
119 * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
120 * the theory. Returns false if there is a direct conflict (via rewrite for example).
122 bool propagateSharedEquality(theory::TheoryId theory
, TNode a
, TNode b
, bool value
);
125 * Called from the equality engine when a trigger equality is deduced.
127 bool propagateEquality(TNode equality
, bool polarity
);
130 TheoryEngine
* d_theoryEngine
;
132 /** Are we in conflict */
133 context::CDO
<bool> d_inConflict
;
135 /** Conflicting terms, if any */
136 Node d_conflictLHS
, d_conflictRHS
;
138 /** Polarity of the conflict */
139 bool d_conflictPolarity
;
141 /** Called by the equality engine notify to mark the conflict */
142 void conflict(TNode lhs
, TNode rhs
, bool polarity
) {
144 // Only remember it if we're not already in conflict
148 d_conflictPolarity
= polarity
;
153 * Should be called before any public non-const method in order to
154 * enqueue the conflict to the theory engine.
156 void checkForConflict();
160 SharedTermsDatabase(TheoryEngine
* theoryEngine
, context::Context
* context
);
161 ~SharedTermsDatabase();
164 * Asserts the equality to the shared terms database,
166 void assertEquality(TNode equality
, bool polarity
, TNode reason
);
169 * Return whether the equality is alreday known to the engine
171 bool isKnown(TNode literal
) const;
174 * Returns an explanation of the propagation that came from the database.
176 Node
explain(TNode literal
) const;
179 * Add an equality to propagate.
181 void addEqualityToPropagate(TNode equality
);
184 * Add a shared term to the database. The shared term is a subterm of the atom and
185 * should be associated with the given theory.
187 void addSharedTerm(TNode atom
, TNode term
, theory::Theory::Set theories
);
190 * Mark that the given theories have been notified of the given shared term.
192 void markNotified(TNode term
, theory::Theory::Set theories
);
195 * Returns true if the atom contains any shared terms, false otherwise.
197 bool hasSharedTerms(TNode atom
) const;
200 * Iterator pointing to the first shared term belonging to the given atom.
202 shared_terms_iterator
begin(TNode atom
) const;
205 * Iterator pointing to the end of the list of shared terms belonging to the given atom.
207 shared_terms_iterator
end(TNode atom
) const;
210 * Get the theories that share the term in a given atom (and have not yet been notified).
212 theory::Theory::Set
getTheoriesToNotify(TNode atom
, TNode term
) const;
215 * Get the theories that share the term and have been notified already.
217 theory::Theory::Set
getNotifiedTheories(TNode term
) const;
220 * Returns true if the term is currently registered as shared with some theory.
222 bool isShared(TNode term
) const {
223 return d_alreadyNotifiedMap
.find(term
) != d_alreadyNotifiedMap
.end();
227 * Returns true if the literal is an (dis-)equality with both sides registered as shared with
230 bool isSharedEquality(TNode literal
) const {
231 TNode atom
= literal
.getKind() == kind::NOT
? literal
[0] : literal
;
232 return atom
.getKind() == kind::EQUAL
&& isShared(atom
[0]) && isShared(atom
[1]);
236 * Returns true if the shared terms a and b are known to be equal.
238 bool areEqual(TNode a
, TNode b
) const;
241 * Retursn true if the shared terms a and b are known to be dis-equal.
243 bool areDisequal(TNode a
, TNode b
) const;
246 * get equality engine
248 theory::eq::EqualityEngine
* getEqualityEngine() { return &d_equalityEngine
; }
253 * This method gets called on backtracks from the context manager.
255 void contextNotifyPop() override
{ backtrack(); }