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 : : * Base for theory interface.
11 : : */
12 : :
13 : : #include "theory/theory.h"
14 : :
15 : : #include <iostream>
16 : : #include <sstream>
17 : : #include <string>
18 : : #include <vector>
19 : :
20 : : #include "base/check.h"
21 : : #include "expr/node_algorithm.h"
22 : : #include "expr/skolem_manager.h"
23 : : #include "options/arith_options.h"
24 : : #include "options/smt_options.h"
25 : : #include "options/theory_options.h"
26 : : #include "theory/ee_setup_info.h"
27 : : #include "theory/ext_theory.h"
28 : : #include "theory/output_channel.h"
29 : : #include "theory/quantifiers_engine.h"
30 : : #include "theory/substitutions.h"
31 : : #include "theory/theory_inference_manager.h"
32 : : #include "theory/theory_model.h"
33 : : #include "theory/theory_rewriter.h"
34 : : #include "theory/theory_state.h"
35 : : #include "theory/trust_substitutions.h"
36 : :
37 : : using namespace std;
38 : :
39 : : namespace cvc5::internal {
40 : : namespace theory {
41 : :
42 : 0 : std::ostream& operator<<(std::ostream& os, Theory::Effort level)
43 : : {
44 [ - - ][ - - ]: 0 : switch (level)
45 : : {
46 : 0 : case Theory::EFFORT_STANDARD: os << "EFFORT_STANDARD"; break;
47 : 0 : case Theory::EFFORT_FULL: os << "EFFORT_FULL"; break;
48 : 0 : case Theory::EFFORT_LAST_CALL: os << "EFFORT_LAST_CALL"; break;
49 : 0 : default: Unreachable();
50 : : }
51 : 0 : return os;
52 : : } /* ostream& operator<<(ostream&, Theory::Effort) */
53 : :
54 : 715365 : Theory::Theory(TheoryId id,
55 : : Env& env,
56 : : OutputChannel& out,
57 : : Valuation valuation,
58 : 715365 : std::string name)
59 : : : EnvObj(env),
60 : 715365 : d_instanceName(name),
61 : 2146095 : d_checkTime(statisticsRegistry().registerTimer(getStatsPrefix(id) + name
62 : 1430730 : + "checkTime")),
63 : 1430730 : d_computeCareGraphTime(statisticsRegistry().registerTimer(
64 : 1430730 : getStatsPrefix(id) + name + "computeCareGraphTime")),
65 : 715365 : d_out(&out),
66 : 715365 : d_valuation(valuation),
67 : 715365 : d_equalityEngine(nullptr),
68 : 715365 : d_allocEqualityEngine(nullptr),
69 : 715365 : d_theoryState(nullptr),
70 : 715365 : d_inferManager(nullptr),
71 : 715365 : d_quantEngine(nullptr),
72 [ + + ]: 715365 : d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
73 : : : nullptr),
74 : 715365 : d_checkEarlyExit(true),
75 : 715365 : d_id(id),
76 : 715365 : d_facts(d_env.getContext()),
77 : 715365 : d_factsHead(d_env.getContext(), 0),
78 : 715365 : d_careGraph(nullptr)
79 : : {
80 : 715365 : }
81 : :
82 : 710493 : Theory::~Theory() {}
83 : :
84 : 102192 : bool Theory::needsEqualityEngine(CVC5_UNUSED EeSetupInfo& esi)
85 : : {
86 : : // by default, this theory does not use an (official) equality engine
87 : 102192 : return false;
88 : : }
89 : :
90 : 715344 : void Theory::setEqualityEngine(eq::EqualityEngine* ee)
91 : : {
92 : : // set the equality engine pointer
93 : 715344 : d_equalityEngine = ee;
94 [ + + ]: 715344 : if (d_theoryState != nullptr)
95 : : {
96 : 664248 : d_theoryState->setEqualityEngine(ee);
97 : : }
98 [ + + ]: 715344 : if (d_inferManager != nullptr)
99 : : {
100 : 664248 : d_inferManager->setEqualityEngine(ee);
101 : : }
102 : 715344 : }
103 : :
104 : 715344 : void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
105 : : {
106 : : // quantifiers engine may be null if not in quantified logic
107 : 715344 : d_quantEngine = qe;
108 : 715344 : }
109 : :
110 : 715344 : void Theory::setDecisionManager(DecisionManager* dm)
111 : : {
112 [ - + ][ - + ]: 715344 : Assert(dm != nullptr);
[ - - ]
113 [ + + ]: 715344 : if (d_inferManager != nullptr)
114 : : {
115 : 664248 : d_inferManager->setDecisionManager(dm);
116 : : }
117 : 715344 : }
118 : :
119 : 0 : void Theory::finishInitStandalone()
120 : : {
121 : 0 : EeSetupInfo esi;
122 [ - - ]: 0 : if (needsEqualityEngine(esi))
123 : : {
124 : : // always associated with the same SAT context as the theory
125 : : d_allocEqualityEngine =
126 : 0 : std::make_unique<eq::EqualityEngine>(d_env,
127 : 0 : context(),
128 : 0 : *esi.d_notify,
129 : : esi.d_name,
130 : 0 : esi.d_constantsAreTriggers);
131 : : // use it as the official equality engine
132 : 0 : setEqualityEngine(d_allocEqualityEngine.get());
133 : : }
134 : 0 : finishInit();
135 : 0 : }
136 : :
137 : 273861019 : TheoryId Theory::theoryOf(TNode node,
138 : : options::TheoryOfMode mode,
139 : : TheoryId usortOwner)
140 : : {
141 : 273861019 : TheoryId tid = THEORY_BUILTIN;
142 [ + + ][ - ]: 273861019 : switch (mode)
143 : : {
144 : 196055878 : case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
145 : : // Constants, variables, 0-ary constructors
146 [ + + ]: 196055878 : if (node.isVar())
147 : : {
148 : 10968638 : tid = theoryOf(node.getType(), usortOwner);
149 : : }
150 [ + + ]: 185087240 : else if (node.getKind() == Kind::EQUAL)
151 : : {
152 : : // Equality is owned by the theory that owns the domain
153 : 15744514 : tid = theoryOf(node[0].getType(), usortOwner);
154 : : }
155 : : else
156 : : {
157 : : // Regular nodes are owned by the kind. Notice that constants are a
158 : : // special case here, where the theory of the kind of a constant
159 : : // always coincides with the type of that constant.
160 : 169342726 : tid = kindToTheoryId(node.getKind());
161 : : }
162 : 196055878 : break;
163 : 77805141 : case options::TheoryOfMode::THEORY_OF_TERM_BASED:
164 : : // Variables
165 [ + + ]: 77805141 : if (node.isVar())
166 : : {
167 [ + + ]: 10360661 : if (theoryOf(node.getType(), usortOwner) != theory::THEORY_BOOL)
168 : : {
169 : : // We treat the variables as uninterpreted
170 : 10275831 : tid = THEORY_UF;
171 : : }
172 : : else
173 : : {
174 : : // Other Boolean variables are Bool
175 : 84830 : tid = THEORY_BOOL;
176 : : }
177 : : }
178 [ + + ]: 67444480 : else if (node.getKind() == Kind::EQUAL)
179 : : { // Equality
180 : 11401355 : TNode l = node[0];
181 : 11401355 : TNode r = node[1];
182 : 11401355 : TypeNode ltype = l.getType();
183 : 11401355 : TypeNode rtype = r.getType();
184 : : // If the types are different, we must assign based on type due
185 : : // to handling subtypes (limited to arithmetic). Also, if we are
186 : : // a Boolean equality, we must assign THEORY_BOOL.
187 [ + - ][ + + ]: 11401355 : if (ltype != rtype || ltype.isBoolean())
[ + + ]
188 : : {
189 : 16735 : tid = theoryOf(ltype, usortOwner);
190 : : }
191 : : else
192 : : {
193 : : // If both sides belong to the same theory the choice is easy
194 : 11384620 : TheoryId T1 = theoryOf(l, mode, usortOwner);
195 : 11384620 : TheoryId T2 = theoryOf(r, mode, usortOwner);
196 [ + + ]: 11384620 : if (T1 == T2)
197 : : {
198 : 6895293 : tid = T1;
199 : : }
200 : : else
201 : : {
202 : 4489327 : TheoryId T3 = theoryOf(ltype, usortOwner);
203 : : // This is a case of
204 : : // * x*y = f(z) -> UF
205 : : // * x = c -> UF
206 : : // * f(x) = read(a, y) -> either UF or ARRAY
207 : : // at least one of the theories has to be parametric, i.e. theory
208 : : // of the type is different from the theory of the term
209 [ + + ]: 4489327 : if (T1 == T3)
210 : : {
211 : 838540 : tid = T2;
212 : : }
213 [ + + ]: 3650787 : else if (T2 == T3)
214 : : {
215 : 3578735 : tid = T1;
216 : : }
217 : : else
218 : : {
219 : : // If both are parametric, we take the smaller one (arbitrary)
220 [ + + ]: 72052 : tid = T1 < T2 ? T1 : T2;
221 : : }
222 : : }
223 : : }
224 : 11401355 : }
225 : : else
226 : : {
227 : : // Regular nodes are owned by the kind, which includes constants as a
228 : : // special case.
229 : 56043125 : tid = kindToTheoryId(node.getKind());
230 : : }
231 : 77805141 : break;
232 : 0 : default: Unreachable();
233 : : }
234 : 273861019 : return tid;
235 : : }
236 : :
237 : 2165994 : void Theory::notifySharedTerm(CVC5_UNUSED TNode n)
238 : : {
239 : : // do nothing
240 : 2165994 : }
241 : :
242 : 5286876 : void Theory::notifyInConflict()
243 : : {
244 [ + + ]: 5286876 : if (d_inferManager != nullptr)
245 : : {
246 : 4909242 : d_inferManager->notifyInConflict();
247 : : }
248 : 5286876 : }
249 : :
250 : 55694 : void Theory::computeCareGraph()
251 : : {
252 [ - + ][ - + ]: 55694 : Assert(d_theoryState != nullptr);
[ - - ]
253 [ + - ]: 55694 : Trace("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
254 : 55694 : const context::CDList<TNode>& sharedTerms = d_theoryState->getSharedTerms();
255 : 55694 : size_t ssize = sharedTerms.size();
256 [ + + ]: 64003 : for (size_t i = 0; i < ssize; ++i)
257 : : {
258 : 8309 : TNode a = sharedTerms[i];
259 : 8309 : TypeNode aType = a.getType();
260 [ + + ]: 26512 : for (size_t j = i + 1; j < ssize; ++j)
261 : : {
262 : 18203 : TNode b = sharedTerms[j];
263 [ + + ]: 18203 : if (b.getType() != aType)
264 : : {
265 : : // We don't care about the terms of different types
266 : 6228 : continue;
267 : : }
268 [ + + ]: 11975 : switch (d_valuation.getEqualityStatus(a, b))
269 : : {
270 : 7784 : case EQUALITY_TRUE_AND_PROPAGATED:
271 : : case EQUALITY_FALSE_AND_PROPAGATED:
272 : : // If we know about it, we should have propagated it, so we can skip
273 : 7784 : break;
274 : 4191 : default:
275 : : // Let's split on it
276 : 4191 : addCarePair(a, b);
277 : 4191 : break;
278 : : }
279 [ + + ]: 18203 : }
280 : 8309 : }
281 : 55694 : }
282 : :
283 : 0 : void Theory::printFacts(std::ostream& os) const
284 : : {
285 : 0 : unsigned i, n = d_facts.size();
286 [ - - ]: 0 : for (i = 0; i < n; i++)
287 : : {
288 : 0 : const Assertion& a_i = d_facts[i];
289 : 0 : Node assertion = a_i;
290 : 0 : os << d_id << '[' << i << ']' << " " << assertion << endl;
291 : 0 : }
292 : 0 : }
293 : :
294 : 0 : void Theory::debugPrintFacts() const
295 : : {
296 : 0 : TraceChannel.getStream() << "Theory::debugPrintFacts()" << endl;
297 : 0 : printFacts(TraceChannel.getStream());
298 : 0 : }
299 : :
300 : 194419 : bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
301 : : {
302 : : // if we are using an equality engine, assert it to the model
303 [ + + ][ + + ]: 194419 : if (d_equalityEngine != nullptr && !termSet.empty())
[ + + ]
304 : : {
305 [ + - ]: 126944 : Trace("model-builder") << "Assert Equality engine for " << d_id
306 : 63472 : << std::endl;
307 [ - + ]: 63472 : if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
308 : : {
309 : 0 : return false;
310 : : }
311 : : }
312 [ + - ]: 194419 : Trace("model-builder") << "Collect Model values for " << d_id << std::endl;
313 : : // now, collect theory-specific value assigments
314 : 194419 : return collectModelValues(m, termSet);
315 : : }
316 : :
317 : 281363 : void Theory::computeRelevantTerms(CVC5_UNUSED std::set<Node>& termSet)
318 : : {
319 : : // by default, there are no additional relevant terms
320 : 281363 : }
321 : :
322 : 513992 : void Theory::collectAssertedTerms(std::set<Node>& termSet,
323 : : bool includeShared,
324 : : const std::set<Kind>& irrKinds) const
325 : : {
326 : : // Collect all terms appearing in assertions
327 : 513992 : context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
328 : 513992 : assert_it_end = facts_end();
329 [ + + ]: 24219378 : for (; assert_it != assert_it_end; ++assert_it)
330 : : {
331 : 23705386 : collectTerms(*assert_it, termSet, irrKinds);
332 : : }
333 : :
334 [ + - ]: 513992 : if (includeShared)
335 : : {
336 [ - + ][ - + ]: 513992 : Assert(d_theoryState != nullptr);
[ - - ]
337 : : // Add terms that are shared terms
338 : : context::CDList<TNode>::const_iterator
339 : 513992 : shared_it = d_theoryState->shared_terms_begin(),
340 : 513992 : shared_it_end = d_theoryState->shared_terms_end();
341 [ + + ]: 8009661 : for (; shared_it != shared_it_end; ++shared_it)
342 : : {
343 : 7495669 : collectTerms(*shared_it, termSet, irrKinds);
344 : : }
345 : : }
346 : 513992 : }
347 : 383397 : void Theory::collectAssertedTermsForModel(std::set<Node>& termSet,
348 : : bool includeShared) const
349 : : {
350 : : // use the irrelevant model kinds from the theory state
351 : : const std::set<Kind>& irrKinds =
352 : 383397 : d_theoryState->getModel()->getIrrelevantKinds();
353 : 383397 : collectAssertedTerms(termSet, includeShared, irrKinds);
354 : 383397 : }
355 : :
356 : 31201055 : void Theory::collectTerms(TNode n,
357 : : std::set<Node>& termSet,
358 : : const std::set<Kind>& irrKinds) const
359 : : {
360 : 31201055 : std::vector<TNode> visit;
361 : 31201055 : TNode cur;
362 : 31201055 : visit.push_back(n);
363 : : do
364 : : {
365 : 106504305 : cur = visit.back();
366 : 106504305 : visit.pop_back();
367 [ + + ]: 106504305 : if (termSet.find(cur) != termSet.end())
368 : : {
369 : : // already visited
370 : 54889532 : continue;
371 : : }
372 : 51614773 : Kind k = cur.getKind();
373 : : // only add to term set if a relevant kind
374 [ + + ]: 51614773 : if (irrKinds.find(k) == irrKinds.end())
375 : : {
376 : 31918126 : termSet.insert(cur);
377 : : }
378 : : // traverse owned terms, don't go under quantifiers
379 [ + + ][ + + ]: 92695039 : if ((k == Kind::NOT || k == Kind::EQUAL || d_env.theoryOf(cur) == d_id)
[ + + ][ - - ]
380 [ + + ][ + + ]: 92695039 : && !cur.isClosure())
[ + + ]
381 : : {
382 : 47115892 : visit.insert(visit.end(), cur.begin(), cur.end());
383 : : }
384 [ + + ]: 106504305 : } while (!visit.empty());
385 : 31201055 : }
386 : :
387 : 14381 : bool Theory::collectModelValues(CVC5_UNUSED TheoryModel* m,
388 : : CVC5_UNUSED const std::set<Node>& termSet)
389 : : {
390 : 14381 : return true;
391 : : }
392 : :
393 : 89505 : bool Theory::ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions)
394 : : {
395 [ - + ][ - + ]: 89505 : Assert(tin.getKind() == TrustNodeKind::LEMMA);
[ - - ]
396 : 89505 : TNode in = tin.getNode();
397 [ + + ]: 89505 : if (in.getKind() == Kind::EQUAL)
398 : : {
399 : : // (and (= x t) phi) can be replaced by phi[x/t] if
400 : : // 1) x is a variable
401 : : // 2) x is not in the term t
402 : : // 3) x : T and t : S, then S <: T
403 : 65023 : if (in[0].isVar() && d_valuation.isLegalElimination(in[0], in[1]))
404 : : {
405 : 33649 : outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
406 : 33649 : return true;
407 : : }
408 : 31374 : if (in[1].isVar() && d_valuation.isLegalElimination(in[1], in[0]))
409 : : {
410 : 1056 : outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
411 : 1056 : return true;
412 : : }
413 : : }
414 : :
415 : 54800 : return false;
416 : 89505 : }
417 : :
418 : 0 : std::pair<bool, Node> Theory::entailmentCheck(CVC5_UNUSED TNode lit)
419 : : {
420 : 0 : return make_pair(false, Node::null());
421 : : }
422 : :
423 : 117274 : void Theory::addCarePair(TNode t1, TNode t2)
424 : : {
425 [ - + ][ - + ]: 117274 : Assert(d_careGraph != nullptr);
[ - - ]
426 [ + - ]: 234548 : Trace("sharing") << "Theory::addCarePair: add pair " << d_id << " " << t1
427 : 117274 : << " " << t2 << std::endl;
428 : 117274 : d_careGraph->insert(CarePair(t1, t2, d_id));
429 : 117274 : }
430 : 486237 : void Theory::addCarePairArgs(TNode a, TNode b)
431 : : {
432 [ - + ][ - + ]: 486237 : Assert(d_careGraph != nullptr);
[ - - ]
433 [ - + ][ - + ]: 486237 : Assert(d_equalityEngine != nullptr);
[ - - ]
434 [ + - ][ + - ]: 486237 : Assert(a.hasOperator() && b.hasOperator());
[ - + ][ - + ]
[ - - ]
435 [ - + ][ - + ]: 486237 : Assert(a.getOperator() == b.getOperator());
[ - - ]
436 [ - + ][ - + ]: 486237 : Assert(a.getNumChildren() == b.getNumChildren());
[ - - ]
437 [ + - ]: 972474 : Trace("sharing") << "Theory::addCarePairArgs: checking function " << d_id
438 : 486237 : << " " << a << " " << b << std::endl;
439 [ + + ]: 1469402 : for (size_t k = 0, nchildren = a.getNumChildren(); k < nchildren; ++k)
440 : : {
441 : 983165 : TNode x = a[k];
442 : 983165 : TNode y = b[k];
443 [ + + ][ - - ]: 983165 : if (d_equalityEngine->isTriggerTerm(x, d_id)
444 [ + + ][ + - ]: 1633726 : && d_equalityEngine->isTriggerTerm(y, d_id)
[ - - ]
445 : 1633726 : && !d_equalityEngine->areEqual(x, y))
446 : : {
447 : 104558 : TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id);
448 : 104558 : TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id);
449 : 104558 : addCarePair(x_shared, y_shared);
450 : 104558 : }
451 : 983165 : }
452 : 486237 : }
453 : :
454 : 63901 : void Theory::processCarePairArgs(TNode a, TNode b)
455 : : {
456 : : // if a and b are already equal, we ignore this pair
457 [ + + ]: 63901 : if (d_theoryState->areEqual(a, b))
458 : : {
459 : 1431 : return;
460 : : }
461 : : // otherwise, we add pairs for each of their arguments
462 : 62470 : addCarePairArgs(a, b);
463 : : }
464 : :
465 : 274183 : bool Theory::areCareDisequal(TNode x, TNode y)
466 : : {
467 [ - + ][ - + ]: 274183 : Assert(d_equalityEngine != nullptr);
[ - - ]
468 [ - + ][ - + ]: 274183 : Assert(d_equalityEngine->hasTerm(x));
[ - - ]
469 [ - + ][ - + ]: 274183 : Assert(d_equalityEngine->hasTerm(y));
[ - - ]
470 [ - + ][ - + ]: 274183 : Assert(x != y);
[ - - ]
471 [ + + ][ + - ]: 274183 : Assert(!x.isConst() || !y.isConst());
[ - + ][ - + ]
[ - - ]
472 : : // first just check if they are disequal, which is sufficient for
473 : : // non-shared terms.
474 [ + + ]: 274183 : if (d_equalityEngine->areDisequal(x, y, false))
475 : : {
476 : 23877 : return true;
477 : : }
478 : : // if we aren't shared, we are not disequal
479 [ + + ][ - - ]: 250306 : if (!d_equalityEngine->isTriggerTerm(x, d_id)
480 [ + + ][ + + ]: 250306 : || !d_equalityEngine->isTriggerTerm(y, d_id))
[ + + ][ + - ]
[ - - ]
481 : : {
482 : 77080 : return false;
483 : : }
484 : : // otherwise use getEqualityStatus to ask the appropriate theory whether
485 : : // x and y are disequal.
486 : 173226 : TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id);
487 : 173226 : TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id);
488 : 173226 : EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
489 [ + - ][ + - ]: 173226 : if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE
490 [ + + ]: 173226 : || eqStatus == EQUALITY_FALSE_IN_MODEL)
491 : : {
492 : 162739 : return true;
493 : : }
494 : 10487 : return false;
495 : 173226 : }
496 : :
497 : 280857 : void Theory::getCareGraph(CareGraph* careGraph)
498 : : {
499 [ - + ][ - + ]: 280857 : Assert(careGraph != nullptr);
[ - - ]
500 : :
501 [ + - ]: 280857 : Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
502 : 280857 : TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
503 : 280857 : d_careGraph = careGraph;
504 : 280857 : computeCareGraph();
505 : 280857 : d_careGraph = nullptr;
506 : 280857 : }
507 : :
508 : 0 : bool Theory::proofsEnabled() const
509 : : {
510 : 0 : return d_env.getProofNodeManager() != nullptr;
511 : : }
512 : :
513 : 16442 : EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
514 : : {
515 : : // if not using an equality engine, then by default we don't know the status
516 [ + + ]: 16442 : if (d_equalityEngine == nullptr)
517 : : {
518 : 178 : return EQUALITY_UNKNOWN;
519 : : }
520 [ + - ]: 32528 : Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a
521 : 16264 : << ", " << b << ")" << std::endl;
522 : 16264 : Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
523 : :
524 : : // Check for equality (simplest)
525 [ + + ]: 16264 : if (d_equalityEngine->areEqual(a, b))
526 : : {
527 : : // The terms are implied to be equal
528 : 6771 : return EQUALITY_TRUE;
529 : : }
530 : :
531 : : // Check for disequality
532 [ + + ]: 9493 : if (d_equalityEngine->areDisequal(a, b, false))
533 : : {
534 : : // The terms are implied to be dis-equal
535 : 2577 : return EQUALITY_FALSE;
536 : : }
537 : :
538 : : // All other terms are unknown, which is conservative. A theory may override
539 : : // this method if it knows more information.
540 : 6916 : return EQUALITY_UNKNOWN;
541 : : }
542 : :
543 : 34167290 : void Theory::check(Effort level)
544 : : {
545 : : // see if we are already done (as an optimization)
546 [ + + ][ + + ]: 34167290 : if (d_checkEarlyExit && done() && level < EFFORT_FULL)
[ + + ][ + + ]
547 : : {
548 : 22472727 : return;
549 : : }
550 [ - + ][ - + ]: 11694563 : Assert(d_theoryState != nullptr);
[ - - ]
551 : : // standard calls for resource, stats
552 : 11694563 : d_out->spendResource(Resource::TheoryCheckStep);
553 : 11694563 : TimerStat::CodeTimer checkTimer(d_checkTime);
554 [ + - ]: 23389126 : Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
555 : 11694563 : << std::endl;
556 : : // pre-check at level
557 [ - + ]: 11694563 : if (preCheck(level))
558 : : {
559 : : // check aborted for a theory-specific reason
560 : 0 : return;
561 : : }
562 [ + - ]: 11694563 : Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
563 : : // process the pending fact queue
564 [ + + ][ + + ]: 44439376 : while (!done() && !d_theoryState->isInConflict())
[ + + ]
565 : : {
566 : : // Get the next assertion from the fact queue
567 : 32744816 : Assertion assertion = get();
568 : 32744816 : TNode fact = assertion.d_assertion;
569 [ + - ]: 65489632 : Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
570 : 32744816 : << std::endl;
571 : 32744816 : bool polarity = fact.getKind() != Kind::NOT;
572 [ + + ]: 32744816 : TNode atom = polarity ? fact : fact[0];
573 : : // call the pre-notify method
574 [ + + ]: 32744816 : if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
575 : : {
576 : : // handled in theory-specific way that doesn't involve equality engine
577 : 11499824 : continue;
578 : : }
579 [ + - ]: 42489984 : Trace("theory-check") << "Theory::assert " << fact << " " << d_id
580 : 21244992 : << std::endl;
581 : : // Theories that don't have an equality engine should always return true
582 : : // for preNotifyFact
583 [ - + ][ - + ]: 21244992 : Assert(d_equalityEngine != nullptr);
[ - - ]
584 : : // assert to the equality engine
585 [ + + ]: 21244992 : if (atom.getKind() == Kind::EQUAL)
586 : : {
587 : 14923674 : d_equalityEngine->assertEquality(atom, polarity, fact);
588 : : }
589 : : else
590 : : {
591 : 6321324 : d_equalityEngine->assertPredicate(atom, polarity, fact);
592 : : }
593 [ + - ]: 42489978 : Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
594 : 21244989 : << std::endl;
595 : : // notify the theory of the new fact, which is not internal
596 : 21244989 : notifyFact(atom, polarity, fact, false);
597 [ + + ][ + + ]: 55744470 : }
[ + + ]
598 [ + - ]: 11694560 : Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
599 : : // post-check at level
600 : 11694560 : postCheck(level);
601 [ + - ]: 11694559 : Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
602 [ + - ]: 11694563 : }
603 : :
604 : 4572824 : bool Theory::preCheck(CVC5_UNUSED Effort level) { return false; }
605 : :
606 : 1 : void Theory::postCheck(CVC5_UNUSED Effort level) {}
607 : :
608 : 10622089 : bool Theory::preNotifyFact(CVC5_UNUSED TNode atom,
609 : : CVC5_UNUSED bool polarity,
610 : : CVC5_UNUSED TNode fact,
611 : : CVC5_UNUSED bool isPrereg,
612 : : CVC5_UNUSED bool isInternal)
613 : : {
614 : 10622089 : return false;
615 : : }
616 : :
617 : 13401 : void Theory::notifyFact(CVC5_UNUSED TNode atom,
618 : : CVC5_UNUSED bool polarity,
619 : : CVC5_UNUSED TNode fact,
620 : : CVC5_UNUSED bool isInternal)
621 : : {
622 : 13401 : }
623 : :
624 : 70434 : void Theory::preRegisterTerm(CVC5_UNUSED TNode node) {}
625 : :
626 : 3736729 : void Theory::addSharedTerm(TNode n)
627 : : {
628 [ + - ]: 7473458 : Trace("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
629 : 3736729 : << std::endl;
630 [ + - ]: 7473458 : Trace("theory::assertions")
631 : 3736729 : << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
632 [ + + ]: 3736729 : if (d_theoryState != nullptr)
633 : : {
634 : 3725188 : d_theoryState->addSharedTerm(n);
635 : : }
636 : : // now call theory-specific method notifySharedTerm
637 : 3736730 : notifySharedTerm(n);
638 : : // if we have an equality engine, add the trigger term
639 [ + + ]: 3736728 : if (d_equalityEngine != nullptr)
640 : : {
641 : 3725187 : d_equalityEngine->addTriggerTerm(n, d_id);
642 : : }
643 : 3736728 : }
644 : :
645 : 621588 : eq::EqualityEngine* Theory::getEqualityEngine()
646 : : {
647 : : // get the assigned equality engine, which is a pointer stored in this class
648 : 621588 : return d_equalityEngine;
649 : : }
650 : :
651 : 22122 : bool Theory::expUsingCentralEqualityEngine(TheoryId id)
652 : : {
653 [ + + ][ + + ]: 22122 : return id != THEORY_ARITH && id != THEORY_ARRAYS;
654 : : }
655 : :
656 : 32744816 : theory::Assertion Theory::get()
657 : : {
658 [ - + ][ - + ]: 32744816 : Assert(!done()) << "Theory::get() called with assertion queue empty!";
[ - - ]
659 : :
660 : : // Get the assertion
661 : 32744816 : Assertion fact = d_facts[d_factsHead];
662 : 32744816 : d_factsHead = d_factsHead + 1;
663 : :
664 [ + - ]: 65489632 : Trace("theory") << "Theory::get() => " << fact << " ("
665 : 32744816 : << d_facts.size() - d_factsHead << " left)" << std::endl;
666 : :
667 : 32744816 : return fact;
668 : 0 : }
669 : :
670 : : } // namespace theory
671 : : } // namespace cvc5::internal
|
