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