Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Dejan Jovanovic, Andrew Reynolds, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * [[ Add lengthier description here ]]
14 : : * \todo document this file
15 : : */
16 : :
17 : : #include "cvc5_private.h"
18 : :
19 : : #pragma once
20 : :
21 : : #include <unordered_map>
22 : :
23 : : #include "context/cdhashset.h"
24 : : #include "expr/node.h"
25 : : #include "proof/proof_node_manager.h"
26 : : #include "proof/trust_node.h"
27 : : #include "smt/env_obj.h"
28 : : #include "theory/ee_setup_info.h"
29 : : #include "theory/output_channel.h"
30 : : #include "theory/theory_id.h"
31 : : #include "theory/uf/equality_engine.h"
32 : : #include "theory/uf/proof_equality_engine.h"
33 : : #include "util/statistics_stats.h"
34 : :
35 : : namespace cvc5::internal {
36 : :
37 : : class TheoryEngine;
38 : :
39 : : class SharedTermsDatabase : protected EnvObj, public context::ContextNotifyObj
40 : : {
41 : : public:
42 : : /** A container for a list of shared terms */
43 : : typedef std::vector<TNode> shared_terms_list;
44 : :
45 : : /** The iterator to go through the shared terms list */
46 : : typedef shared_terms_list::const_iterator shared_terms_iterator;
47 : :
48 : : private:
49 : :
50 : : /** Some statistics */
51 : : IntStat d_statSharedTerms;
52 : :
53 : : // Needs to be a map from Nodes as after a backtrack they might not exist
54 : : typedef std::unordered_map<Node, shared_terms_list> SharedTermsMap;
55 : :
56 : : /** A map from atoms to a list of shared terms */
57 : : SharedTermsMap d_atomsToTerms;
58 : :
59 : : /** Each time we add a shared term, we add it's parent to this list */
60 : : std::vector<TNode> d_addedSharedTerms;
61 : :
62 : : /** Context-dependent size of the d_addedSharedTerms list */
63 : : context::CDO<unsigned> d_addedSharedTermsSize;
64 : :
65 : : /** A map from atoms and subterms to the theories that use it */
66 : : typedef context::CDHashMap<std::pair<Node, TNode>,
67 : : theory::TheoryIdSet,
68 : : TNodePairHashFunction>
69 : : SharedTermsTheoriesMap;
70 : : SharedTermsTheoriesMap d_termsToTheories;
71 : :
72 : : /** Map from term to theories that have already been notified about the shared term */
73 : : typedef context::CDHashMap<TNode, theory::TheoryIdSet> AlreadyNotifiedMap;
74 : : AlreadyNotifiedMap d_alreadyNotifiedMap;
75 : :
76 : : /** The registered equalities for propagation */
77 : : typedef context::CDHashSet<Node> RegisteredEqualitiesSet;
78 : : RegisteredEqualitiesSet d_registeredEqualities;
79 : :
80 : : private:
81 : : /** This method removes all the un-necessary stuff from the maps */
82 : : void backtrack();
83 : :
84 : : // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
85 : : class EENotifyClass : public theory::eq::EqualityEngineNotify {
86 : : SharedTermsDatabase& d_sharedTerms;
87 : : public:
88 : 49903 : EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
89 : 10662400 : bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
90 : : {
91 [ - + ][ - + ]: 10662400 : Assert(predicate.getKind() == Kind::EQUAL);
[ - - ]
92 : 10662400 : d_sharedTerms.propagateEquality(predicate, value);
93 : 10662400 : return true;
94 : : }
95 : :
96 : 6715920 : bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
97 : : TNode t1,
98 : : TNode t2,
99 : : bool value) override
100 : : {
101 : 6715920 : return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
102 : : }
103 : :
104 : 22777 : void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
105 : : {
106 : 22777 : d_sharedTerms.conflict(t1, t2, true);
107 : 22777 : }
108 : :
109 : 1087580 : void eqNotifyNewClass(TNode t) override {}
110 : 16346200 : void eqNotifyMerge(TNode t1, TNode t2) override {}
111 : 2526100 : void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
112 : : };
113 : :
114 : : /** The notify class for d_equalityEngine */
115 : : EENotifyClass d_EENotify;
116 : :
117 : : /**
118 : : * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
119 : : * the theory. Returns false if there is a direct conflict (via rewrite for example).
120 : : */
121 : : bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);
122 : :
123 : : /**
124 : : * Called from the equality engine when a trigger equality is deduced.
125 : : */
126 : : bool propagateEquality(TNode equality, bool polarity);
127 : :
128 : : /** Theory engine */
129 : : TheoryEngine* d_theoryEngine;
130 : :
131 : : /** Are we in conflict */
132 : : context::CDO<bool> d_inConflict;
133 : :
134 : : /** Conflicting terms, if any */
135 : : Node d_conflictLHS, d_conflictRHS;
136 : :
137 : : /** Polarity of the conflict */
138 : : bool d_conflictPolarity;
139 : :
140 : : /** Called by the equality engine notify to mark the conflict */
141 : 22777 : void conflict(TNode lhs, TNode rhs, bool polarity) {
142 [ + - ]: 22777 : if (!d_inConflict) {
143 : : // Only remember it if we're not already in conflict
144 : 22777 : d_inConflict = true;
145 : 22777 : d_conflictLHS = lhs;
146 : 22777 : d_conflictRHS = rhs;
147 : 22777 : d_conflictPolarity = polarity;
148 : : }
149 : 22777 : }
150 : :
151 : : /**
152 : : * Should be called before any public non-const method in order to
153 : : * enqueue the conflict to the theory engine.
154 : : */
155 : : void checkForConflict();
156 : :
157 : : public:
158 : : /**
159 : : * @param theoryEngine The parent theory engine
160 : : * @param context The SAT context
161 : : * @param userContext The user context
162 : : * @param pnm The proof node manager to use, which is non-null if proofs
163 : : * are enabled.
164 : : */
165 : : SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine);
166 : :
167 : : //-------------------------------------------- initialization
168 : : /** Called to set the equality engine. */
169 : : void setEqualityEngine(theory::eq::EqualityEngine* ee);
170 : : /**
171 : : * Returns true if we need an equality engine, this has the same contract
172 : : * as Theory::needsEqualityEngine.
173 : : */
174 : : bool needsEqualityEngine(theory::EeSetupInfo& esi);
175 : : //-------------------------------------------- end initialization
176 : :
177 : : /**
178 : : * Asserts n to the shared terms database with given polarity and reason
179 : : */
180 : : void assertShared(TNode n, bool polarity, TNode reason);
181 : :
182 : : /**
183 : : * Return whether the equality is alreday known to the engine
184 : : */
185 : : bool isKnown(TNode literal) const;
186 : :
187 : : /**
188 : : * Returns an explanation of the propagation that came from the database.
189 : : */
190 : : TrustNode explain(TNode literal) const;
191 : :
192 : : /**
193 : : * Add an equality to propagate.
194 : : */
195 : : void addEqualityToPropagate(TNode equality);
196 : :
197 : : /**
198 : : * Add a shared term to the database. The shared term is a subterm of the atom and
199 : : * should be associated with the given theory.
200 : : */
201 : : void addSharedTerm(TNode atom, TNode term, theory::TheoryIdSet theories);
202 : :
203 : : /**
204 : : * Mark that the given theories have been notified of the given shared term.
205 : : */
206 : : void markNotified(TNode term, theory::TheoryIdSet theories);
207 : :
208 : : /**
209 : : * Returns true if the atom contains any shared terms, false otherwise.
210 : : */
211 : : bool hasSharedTerms(TNode atom) const;
212 : :
213 : : /**
214 : : * Iterator pointing to the first shared term belonging to the given atom.
215 : : */
216 : : shared_terms_iterator begin(TNode atom) const;
217 : :
218 : : /**
219 : : * Iterator pointing to the end of the list of shared terms belonging to the given atom.
220 : : */
221 : : shared_terms_iterator end(TNode atom) const;
222 : :
223 : : /**
224 : : * Get the theories that share the term in a given atom (and have not yet been notified).
225 : : */
226 : : theory::TheoryIdSet getTheoriesToNotify(TNode atom, TNode term) const;
227 : :
228 : : /**
229 : : * Get the theories that share the term and have been notified already.
230 : : */
231 : : theory::TheoryIdSet getNotifiedTheories(TNode term) const;
232 : :
233 : : /**
234 : : * Returns true if the term is currently registered as shared with some theory.
235 : : */
236 : 4170460 : bool isShared(TNode term) const {
237 : 4170460 : return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
238 : : }
239 : :
240 : : /**
241 : : * Returns true if the literal is an (dis-)equality with both sides registered as shared with
242 : : * some theory.
243 : : */
244 : : bool isSharedEquality(TNode literal) const {
245 : : TNode atom = literal.getKind() == Kind::NOT ? literal[0] : literal;
246 : : return atom.getKind() == Kind::EQUAL && isShared(atom[0])
247 : : && isShared(atom[1]);
248 : : }
249 : :
250 : : /**
251 : : * Returns true if the shared terms a and b are known to be equal.
252 : : */
253 : : bool areEqual(TNode a, TNode b) const;
254 : :
255 : : /**
256 : : * Retursn true if the shared terms a and b are known to be dis-equal.
257 : : */
258 : : bool areDisequal(TNode a, TNode b) const;
259 : :
260 : : /**
261 : : * get equality engine
262 : : */
263 : : theory::eq::EqualityEngine* getEqualityEngine();
264 : :
265 : : protected:
266 : : /**
267 : : * This method gets called on backtracks from the context manager.
268 : : */
269 : 8700660 : void contextNotifyPop() override { backtrack(); }
270 : : /** Equality engine */
271 : : theory::eq::EqualityEngine* d_equalityEngine;
272 : : /** Proof equality engine, if we allocated one */
273 : : std::unique_ptr<theory::eq::ProofEqEngine> d_pfeeAlloc;
274 : : /** The proof equality engine we are using */
275 : : theory::eq::ProofEqEngine* d_pfee;
276 : : /** The proof node manager */
277 : : ProofNodeManager* d_pnm;
278 : : /** The output channel for propagations */
279 : : theory::OutputChannel& d_out;
280 : : };
281 : :
282 : : } // namespace cvc5::internal
|
