1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King, Dejan Jovanovic |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* Base for theory interface. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/theory.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
#include <sstream> |
20 |
|
#include <string> |
21 |
|
#include <vector> |
22 |
|
|
23 |
|
#include "base/check.h" |
24 |
|
#include "expr/node_algorithm.h" |
25 |
|
#include "options/smt_options.h" |
26 |
|
#include "options/theory_options.h" |
27 |
|
#include "smt/smt_statistics_registry.h" |
28 |
|
#include "theory/ee_setup_info.h" |
29 |
|
#include "theory/ext_theory.h" |
30 |
|
#include "theory/output_channel.h" |
31 |
|
#include "theory/quantifiers_engine.h" |
32 |
|
#include "theory/substitutions.h" |
33 |
|
#include "theory/theory_inference_manager.h" |
34 |
|
#include "theory/theory_model.h" |
35 |
|
#include "theory/theory_rewriter.h" |
36 |
|
#include "theory/theory_state.h" |
37 |
|
#include "theory/trust_substitutions.h" |
38 |
|
|
39 |
|
using namespace std; |
40 |
|
|
41 |
|
namespace cvc5 { |
42 |
|
namespace theory { |
43 |
|
|
44 |
|
/** Default value for the uninterpreted sorts is the UF theory */ |
45 |
|
TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; |
46 |
|
|
47 |
|
std::ostream& operator<<(std::ostream& os, Theory::Effort level){ |
48 |
|
switch(level){ |
49 |
|
case Theory::EFFORT_STANDARD: |
50 |
|
os << "EFFORT_STANDARD"; break; |
51 |
|
case Theory::EFFORT_FULL: |
52 |
|
os << "EFFORT_FULL"; break; |
53 |
|
case Theory::EFFORT_LAST_CALL: |
54 |
|
os << "EFFORT_LAST_CALL"; break; |
55 |
|
default: |
56 |
|
Unreachable(); |
57 |
|
} |
58 |
|
return os; |
59 |
|
}/* ostream& operator<<(ostream&, Theory::Effort) */ |
60 |
|
|
61 |
123022 |
Theory::Theory(TheoryId id, |
62 |
|
context::Context* satContext, |
63 |
|
context::UserContext* userContext, |
64 |
|
OutputChannel& out, |
65 |
|
Valuation valuation, |
66 |
|
const LogicInfo& logicInfo, |
67 |
|
ProofNodeManager* pnm, |
68 |
123022 |
std::string name) |
69 |
|
: d_id(id), |
70 |
|
d_satContext(satContext), |
71 |
|
d_userContext(userContext), |
72 |
|
d_logicInfo(logicInfo), |
73 |
|
d_facts(satContext), |
74 |
|
d_factsHead(satContext, 0), |
75 |
|
d_sharedTermsIndex(satContext, 0), |
76 |
|
d_careGraph(nullptr), |
77 |
|
d_instanceName(name), |
78 |
246044 |
d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) |
79 |
246044 |
+ name + "checkTime")), |
80 |
123022 |
d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( |
81 |
246044 |
getStatsPrefix(id) + name + "computeCareGraphTime")), |
82 |
|
d_sharedTerms(satContext), |
83 |
|
d_out(&out), |
84 |
|
d_valuation(valuation), |
85 |
|
d_equalityEngine(nullptr), |
86 |
|
d_allocEqualityEngine(nullptr), |
87 |
|
d_theoryState(nullptr), |
88 |
|
d_inferManager(nullptr), |
89 |
|
d_quantEngine(nullptr), |
90 |
492088 |
d_pnm(pnm) |
91 |
|
{ |
92 |
123022 |
} |
93 |
|
|
94 |
123022 |
Theory::~Theory() { |
95 |
123022 |
} |
96 |
|
|
97 |
18920 |
bool Theory::needsEqualityEngine(EeSetupInfo& esi) |
98 |
|
{ |
99 |
|
// by default, this theory does not use an (official) equality engine |
100 |
18920 |
return false; |
101 |
|
} |
102 |
|
|
103 |
122980 |
void Theory::setEqualityEngine(eq::EqualityEngine* ee) |
104 |
|
{ |
105 |
|
// set the equality engine pointer |
106 |
122980 |
d_equalityEngine = ee; |
107 |
122980 |
if (d_theoryState != nullptr) |
108 |
|
{ |
109 |
104060 |
d_theoryState->setEqualityEngine(ee); |
110 |
|
} |
111 |
122980 |
if (d_inferManager != nullptr) |
112 |
|
{ |
113 |
104060 |
d_inferManager->setEqualityEngine(ee); |
114 |
|
} |
115 |
122980 |
} |
116 |
|
|
117 |
122980 |
void Theory::setQuantifiersEngine(QuantifiersEngine* qe) |
118 |
|
{ |
119 |
|
// quantifiers engine may be null if not in quantified logic |
120 |
122980 |
d_quantEngine = qe; |
121 |
122980 |
} |
122 |
|
|
123 |
122980 |
void Theory::setDecisionManager(DecisionManager* dm) |
124 |
|
{ |
125 |
122980 |
Assert(dm != nullptr); |
126 |
122980 |
if (d_inferManager != nullptr) |
127 |
|
{ |
128 |
104060 |
d_inferManager->setDecisionManager(dm); |
129 |
|
} |
130 |
122980 |
} |
131 |
|
|
132 |
|
void Theory::finishInitStandalone() |
133 |
|
{ |
134 |
|
EeSetupInfo esi; |
135 |
|
if (needsEqualityEngine(esi)) |
136 |
|
{ |
137 |
|
// always associated with the same SAT context as the theory (d_satContext) |
138 |
|
d_allocEqualityEngine.reset(new eq::EqualityEngine( |
139 |
|
*esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers)); |
140 |
|
// use it as the official equality engine |
141 |
|
setEqualityEngine(d_allocEqualityEngine.get()); |
142 |
|
} |
143 |
|
finishInit(); |
144 |
|
} |
145 |
|
|
146 |
160164906 |
TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) |
147 |
|
{ |
148 |
160164906 |
TheoryId tid = THEORY_BUILTIN; |
149 |
160164906 |
switch(mode) { |
150 |
104170135 |
case options::TheoryOfMode::THEORY_OF_TYPE_BASED: |
151 |
|
// Constants, variables, 0-ary constructors |
152 |
104170135 |
if (node.isVar()) |
153 |
|
{ |
154 |
4398786 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
155 |
|
{ |
156 |
221226 |
tid = THEORY_UF; |
157 |
|
} |
158 |
|
else |
159 |
|
{ |
160 |
4177560 |
tid = Theory::theoryOf(node.getType()); |
161 |
|
} |
162 |
|
} |
163 |
99771349 |
else if (node.getKind() == kind::EQUAL) |
164 |
|
{ |
165 |
|
// Equality is owned by the theory that owns the domain |
166 |
5985707 |
tid = Theory::theoryOf(node[0].getType()); |
167 |
|
} |
168 |
|
else |
169 |
|
{ |
170 |
|
// Regular nodes are owned by the kind. Notice that constants are a |
171 |
|
// special case here, where the theory of the kind of a constant |
172 |
|
// always coincides with the type of that constant. |
173 |
93785642 |
tid = kindToTheoryId(node.getKind()); |
174 |
|
} |
175 |
104170135 |
break; |
176 |
55994771 |
case options::TheoryOfMode::THEORY_OF_TERM_BASED: |
177 |
|
// Variables |
178 |
55994771 |
if (node.isVar()) |
179 |
|
{ |
180 |
5107066 |
if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) |
181 |
|
{ |
182 |
|
// We treat the variables as uninterpreted |
183 |
5100837 |
tid = s_uninterpretedSortOwner; |
184 |
|
} |
185 |
|
else |
186 |
|
{ |
187 |
6229 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
188 |
|
{ |
189 |
|
// Boolean vars go to UF |
190 |
3178 |
tid = THEORY_UF; |
191 |
|
} |
192 |
|
else |
193 |
|
{ |
194 |
|
// Except for the Boolean ones |
195 |
3051 |
tid = THEORY_BOOL; |
196 |
|
} |
197 |
|
} |
198 |
|
} |
199 |
50887705 |
else if (node.getKind() == kind::EQUAL) |
200 |
|
{ // Equality |
201 |
|
// If one of them is an ITE, it's irelevant, since they will get |
202 |
|
// replaced out anyhow |
203 |
4777380 |
if (node[0].getKind() == kind::ITE) |
204 |
|
{ |
205 |
5122 |
tid = Theory::theoryOf(node[0].getType()); |
206 |
|
} |
207 |
4772258 |
else if (node[1].getKind() == kind::ITE) |
208 |
|
{ |
209 |
9539 |
tid = Theory::theoryOf(node[1].getType()); |
210 |
|
} |
211 |
|
else |
212 |
|
{ |
213 |
9525438 |
TNode l = node[0]; |
214 |
9525438 |
TNode r = node[1]; |
215 |
9525438 |
TypeNode ltype = l.getType(); |
216 |
9525438 |
TypeNode rtype = r.getType(); |
217 |
|
// If the types are different, we must assign based on type due |
218 |
|
// to handling subtypes (limited to arithmetic). Also, if we are |
219 |
|
// a Boolean equality, we must assign THEORY_BOOL. |
220 |
4762719 |
if (ltype != rtype || ltype.isBoolean()) |
221 |
|
{ |
222 |
58031 |
tid = Theory::theoryOf(ltype); |
223 |
|
} |
224 |
|
else |
225 |
|
{ |
226 |
|
// If both sides belong to the same theory the choice is easy |
227 |
4704688 |
TheoryId T1 = Theory::theoryOf(l); |
228 |
4704688 |
TheoryId T2 = Theory::theoryOf(r); |
229 |
4704688 |
if (T1 == T2) |
230 |
|
{ |
231 |
2702922 |
tid = T1; |
232 |
|
} |
233 |
|
else |
234 |
|
{ |
235 |
2001766 |
TheoryId T3 = Theory::theoryOf(ltype); |
236 |
|
// This is a case of |
237 |
|
// * x*y = f(z) -> UF |
238 |
|
// * x = c -> UF |
239 |
|
// * f(x) = read(a, y) -> either UF or ARRAY |
240 |
|
// at least one of the theories has to be parametric, i.e. theory |
241 |
|
// of the type is different from the theory of the term |
242 |
2001766 |
if (T1 == T3) |
243 |
|
{ |
244 |
50600 |
tid = T2; |
245 |
|
} |
246 |
1951166 |
else if (T2 == T3) |
247 |
|
{ |
248 |
1897243 |
tid = T1; |
249 |
|
} |
250 |
|
else |
251 |
|
{ |
252 |
|
// If both are parametric, we take the smaller one (arbitrary) |
253 |
53923 |
tid = T1 < T2 ? T1 : T2; |
254 |
|
} |
255 |
|
} |
256 |
|
} |
257 |
|
} |
258 |
|
} |
259 |
|
else |
260 |
|
{ |
261 |
|
// Regular nodes are owned by the kind, which includes constants as a |
262 |
|
// special case. |
263 |
46110325 |
tid = kindToTheoryId(node.getKind()); |
264 |
|
} |
265 |
55994771 |
break; |
266 |
|
default: |
267 |
|
Unreachable(); |
268 |
|
} |
269 |
160164906 |
Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl; |
270 |
160164906 |
return tid; |
271 |
|
} |
272 |
|
|
273 |
997589 |
void Theory::notifySharedTerm(TNode n) |
274 |
|
{ |
275 |
|
// do nothing |
276 |
997589 |
} |
277 |
|
|
278 |
5967 |
void Theory::computeCareGraph() { |
279 |
5967 |
Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl; |
280 |
6463 |
for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { |
281 |
992 |
TNode a = d_sharedTerms[i]; |
282 |
992 |
TypeNode aType = a.getType(); |
283 |
4822 |
for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) { |
284 |
8196 |
TNode b = d_sharedTerms[j]; |
285 |
4326 |
if (b.getType() != aType) { |
286 |
|
// We don't care about the terms of different types |
287 |
456 |
continue; |
288 |
|
} |
289 |
3870 |
switch (d_valuation.getEqualityStatus(a, b)) { |
290 |
3244 |
case EQUALITY_TRUE_AND_PROPAGATED: |
291 |
|
case EQUALITY_FALSE_AND_PROPAGATED: |
292 |
|
// If we know about it, we should have propagated it, so we can skip |
293 |
3244 |
break; |
294 |
626 |
default: |
295 |
|
// Let's split on it |
296 |
626 |
addCarePair(a, b); |
297 |
626 |
break; |
298 |
|
} |
299 |
|
} |
300 |
|
} |
301 |
5967 |
} |
302 |
|
|
303 |
|
void Theory::printFacts(std::ostream& os) const { |
304 |
|
unsigned i, n = d_facts.size(); |
305 |
|
for(i = 0; i < n; i++){ |
306 |
|
const Assertion& a_i = d_facts[i]; |
307 |
|
Node assertion = a_i; |
308 |
|
os << d_id << '[' << i << ']' << " " << assertion << endl; |
309 |
|
} |
310 |
|
} |
311 |
|
|
312 |
|
void Theory::debugPrintFacts() const{ |
313 |
|
DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl; |
314 |
|
printFacts(DebugChannel.getStream()); |
315 |
|
} |
316 |
|
|
317 |
17937 |
bool Theory::isLegalElimination(TNode x, TNode val) |
318 |
|
{ |
319 |
17937 |
Assert(x.isVar()); |
320 |
35874 |
if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE |
321 |
17937 |
|| val.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
322 |
|
{ |
323 |
|
return false; |
324 |
|
} |
325 |
17937 |
if (expr::hasSubterm(val, x)) |
326 |
|
{ |
327 |
4748 |
return false; |
328 |
|
} |
329 |
13189 |
if (!val.getType().isSubtypeOf(x.getType())) |
330 |
|
{ |
331 |
|
return false; |
332 |
|
} |
333 |
13189 |
if (!options::produceModels()) |
334 |
|
{ |
335 |
|
// don't care about the model, we are fine |
336 |
10238 |
return true; |
337 |
|
} |
338 |
|
// if there is a model object |
339 |
2951 |
TheoryModel* tm = d_valuation.getModel(); |
340 |
2951 |
Assert(tm != nullptr); |
341 |
2951 |
return tm->isLegalElimination(x, val); |
342 |
|
} |
343 |
|
|
344 |
13433 |
std::unordered_set<TNode> Theory::currentlySharedTerms() const |
345 |
|
{ |
346 |
13433 |
std::unordered_set<TNode> currentlyShared; |
347 |
265177 |
for (shared_terms_iterator i = shared_terms_begin(), |
348 |
13433 |
i_end = shared_terms_end(); i != i_end; ++i) { |
349 |
251744 |
currentlyShared.insert (*i); |
350 |
|
} |
351 |
13433 |
return currentlyShared; |
352 |
|
} |
353 |
|
|
354 |
94448 |
bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) |
355 |
|
{ |
356 |
|
// if we are using an equality engine, assert it to the model |
357 |
94448 |
if (d_equalityEngine != nullptr) |
358 |
|
{ |
359 |
63927 |
if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) |
360 |
|
{ |
361 |
|
return false; |
362 |
|
} |
363 |
|
} |
364 |
|
// now, collect theory-specific value assigments |
365 |
94448 |
return collectModelValues(m, termSet); |
366 |
|
} |
367 |
|
|
368 |
98635 |
void Theory::computeRelevantTerms(std::set<Node>& termSet) |
369 |
|
{ |
370 |
|
// by default, there are no additional relevant terms |
371 |
98635 |
} |
372 |
|
|
373 |
34982 |
bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) |
374 |
|
{ |
375 |
34982 |
return true; |
376 |
|
} |
377 |
|
|
378 |
46349 |
Theory::PPAssertStatus Theory::ppAssert(TrustNode tin, |
379 |
|
TrustSubstitutionMap& outSubstitutions) |
380 |
|
{ |
381 |
92698 |
TNode in = tin.getNode(); |
382 |
46349 |
if (in.getKind() == kind::EQUAL) |
383 |
|
{ |
384 |
|
// (and (= x t) phi) can be replaced by phi[x/t] if |
385 |
|
// 1) x is a variable |
386 |
|
// 2) x is not in the term t |
387 |
|
// 3) x : T and t : S, then S <: T |
388 |
78165 |
if (in[0].isVar() && isLegalElimination(in[0], in[1]) |
389 |
73611 |
&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
390 |
|
{ |
391 |
10428 |
outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); |
392 |
10428 |
return PP_ASSERT_STATUS_SOLVED; |
393 |
|
} |
394 |
32206 |
if (in[1].isVar() && isLegalElimination(in[1], in[0]) |
395 |
32205 |
&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
396 |
|
{ |
397 |
306 |
outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); |
398 |
306 |
return PP_ASSERT_STATUS_SOLVED; |
399 |
|
} |
400 |
10327 |
if (in[0].isConst() && in[1].isConst()) |
401 |
|
{ |
402 |
|
if (in[0] != in[1]) |
403 |
|
{ |
404 |
|
return PP_ASSERT_STATUS_CONFLICT; |
405 |
|
} |
406 |
|
} |
407 |
|
} |
408 |
74044 |
else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL |
409 |
73629 |
&& in[0][0].getType().isBoolean()) |
410 |
|
{ |
411 |
37 |
TNode eq = in[0]; |
412 |
35 |
if (eq[0].isVar()) |
413 |
|
{ |
414 |
44 |
Node res = eq[0].eqNode(eq[1].notNode()); |
415 |
44 |
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
416 |
22 |
return ppAssert(tn, outSubstitutions); |
417 |
|
} |
418 |
13 |
else if (eq[1].isVar()) |
419 |
|
{ |
420 |
22 |
Node res = eq[1].eqNode(eq[0].notNode()); |
421 |
22 |
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
422 |
11 |
return ppAssert(tn, outSubstitutions); |
423 |
|
} |
424 |
|
} |
425 |
|
|
426 |
35582 |
return PP_ASSERT_STATUS_UNSOLVED; |
427 |
|
} |
428 |
|
|
429 |
|
std::pair<bool, Node> Theory::entailmentCheck(TNode lit) |
430 |
|
{ |
431 |
|
return make_pair(false, Node::null()); |
432 |
|
} |
433 |
|
|
434 |
43381 |
void Theory::addCarePair(TNode t1, TNode t2) { |
435 |
43381 |
if (d_careGraph) { |
436 |
43381 |
d_careGraph->insert(CarePair(t1, t2, d_id)); |
437 |
|
} |
438 |
43381 |
} |
439 |
|
|
440 |
63099 |
void Theory::getCareGraph(CareGraph* careGraph) { |
441 |
63099 |
Assert(careGraph != NULL); |
442 |
|
|
443 |
63099 |
Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; |
444 |
126198 |
TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); |
445 |
63099 |
d_careGraph = careGraph; |
446 |
63099 |
computeCareGraph(); |
447 |
63099 |
d_careGraph = NULL; |
448 |
63099 |
} |
449 |
|
|
450 |
18279 |
bool Theory::proofsEnabled() const |
451 |
|
{ |
452 |
18279 |
return d_pnm != nullptr; |
453 |
|
} |
454 |
|
|
455 |
15794 |
EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) |
456 |
|
{ |
457 |
|
// if not using an equality engine, then by default we don't know the status |
458 |
15794 |
if (d_equalityEngine == nullptr) |
459 |
|
{ |
460 |
4520 |
return EQUALITY_UNKNOWN; |
461 |
|
} |
462 |
11274 |
Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl; |
463 |
11274 |
Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); |
464 |
|
|
465 |
|
// Check for equality (simplest) |
466 |
11274 |
if (d_equalityEngine->areEqual(a, b)) |
467 |
|
{ |
468 |
|
// The terms are implied to be equal |
469 |
4614 |
return EQUALITY_TRUE; |
470 |
|
} |
471 |
|
|
472 |
|
// Check for disequality |
473 |
6660 |
if (d_equalityEngine->areDisequal(a, b, false)) |
474 |
|
{ |
475 |
|
// The terms are implied to be dis-equal |
476 |
2561 |
return EQUALITY_FALSE; |
477 |
|
} |
478 |
|
|
479 |
|
// All other terms are unknown, which is conservative. A theory may override |
480 |
|
// this method if it knows more information. |
481 |
4099 |
return EQUALITY_UNKNOWN; |
482 |
|
} |
483 |
|
|
484 |
11639761 |
void Theory::check(Effort level) |
485 |
|
{ |
486 |
|
// see if we are already done (as an optimization) |
487 |
11639761 |
if (done() && level < EFFORT_FULL) |
488 |
|
{ |
489 |
15915947 |
return; |
490 |
|
} |
491 |
3801016 |
Assert(d_theoryState!=nullptr); |
492 |
|
// standard calls for resource, stats |
493 |
3801016 |
d_out->spendResource(Resource::TheoryCheckStep); |
494 |
7363575 |
TimerStat::CodeTimer checkTimer(d_checkTime); |
495 |
7602032 |
Trace("theory-check") << "Theory::preCheck " << level << " " << d_id |
496 |
3801016 |
<< std::endl; |
497 |
|
// pre-check at level |
498 |
3801016 |
if (preCheck(level)) |
499 |
|
{ |
500 |
|
// check aborted for a theory-specific reason |
501 |
238457 |
return; |
502 |
|
} |
503 |
3562559 |
Assert(d_theoryState != nullptr); |
504 |
3562559 |
Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl; |
505 |
|
// process the pending fact queue |
506 |
25539807 |
while (!done() && !d_theoryState->isInConflict()) |
507 |
|
{ |
508 |
|
// Get the next assertion from the fact queue |
509 |
16695578 |
Assertion assertion = get(); |
510 |
16695578 |
TNode fact = assertion.d_assertion; |
511 |
21977254 |
Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id |
512 |
10988627 |
<< std::endl; |
513 |
10988627 |
bool polarity = fact.getKind() != kind::NOT; |
514 |
16695578 |
TNode atom = polarity ? fact : fact[0]; |
515 |
|
// call the pre-notify method |
516 |
10988627 |
if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false)) |
517 |
|
{ |
518 |
|
// handled in theory-specific way that doesn't involve equality engine |
519 |
5281676 |
continue; |
520 |
|
} |
521 |
11413902 |
Trace("theory-check") << "Theory::assert " << fact << " " << d_id |
522 |
5706951 |
<< std::endl; |
523 |
|
// Theories that don't have an equality engine should always return true |
524 |
|
// for preNotifyFact |
525 |
5706951 |
Assert(d_equalityEngine != nullptr); |
526 |
|
// assert to the equality engine |
527 |
5706951 |
if (atom.getKind() == kind::EQUAL) |
528 |
|
{ |
529 |
4527274 |
d_equalityEngine->assertEquality(atom, polarity, fact); |
530 |
|
} |
531 |
|
else |
532 |
|
{ |
533 |
1179680 |
d_equalityEngine->assertPredicate(atom, polarity, fact); |
534 |
|
} |
535 |
11413896 |
Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id |
536 |
5706948 |
<< std::endl; |
537 |
|
// notify the theory of the new fact, which is not internal |
538 |
5706948 |
notifyFact(atom, polarity, fact, false); |
539 |
|
} |
540 |
3562556 |
Trace("theory-check") << "Theory::postCheck " << d_id << std::endl; |
541 |
|
// post-check at level |
542 |
3562556 |
postCheck(level); |
543 |
3562555 |
Trace("theory-check") << "Theory::finish check " << d_id << std::endl; |
544 |
|
} |
545 |
|
|
546 |
1683741 |
bool Theory::preCheck(Effort level) { return false; } |
547 |
|
|
548 |
2 |
void Theory::postCheck(Effort level) {} |
549 |
|
|
550 |
2184511 |
bool Theory::preNotifyFact( |
551 |
|
TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) |
552 |
|
{ |
553 |
2184511 |
return false; |
554 |
|
} |
555 |
|
|
556 |
1104 |
void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal) |
557 |
|
{ |
558 |
1104 |
} |
559 |
|
|
560 |
21406 |
void Theory::preRegisterTerm(TNode node) {} |
561 |
|
|
562 |
1693044 |
void Theory::addSharedTerm(TNode n) |
563 |
|
{ |
564 |
3386088 |
Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" |
565 |
1693044 |
<< std::endl; |
566 |
3386088 |
Debug("theory::assertions") |
567 |
1693044 |
<< "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; |
568 |
1693044 |
d_sharedTerms.push_back(n); |
569 |
|
// now call theory-specific method notifySharedTerm |
570 |
1693044 |
notifySharedTerm(n); |
571 |
|
// if we have an equality engine, add the trigger term |
572 |
1693044 |
if (d_equalityEngine != nullptr) |
573 |
|
{ |
574 |
1687315 |
d_equalityEngine->addTriggerTerm(n, d_id); |
575 |
|
} |
576 |
1693044 |
} |
577 |
|
|
578 |
288783 |
eq::EqualityEngine* Theory::getEqualityEngine() |
579 |
|
{ |
580 |
|
// get the assigned equality engine, which is a pointer stored in this class |
581 |
288783 |
return d_equalityEngine; |
582 |
|
} |
583 |
|
|
584 |
|
} // namespace theory |
585 |
28194 |
} // namespace cvc5 |