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 : 401821 : Theory::Theory(TheoryId id,
55 : : Env& env,
56 : : OutputChannel& out,
57 : : Valuation valuation,
58 : 401821 : std::string name)
59 : : : EnvObj(env),
60 : 401821 : d_instanceName(name),
61 : 1205463 : d_checkTime(statisticsRegistry().registerTimer(getStatsPrefix(id) + name
62 : 803642 : + "checkTime")),
63 : 803642 : d_computeCareGraphTime(statisticsRegistry().registerTimer(
64 : 803642 : getStatsPrefix(id) + name + "computeCareGraphTime")),
65 : 401821 : d_out(&out),
66 : 401821 : d_valuation(valuation),
67 : 401821 : d_equalityEngine(nullptr),
68 : 401821 : d_allocEqualityEngine(nullptr),
69 : 401821 : d_theoryState(nullptr),
70 : 401821 : d_inferManager(nullptr),
71 : 401821 : d_quantEngine(nullptr),
72 [ + + ]: 401821 : d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
73 : : : nullptr),
74 : 401821 : d_checkEarlyExit(true),
75 : 401821 : d_id(id),
76 : 401821 : d_facts(d_env.getContext()),
77 : 401821 : d_factsHead(d_env.getContext(), 0),
78 : 401821 : d_careGraph(nullptr)
79 : : {
80 : 401821 : }
81 : :
82 : 401639 : Theory::~Theory() {}
83 : :
84 : 57400 : bool Theory::needsEqualityEngine(CVC5_UNUSED EeSetupInfo& esi)
85 : : {
86 : : // by default, this theory does not use an (official) equality engine
87 : 57400 : return false;
88 : : }
89 : :
90 : 401800 : void Theory::setEqualityEngine(eq::EqualityEngine* ee)
91 : : {
92 : : // set the equality engine pointer
93 : 401800 : d_equalityEngine = ee;
94 [ + + ]: 401800 : if (d_theoryState != nullptr)
95 : : {
96 : 373100 : d_theoryState->setEqualityEngine(ee);
97 : : }
98 [ + + ]: 401800 : if (d_inferManager != nullptr)
99 : : {
100 : 373100 : d_inferManager->setEqualityEngine(ee);
101 : : }
102 : 401800 : }
103 : :
104 : 401800 : void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
105 : : {
106 : : // quantifiers engine may be null if not in quantified logic
107 : 401800 : d_quantEngine = qe;
108 : 401800 : }
109 : :
110 : 401800 : void Theory::setDecisionManager(DecisionManager* dm)
111 : : {
112 [ - + ][ - + ]: 401800 : Assert(dm != nullptr);
[ - - ]
113 [ + + ]: 401800 : if (d_inferManager != nullptr)
114 : : {
115 : 373100 : d_inferManager->setDecisionManager(dm);
116 : : }
117 : 401800 : }
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 : 281298520 : TheoryId Theory::theoryOf(TNode node,
138 : : options::TheoryOfMode mode,
139 : : TheoryId usortOwner)
140 : : {
141 : 281298520 : TheoryId tid = THEORY_BUILTIN;
142 [ + + ][ - ]: 281298520 : switch (mode)
143 : : {
144 : 198635028 : case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
145 : : // Constants, variables, 0-ary constructors
146 [ + + ]: 198635028 : if (node.isVar())
147 : : {
148 : 11256700 : tid = theoryOf(node.getType(), usortOwner);
149 : : }
150 [ + + ]: 187378328 : else if (node.getKind() == Kind::EQUAL)
151 : : {
152 : : // Equality is owned by the theory that owns the domain
153 : 15902411 : 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 : 171475917 : tid = kindToTheoryId(node.getKind());
161 : : }
162 : 198635028 : break;
163 : 82663492 : case options::TheoryOfMode::THEORY_OF_TERM_BASED:
164 : : // Variables
165 [ + + ]: 82663492 : if (node.isVar())
166 : : {
167 [ + + ]: 11020916 : if (theoryOf(node.getType(), usortOwner) != theory::THEORY_BOOL)
168 : : {
169 : : // We treat the variables as uninterpreted
170 : 10853154 : tid = THEORY_UF;
171 : : }
172 : : else
173 : : {
174 : : // Other Boolean variables are Bool
175 : 167762 : tid = THEORY_BOOL;
176 : : }
177 : : }
178 [ + + ]: 71642576 : else if (node.getKind() == Kind::EQUAL)
179 : : { // Equality
180 : 11703496 : TNode l = node[0];
181 : 11703496 : TNode r = node[1];
182 : 11703496 : TypeNode ltype = l.getType();
183 : 11703496 : 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 [ + - ][ + + ]: 11703496 : if (ltype != rtype || ltype.isBoolean())
[ + + ]
188 : : {
189 : 17105 : tid = theoryOf(ltype, usortOwner);
190 : : }
191 : : else
192 : : {
193 : : // If both sides belong to the same theory the choice is easy
194 : 11686391 : TheoryId T1 = theoryOf(l, mode, usortOwner);
195 : 11686391 : TheoryId T2 = theoryOf(r, mode, usortOwner);
196 [ + + ]: 11686391 : if (T1 == T2)
197 : : {
198 : 7061303 : tid = T1;
199 : : }
200 : : else
201 : : {
202 : 4625088 : 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 [ + + ]: 4625088 : if (T1 == T3)
210 : : {
211 : 869988 : tid = T2;
212 : : }
213 [ + + ]: 3755100 : else if (T2 == T3)
214 : : {
215 : 3683017 : tid = T1;
216 : : }
217 : : else
218 : : {
219 : : // If both are parametric, we take the smaller one (arbitrary)
220 [ + + ]: 72083 : tid = T1 < T2 ? T1 : T2;
221 : : }
222 : : }
223 : : }
224 : 11703496 : }
225 : : else
226 : : {
227 : : // Regular nodes are owned by the kind, which includes constants as a
228 : : // special case.
229 : 59939080 : tid = kindToTheoryId(node.getKind());
230 : : }
231 : 82663492 : break;
232 : 0 : default: Unreachable();
233 : : }
234 : 281298520 : return tid;
235 : : }
236 : :
237 : 2317693 : void Theory::notifySharedTerm(CVC5_UNUSED TNode n)
238 : : {
239 : : // do nothing
240 : 2317693 : }
241 : :
242 : 5311754 : void Theory::notifyInConflict()
243 : : {
244 [ + + ]: 5311754 : if (d_inferManager != nullptr)
245 : : {
246 : 4932343 : d_inferManager->notifyInConflict();
247 : : }
248 : 5311754 : }
249 : :
250 : 33640 : void Theory::computeCareGraph()
251 : : {
252 [ - + ][ - + ]: 33640 : Assert(d_theoryState != nullptr);
[ - - ]
253 [ + - ]: 33640 : Trace("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
254 : 33640 : const context::CDList<TNode>& sharedTerms = d_theoryState->getSharedTerms();
255 : 33640 : size_t ssize = sharedTerms.size();
256 [ + + ]: 36589 : for (size_t i = 0; i < ssize; ++i)
257 : : {
258 : 2949 : TNode a = sharedTerms[i];
259 : 2949 : TypeNode aType = a.getType();
260 [ + + ]: 13112 : for (size_t j = i + 1; j < ssize; ++j)
261 : : {
262 : 10163 : TNode b = sharedTerms[j];
263 [ + + ]: 10163 : if (b.getType() != aType)
264 : : {
265 : : // We don't care about the terms of different types
266 : 2208 : continue;
267 : : }
268 [ + + ]: 7955 : switch (d_valuation.getEqualityStatus(a, b))
269 : : {
270 : 5774 : 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 : 5774 : break;
274 : 2181 : default:
275 : : // Let's split on it
276 : 2181 : addCarePair(a, b);
277 : 2181 : break;
278 : : }
279 [ + + ]: 10163 : }
280 : 2949 : }
281 : 33640 : }
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 : 158357 : 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 [ + + ][ + + ]: 158357 : if (d_equalityEngine != nullptr && !termSet.empty())
[ + + ]
304 : : {
305 [ + - ]: 121912 : Trace("model-builder") << "Assert Equality engine for " << d_id
306 : 60956 : << std::endl;
307 [ - + ]: 60956 : if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
308 : : {
309 : 0 : return false;
310 : : }
311 : : }
312 [ + - ]: 158357 : Trace("model-builder") << "Collect Model values for " << d_id << std::endl;
313 : : // now, collect theory-specific value assigments
314 : 158357 : return collectModelValues(m, termSet);
315 : : }
316 : :
317 : 228506 : void Theory::computeRelevantTerms(CVC5_UNUSED std::set<Node>& termSet)
318 : : {
319 : : // by default, there are no additional relevant terms
320 : 228506 : }
321 : :
322 : 431702 : 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 : 431702 : context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
328 : 431702 : assert_it_end = facts_end();
329 [ + + ]: 26530844 : for (; assert_it != assert_it_end; ++assert_it)
330 : : {
331 : 26099142 : collectTerms(*assert_it, termSet, irrKinds);
332 : : }
333 : :
334 [ + - ]: 431702 : if (includeShared)
335 : : {
336 [ - + ][ - + ]: 431702 : Assert(d_theoryState != nullptr);
[ - - ]
337 : : // Add terms that are shared terms
338 : : context::CDList<TNode>::const_iterator
339 : 431702 : shared_it = d_theoryState->shared_terms_begin(),
340 : 431702 : shared_it_end = d_theoryState->shared_terms_end();
341 [ + + ]: 8288956 : for (; shared_it != shared_it_end; ++shared_it)
342 : : {
343 : 7857254 : collectTerms(*shared_it, termSet, irrKinds);
344 : : }
345 : : }
346 : 431702 : }
347 : 325608 : 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 : 325608 : d_theoryState->getModel()->getIrrelevantKinds();
353 : 325608 : collectAssertedTerms(termSet, includeShared, irrKinds);
354 : 325608 : }
355 : :
356 : 33956396 : void Theory::collectTerms(TNode n,
357 : : std::set<Node>& termSet,
358 : : const std::set<Kind>& irrKinds) const
359 : : {
360 : 33956396 : std::vector<TNode> visit;
361 : 33956396 : TNode cur;
362 : 33956396 : visit.push_back(n);
363 : : do
364 : : {
365 : 117687034 : cur = visit.back();
366 : 117687034 : visit.pop_back();
367 [ + + ]: 117687034 : if (termSet.find(cur) != termSet.end())
368 : : {
369 : : // already visited
370 : 60727735 : continue;
371 : : }
372 : 56959299 : Kind k = cur.getKind();
373 : : // only add to term set if a relevant kind
374 [ + + ]: 56959299 : if (irrKinds.find(k) == irrKinds.end())
375 : : {
376 : 33405325 : termSet.insert(cur);
377 : : }
378 : : // traverse owned terms, don't go under quantifiers
379 [ + + ][ + + ]: 101726801 : if ((k == Kind::NOT || k == Kind::EQUAL || d_env.theoryOf(cur) == d_id)
[ + + ][ - - ]
380 [ + + ][ + + ]: 101726801 : && !cur.isClosure())
[ + + ]
381 : : {
382 : 51996045 : visit.insert(visit.end(), cur.begin(), cur.end());
383 : : }
384 [ + + ]: 117687034 : } while (!visit.empty());
385 : 33956396 : }
386 : :
387 : 11037 : bool Theory::collectModelValues(CVC5_UNUSED TheoryModel* m,
388 : : CVC5_UNUSED const std::set<Node>& termSet)
389 : : {
390 : 11037 : return true;
391 : : }
392 : :
393 : 83335 : bool Theory::ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions)
394 : : {
395 [ - + ][ - + ]: 83335 : Assert(tin.getKind() == TrustNodeKind::LEMMA);
[ - - ]
396 : 83335 : TNode in = tin.getNode();
397 [ + + ]: 83335 : 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 : 64422 : if (in[0].isVar() && d_valuation.isLegalElimination(in[0], in[1]))
404 : : {
405 : 33008 : outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
406 : 33008 : return true;
407 : : }
408 : 31414 : 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 : 49271 : return false;
416 : 83335 : }
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 : 114714 : void Theory::addCarePair(TNode t1, TNode t2)
424 : : {
425 [ - + ][ - + ]: 114714 : Assert(d_careGraph != nullptr);
[ - - ]
426 [ + - ]: 229428 : Trace("sharing") << "Theory::addCarePair: add pair " << d_id << " " << t1
427 : 114714 : << " " << t2 << std::endl;
428 : 114714 : d_careGraph->insert(CarePair(t1, t2, d_id));
429 : 114714 : }
430 : 486629 : void Theory::addCarePairArgs(TNode a, TNode b)
431 : : {
432 [ - + ][ - + ]: 486629 : Assert(d_careGraph != nullptr);
[ - - ]
433 [ - + ][ - + ]: 486629 : Assert(d_equalityEngine != nullptr);
[ - - ]
434 [ + - ][ + - ]: 486629 : Assert(a.hasOperator() && b.hasOperator());
[ - + ][ - + ]
[ - - ]
435 [ - + ][ - + ]: 486629 : Assert(a.getOperator() == b.getOperator());
[ - - ]
436 [ - + ][ - + ]: 486629 : Assert(a.getNumChildren() == b.getNumChildren());
[ - - ]
437 [ + - ]: 973258 : Trace("sharing") << "Theory::addCarePairArgs: checking function " << d_id
438 : 486629 : << " " << a << " " << b << std::endl;
439 [ + + ]: 1471389 : for (size_t k = 0, nchildren = a.getNumChildren(); k < nchildren; ++k)
440 : : {
441 : 984760 : TNode x = a[k];
442 : 984760 : TNode y = b[k];
443 [ + + ][ - - ]: 984760 : if (d_equalityEngine->isTriggerTerm(x, d_id)
444 [ + + ][ + - ]: 1636633 : && d_equalityEngine->isTriggerTerm(y, d_id)
[ - - ]
445 : 1636633 : && !d_equalityEngine->areEqual(x, y))
446 : : {
447 : 104006 : TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id);
448 : 104006 : TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id);
449 : 104006 : addCarePair(x_shared, y_shared);
450 : 104006 : }
451 : 984760 : }
452 : 486629 : }
453 : :
454 : 64538 : void Theory::processCarePairArgs(TNode a, TNode b)
455 : : {
456 : : // if a and b are already equal, we ignore this pair
457 [ + + ]: 64538 : if (d_theoryState->areEqual(a, b))
458 : : {
459 : 1439 : return;
460 : : }
461 : : // otherwise, we add pairs for each of their arguments
462 : 63099 : addCarePairArgs(a, b);
463 : : }
464 : :
465 : 273687 : bool Theory::areCareDisequal(TNode x, TNode y)
466 : : {
467 [ - + ][ - + ]: 273687 : Assert(d_equalityEngine != nullptr);
[ - - ]
468 [ - + ][ - + ]: 273687 : Assert(d_equalityEngine->hasTerm(x));
[ - - ]
469 [ - + ][ - + ]: 273687 : Assert(d_equalityEngine->hasTerm(y));
[ - - ]
470 [ - + ][ - + ]: 273687 : Assert(x != y);
[ - - ]
471 [ + + ][ + - ]: 273687 : Assert(!x.isConst() || !y.isConst());
[ - + ][ - + ]
[ - - ]
472 : : // first just check if they are disequal, which is sufficient for
473 : : // non-shared terms.
474 [ + + ]: 273687 : if (d_equalityEngine->areDisequal(x, y, false))
475 : : {
476 : 23451 : return true;
477 : : }
478 : : // if we aren't shared, we are not disequal
479 [ + + ][ - - ]: 250236 : if (!d_equalityEngine->isTriggerTerm(x, d_id)
480 [ + + ][ + + ]: 250236 : || !d_equalityEngine->isTriggerTerm(y, d_id))
[ + + ][ + - ]
[ - - ]
481 : : {
482 : 77708 : return false;
483 : : }
484 : : // otherwise use getEqualityStatus to ask the appropriate theory whether
485 : : // x and y are disequal.
486 : 172528 : TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id);
487 : 172528 : TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id);
488 : 172528 : EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
489 [ + - ][ + - ]: 172528 : if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE
490 [ + + ]: 172528 : || eqStatus == EQUALITY_FALSE_IN_MODEL)
491 : : {
492 : 162073 : return true;
493 : : }
494 : 10455 : return false;
495 : 172528 : }
496 : :
497 : 190224 : void Theory::getCareGraph(CareGraph* careGraph)
498 : : {
499 [ - + ][ - + ]: 190224 : Assert(careGraph != nullptr);
[ - - ]
500 : :
501 [ + - ]: 190224 : Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
502 : 190224 : TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
503 : 190224 : d_careGraph = careGraph;
504 : 190224 : computeCareGraph();
505 : 190224 : d_careGraph = nullptr;
506 : 190224 : }
507 : :
508 : 0 : bool Theory::proofsEnabled() const
509 : : {
510 : 0 : return d_env.getProofNodeManager() != nullptr;
511 : : }
512 : :
513 : 16448 : 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 [ + + ]: 16448 : if (d_equalityEngine == nullptr)
517 : : {
518 : 178 : return EQUALITY_UNKNOWN;
519 : : }
520 [ + - ]: 32540 : Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a
521 : 16270 : << ", " << b << ")" << std::endl;
522 : 16270 : Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
523 : :
524 : : // Check for equality (simplest)
525 [ + + ]: 16270 : if (d_equalityEngine->areEqual(a, b))
526 : : {
527 : : // The terms are implied to be equal
528 : 6772 : return EQUALITY_TRUE;
529 : : }
530 : :
531 : : // Check for disequality
532 [ + + ]: 9498 : if (d_equalityEngine->areDisequal(a, b, false))
533 : : {
534 : : // The terms are implied to be dis-equal
535 : 2578 : 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 : 6920 : return EQUALITY_UNKNOWN;
541 : : }
542 : :
543 : 39095429 : void Theory::check(Effort level)
544 : : {
545 : : // see if we are already done (as an optimization)
546 [ + + ][ + + ]: 39095429 : if (d_checkEarlyExit && done() && level < EFFORT_FULL)
[ + + ][ + + ]
547 : : {
548 : 26952264 : return;
549 : : }
550 [ - + ][ - + ]: 12143165 : Assert(d_theoryState != nullptr);
[ - - ]
551 : : // standard calls for resource, stats
552 : 12143165 : d_out->spendResource(Resource::TheoryCheckStep);
553 : 12143165 : TimerStat::CodeTimer checkTimer(d_checkTime);
554 [ + - ]: 24286330 : Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
555 : 12143165 : << std::endl;
556 : : // pre-check at level
557 [ - + ]: 12143165 : if (preCheck(level))
558 : : {
559 : : // check aborted for a theory-specific reason
560 : 0 : return;
561 : : }
562 [ + - ]: 12143165 : Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
563 : : // process the pending fact queue
564 [ + + ][ + + ]: 46889114 : while (!done() && !d_theoryState->isInConflict())
[ + + ]
565 : : {
566 : : // Get the next assertion from the fact queue
567 : 34745952 : Assertion assertion = get();
568 : 34745952 : TNode fact = assertion.d_assertion;
569 [ + - ]: 69491904 : Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
570 : 34745952 : << std::endl;
571 : 34745952 : bool polarity = fact.getKind() != Kind::NOT;
572 [ + + ]: 34745952 : TNode atom = polarity ? fact : fact[0];
573 : : // call the pre-notify method
574 [ + + ]: 34745952 : if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
575 : : {
576 : : // handled in theory-specific way that doesn't involve equality engine
577 : 11895404 : continue;
578 : : }
579 [ + - ]: 45701096 : Trace("theory-check") << "Theory::assert " << fact << " " << d_id
580 : 22850548 : << std::endl;
581 : : // Theories that don't have an equality engine should always return true
582 : : // for preNotifyFact
583 [ - + ][ - + ]: 22850548 : Assert(d_equalityEngine != nullptr);
[ - - ]
584 : : // assert to the equality engine
585 [ + + ]: 22850548 : if (atom.getKind() == Kind::EQUAL)
586 : : {
587 : 15288219 : d_equalityEngine->assertEquality(atom, polarity, fact);
588 : : }
589 : : else
590 : : {
591 : 7562335 : d_equalityEngine->assertPredicate(atom, polarity, fact);
592 : : }
593 [ + - ]: 45701090 : Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
594 : 22850545 : << std::endl;
595 : : // notify the theory of the new fact, which is not internal
596 : 22850545 : notifyFact(atom, polarity, fact, false);
597 [ + + ][ + + ]: 58536766 : }
[ + + ]
598 [ + - ]: 12143162 : Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
599 : : // post-check at level
600 : 12143162 : postCheck(level);
601 [ + - ]: 12143161 : Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
602 [ + - ]: 12143165 : }
603 : :
604 : 4521790 : bool Theory::preCheck(CVC5_UNUSED Effort level) { return false; }
605 : :
606 : 1 : void Theory::postCheck(CVC5_UNUSED Effort level) {}
607 : :
608 : 12264863 : 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 : 12264863 : return false;
615 : : }
616 : :
617 : 13721 : void Theory::notifyFact(CVC5_UNUSED TNode atom,
618 : : CVC5_UNUSED bool polarity,
619 : : CVC5_UNUSED TNode fact,
620 : : CVC5_UNUSED bool isInternal)
621 : : {
622 : 13721 : }
623 : :
624 : 48671 : void Theory::preRegisterTerm(CVC5_UNUSED TNode node) {}
625 : :
626 : 3921405 : void Theory::addSharedTerm(TNode n)
627 : : {
628 [ + - ]: 7842810 : Trace("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
629 : 3921405 : << std::endl;
630 [ + - ]: 7842810 : Trace("theory::assertions")
631 : 3921405 : << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
632 [ + + ]: 3921405 : if (d_theoryState != nullptr)
633 : : {
634 : 3900122 : d_theoryState->addSharedTerm(n);
635 : : }
636 : : // now call theory-specific method notifySharedTerm
637 : 3921406 : notifySharedTerm(n);
638 : : // if we have an equality engine, add the trigger term
639 [ + + ]: 3921404 : if (d_equalityEngine != nullptr)
640 : : {
641 : 3900121 : d_equalityEngine->addTriggerTerm(n, d_id);
642 : : }
643 : 3921404 : }
644 : :
645 : 564264 : eq::EqualityEngine* Theory::getEqualityEngine()
646 : : {
647 : : // get the assigned equality engine, which is a pointer stored in this class
648 : 564264 : return d_equalityEngine;
649 : : }
650 : :
651 : 22602 : bool Theory::expUsingCentralEqualityEngine(TheoryId id)
652 : : {
653 [ + + ][ + + ]: 22602 : return id != THEORY_ARITH && id != THEORY_ARRAYS;
654 : : }
655 : :
656 : 34745952 : theory::Assertion Theory::get()
657 : : {
658 [ - + ][ - + ]: 34745952 : Assert(!done()) << "Theory::get() called with assertion queue empty!";
[ - - ]
659 : :
660 : : // Get the assertion
661 : 34745952 : Assertion fact = d_facts[d_factsHead];
662 : 34745952 : d_factsHead = d_factsHead + 1;
663 : :
664 [ + - ]: 69491904 : Trace("theory") << "Theory::get() => " << fact << " ("
665 : 34745952 : << d_facts.size() - d_factsHead << " left)" << std::endl;
666 : :
667 : 34745952 : return fact;
668 : 0 : }
669 : :
670 : : } // namespace theory
671 : : } // namespace cvc5::internal
|
