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