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/arith_options.h" |
26 |
|
#include "options/smt_options.h" |
27 |
|
#include "options/theory_options.h" |
28 |
|
#include "smt/smt_statistics_registry.h" |
29 |
|
#include "theory/ee_setup_info.h" |
30 |
|
#include "theory/ext_theory.h" |
31 |
|
#include "theory/output_channel.h" |
32 |
|
#include "theory/quantifiers_engine.h" |
33 |
|
#include "theory/substitutions.h" |
34 |
|
#include "theory/theory_inference_manager.h" |
35 |
|
#include "theory/theory_model.h" |
36 |
|
#include "theory/theory_rewriter.h" |
37 |
|
#include "theory/theory_state.h" |
38 |
|
#include "theory/trust_substitutions.h" |
39 |
|
|
40 |
|
using namespace std; |
41 |
|
|
42 |
|
namespace cvc5 { |
43 |
|
namespace theory { |
44 |
|
|
45 |
|
/** Default value for the uninterpreted sorts is the UF theory */ |
46 |
|
TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; |
47 |
|
|
48 |
|
std::ostream& operator<<(std::ostream& os, Theory::Effort level){ |
49 |
|
switch(level){ |
50 |
|
case Theory::EFFORT_STANDARD: |
51 |
|
os << "EFFORT_STANDARD"; break; |
52 |
|
case Theory::EFFORT_FULL: |
53 |
|
os << "EFFORT_FULL"; break; |
54 |
|
case Theory::EFFORT_LAST_CALL: |
55 |
|
os << "EFFORT_LAST_CALL"; break; |
56 |
|
default: |
57 |
|
Unreachable(); |
58 |
|
} |
59 |
|
return os; |
60 |
|
}/* ostream& operator<<(ostream&, Theory::Effort) */ |
61 |
|
|
62 |
128092 |
Theory::Theory(TheoryId id, |
63 |
|
Env& env, |
64 |
|
OutputChannel& out, |
65 |
|
Valuation valuation, |
66 |
128092 |
std::string name) |
67 |
|
: d_id(id), |
68 |
|
d_env(env), |
69 |
128092 |
d_facts(d_env.getContext()), |
70 |
128092 |
d_factsHead(d_env.getContext(), 0), |
71 |
128092 |
d_sharedTermsIndex(d_env.getContext(), 0), |
72 |
|
d_careGraph(nullptr), |
73 |
|
d_instanceName(name), |
74 |
256184 |
d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) |
75 |
256184 |
+ name + "checkTime")), |
76 |
128092 |
d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( |
77 |
256184 |
getStatsPrefix(id) + name + "computeCareGraphTime")), |
78 |
128092 |
d_sharedTerms(d_env.getContext()), |
79 |
|
d_out(&out), |
80 |
|
d_valuation(valuation), |
81 |
|
d_equalityEngine(nullptr), |
82 |
|
d_allocEqualityEngine(nullptr), |
83 |
|
d_theoryState(nullptr), |
84 |
|
d_inferManager(nullptr), |
85 |
|
d_quantEngine(nullptr), |
86 |
128092 |
d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() |
87 |
1152828 |
: nullptr) |
88 |
|
{ |
89 |
128092 |
} |
90 |
|
|
91 |
128092 |
Theory::~Theory() { |
92 |
128092 |
} |
93 |
|
|
94 |
19700 |
bool Theory::needsEqualityEngine(EeSetupInfo& esi) |
95 |
|
{ |
96 |
|
// by default, this theory does not use an (official) equality engine |
97 |
19700 |
return false; |
98 |
|
} |
99 |
|
|
100 |
128050 |
void Theory::setEqualityEngine(eq::EqualityEngine* ee) |
101 |
|
{ |
102 |
|
// set the equality engine pointer |
103 |
128050 |
d_equalityEngine = ee; |
104 |
128050 |
if (d_theoryState != nullptr) |
105 |
|
{ |
106 |
118200 |
d_theoryState->setEqualityEngine(ee); |
107 |
|
} |
108 |
128050 |
if (d_inferManager != nullptr) |
109 |
|
{ |
110 |
118200 |
d_inferManager->setEqualityEngine(ee); |
111 |
|
} |
112 |
128050 |
} |
113 |
|
|
114 |
128050 |
void Theory::setQuantifiersEngine(QuantifiersEngine* qe) |
115 |
|
{ |
116 |
|
// quantifiers engine may be null if not in quantified logic |
117 |
128050 |
d_quantEngine = qe; |
118 |
128050 |
} |
119 |
|
|
120 |
128050 |
void Theory::setDecisionManager(DecisionManager* dm) |
121 |
|
{ |
122 |
128050 |
Assert(dm != nullptr); |
123 |
128050 |
if (d_inferManager != nullptr) |
124 |
|
{ |
125 |
118200 |
d_inferManager->setDecisionManager(dm); |
126 |
|
} |
127 |
128050 |
} |
128 |
|
|
129 |
|
void Theory::finishInitStandalone() |
130 |
|
{ |
131 |
|
EeSetupInfo esi; |
132 |
|
if (needsEqualityEngine(esi)) |
133 |
|
{ |
134 |
|
// always associated with the same SAT context as the theory |
135 |
|
d_allocEqualityEngine.reset( |
136 |
|
new eq::EqualityEngine(*esi.d_notify, |
137 |
|
getSatContext(), |
138 |
|
esi.d_name, |
139 |
|
esi.d_constantsAreTriggers)); |
140 |
|
// use it as the official equality engine |
141 |
|
setEqualityEngine(d_allocEqualityEngine.get()); |
142 |
|
} |
143 |
|
finishInit(); |
144 |
|
} |
145 |
|
|
146 |
170675983 |
TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) |
147 |
|
{ |
148 |
170675983 |
TheoryId tid = THEORY_BUILTIN; |
149 |
170675983 |
switch(mode) { |
150 |
117732460 |
case options::TheoryOfMode::THEORY_OF_TYPE_BASED: |
151 |
|
// Constants, variables, 0-ary constructors |
152 |
117732460 |
if (node.isVar()) |
153 |
|
{ |
154 |
4714605 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
155 |
|
{ |
156 |
230504 |
tid = THEORY_UF; |
157 |
|
} |
158 |
|
else |
159 |
|
{ |
160 |
4484101 |
tid = Theory::theoryOf(node.getType()); |
161 |
|
} |
162 |
|
} |
163 |
113017855 |
else if (node.getKind() == kind::EQUAL) |
164 |
|
{ |
165 |
|
// Equality is owned by the theory that owns the domain |
166 |
7334598 |
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 |
105683257 |
tid = kindToTheoryId(node.getKind()); |
174 |
|
} |
175 |
117732460 |
break; |
176 |
52943523 |
case options::TheoryOfMode::THEORY_OF_TERM_BASED: |
177 |
|
// Variables |
178 |
52943523 |
if (node.isVar()) |
179 |
|
{ |
180 |
5047412 |
if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) |
181 |
|
{ |
182 |
|
// We treat the variables as uninterpreted |
183 |
5035684 |
tid = s_uninterpretedSortOwner; |
184 |
|
} |
185 |
|
else |
186 |
|
{ |
187 |
11728 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
188 |
|
{ |
189 |
|
// Boolean vars go to UF |
190 |
7265 |
tid = THEORY_UF; |
191 |
|
} |
192 |
|
else |
193 |
|
{ |
194 |
|
// Except for the Boolean ones |
195 |
4463 |
tid = THEORY_BOOL; |
196 |
|
} |
197 |
|
} |
198 |
|
} |
199 |
47896111 |
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 |
4483490 |
if (node[0].getKind() == kind::ITE) |
204 |
|
{ |
205 |
5053 |
tid = Theory::theoryOf(node[0].getType()); |
206 |
|
} |
207 |
4478437 |
else if (node[1].getKind() == kind::ITE) |
208 |
|
{ |
209 |
10607 |
tid = Theory::theoryOf(node[1].getType()); |
210 |
|
} |
211 |
|
else |
212 |
|
{ |
213 |
8935660 |
TNode l = node[0]; |
214 |
8935660 |
TNode r = node[1]; |
215 |
8935660 |
TypeNode ltype = l.getType(); |
216 |
8935660 |
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 |
4467830 |
if (ltype != rtype || ltype.isBoolean()) |
221 |
|
{ |
222 |
59111 |
tid = Theory::theoryOf(ltype); |
223 |
|
} |
224 |
|
else |
225 |
|
{ |
226 |
|
// If both sides belong to the same theory the choice is easy |
227 |
4408719 |
TheoryId T1 = Theory::theoryOf(l); |
228 |
4408719 |
TheoryId T2 = Theory::theoryOf(r); |
229 |
4408719 |
if (T1 == T2) |
230 |
|
{ |
231 |
2552330 |
tid = T1; |
232 |
|
} |
233 |
|
else |
234 |
|
{ |
235 |
1856389 |
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 |
1856389 |
if (T1 == T3) |
243 |
|
{ |
244 |
47982 |
tid = T2; |
245 |
|
} |
246 |
1808407 |
else if (T2 == T3) |
247 |
|
{ |
248 |
1760964 |
tid = T1; |
249 |
|
} |
250 |
|
else |
251 |
|
{ |
252 |
|
// If both are parametric, we take the smaller one (arbitrary) |
253 |
47443 |
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 |
43412621 |
tid = kindToTheoryId(node.getKind()); |
264 |
|
} |
265 |
52943523 |
break; |
266 |
|
default: |
267 |
|
Unreachable(); |
268 |
|
} |
269 |
170675983 |
Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl; |
270 |
170675983 |
return tid; |
271 |
|
} |
272 |
|
|
273 |
907586 |
void Theory::notifySharedTerm(TNode n) |
274 |
|
{ |
275 |
|
// do nothing |
276 |
907586 |
} |
277 |
|
|
278 |
2443415 |
void Theory::notifyInConflict() |
279 |
|
{ |
280 |
2443415 |
if (d_inferManager != nullptr) |
281 |
|
{ |
282 |
2255460 |
d_inferManager->notifyInConflict(); |
283 |
|
} |
284 |
2443415 |
} |
285 |
|
|
286 |
6542 |
void Theory::computeCareGraph() { |
287 |
6542 |
Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl; |
288 |
7070 |
for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { |
289 |
1056 |
TNode a = d_sharedTerms[i]; |
290 |
1056 |
TypeNode aType = a.getType(); |
291 |
5094 |
for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) { |
292 |
8676 |
TNode b = d_sharedTerms[j]; |
293 |
4566 |
if (b.getType() != aType) { |
294 |
|
// We don't care about the terms of different types |
295 |
456 |
continue; |
296 |
|
} |
297 |
4110 |
switch (d_valuation.getEqualityStatus(a, b)) { |
298 |
3304 |
case EQUALITY_TRUE_AND_PROPAGATED: |
299 |
|
case EQUALITY_FALSE_AND_PROPAGATED: |
300 |
|
// If we know about it, we should have propagated it, so we can skip |
301 |
3304 |
break; |
302 |
806 |
default: |
303 |
|
// Let's split on it |
304 |
806 |
addCarePair(a, b); |
305 |
806 |
break; |
306 |
|
} |
307 |
|
} |
308 |
|
} |
309 |
6542 |
} |
310 |
|
|
311 |
|
void Theory::printFacts(std::ostream& os) const { |
312 |
|
unsigned i, n = d_facts.size(); |
313 |
|
for(i = 0; i < n; i++){ |
314 |
|
const Assertion& a_i = d_facts[i]; |
315 |
|
Node assertion = a_i; |
316 |
|
os << d_id << '[' << i << ']' << " " << assertion << endl; |
317 |
|
} |
318 |
|
} |
319 |
|
|
320 |
|
void Theory::debugPrintFacts() const{ |
321 |
|
DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl; |
322 |
|
printFacts(DebugChannel.getStream()); |
323 |
|
} |
324 |
|
|
325 |
17891 |
bool Theory::isLegalElimination(TNode x, TNode val) |
326 |
|
{ |
327 |
17891 |
Assert(x.isVar()); |
328 |
35782 |
if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE |
329 |
17891 |
|| val.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
330 |
|
{ |
331 |
|
return false; |
332 |
|
} |
333 |
17891 |
if (expr::hasSubterm(val, x)) |
334 |
|
{ |
335 |
4757 |
return false; |
336 |
|
} |
337 |
13134 |
if (!val.getType().isSubtypeOf(x.getType())) |
338 |
|
{ |
339 |
|
return false; |
340 |
|
} |
341 |
13134 |
if (!options::produceModels() && !getLogicInfo().isQuantified()) |
342 |
|
{ |
343 |
|
// Don't care about the model and logic is not quantified, we can eliminate. |
344 |
2949 |
return true; |
345 |
|
} |
346 |
|
// If models are enabled, then it depends on whether the term contains any |
347 |
|
// unevaluable operators like FORALL, SINE, etc. Having such operators makes |
348 |
|
// model construction contain non-constant values for variables, which is |
349 |
|
// not ideal from a user perspective. |
350 |
|
// We also insist on this check since the term to eliminate should never |
351 |
|
// contain quantifiers, or else variable shadowing issues may arise. |
352 |
|
// there should be a model object |
353 |
10185 |
TheoryModel* tm = d_valuation.getModel(); |
354 |
10185 |
Assert(tm != nullptr); |
355 |
10185 |
return tm->isLegalElimination(x, val); |
356 |
|
} |
357 |
|
|
358 |
14564 |
std::unordered_set<TNode> Theory::currentlySharedTerms() const |
359 |
|
{ |
360 |
14564 |
std::unordered_set<TNode> currentlyShared; |
361 |
271708 |
for (shared_terms_iterator i = shared_terms_begin(), |
362 |
14564 |
i_end = shared_terms_end(); i != i_end; ++i) { |
363 |
257144 |
currentlyShared.insert (*i); |
364 |
|
} |
365 |
14564 |
return currentlyShared; |
366 |
|
} |
367 |
|
|
368 |
102801 |
bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) |
369 |
|
{ |
370 |
|
// if we are using an equality engine, assert it to the model |
371 |
102801 |
if (d_equalityEngine != nullptr && !termSet.empty()) |
372 |
|
{ |
373 |
56864 |
Trace("model-builder") << "Assert Equality engine for " << d_id |
374 |
28432 |
<< std::endl; |
375 |
28432 |
if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) |
376 |
|
{ |
377 |
|
return false; |
378 |
|
} |
379 |
|
} |
380 |
102801 |
Trace("model-builder") << "Collect Model values for " << d_id << std::endl; |
381 |
|
// now, collect theory-specific value assigments |
382 |
102801 |
return collectModelValues(m, termSet); |
383 |
|
} |
384 |
|
|
385 |
99553 |
void Theory::computeRelevantTerms(std::set<Node>& termSet) |
386 |
|
{ |
387 |
|
// by default, there are no additional relevant terms |
388 |
99553 |
} |
389 |
|
|
390 |
37963 |
bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) |
391 |
|
{ |
392 |
37963 |
return true; |
393 |
|
} |
394 |
|
|
395 |
46427 |
Theory::PPAssertStatus Theory::ppAssert(TrustNode tin, |
396 |
|
TrustSubstitutionMap& outSubstitutions) |
397 |
|
{ |
398 |
92854 |
TNode in = tin.getNode(); |
399 |
46427 |
if (in.getKind() == kind::EQUAL) |
400 |
|
{ |
401 |
|
// (and (= x t) phi) can be replaced by phi[x/t] if |
402 |
|
// 1) x is a variable |
403 |
|
// 2) x is not in the term t |
404 |
|
// 3) x : T and t : S, then S <: T |
405 |
78056 |
if (in[0].isVar() && isLegalElimination(in[0], in[1]) |
406 |
73427 |
&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
407 |
|
{ |
408 |
10376 |
outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); |
409 |
10376 |
return PP_ASSERT_STATUS_SOLVED; |
410 |
|
} |
411 |
32170 |
if (in[1].isVar() && isLegalElimination(in[1], in[0]) |
412 |
32170 |
&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
413 |
|
{ |
414 |
247 |
outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); |
415 |
247 |
return PP_ASSERT_STATUS_SOLVED; |
416 |
|
} |
417 |
10394 |
if (in[0].isConst() && in[1].isConst()) |
418 |
|
{ |
419 |
|
if (in[0] != in[1]) |
420 |
|
{ |
421 |
|
return PP_ASSERT_STATUS_CONFLICT; |
422 |
|
} |
423 |
|
} |
424 |
|
} |
425 |
74348 |
else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL |
426 |
73927 |
&& in[0][0].getType().isBoolean()) |
427 |
|
{ |
428 |
45 |
TNode eq = in[0]; |
429 |
41 |
if (eq[0].isVar()) |
430 |
|
{ |
431 |
74 |
Node res = eq[0].eqNode(eq[1].notNode()); |
432 |
74 |
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
433 |
37 |
return ppAssert(tn, outSubstitutions); |
434 |
|
} |
435 |
4 |
else if (eq[1].isVar()) |
436 |
|
{ |
437 |
|
Node res = eq[1].eqNode(eq[0].notNode()); |
438 |
|
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
439 |
|
return ppAssert(tn, outSubstitutions); |
440 |
|
} |
441 |
|
} |
442 |
|
|
443 |
35767 |
return PP_ASSERT_STATUS_UNSOLVED; |
444 |
|
} |
445 |
|
|
446 |
|
std::pair<bool, Node> Theory::entailmentCheck(TNode lit) |
447 |
|
{ |
448 |
|
return make_pair(false, Node::null()); |
449 |
|
} |
450 |
|
|
451 |
41956 |
void Theory::addCarePair(TNode t1, TNode t2) { |
452 |
41956 |
if (d_careGraph) { |
453 |
41956 |
d_careGraph->insert(CarePair(t1, t2, d_id)); |
454 |
|
} |
455 |
41956 |
} |
456 |
|
|
457 |
68259 |
void Theory::getCareGraph(CareGraph* careGraph) { |
458 |
68259 |
Assert(careGraph != NULL); |
459 |
|
|
460 |
68259 |
Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; |
461 |
136518 |
TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); |
462 |
68259 |
d_careGraph = careGraph; |
463 |
68259 |
computeCareGraph(); |
464 |
68259 |
d_careGraph = NULL; |
465 |
68259 |
} |
466 |
|
|
467 |
|
bool Theory::proofsEnabled() const |
468 |
|
{ |
469 |
|
return d_env.getProofNodeManager() != nullptr; |
470 |
|
} |
471 |
|
|
472 |
20253 |
EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) |
473 |
|
{ |
474 |
|
// if not using an equality engine, then by default we don't know the status |
475 |
20253 |
if (d_equalityEngine == nullptr) |
476 |
|
{ |
477 |
5768 |
return EQUALITY_UNKNOWN; |
478 |
|
} |
479 |
14485 |
Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl; |
480 |
14485 |
Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); |
481 |
|
|
482 |
|
// Check for equality (simplest) |
483 |
14485 |
if (d_equalityEngine->areEqual(a, b)) |
484 |
|
{ |
485 |
|
// The terms are implied to be equal |
486 |
7296 |
return EQUALITY_TRUE; |
487 |
|
} |
488 |
|
|
489 |
|
// Check for disequality |
490 |
7189 |
if (d_equalityEngine->areDisequal(a, b, false)) |
491 |
|
{ |
492 |
|
// The terms are implied to be dis-equal |
493 |
2649 |
return EQUALITY_FALSE; |
494 |
|
} |
495 |
|
|
496 |
|
// All other terms are unknown, which is conservative. A theory may override |
497 |
|
// this method if it knows more information. |
498 |
4540 |
return EQUALITY_UNKNOWN; |
499 |
|
} |
500 |
|
|
501 |
14289483 |
void Theory::check(Effort level) |
502 |
|
{ |
503 |
|
// see if we are already done (as an optimization) |
504 |
14289483 |
if (done() && level < EFFORT_FULL) |
505 |
|
{ |
506 |
18803442 |
return; |
507 |
|
} |
508 |
4887762 |
Assert(d_theoryState!=nullptr); |
509 |
|
// standard calls for resource, stats |
510 |
4887762 |
d_out->spendResource(Resource::TheoryCheckStep); |
511 |
9775524 |
TimerStat::CodeTimer checkTimer(d_checkTime); |
512 |
9775524 |
Trace("theory-check") << "Theory::preCheck " << level << " " << d_id |
513 |
4887762 |
<< std::endl; |
514 |
|
// pre-check at level |
515 |
4887762 |
if (preCheck(level)) |
516 |
|
{ |
517 |
|
// check aborted for a theory-specific reason |
518 |
|
return; |
519 |
|
} |
520 |
4887762 |
Assert(d_theoryState != nullptr); |
521 |
4887762 |
Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl; |
522 |
|
// process the pending fact queue |
523 |
33183278 |
while (!done() && !d_theoryState->isInConflict()) |
524 |
|
{ |
525 |
|
// Get the next assertion from the fact queue |
526 |
22514948 |
Assertion assertion = get(); |
527 |
22514948 |
TNode fact = assertion.d_assertion; |
528 |
28295522 |
Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id |
529 |
14147761 |
<< std::endl; |
530 |
14147761 |
bool polarity = fact.getKind() != kind::NOT; |
531 |
22514948 |
TNode atom = polarity ? fact : fact[0]; |
532 |
|
// call the pre-notify method |
533 |
14147761 |
if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false)) |
534 |
|
{ |
535 |
|
// handled in theory-specific way that doesn't involve equality engine |
536 |
5780574 |
continue; |
537 |
|
} |
538 |
16734374 |
Trace("theory-check") << "Theory::assert " << fact << " " << d_id |
539 |
8367187 |
<< std::endl; |
540 |
|
// Theories that don't have an equality engine should always return true |
541 |
|
// for preNotifyFact |
542 |
8367187 |
Assert(d_equalityEngine != nullptr); |
543 |
|
// assert to the equality engine |
544 |
8367187 |
if (atom.getKind() == kind::EQUAL) |
545 |
|
{ |
546 |
6021621 |
d_equalityEngine->assertEquality(atom, polarity, fact); |
547 |
|
} |
548 |
|
else |
549 |
|
{ |
550 |
2345569 |
d_equalityEngine->assertPredicate(atom, polarity, fact); |
551 |
|
} |
552 |
16734368 |
Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id |
553 |
8367184 |
<< std::endl; |
554 |
|
// notify the theory of the new fact, which is not internal |
555 |
8367184 |
notifyFact(atom, polarity, fact, false); |
556 |
|
} |
557 |
4887759 |
Trace("theory-check") << "Theory::postCheck " << d_id << std::endl; |
558 |
|
// post-check at level |
559 |
4887759 |
postCheck(level); |
560 |
4887758 |
Trace("theory-check") << "Theory::finish check " << d_id << std::endl; |
561 |
|
} |
562 |
|
|
563 |
1846794 |
bool Theory::preCheck(Effort level) { return false; } |
564 |
|
|
565 |
2 |
void Theory::postCheck(Effort level) {} |
566 |
|
|
567 |
4927937 |
bool Theory::preNotifyFact( |
568 |
|
TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) |
569 |
|
{ |
570 |
4927937 |
return false; |
571 |
|
} |
572 |
|
|
573 |
8384 |
void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal) |
574 |
|
{ |
575 |
8384 |
} |
576 |
|
|
577 |
22148 |
void Theory::preRegisterTerm(TNode node) {} |
578 |
|
|
579 |
1661695 |
void Theory::addSharedTerm(TNode n) |
580 |
|
{ |
581 |
3323390 |
Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" |
582 |
1661695 |
<< std::endl; |
583 |
3323390 |
Debug("theory::assertions") |
584 |
1661695 |
<< "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; |
585 |
1661695 |
d_sharedTerms.push_back(n); |
586 |
|
// now call theory-specific method notifySharedTerm |
587 |
1661695 |
notifySharedTerm(n); |
588 |
|
// if we have an equality engine, add the trigger term |
589 |
1661695 |
if (d_equalityEngine != nullptr) |
590 |
|
{ |
591 |
1656098 |
d_equalityEngine->addTriggerTerm(n, d_id); |
592 |
|
} |
593 |
1661695 |
} |
594 |
|
|
595 |
372681 |
eq::EqualityEngine* Theory::getEqualityEngine() |
596 |
|
{ |
597 |
|
// get the assigned equality engine, which is a pointer stored in this class |
598 |
372681 |
return d_equalityEngine; |
599 |
|
} |
600 |
|
|
601 |
350 |
bool Theory::usesCentralEqualityEngine() const |
602 |
|
{ |
603 |
350 |
return usesCentralEqualityEngine(d_id); |
604 |
|
} |
605 |
|
|
606 |
26029500 |
bool Theory::usesCentralEqualityEngine(TheoryId id) |
607 |
|
{ |
608 |
26029500 |
if (id == THEORY_BUILTIN) |
609 |
|
{ |
610 |
9954894 |
return true; |
611 |
|
} |
612 |
16074606 |
if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) |
613 |
|
{ |
614 |
16030788 |
return false; |
615 |
|
} |
616 |
43818 |
if (id == THEORY_ARITH) |
617 |
|
{ |
618 |
|
// conditional on whether we are using the equality solver |
619 |
70 |
return options::arithEqSolver(); |
620 |
|
} |
621 |
41310 |
return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS |
622 |
23316 |
|| id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS |
623 |
66488 |
|| id == THEORY_SEP || id == THEORY_ARRAYS; |
624 |
|
} |
625 |
|
|
626 |
29990133 |
bool Theory::expUsingCentralEqualityEngine(TheoryId id) |
627 |
|
{ |
628 |
29990133 |
return id != THEORY_ARITH && usesCentralEqualityEngine(id); |
629 |
|
} |
630 |
|
|
631 |
|
} // namespace theory |
632 |
29337 |
} // namespace cvc5 |