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