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 "theory/term_registration_visitor.h"
15 : :
16 : : #include "base/configuration.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "smt/logic_exception.h"
19 : : #include "theory/theory_engine.h"
20 : :
21 : : using namespace cvc5::internal::theory;
22 : :
23 : : namespace cvc5::internal {
24 : :
25 : 0 : std::string PreRegisterVisitor::toString() const {
26 : 0 : std::stringstream ss;
27 : 0 : TNodeToTheorySetMap::const_iterator it = d_visited.begin();
28 [ - - ]: 0 : for (; it != d_visited.end(); ++ it) {
29 : 0 : ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
30 : 0 : << std::endl;
31 : : }
32 : 0 : return ss.str();
33 : 0 : }
34 : :
35 : : /**
36 : : * Return true if we already visited the term current with the given parent,
37 : : * assuming that the set of theories in visitedTheories has already processed
38 : : * current. This method is used by PreRegisterVisitor and SharedTermsVisitor
39 : : * below.
40 : : */
41 : 14755782 : bool isAlreadyVisited(Env& env,
42 : : TheoryIdSet visitedTheories,
43 : : TNode current,
44 : : TNode parent)
45 : : {
46 : 14755782 : TheoryId currentTheoryId = env.theoryOf(current);
47 [ - + ]: 14755782 : if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
48 : : {
49 : : // current theory not visited, return false
50 : 0 : return false;
51 : : }
52 : :
53 [ + + ]: 14755782 : if (current == parent)
54 : : {
55 : : // top-level and current visited, return true
56 : 2167263 : return true;
57 : : }
58 : :
59 : : // The current theory has already visited it, so now it depends on the parent
60 : : // and the type
61 : 12588519 : TheoryId parentTheoryId = env.theoryOf(parent);
62 [ + + ]: 12588519 : if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
63 : : {
64 : : // parent theory not visited, return false
65 : 360368 : return false;
66 : : }
67 : :
68 : : // do we need to consider the type?
69 : 12228151 : TypeNode type = current.getType();
70 [ + + ][ + + ]: 12228151 : if (currentTheoryId == parentTheoryId && !env.isFiniteType(type))
[ + + ][ + + ]
[ - - ]
71 : : {
72 : : // current and parent are the same theory, and we are infinite, return true
73 : 8037949 : return true;
74 : : }
75 : 4190202 : TheoryId typeTheoryId = env.theoryOf(type);
76 : 4190202 : return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
77 : 12228151 : }
78 : :
79 : 50176 : PreRegisterVisitor::PreRegisterVisitor(Env& env, TheoryEngine* engine)
80 : 50176 : : EnvObj(env), d_engine(engine), d_visited(context())
81 : : {
82 : 50176 : }
83 : :
84 : 2380031 : bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
85 : :
86 [ + - ]: 2380031 : Trace("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
87 : 2380031 : Kind k = parent.getKind();
88 [ + - ][ + - ]: 2368999 : if ((isClosureKind(k) || k == Kind::SEP_STAR || k == Kind::SEP_WAND
89 [ - + ][ - - ]: 4749030 : || (k == Kind::SEP_LABEL && current.getType().isBoolean()))
[ + + ][ - - ]
90 [ + + ][ + + ]: 4749030 : && current != parent)
[ - + ]
91 : : {
92 [ + - ]: 4591 : Trace("register::internal") << "quantifier:true" << std::endl;
93 : 4591 : return true;
94 : : }
95 : :
96 : : // Get the theories that have already visited this node
97 : 2375440 : TNodeToTheorySetMap::iterator find = d_visited.find(current);
98 [ + + ]: 2375440 : if (find == d_visited.end()) {
99 : : // not visited at all, return false
100 : 1272931 : return false;
101 : : }
102 : :
103 : 1102509 : TheoryIdSet visitedTheories = (*find).second;
104 : 1102509 : return isAlreadyVisited(d_env, visitedTheories, current, parent);
105 : : }
106 : :
107 : 527793 : void PreRegisterVisitor::visit(TNode current, TNode parent) {
108 : :
109 [ + - ]: 527793 : Trace("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
110 [ - + ]: 527793 : if (TraceIsOn("register::internal")) {
111 : 0 : Trace("register::internal") << toString() << std::endl;
112 : : }
113 : :
114 : : // get the theories we already preregistered with
115 : 527793 : TheoryIdSet visitedTheories = d_visited[current];
116 : :
117 : : // call the preregistration on current, parent or type theories and update
118 : : // visitedTheories. The set of preregistering theories coincides with
119 : : // visitedTheories here.
120 : 527797 : preRegister(
121 : : d_env, d_engine, visitedTheories, current, parent, visitedTheories);
122 : :
123 [ + - ]: 1055582 : Trace("register::internal")
124 : 0 : << "PreRegisterVisitor::visit(" << current << "," << parent
125 : 0 : << "): now registered with "
126 [ - + ][ - - ]: 527791 : << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
127 : : // update the theories set for current
128 : 527791 : d_visited[current] = visitedTheories;
129 [ - + ][ - + ]: 527791 : Assert(d_visited.find(current) != d_visited.end());
[ - - ]
130 [ - + ][ - + ]: 527791 : Assert(alreadyVisited(current, parent));
[ - - ]
131 : 527791 : }
132 : :
133 : 12297068 : void PreRegisterVisitor::preRegister(Env& env,
134 : : TheoryEngine* te,
135 : : TheoryIdSet& visitedTheories,
136 : : TNode current,
137 : : TNode parent,
138 : : TheoryIdSet preregTheories)
139 : : {
140 : : // Preregister with the current theory, if necessary
141 : 12297068 : TheoryId currentTheoryId = env.theoryOf(current);
142 : 12297100 : preRegisterWithTheory(
143 : : te, visitedTheories, currentTheoryId, current, parent, preregTheories);
144 : :
145 [ + + ]: 12297052 : if (current != parent)
146 : : {
147 : : // preregister with parent theory, if necessary
148 : 10130545 : TheoryId parentTheoryId = env.theoryOf(parent);
149 : 10130545 : preRegisterWithTheory(
150 : : te, visitedTheories, parentTheoryId, current, parent, preregTheories);
151 : :
152 : : // Note that if enclosed by different theories it's shared, for example,
153 : : // in read(a, f(a)), f(a) should be shared with integers.
154 : 10130545 : TypeNode type = current.getType();
155 [ + + ][ + + ]: 10130545 : if (currentTheoryId != parentTheoryId || env.isFiniteType(type))
[ + + ][ + + ]
[ - - ]
156 : : {
157 : : // preregister with the type's theory, if necessary
158 : 3258523 : TheoryId typeTheoryId = env.theoryOf(type);
159 : 3258523 : preRegisterWithTheory(
160 : : te, visitedTheories, typeTheoryId, current, parent, preregTheories);
161 : : }
162 : 10130545 : }
163 : 12297052 : }
164 : 25686136 : void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
165 : : TheoryIdSet& visitedTheories,
166 : : TheoryId id,
167 : : TNode current,
168 : : TNode parent,
169 : : TheoryIdSet preregTheories)
170 : : {
171 [ + + ]: 25686136 : if (TheoryIdSetUtil::setContains(id, visitedTheories))
172 : : {
173 : : // already visited
174 : 10718347 : return;
175 : : }
176 : 14967789 : visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
177 [ + + ]: 14967789 : if (TheoryIdSetUtil::setContains(id, preregTheories))
178 : : {
179 : : // already pregregistered
180 : 10780952 : return;
181 : : }
182 [ + - ]: 4186837 : if (Configuration::isAssertionBuild())
183 : : {
184 [ + - ]: 8373674 : Trace("register::internal")
185 : 0 : << "PreRegisterVisitor::visit(" << current << "," << parent
186 : 4186837 : << "): adding " << id << std::endl;
187 : : // This should never throw an exception, since theories should be
188 : : // guaranteed to be initialized.
189 [ - + ]: 4186837 : if (!te->isTheoryEnabled(id))
190 : : {
191 : 0 : std::stringstream ss;
192 : 0 : ss << "The logic doesn't include theory " << id
193 : 0 : << ", but found a term in that theory." << std::endl;
194 : 0 : throw LogicException(ss.str());
195 : 0 : }
196 : : }
197 : : // call the theory's preRegisterTerm method
198 : 4186837 : Theory* th = te->theoryOf(id);
199 : 4186837 : th->preRegisterTerm(current);
200 : : }
201 : :
202 : 313013 : void PreRegisterVisitor::start(CVC5_UNUSED TNode node) {}
203 : :
204 : 50176 : SharedTermsVisitor::SharedTermsVisitor(Env& env,
205 : : TheoryEngine* te,
206 : 50176 : SharedTermsDatabase& sharedTerms)
207 : : : EnvObj(env),
208 : 50176 : d_engine(te),
209 : 50176 : d_sharedTerms(sharedTerms),
210 : 50176 : d_preregistered(context())
211 : : {
212 : 50176 : }
213 : :
214 : 0 : std::string SharedTermsVisitor::toString() const {
215 : 0 : std::stringstream ss;
216 : 0 : TNodeVisitedMap::const_iterator it = d_visited.begin();
217 [ - - ]: 0 : for (; it != d_visited.end(); ++ it) {
218 : 0 : ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
219 : 0 : << std::endl;
220 : : }
221 : 0 : return ss.str();
222 : 0 : }
223 : :
224 : 47402511 : bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
225 : :
226 [ + - ]: 47402511 : Trace("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
227 : 47402511 : Kind k = parent.getKind();
228 [ + + ][ + + ]: 47066609 : if ((isClosureKind(k) || k == Kind::SEP_STAR || k == Kind::SEP_WAND
229 [ + + ][ + + ]: 94467830 : || (k == Kind::SEP_LABEL && current.getType().isBoolean()))
[ + + ][ - - ]
230 [ + + ][ + + ]: 94469120 : && current != parent)
[ + + ]
231 : : {
232 [ + - ]: 145528 : Trace("register::internal") << "quantifier:true" << std::endl;
233 : 145528 : return true;
234 : : }
235 : 47256983 : TNodeVisitedMap::const_iterator find = d_visited.find(current);
236 : : // If node is not visited at all, just return false
237 [ + + ]: 47256983 : if (find == d_visited.end()) {
238 [ + - ]: 33603710 : Trace("register::internal") << "1:false" << std::endl;
239 : 33603710 : return false;
240 : : }
241 : :
242 : 13653273 : TheoryIdSet visitedTheories = (*find).second;
243 : 13653273 : return isAlreadyVisited(d_env, visitedTheories, current, parent);
244 : : }
245 : :
246 : 11769275 : void SharedTermsVisitor::visit(TNode current, TNode parent) {
247 : :
248 [ + - ]: 11769275 : Trace("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
249 [ - + ]: 11769275 : if (TraceIsOn("register::internal")) {
250 : 0 : Trace("register::internal") << toString() << std::endl;
251 : : }
252 : 11769275 : TheoryIdSet visitedTheories = d_visited[current];
253 : 11769275 : TheoryIdSet preregTheories = d_preregistered[current];
254 : :
255 : : // preregister the term with the current, parent or type theories, as needed
256 : 11769303 : PreRegisterVisitor::preRegister(
257 : : d_env, d_engine, visitedTheories, current, parent, preregTheories);
258 : :
259 : : // Record the new theories that we visited
260 : 11769261 : d_visited[current] = visitedTheories;
261 : :
262 : : // add visited theories to those who have preregistered
263 : 23538522 : d_preregistered[current] =
264 : 11769261 : TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);
265 : :
266 : : // If there is more than two theories and a new one has been added notify the shared terms database
267 : 11769261 : TheoryId currentTheoryId = d_env.theoryOf(current);
268 [ + + ]: 11769261 : if (TheoryIdSetUtil::setDifference(
269 : : visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
270 : : {
271 : 2722534 : d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
272 : : }
273 : :
274 [ - + ][ - + ]: 11769261 : Assert(d_visited.find(current) != d_visited.end());
[ - - ]
275 [ - + ][ - + ]: 11769261 : Assert(alreadyVisited(current, parent));
[ - - ]
276 : 11769261 : }
277 : :
278 : 1854266 : void SharedTermsVisitor::start(TNode node) {
279 : 1854266 : d_visited.clear();
280 : 1854266 : d_atom = node;
281 : 1854266 : }
282 : :
283 : 1854252 : void SharedTermsVisitor::done(CVC5_UNUSED TNode node) { clear(); }
284 : :
285 : 1854252 : void SharedTermsVisitor::clear() {
286 : 1854252 : d_atom = TNode();
287 : 1854252 : d_visited.clear();
288 : 1854252 : }
289 : :
290 : : } // namespace cvc5::internal
|
