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 : : * The theory engine.
11 : : */
12 : :
13 : : #include "theory/theory_engine.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "base/map_util.h"
18 : : #include "decision/decision_engine.h"
19 : : #include "expr/attribute.h"
20 : : #include "expr/node_builder.h"
21 : : #include "expr/node_visitor.h"
22 : : #include "options/parallel_options.h"
23 : : #include "options/quantifiers_options.h"
24 : : #include "options/smt_options.h"
25 : : #include "options/theory_options.h"
26 : : #include "printer/printer.h"
27 : : #include "proof/lazy_proof.h"
28 : : #include "proof/proof_checker.h"
29 : : #include "proof/proof_ensure_closed.h"
30 : : #include "prop/prop_engine.h"
31 : : #include "smt/env.h"
32 : : #include "smt/logic_exception.h"
33 : : #include "smt/solver_engine_state.h"
34 : : #include "theory/combination_care_graph.h"
35 : : #include "theory/conflict_processor.h"
36 : : #include "theory/decision_manager.h"
37 : : #include "theory/ee_manager_central.h"
38 : : #include "theory/partition_generator.h"
39 : : #include "theory/plugin_module.h"
40 : : #include "theory/quantifiers/first_order_model.h"
41 : : #include "theory/quantifiers_engine.h"
42 : : #include "theory/relevance_manager.h"
43 : : #include "theory/rewriter.h"
44 : : #include "theory/shared_solver.h"
45 : : #include "theory/theory.h"
46 : : #include "theory/theory_engine_proof_generator.h"
47 : : #include "theory/theory_id.h"
48 : : #include "theory/theory_model.h"
49 : : #include "theory/theory_traits.h"
50 : : #include "theory/uf/equality_engine.h"
51 : : #include "util/resource_manager.h"
52 : :
53 : : using namespace std;
54 : :
55 : : using namespace cvc5::internal::theory;
56 : :
57 : : namespace cvc5::internal {
58 : :
59 : : /* -------------------------------------------------------------------------- */
60 : :
61 : : namespace theory {
62 : :
63 : : /**
64 : : * IMPORTANT: The order of the theories is important. For example, strings
65 : : * depends on arith, quantifiers needs to come as the very last.
66 : : * Do not change this order.
67 : : */
68 : :
69 : : #define CVC5_FOR_EACH_THEORY \
70 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_BUILTIN) \
71 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_BOOL) \
72 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_UF) \
73 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_ARITH) \
74 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_BV) \
75 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_FF) \
76 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_FP) \
77 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_ARRAYS) \
78 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_DATATYPES) \
79 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_SEP) \
80 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_SETS) \
81 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_BAGS) \
82 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_STRINGS) \
83 : : CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::internal::theory::THEORY_QUANTIFIERS)
84 : :
85 : : } // namespace theory
86 : :
87 : : /* -------------------------------------------------------------------------- */
88 : :
89 : : /**
90 : : * Compute the string for a given theory id. In this module, we use
91 : : * THEORY_SAT_SOLVER as an id, which is not a normal id but maps to
92 : : * THEORY_LAST. Thus, we need our own string conversion here.
93 : : *
94 : : * @param id The theory id
95 : : * @return The string corresponding to the theory id
96 : : */
97 : 0 : std::string getTheoryString(theory::TheoryId id)
98 : : {
99 [ - - ]: 0 : if (id == theory::THEORY_SAT_SOLVER)
100 : : {
101 : 0 : return "THEORY_SAT_SOLVER";
102 : : }
103 : : else
104 : : {
105 : 0 : std::stringstream ss;
106 : 0 : ss << id;
107 : 0 : return ss.str();
108 : 0 : }
109 : : }
110 : :
111 : 51364 : void TheoryEngine::finishInit()
112 : : {
113 : 51364 : d_modules.clear();
114 [ + - ]: 51364 : Trace("theory") << "Begin TheoryEngine::finishInit" << std::endl;
115 : : // NOTE: This seems to be required since
116 : : // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without
117 : : // using the CVC5_FOR_EACH_THEORY_STATEMENT macro. -AJR
118 : 51364 : std::vector<theory::Theory*> paraTheories;
119 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
120 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
121 : : #endif
122 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
123 : : if (theory::TheoryTraits<THEORY>::isParametric && isTheoryEnabled(THEORY)) \
124 : : { \
125 : : paraTheories.push_back(theoryOf(THEORY)); \
126 : : }
127 : : // Collect the parametric theories, which are given to the theory combination
128 : : // manager below
129 [ + + ][ + + ]: 51364 : CVC5_FOR_EACH_THEORY;
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
130 : :
131 : : // Initialize the theory combination architecture
132 [ + - ]: 51364 : if (options().theory.tcMode == options::TcMode::CARE_GRAPH)
133 : : {
134 : 51364 : d_tc.reset(new CombinationCareGraph(d_env, *this, paraTheories));
135 : : }
136 : : else
137 : : {
138 : 0 : Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
139 : 0 : << options().theory.tcMode << " not supported";
140 : : }
141 : : // create the relevance filter if any option requires it
142 [ + + ][ + + ]: 51364 : if (options().theory.relevanceFilter || options().smt.produceDifficulty)
[ + + ]
143 : : {
144 : 486 : d_relManager.reset(new RelevanceManager(d_env, this));
145 : 486 : d_modules.push_back(d_relManager.get());
146 : : }
147 : :
148 : : // initialize the quantifiers engine
149 [ + + ]: 51364 : if (logicInfo().isQuantified())
150 : : {
151 : : // get the quantifiers engine, which is initialized by the quantifiers
152 : : // theory
153 : 44518 : d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
154 [ - + ][ - + ]: 44518 : Assert(d_quantEngine != nullptr);
[ - - ]
155 : : }
156 : : // finish initializing the quantifiers engine, which must come before
157 : : // initializing theory combination, since quantifiers engine may have a
158 : : // special model builder object
159 [ + + ]: 51364 : if (logicInfo().isQuantified())
160 : : {
161 : 44518 : d_quantEngine->finishInit(this);
162 : : }
163 : : // initialize the theory combination manager, which decides and allocates the
164 : : // equality engines to use for all theories.
165 : 51364 : d_tc->finishInit();
166 : : // get pointer to the shared solver
167 : 51364 : d_sharedSolver = d_tc->getSharedSolver();
168 : :
169 : : // finish initializing the theories by linking them with the appropriate
170 : : // utilities and then calling their finishInit method.
171 : 51364 : for (TheoryId theoryId = theory::THEORY_FIRST;
172 [ + + ]: 770460 : theoryId != theory::THEORY_LAST;
173 : 719096 : ++theoryId)
174 : : {
175 : 719096 : Theory* t = d_theoryTable[theoryId];
176 [ - + ]: 719096 : if (t == nullptr)
177 : : {
178 : 0 : continue;
179 : : }
180 : : // setup the pointers to the utilities
181 : 719096 : const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
182 [ - + ][ - + ]: 719096 : Assert(eeti != nullptr);
[ - - ]
183 : : // the theory's official equality engine is the one specified by the
184 : : // equality engine manager
185 : 719096 : t->setEqualityEngine(eeti->d_usedEe);
186 : : // set the quantifiers engine
187 : 719096 : t->setQuantifiersEngine(d_quantEngine);
188 : : // set the decision manager for the theory
189 : 719096 : t->setDecisionManager(d_decManager.get());
190 : : // finish initializing the theory
191 : 719096 : t->finishInit();
192 : : }
193 : :
194 [ - + ]: 51364 : if (options().parallel.computePartitions > 1)
195 : : {
196 : : d_partitionGen =
197 : 0 : std::make_unique<PartitionGenerator>(d_env, this, getPropEngine());
198 : 0 : d_modules.push_back(d_partitionGen.get());
199 : : }
200 : :
201 : : // add user-provided plugins
202 : 51364 : const std::vector<Plugin*> plugins = d_env.getPlugins();
203 [ + - ]: 102728 : Trace("theory") << "initialize with " << plugins.size()
204 : 51364 : << " user-provided plugins" << std::endl;
205 [ + + ]: 51392 : for (Plugin* p : plugins)
206 : : {
207 : 28 : d_userPlugins.push_back(
208 : 56 : std::unique_ptr<PluginModule>(new PluginModule(d_env, this, p)));
209 : 28 : d_modules.push_back(d_userPlugins.back().get());
210 : : }
211 [ + - ]: 51364 : Trace("theory") << "End TheoryEngine::finishInit" << std::endl;
212 : 51364 : }
213 : :
214 : 51364 : TheoryEngine::TheoryEngine(Env& env)
215 : : : EnvObj(env),
216 : 51364 : d_propEngine(nullptr),
217 : 62251 : d_lazyProof(
218 [ + + ]: 51364 : env.isTheoryProofProducing()
219 : : ? new LazyCDProof(
220 : 21774 : env, nullptr, userContext(), "TheoryEngine::LazyCDProof")
221 : : : nullptr),
222 : 51364 : d_tepg(new TheoryEngineProofGenerator(env, userContext())),
223 : 51364 : d_tc(nullptr),
224 : 51364 : d_sharedSolver(nullptr),
225 : 51364 : d_quantEngine(nullptr),
226 : 51364 : d_decManager(new DecisionManager(userContext())),
227 : 51364 : d_relManager(nullptr),
228 : 51364 : d_inConflict(context(), false),
229 : 51364 : d_modelUnsound(context(), false),
230 : 51364 : d_modelUnsoundTheory(context(), THEORY_BUILTIN),
231 : 51364 : d_modelUnsoundId(context(), IncompleteId::UNKNOWN),
232 : 51364 : d_refutationUnsound(userContext(), false),
233 : 51364 : d_refutationUnsoundTheory(userContext(), THEORY_BUILTIN),
234 : 51364 : d_refutationUnsoundId(userContext(), IncompleteId::UNKNOWN),
235 : 51364 : d_propagationMap(context()),
236 : 51364 : d_propagationMapTimestamp(context(), 0),
237 : 51364 : d_propagatedLiterals(context()),
238 : 51364 : d_propagatedLiteralsIndex(context(), 0),
239 : 51364 : d_atomRequests(context()),
240 : 51364 : d_stats(statisticsRegistry()),
241 : 51364 : d_true(),
242 : 51364 : d_false(),
243 : 51364 : d_interrupted(false),
244 : 51364 : d_inPreregister(false),
245 : 51364 : d_factsAsserted(context(), false),
246 : 205456 : d_cp(nullptr)
247 : : {
248 : 51364 : for (TheoryId theoryId = theory::THEORY_FIRST;
249 [ + + ]: 770460 : theoryId != theory::THEORY_LAST;
250 : 719096 : ++theoryId)
251 : : {
252 : 719096 : d_theoryTable[theoryId] = nullptr;
253 : 719096 : d_theoryOut[theoryId] = nullptr;
254 : : }
255 : :
256 [ + + ]: 51364 : if (options().smt.sortInference)
257 : : {
258 : 45 : d_sortInfer.reset(new SortInference(env));
259 : : }
260 : 51364 : if (options().theory.conflictProcessMode
261 [ + + ]: 51364 : != options::ConflictProcessMode::NONE)
262 : : {
263 : 7 : bool useExtRewriter = (options().theory.conflictProcessMode
264 : 7 : == options::ConflictProcessMode::MINIMIZE_EXT);
265 : 7 : d_cp.reset(new ConflictProcessor(env, useExtRewriter));
266 : : }
267 : :
268 : 51364 : d_true = nodeManager()->mkConst<bool>(true);
269 : 51364 : d_false = nodeManager()->mkConst<bool>(false);
270 : 51364 : }
271 : :
272 : 102032 : TheoryEngine::~TheoryEngine()
273 : : {
274 : 51016 : for (TheoryId theoryId = theory::THEORY_FIRST;
275 [ + + ]: 765240 : theoryId != theory::THEORY_LAST;
276 : 714224 : ++theoryId)
277 : : {
278 [ + + ]: 714224 : if (d_theoryTable[theoryId] != nullptr)
279 : : {
280 [ + - ]: 714197 : delete d_theoryTable[theoryId];
281 [ + - ]: 714197 : delete d_theoryOut[theoryId];
282 : : }
283 : : }
284 : 102032 : }
285 : :
286 : 315129 : void TheoryEngine::interrupt() { d_interrupted = true; }
287 : 2228782 : void TheoryEngine::preRegister(TNode preprocessed)
288 : : {
289 [ + - ]: 4457564 : Trace("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
290 : 2228782 : << std::endl;
291 : 2228782 : d_preregisterQueue.push(preprocessed);
292 : :
293 [ + + ]: 2228782 : if (!d_inPreregister)
294 : : {
295 : : // We're in pre-register
296 : 2076496 : d_inPreregister = true;
297 : :
298 : : // Process the pre-registration queue
299 [ + + ]: 4305262 : while (!d_preregisterQueue.empty())
300 : : {
301 : : // Get the next atom to pre-register
302 : 2228782 : preprocessed = d_preregisterQueue.front();
303 : 2228782 : d_preregisterQueue.pop();
304 : :
305 : : // the atom should not have free variables
306 [ + - ]: 4457564 : Trace("theory") << "TheoryEngine::preRegister: " << preprocessed
307 : 2228782 : << std::endl;
308 [ + - ]: 2228782 : if (Configuration::isAssertionBuild())
309 : : {
310 : 2228782 : std::unordered_set<Node> fvs;
311 : 2228782 : expr::getFreeVariables(preprocessed, fvs);
312 [ - + ]: 2228782 : if (!fvs.empty())
313 : : {
314 : 0 : Unhandled() << "Preregistered term with free variable: "
315 : 0 : << preprocessed << ", fv=" << *fvs.begin();
316 : : }
317 : 2228782 : }
318 : : // should not have witness
319 [ - + ][ - + ]: 2228782 : Assert(!expr::hasSubtermKind(Kind::WITNESS, preprocessed));
[ - - ]
320 : :
321 : : // pre-register with the shared solver, which handles
322 : : // calling prepregister on individual theories, adding shared terms,
323 : : // and setting up equalities to propagate in the shared term database.
324 [ - + ][ - + ]: 2228782 : Assert(d_sharedSolver != nullptr);
[ - - ]
325 : 2228782 : d_sharedSolver->preRegister(preprocessed);
326 : : }
327 : :
328 : : // Leaving pre-register
329 : 2076480 : d_inPreregister = false;
330 : : }
331 : 2228766 : }
332 : :
333 : 0 : void TheoryEngine::printAssertions(const char* tag)
334 : : {
335 [ - - ]: 0 : if (TraceIsOn(tag))
336 : : {
337 [ - - ]: 0 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
338 : : {
339 : 0 : Theory* theory = d_theoryTable[theoryId];
340 : 0 : if (theory && isTheoryEnabled(theoryId))
341 : : {
342 [ - - ]: 0 : Trace(tag) << "--------------------------------------------" << endl;
343 [ - - ]: 0 : Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
344 : : {
345 : 0 : context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
346 : : it_end =
347 : 0 : theory->facts_end();
348 [ - - ]: 0 : for (unsigned i = 0; it != it_end; ++it, ++i)
349 : : {
350 [ - - ]: 0 : if ((*it).d_isPreregistered)
351 : : {
352 [ - - ]: 0 : Trace(tag) << "[" << i << "]: ";
353 : : }
354 : : else
355 : : {
356 [ - - ]: 0 : Trace(tag) << "(" << i << "): ";
357 : : }
358 [ - - ]: 0 : Trace(tag) << (*it).d_assertion << endl;
359 : : }
360 : : }
361 : :
362 [ - - ]: 0 : if (logicInfo().isSharingEnabled())
363 : : {
364 : 0 : TheoryState* state = theory->getTheoryState();
365 [ - - ]: 0 : if (state != nullptr)
366 : : {
367 [ - - ]: 0 : Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
368 : : context::CDList<TNode>::const_iterator
369 : 0 : it = state->shared_terms_begin(),
370 : 0 : it_end = state->shared_terms_end();
371 [ - - ]: 0 : for (unsigned i = 0; it != it_end; ++it, ++i)
372 : : {
373 [ - - ]: 0 : Trace(tag) << "[" << i << "]: " << (*it) << endl;
374 : : }
375 : : }
376 : : }
377 : : }
378 : : }
379 : : }
380 : 0 : }
381 : :
382 : : /**
383 : : * Check all (currently-active) theories for conflicts.
384 : : * @param effort the effort level to use
385 : : */
386 : 11199270 : void TheoryEngine::check(Theory::Effort effort)
387 : : {
388 : : // spendResource();
389 : :
390 : : // Reset the interrupt flag
391 : 11199270 : d_interrupted = false;
392 : :
393 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
394 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
395 : : #endif
396 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
397 : : if (theory::TheoryTraits<THEORY>::hasCheck && isTheoryEnabled(THEORY)) \
398 : : { \
399 : : theoryOf(THEORY)->check(effort); \
400 : : if (d_inConflict) \
401 : : { \
402 : : Trace("conflict") << THEORY << " in conflict. " << std::endl; \
403 : : break; \
404 : : } \
405 : : if (rm->out()) \
406 : : { \
407 : : interrupt(); \
408 : : return; \
409 : : } \
410 : : }
411 : :
412 : : // Do the checking
413 : : try
414 : : {
415 : : // Mark the output channel unused (if this is FULL_EFFORT, and nothing
416 : : // is done by the theories, no additional check will be needed)
417 : 11199270 : d_outputChannelUsed = false;
418 : :
419 : : // Mark the lemmas flag (no lemmas added)
420 : 11199270 : d_lemmasAdded = false;
421 : :
422 [ + - ]: 22398540 : Trace("theory") << "TheoryEngine::check(" << effort
423 : 0 : << "): d_factsAsserted = "
424 [ - - ]: 11199270 : << (d_factsAsserted ? "true" : "false") << endl;
425 : :
426 : : // If in full effort, we have a fake new assertion just to jumpstart the
427 : : // checking
428 [ + + ]: 11199270 : if (Theory::fullEffort(effort))
429 : : {
430 : 175209 : spendResource(Resource::TheoryFullCheckStep);
431 : 175209 : d_factsAsserted = true;
432 : 175209 : d_tc->resetRound();
433 : : }
434 : :
435 : : // check with the theory modules
436 [ + + ]: 11201053 : for (TheoryEngineModule* tem : d_modules)
437 : : {
438 : 1783 : tem->check(effort);
439 : : }
440 : :
441 : 11199270 : auto rm = d_env.getResourceManager();
442 : :
443 : : // Check until done
444 [ + + ][ + + ]: 20019735 : while (d_factsAsserted && !d_inConflict && !d_lemmasAdded)
[ + + ][ + + ]
445 : : {
446 [ + - ]: 18224064 : Trace("theory") << "TheoryEngine::check(" << effort << "): running check"
447 : 9112032 : << endl;
448 : :
449 [ + - ]: 9112032 : Trace("theory::assertions") << endl;
450 [ - + ]: 9112032 : if (TraceIsOn("theory::assertions"))
451 : : {
452 : 0 : printAssertions("theory::assertions");
453 : : }
454 : :
455 [ + + ]: 9112032 : if (Theory::fullEffort(effort))
456 : : {
457 [ + - ]: 189977 : Trace("theory::assertions::fulleffort") << endl;
458 [ - + ]: 189977 : if (TraceIsOn("theory::assertions::fulleffort"))
459 : : {
460 : 0 : printAssertions("theory::assertions::fulleffort");
461 : : }
462 : : }
463 : :
464 : : // Note that we've discharged all the facts
465 : 9112032 : d_factsAsserted = false;
466 : :
467 : : // Do the checking
468 [ + + ][ + + ]: 9112032 : CVC5_FOR_EACH_THEORY;
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ - + ]
[ - - ][ - + ]
469 : :
470 [ + - ]: 17640930 : Trace("theory") << "TheoryEngine::check(" << effort
471 : 0 : << "): running propagation after the initial check"
472 : 8820465 : << endl;
473 : :
474 : : // We are still satisfiable, propagate as much as possible
475 : 8820465 : propagate(effort);
476 : :
477 : : // Interrupt in case we reached a resource limit.
478 [ - + ]: 8820465 : if (rm->out())
479 : : {
480 : 0 : interrupt();
481 : 0 : return;
482 : : }
483 : :
484 [ + + ]: 8820465 : if (Theory::fullEffort(effort))
485 : : {
486 : 145267 : d_stats.d_fullEffortChecks++;
487 : : // We do combination if all has been processed and we are in fullcheck
488 [ + + ][ + + ]: 281404 : if (logicInfo().isSharingEnabled() && !d_factsAsserted && !needCheck()
489 [ + + ][ + - ]: 281404 : && !d_inConflict)
[ + + ]
490 : : {
491 : 69279 : d_stats.d_combineTheoriesCalls++;
492 : : // Do the combination
493 [ + - ]: 138558 : Trace("theory") << "TheoryEngine::check(" << effort
494 : 69279 : << "): running combination" << endl;
495 : : {
496 : : TimerStat::CodeTimer combineTheoriesTimer(
497 : 69279 : d_stats.d_combineTheoriesTime);
498 : 69279 : d_tc->combineTheories();
499 : 69279 : }
500 [ + + ]: 69279 : if (logicInfo().isQuantified())
501 : : {
502 : 50616 : d_quantEngine->notifyCombineTheories();
503 : : }
504 : : }
505 : : }
506 : : else
507 : : {
508 [ - + ][ - + ]: 8675198 : Assert(effort == Theory::EFFORT_STANDARD);
[ - - ]
509 : 8675198 : d_stats.d_stdEffortChecks++;
510 : : }
511 : :
512 : : // Interrupt in case we reached a resource limit.
513 [ - + ]: 8820465 : if (rm->out())
514 : : {
515 : 0 : interrupt();
516 : 0 : return;
517 : : }
518 : : }
519 : :
520 : : // Must consult quantifiers theory for last call to ensure sat, or otherwise
521 : : // add a lemma
522 [ + + ][ + + ]: 11199176 : if (Theory::fullEffort(effort) && !d_inConflict && !needCheck())
[ + + ][ + + ]
523 : : {
524 : 60507 : d_stats.d_lcEffortChecks++;
525 [ + - ]: 60507 : Trace("theory::assertions-model") << endl;
526 [ - + ]: 60507 : if (TraceIsOn("theory::assertions-model"))
527 : : {
528 : 0 : printAssertions("theory::assertions-model");
529 : : }
530 : : // reset the model in the combination engine
531 : 60507 : d_tc->resetModel();
532 : : // checks for theories requiring the model go at last call
533 [ + + ]: 907605 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
534 : : {
535 [ + + ]: 847098 : if (theoryId != THEORY_QUANTIFIERS)
536 : : {
537 : 786591 : Theory* theory = d_theoryTable[theoryId];
538 [ + - ][ + + ]: 786591 : if (theory && isTheoryEnabled(theoryId))
[ + + ]
539 : : {
540 [ + + ]: 493505 : if (theory->needsCheckLastEffort())
541 : : {
542 [ + + ]: 23170 : if (!d_tc->buildModel())
543 : : {
544 : : // We don't check if the model building fails, but for
545 : : // uniformity ask all theories needsCheckLastEffort method.
546 : 393 : continue;
547 : : }
548 : 22777 : theory->check(Theory::EFFORT_LAST_CALL);
549 : : }
550 : : }
551 : : }
552 : : }
553 [ + - ]: 60507 : if (!d_inConflict)
554 : : {
555 [ + + ]: 60507 : if (logicInfo().isQuantified())
556 : : {
557 : : // quantifiers engine must check at last call effort
558 : 51096 : d_quantEngine->check(Theory::EFFORT_LAST_CALL);
559 : : }
560 : : // notify the theory modules of the model
561 [ + + ]: 60903 : for (TheoryEngineModule* tem : d_modules)
562 : : {
563 [ + + ]: 415 : if (!tem->needsCandidateModel())
564 : : {
565 : : // module does not need candidate model
566 : 391 : continue;
567 : : }
568 [ - + ]: 24 : if (!d_tc->buildModel())
569 : : {
570 : : // model failed to build, we are done
571 : 0 : break;
572 : : }
573 : 24 : tem->notifyCandidateModel(getModel());
574 : : }
575 : : }
576 : : }
577 : :
578 [ + - ]: 22398314 : Trace("theory") << "TheoryEngine::check(" << effort << "): done, we are "
579 [ - - ]: 0 : << (d_inConflict ? "unsat" : "sat")
580 [ - - ]: 11199157 : << (d_lemmasAdded ? " with new lemmas"
581 : 11199157 : : " with no new lemmas");
582 [ + - ][ - - ]: 22398314 : Trace("theory") << ", need check = " << (needCheck() ? "YES" : "NO")
583 : 11199157 : << endl;
584 : :
585 : : // post check with the theory modules
586 [ + + ]: 11200940 : for (TheoryEngineModule* tem : d_modules)
587 : : {
588 : 1783 : tem->postCheck(effort);
589 : : }
590 [ + + ]: 11199157 : if (Theory::fullEffort(effort))
591 : : {
592 [ + + ][ + + ]: 175183 : if (!d_inConflict && !needCheck())
[ + + ]
593 : : {
594 : : // if some theory believes there is a conflict, but it is was not
595 : : // processed, we mark incomplete.
596 [ + + ]: 372030 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST;
597 : 347228 : ++theoryId)
598 : : {
599 : 347228 : Theory* theory = d_theoryTable[theoryId];
600 [ + - ][ + + ]: 347228 : if (theory && theory->getTheoryState() != nullptr)
[ + + ]
601 : : {
602 [ - + ]: 322426 : if (theory->getTheoryState()->isInConflict())
603 : : {
604 : 0 : setModelUnsound(theoryId,
605 : : IncompleteId::UNPROCESSED_THEORY_CONFLICT);
606 : 0 : DebugUnhandled()
607 : 0 : << "Unprocessed theory conflict from " << theoryId;
608 : : break;
609 : : }
610 : : }
611 : : }
612 : : // Do post-processing of model from the theories (e.g. used for
613 : : // THEORY_SEP to construct heap model)
614 : 24802 : d_tc->postProcessModel(d_modelUnsound.get());
615 : : }
616 : : }
617 : : }
618 [ - + ]: 12 : catch (const theory::Interrupted&)
619 : : {
620 [ + - ]: 12 : Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
621 : 12 : }
622 : : }
623 : :
624 : 8820465 : void TheoryEngine::propagate(Theory::Effort effort)
625 : : {
626 : : // Reset the interrupt flag
627 : 8820465 : d_interrupted = false;
628 : :
629 : : // Definition of the statement that is to be run by every theory
630 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
631 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
632 : : #endif
633 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
634 : : if (theory::TheoryTraits<THEORY>::hasPropagate && isTheoryEnabled(THEORY)) \
635 : : { \
636 : : theoryOf(THEORY)->propagate(effort); \
637 : : }
638 : :
639 : : // Reset the interrupt flag
640 : 8820465 : d_interrupted = false;
641 : :
642 : : // Propagate for each theory using the statement above
643 [ + + ][ + + ]: 8820465 : CVC5_FOR_EACH_THEORY;
644 : 8820465 : }
645 : :
646 : 7363917 : Node TheoryEngine::getNextDecisionRequest()
647 : : {
648 : 7363917 : return d_decManager->getNextDecisionRequest();
649 : : }
650 : :
651 : 198211 : bool TheoryEngine::properConflict(TNode conflict) const
652 : : {
653 : : bool value;
654 [ + + ]: 198211 : if (conflict.getKind() == Kind::AND)
655 : : {
656 [ + + ]: 2231952 : for (unsigned i = 0; i < conflict.getNumChildren(); ++i)
657 : : {
658 [ - + ]: 2035178 : if (!getPropEngine()->hasValue(conflict[i], value))
659 : : {
660 [ - - ]: 0 : Trace("properConflict")
661 : 0 : << "Bad conflict is due to unassigned atom: " << conflict[i]
662 : 0 : << endl;
663 : 0 : return false;
664 : : }
665 [ - + ]: 2035178 : if (!value)
666 : : {
667 [ - - ]: 0 : Trace("properConflict")
668 : 0 : << "Bad conflict is due to false atom: " << conflict[i] << endl;
669 : 0 : return false;
670 : : }
671 [ - + ]: 2035178 : if (conflict[i] != rewrite(conflict[i]))
672 : : {
673 [ - - ]: 0 : Trace("properConflict")
674 [ - - ]: 0 : << "Bad conflict is due to atom not in normal form: " << conflict[i]
675 : 0 : << " vs " << rewrite(conflict[i]) << endl;
676 : 0 : return false;
677 : : }
678 : : }
679 : : }
680 : : else
681 : : {
682 [ - + ]: 1437 : if (!getPropEngine()->hasValue(conflict, value))
683 : : {
684 [ - - ]: 0 : Trace("properConflict")
685 : 0 : << "Bad conflict is due to unassigned atom: " << conflict << endl;
686 : 0 : return false;
687 : : }
688 [ - + ]: 1437 : if (!value)
689 : : {
690 [ - - ]: 0 : Trace("properConflict")
691 : 0 : << "Bad conflict is due to false atom: " << conflict << endl;
692 : 0 : return false;
693 : : }
694 [ - + ]: 1437 : if (conflict != rewrite(conflict))
695 : : {
696 [ - - ]: 0 : Trace("properConflict")
697 : 0 : << "Bad conflict is due to atom not in normal form: " << conflict
698 : 0 : << " vs " << rewrite(conflict) << endl;
699 : 0 : return false;
700 : : }
701 : : }
702 : 198211 : return true;
703 : : }
704 : :
705 : 1897173 : TheoryModel* TheoryEngine::getModel()
706 : : {
707 [ - + ][ - + ]: 1897173 : Assert(d_tc != nullptr);
[ - - ]
708 : 1897173 : TheoryModel* m = d_tc->getModel();
709 [ - + ][ - + ]: 1897173 : Assert(m != nullptr);
[ - - ]
710 : 1897173 : return m;
711 : : }
712 : :
713 : 24746 : TheoryModel* TheoryEngine::getBuiltModel()
714 : : {
715 [ - + ][ - + ]: 24746 : Assert(d_tc != nullptr);
[ - - ]
716 : : // If this method was called, produceModels should be true.
717 [ - + ][ - + ]: 24746 : AlwaysAssert(options().smt.produceModels);
[ - - ]
718 : : // we must build model at this point
719 [ - + ]: 24746 : if (!d_tc->buildModel())
720 : : {
721 : 0 : return nullptr;
722 : : }
723 : 24746 : return d_tc->getModel();
724 : : }
725 : :
726 : 25545 : bool TheoryEngine::buildModel()
727 : : {
728 [ - + ][ - + ]: 25545 : Assert(d_tc != nullptr);
[ - - ]
729 : 25545 : return d_tc->buildModel();
730 : : }
731 : :
732 : 197190925 : bool TheoryEngine::isTheoryEnabled(theory::TheoryId theoryId) const
733 : : {
734 : 197190925 : return logicInfo().isTheoryEnabled(theoryId);
735 : : }
736 : :
737 : 70185589 : theory::TheoryId TheoryEngine::theoryExpPropagation(theory::TheoryId tid) const
738 : : {
739 [ + + ]: 70185589 : if (options().theory.eeMode == options::EqEngineMode::CENTRAL)
740 : : {
741 : 32955 : if (EqEngineManagerCentral::usesCentralEqualityEngine(options(), tid)
742 [ + + ][ + + ]: 32955 : && Theory::expUsingCentralEqualityEngine(tid))
[ + + ]
743 : : {
744 : 12762 : return THEORY_BUILTIN;
745 : : }
746 : : }
747 : 70172827 : return tid;
748 : : }
749 : :
750 : 50795 : bool TheoryEngine::presolve()
751 : : {
752 : : // Reset the interrupt flag
753 : 50795 : d_interrupted = false;
754 : :
755 : : // Reset the decision manager. This clears its decision strategies that are
756 : : // no longer valid in this user context.
757 : 50795 : d_decManager->presolve();
758 : :
759 : : try
760 : : {
761 : : // Definition of the statement that is to be run by every theory
762 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
763 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
764 : : #endif
765 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
766 : : if (theory::TheoryTraits<THEORY>::hasPresolve) \
767 : : { \
768 : : theoryOf(THEORY)->presolve(); \
769 : : if (d_inConflict) \
770 : : { \
771 : : return true; \
772 : : } \
773 : : }
774 : :
775 : : // Presolve for each theory using the statement above
776 [ + + ][ - + ]: 50795 : CVC5_FOR_EACH_THEORY;
[ - + ][ - + ]
[ - + ][ - + ]
[ - + ][ - + ]
[ - + ]
777 : : }
778 [ - - ]: 0 : catch (const theory::Interrupted&)
779 : : {
780 [ - - ]: 0 : Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
781 : 0 : }
782 : : // presolve with the theory engine modules as well
783 [ + + ]: 51304 : for (TheoryEngineModule* tem : d_modules)
784 : : {
785 : 511 : tem->presolve();
786 : : }
787 : :
788 : : // return whether we have a conflict
789 : 50793 : return false;
790 : : } /* TheoryEngine::presolve() */
791 : :
792 : 50779 : void TheoryEngine::postsolve(prop::SatValue result)
793 : : {
794 : : // postsolve with the theory engine modules as well
795 [ + + ]: 51290 : for (TheoryEngineModule* tem : d_modules)
796 : : {
797 : 511 : tem->postsolve(result);
798 : : }
799 : :
800 : : // Reset the interrupt flag
801 : 50779 : d_interrupted = false;
802 : 50779 : }
803 : :
804 : 4953 : void TheoryEngine::notifyRestart()
805 : : {
806 : : // Reset the interrupt flag
807 : 4953 : d_interrupted = false;
808 : :
809 : : // Definition of the statement that is to be run by every theory
810 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
811 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
812 : : #endif
813 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
814 : : if (theory::TheoryTraits<THEORY>::hasNotifyRestart \
815 : : && isTheoryEnabled(THEORY)) \
816 : : { \
817 : : theoryOf(THEORY)->notifyRestart(); \
818 : : }
819 : :
820 : : // notify each theory using the statement above
821 [ + + ]: 4953 : CVC5_FOR_EACH_THEORY;
822 : 4953 : }
823 : :
824 : 346565 : void TheoryEngine::ppStaticLearn(TNode in, std::vector<TrustNode>& learned)
825 : : {
826 : : // Reset the interrupt flag
827 : 346565 : d_interrupted = false;
828 : :
829 : : // Definition of the statement that is to be run by every theory
830 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
831 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
832 : : #endif
833 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
834 : : if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) \
835 : : { \
836 : : theoryOf(THEORY)->ppStaticLearn(in, learned); \
837 : : }
838 : :
839 : : // static learning for each theory using the statement above
840 : 346565 : CVC5_FOR_EACH_THEORY;
841 : 346565 : }
842 : :
843 : 326819 : bool TheoryEngine::hasSatValue(TNode n, bool& value) const
844 : : {
845 [ + + ]: 326819 : if (d_propEngine->isSatLiteral(n))
846 : : {
847 : 326706 : return d_propEngine->hasValue(n, value);
848 : : }
849 : 113 : return false;
850 : : }
851 : :
852 : 1909989 : bool TheoryEngine::hasSatValue(TNode n) const
853 : : {
854 [ + + ]: 1909989 : if (d_propEngine->isSatLiteral(n))
855 : : {
856 : : bool value;
857 : 1909053 : return d_propEngine->hasValue(n, value);
858 : : }
859 : 936 : return false;
860 : : }
861 : :
862 : 1726 : bool TheoryEngine::isRelevant(Node lit) const
863 : : {
864 [ + - ]: 1726 : if (d_relManager != nullptr)
865 : : {
866 : 1726 : return d_relManager->isRelevant(lit);
867 : : }
868 : : // otherwise must assume its relevant
869 : 0 : return true;
870 : : }
871 : :
872 : 53751 : bool TheoryEngine::isLegalElimination(TNode x, TNode val)
873 : : {
874 [ - + ][ - + ]: 53751 : Assert(x.isVar());
[ - - ]
875 [ + + ]: 53751 : if (expr::hasSubterm(val, x))
876 : : {
877 : 13121 : return false;
878 : : }
879 [ - + ]: 121890 : if (!CVC5_EQUAL(val.getType(), x.getType()))
880 : : {
881 : 0 : return false;
882 : : }
883 [ + + ][ + + ]: 40630 : if (!options().smt.produceModels || options().smt.modelVarElimUneval)
[ + + ]
884 : : {
885 : : // Don't care about the model, or we allow variables to be eliminated by
886 : : // unevaluatable terms, we can eliminate. Notice that when
887 : : // options().smt.modelVarElimUneval is true, val may contain unevaluatable
888 : : // kinds. This means that e.g. a Boolean variable may be eliminated based on
889 : : // an equality (= b (forall ((x)) (P x))), where its model value is (forall
890 : : // ((x)) (P x)).
891 : 40626 : return true;
892 : : }
893 : : // If models are enabled, then it depends on whether the term contains any
894 : : // unevaluable operators like FORALL, SINE, etc. Having such operators makes
895 : : // model construction contain non-constant values for variables, which is
896 : : // not ideal from a user perspective.
897 : : // We also insist on this check since the term to eliminate should never
898 : : // contain quantifiers, or else variable shadowing issues may arise.
899 : : // there should be a model object
900 : 4 : TheoryModel* tm = getModel();
901 [ - + ][ - + ]: 4 : Assert(tm != nullptr);
[ - - ]
902 : 4 : return tm->isLegalElimination(val);
903 : : }
904 : :
905 : 215569 : bool TheoryEngine::solve(TrustNode tliteral,
906 : : TrustSubstitutionMap& substitutionOut)
907 : : {
908 [ - + ][ - + ]: 215569 : Assert(tliteral.getKind() == TrustNodeKind::LEMMA);
[ - - ]
909 : : // Reset the interrupt flag
910 : 215569 : d_interrupted = false;
911 : :
912 : 215569 : TNode literal = tliteral.getNode();
913 [ + + ]: 215569 : TNode atom = literal.getKind() == Kind::NOT ? literal[0] : literal;
914 [ + - ]: 431138 : Trace("theory::solve") << "TheoryEngine::solve(" << literal
915 [ - + ][ - - ]: 215569 : << "): solving with " << theoryOf(atom)->getId()
916 : 215569 : << endl;
917 : :
918 : 215569 : TheoryId tid = d_env.theoryOf(atom);
919 : : // Note that ppAssert is called before ppRewrite.
920 [ + + ][ + - ]: 215569 : if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
[ + + ]
921 : : {
922 : : // don't throw an exception yet
923 : : // Instead ppStaticRewrite will be called on atom, which may throw an
924 : : // exception if the term is not rewritten.
925 : 12 : return false;
926 : : }
927 : :
928 : 215557 : bool solveStatus = d_theoryTable[tid]->ppAssert(tliteral, substitutionOut);
929 [ + - ]: 431114 : Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => "
930 : 215557 : << solveStatus << endl;
931 : 215557 : return solveStatus;
932 : 215569 : }
933 : :
934 : 4767450 : TrustNode TheoryEngine::ppRewrite(TNode term,
935 : : std::vector<theory::SkolemLemma>& lems)
936 : : {
937 [ - + ][ - + ]: 4767450 : Assert(lems.empty());
[ - - ]
938 : 4767450 : TheoryId tid = d_env.theoryOf(term);
939 : : // We check whether the theory is enabled here (instead of only during solve),
940 : : // since there are corner cases where facts may involve terms that belong
941 : : // to other theories, e.g. equalities between variables belong to UF when
942 : : // theoryof-mode is `term`.
943 [ - + ][ - - ]: 4767450 : if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
[ - + ]
944 : : {
945 : 0 : stringstream ss;
946 : 0 : ss << "The logic was specified as " << logicInfo().getLogicString()
947 : 0 : << ", which doesn't include " << tid
948 : 0 : << ", but got a term for that theory during solving." << std::endl
949 : 0 : << "The term:" << std::endl
950 : 0 : << term;
951 : 0 : throw LogicException(ss.str());
952 : 0 : }
953 : 4767459 : TrustNode trn = d_theoryTable[tid]->ppRewrite(term, lems);
954 : : // should never introduce a skolem to eliminate an equality
955 [ + + ][ + - ]: 4767441 : Assert(lems.empty() || term.getKind() != Kind::EQUAL);
[ - + ][ - + ]
[ - - ]
956 [ + + ]: 4767441 : if (!isProofEnabled())
957 : : {
958 : 2715814 : return trn;
959 : : }
960 [ - + ][ - + ]: 2051627 : Assert(d_lazyProof != nullptr);
[ - - ]
961 : : // if proofs are enabled, must ensure we have proofs for all the skolem lemmas
962 [ + + ]: 2054879 : for (SkolemLemma& skl : lems)
963 : : {
964 : 3252 : TrustNode tskl = skl.d_lemma;
965 [ - + ][ - + ]: 3252 : Assert(tskl.getKind() == TrustNodeKind::LEMMA);
[ - - ]
966 [ + + ]: 3252 : if (tskl.getGenerator() == nullptr)
967 : : {
968 : 1016 : Node proven = tskl.getProven();
969 : : Node tidn =
970 : 1016 : builtin::BuiltinProofRuleChecker::mkTheoryIdNode(nodeManager(), tid);
971 : 2032 : d_lazyProof->addTrustedStep(
972 : : proven, TrustId::THEORY_PREPROCESS_LEMMA, {}, {tidn});
973 [ + - ]: 1016 : skl.d_lemma = TrustNode::mkTrustLemma(proven, d_lazyProof.get());
974 : 1016 : }
975 : 3252 : }
976 : : // notice that we don't ensure proofs are processed for the returned (rewrite)
977 : : // trust node, this is the responsibility of the caller, i.e. theory
978 : : // preprocessor.
979 : 2051627 : return trn;
980 : 0 : }
981 : :
982 : 3692868 : TrustNode TheoryEngine::ppStaticRewrite(TNode term)
983 : : {
984 : 3692868 : TheoryId tid = d_env.theoryOf(term);
985 [ + + ][ + - ]: 3692868 : if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
[ + + ]
986 : : {
987 : : // If the theory is not enabled, then we require eliminating the term
988 : : // here.
989 : 11 : TrustNode tret = d_theoryTable[THEORY_BUILTIN]->ppStaticRewrite(term);
990 [ + + ]: 11 : if (!tret.isNull())
991 : : {
992 : 8 : return tret;
993 : : }
994 : 3 : stringstream ss;
995 : 3 : ss << "The logic was specified as " << logicInfo().getLogicString()
996 : 6 : << ", which doesn't include " << tid
997 : 3 : << ", but got a preprocessing-time term for that theory." << std::endl
998 : 3 : << "The term:" << std::endl
999 : 3 : << term;
1000 : 3 : throw LogicException(ss.str());
1001 : 14 : }
1002 : 3692857 : return d_theoryTable[tid]->ppStaticRewrite(term);
1003 : : }
1004 : :
1005 : 65951 : void TheoryEngine::notifyPreprocessedAssertions(
1006 : : const std::vector<Node>& assertions)
1007 : : {
1008 : : // call all the theories
1009 [ + + ]: 989265 : for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
1010 : 923314 : ++theoryId)
1011 : : {
1012 [ + - ]: 923314 : if (d_theoryTable[theoryId])
1013 : : {
1014 : 923314 : theoryOf(theoryId)->ppNotifyAssertions(assertions);
1015 : : }
1016 : : }
1017 [ + + ]: 65951 : if (d_relManager != nullptr)
1018 : : {
1019 : 483 : d_relManager->notifyPreprocessedAssertions(assertions, true);
1020 : : }
1021 : 65951 : }
1022 : :
1023 : 69856302 : bool TheoryEngine::markPropagation(TNode assertion,
1024 : : TNode originalAssertion,
1025 : : theory::TheoryId toTheoryId,
1026 : : theory::TheoryId fromTheoryId)
1027 : : {
1028 : : // What and where we are asserting
1029 : 69856302 : NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
1030 : : // What and where it came from
1031 : : NodeTheoryPair toExplain(
1032 : 69856302 : originalAssertion, fromTheoryId, d_propagationMapTimestamp);
1033 : :
1034 : : // See if the theory already got this literal
1035 : 69856302 : PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
1036 [ + + ]: 69856302 : if (find != d_propagationMap.end())
1037 : : {
1038 : : // The theory already knows this
1039 [ + - ]: 39326430 : Trace("theory::assertToTheory")
1040 : 19663215 : << "TheoryEngine::markPropagation(): already there" << endl;
1041 : 19663215 : return false;
1042 : : }
1043 : :
1044 [ + - ]: 100386174 : Trace("theory::assertToTheory")
1045 : 0 : << "TheoryEngine::markPropagation(): marking ["
1046 : 0 : << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId
1047 : 50193087 : << " from " << originalAssertion << ", " << fromTheoryId << endl;
1048 : :
1049 : : // Mark the propagation
1050 : 50193087 : d_propagationMap[toAssert] = toExplain;
1051 : 50193087 : d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
1052 : :
1053 : 50193087 : return true;
1054 : 69856302 : }
1055 : :
1056 : 85824543 : void TheoryEngine::assertToTheory(TNode assertion,
1057 : : TNode originalAssertion,
1058 : : theory::TheoryId toTheoryId,
1059 : : theory::TheoryId fromTheoryId)
1060 : : {
1061 [ + - ]: 171649086 : Trace("theory::assertToTheory")
1062 : 0 : << "TheoryEngine::assertToTheory(" << assertion << ", "
1063 : 0 : << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")"
1064 : 85824543 : << endl;
1065 : :
1066 [ - + ][ - + ]: 85824543 : Assert(toTheoryId != fromTheoryId);
[ - - ]
1067 [ + + ][ - + ]: 85824543 : if (toTheoryId != THEORY_SAT_SOLVER && !isTheoryEnabled(toTheoryId))
[ - + ]
1068 : : {
1069 : 0 : stringstream ss;
1070 : 0 : ss << "The logic was specified as " << logicInfo().getLogicString()
1071 : 0 : << ", which doesn't include " << toTheoryId
1072 : 0 : << ", but got an asserted fact to that theory." << endl
1073 : 0 : << "The fact:" << endl
1074 : 0 : << assertion;
1075 : 0 : throw LogicException(ss.str());
1076 : 0 : }
1077 : :
1078 [ + + ]: 85824543 : if (d_inConflict)
1079 : : {
1080 : 183887 : return;
1081 : : }
1082 : :
1083 : : // If sharing is disabled, things are easy
1084 [ + + ]: 85640656 : if (!logicInfo().isSharingEnabled())
1085 : : {
1086 [ - + ][ - + ]: 15784354 : Assert(assertion == originalAssertion);
[ - - ]
1087 [ + + ]: 15784354 : if (fromTheoryId == THEORY_SAT_SOLVER)
1088 : : {
1089 : : // Send to the apropriate theory
1090 : 11409867 : theory::Theory* toTheory = theoryOf(toTheoryId);
1091 : : // We assert it, and we know it's preregistereed
1092 : 11409867 : toTheory->assertFact(assertion, true);
1093 : : // Mark that we have more information
1094 : 11409867 : d_factsAsserted = true;
1095 : : }
1096 : : else
1097 : : {
1098 [ - + ][ - + ]: 4374487 : Assert(toTheoryId == THEORY_SAT_SOLVER);
[ - - ]
1099 : : // Check for propositional conflict
1100 : : bool value;
1101 [ + + ]: 4374487 : if (d_propEngine->hasValue(assertion, value))
1102 : : {
1103 [ + + ]: 3173989 : if (!value)
1104 : : {
1105 [ + - ]: 131978 : Trace("theory::propagate")
1106 : 0 : << "TheoryEngine::assertToTheory(" << assertion << ", "
1107 : 0 : << toTheoryId << ", " << fromTheoryId
1108 : 65989 : << "): conflict (no sharing)" << endl;
1109 [ + - ]: 131978 : Trace("dtview::conflict")
1110 : 65989 : << ":THEORY-CONFLICT: " << assertion << std::endl;
1111 : 65989 : markInConflict();
1112 : : }
1113 : : else
1114 : : {
1115 : 3108000 : return;
1116 : : }
1117 : : }
1118 : 1266487 : d_propagatedLiterals.push_back(assertion);
1119 : : }
1120 : 12676354 : return;
1121 : : }
1122 : :
1123 : : // determine the actual theory that will process/explain the fact, which is
1124 : : // THEORY_BUILTIN if the theory uses the central equality engine
1125 : 69856302 : TheoryId toTheoryIdProp = theoryExpPropagation(toTheoryId);
1126 : : // If sending to the shared solver, it's also simple
1127 [ + + ]: 69856302 : if (toTheoryId == THEORY_BUILTIN)
1128 : : {
1129 [ + + ]: 22741691 : if (markPropagation(
1130 : : assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
1131 : : {
1132 : : // assert to the shared solver
1133 : 12653554 : bool polarity = assertion.getKind() != Kind::NOT;
1134 [ + + ]: 12653554 : TNode atom = polarity ? assertion : assertion[0];
1135 : 12653554 : d_sharedSolver->assertShared(atom, polarity, assertion);
1136 : 12653554 : }
1137 : 22741691 : return;
1138 : : }
1139 : :
1140 : : // Things from the SAT solver are already normalized, so they go
1141 : : // directly to the apropriate theory
1142 [ + + ]: 47114611 : if (fromTheoryId == THEORY_SAT_SOLVER)
1143 : : {
1144 : : // We know that this is normalized, so just send it off to the theory
1145 [ + + ]: 17094919 : if (markPropagation(
1146 : : assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
1147 : : {
1148 : : // Is it preregistered
1149 [ - - ]: 16960504 : bool preregistered = d_propEngine->isSatLiteral(assertion)
1150 [ + + ][ + + ]: 16960504 : && d_env.theoryOf(assertion) == toTheoryId;
[ + + ][ + - ]
[ - - ]
1151 : : // We assert it
1152 : 16960504 : theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1153 : : // Mark that we have more information
1154 : 16960504 : d_factsAsserted = true;
1155 : : }
1156 : 17094919 : return;
1157 : : }
1158 : :
1159 : : // Propagations to the SAT solver are just enqueued for pickup by
1160 : : // the SAT solver later
1161 [ + + ]: 30019692 : if (toTheoryId == THEORY_SAT_SOLVER)
1162 : : {
1163 [ - + ][ - + ]: 22735965 : Assert(toTheoryIdProp == toTheoryId);
[ - - ]
1164 [ + + ]: 22735965 : if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId))
1165 : : {
1166 : : // Enqueue for propagation to the SAT solver
1167 : 13936646 : d_propagatedLiterals.push_back(assertion);
1168 : : // Check for propositional conflicts
1169 : : bool value;
1170 [ + + ][ + + ]: 13936646 : if (d_propEngine->hasValue(assertion, value) && !value)
[ + - ][ + + ]
[ - - ]
1171 : : {
1172 [ + - ]: 208690 : Trace("theory::propagate")
1173 : 0 : << "TheoryEngine::assertToTheory(" << assertion << ", "
1174 : 0 : << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)"
1175 : 104345 : << endl;
1176 [ + - ]: 208690 : Trace("dtview::conflict")
1177 : 104345 : << ":THEORY-CONFLICT: " << assertion << std::endl;
1178 : 104345 : markInConflict();
1179 : : }
1180 : : }
1181 : 22735965 : return;
1182 : : }
1183 : :
1184 : 7283727 : Assert(assertion.getKind() == Kind::EQUAL
1185 : : || (assertion.getKind() == Kind::NOT
1186 : : && assertion[0].getKind() == Kind::EQUAL));
1187 : :
1188 : : // Normalize
1189 : 7283727 : Node normalizedLiteral = rewrite(assertion);
1190 : :
1191 : : // See if it rewrites false directly -> conflict
1192 [ + + ]: 7283727 : if (normalizedLiteral.isConst())
1193 : : {
1194 [ + + ]: 47271 : if (!normalizedLiteral.getConst<bool>())
1195 : : {
1196 : : // Mark the propagation for explanations
1197 [ + - ]: 1037 : if (markPropagation(normalizedLiteral,
1198 : : originalAssertion,
1199 : : toTheoryIdProp,
1200 : : fromTheoryId))
1201 : : {
1202 : : // special case, trust node has no proof generator
1203 : 1037 : TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
1204 : : // Get the explanation (conflict will figure out where it came from)
1205 : 1037 : conflict(trnn, InferenceId::CONFLICT_REWRITE_LIT, toTheoryId);
1206 : 1037 : }
1207 : : else
1208 : : {
1209 : 0 : Unreachable();
1210 : : }
1211 : 1037 : return;
1212 : : }
1213 : : }
1214 : :
1215 : : // Try and assert (note that we assert the non-normalized one)
1216 [ + + ]: 7282690 : if (markPropagation(
1217 : : assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
1218 : : {
1219 : : // Check if has been pre-registered with the theory
1220 [ - - ]: 6641346 : bool preregistered = d_propEngine->isSatLiteral(assertion)
1221 [ + + ][ + + ]: 6641346 : && d_env.theoryOf(assertion) == toTheoryId;
[ + + ][ + - ]
[ - - ]
1222 : : // Assert away
1223 : 6641346 : theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1224 : 6641346 : d_factsAsserted = true;
1225 : : }
1226 : :
1227 : 7282690 : return;
1228 : 7283727 : }
1229 : :
1230 : 28438843 : void TheoryEngine::assertFact(TNode literal)
1231 : : {
1232 [ + - ]: 28438843 : Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
1233 : :
1234 : : // spendResource();
1235 : :
1236 : : // If we're in conflict, nothing to do
1237 [ + + ]: 28438843 : if (d_inConflict)
1238 : : {
1239 : 40419 : return;
1240 : : }
1241 : :
1242 : : // Get the atom
1243 : 28398424 : bool polarity = literal.getKind() != Kind::NOT;
1244 [ + + ]: 28398424 : TNode atom = polarity ? literal : literal[0];
1245 : :
1246 [ + + ]: 28398424 : if (logicInfo().isSharingEnabled())
1247 : : {
1248 : : // If any shared terms, it's time to do sharing work
1249 : 16988558 : d_sharedSolver->preNotifySharedFact(atom);
1250 : :
1251 : : // If it's an equality, assert it to the shared term manager, even though
1252 : : // the terms are not yet shared. As the terms become shared later, the
1253 : : // shared terms manager will then add them to the assert the equality to the
1254 : : // interested theories
1255 [ + + ]: 16988556 : if (atom.getKind() == Kind::EQUAL)
1256 : : {
1257 : : // Assert it to the the owning theory
1258 : 9184853 : assertToTheory(literal,
1259 : : literal,
1260 : 9184853 : /* to */ d_env.theoryOf(atom),
1261 : : /* from */ THEORY_SAT_SOLVER);
1262 : : // Shared terms manager will assert to interested theories directly, as
1263 : : // the terms become shared
1264 : 9184853 : assertToTheory(literal,
1265 : : literal,
1266 : : /* to */ THEORY_BUILTIN,
1267 : : /* from */ THEORY_SAT_SOLVER);
1268 : :
1269 : : // Now, let's check for any atom triggers from lemmas
1270 : 9184853 : AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
1271 [ + + ]: 9227351 : while (!it.done())
1272 : : {
1273 : 42498 : const AtomRequests::Request& request = it.get();
1274 : : Node toAssert =
1275 [ + + ]: 42498 : polarity ? (Node)request.d_atom : request.d_atom.notNode();
1276 [ + - ]: 84996 : Trace("theory::atoms") << "TheoryEngine::assertFact(" << literal
1277 : 42498 : << "): sending requested " << toAssert << endl;
1278 : 42498 : assertToTheory(
1279 : 42498 : toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
1280 [ + + ]: 42498 : if (options().theory.eeMode == options::EqEngineMode::CENTRAL)
1281 : : {
1282 : : // Also send to THEORY_BUILTIN, similar to above
1283 : 48 : assertToTheory(toAssert,
1284 : : literal,
1285 : : /* to */ THEORY_BUILTIN,
1286 : : /* from */ THEORY_SAT_SOLVER);
1287 : : }
1288 : 42498 : it.next();
1289 : 42498 : }
1290 : : }
1291 : : else
1292 : : {
1293 : : // Not an equality, just assert to the appropriate theory
1294 : 7803703 : assertToTheory(literal,
1295 : : literal,
1296 : 7803703 : /* to */ d_env.theoryOf(atom),
1297 : : /* from */ THEORY_SAT_SOLVER);
1298 : : }
1299 : : }
1300 : : else
1301 : : {
1302 : : // Assert the fact to the appropriate theory directly
1303 : 11409867 : assertToTheory(literal,
1304 : : literal,
1305 : 11409867 : /* to */ d_env.theoryOf(atom),
1306 : : /* from */ THEORY_SAT_SOLVER);
1307 : : }
1308 : 28398424 : }
1309 : :
1310 : 31959055 : bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory)
1311 : : {
1312 [ + - ]: 63918110 : Trace("theory::propagate")
1313 : 31959055 : << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
1314 : :
1315 : 63918110 : Trace("dtview::prop") << std::string(context()->getLevel(), ' ')
1316 : 31959055 : << ":THEORY-PROP: " << literal << endl;
1317 : :
1318 : : // spendResource();
1319 : :
1320 : : // Get the atom
1321 : 31959055 : bool polarity = literal.getKind() != Kind::NOT;
1322 [ + + ]: 31959055 : TNode atom = polarity ? literal : literal[0];
1323 : :
1324 [ + + ][ + + ]: 31959055 : if (logicInfo().isSharingEnabled() && atom.getKind() == Kind::EQUAL)
[ + + ]
1325 : : {
1326 [ + + ]: 23240880 : if (d_propEngine->isSatLiteral(literal))
1327 : : {
1328 : : // We propagate SAT literals to SAT
1329 : 18488530 : assertToTheory(
1330 : : literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1331 : : }
1332 [ + + ]: 23240880 : if (theory != THEORY_BUILTIN)
1333 : : {
1334 : : // Assert to the shared terms database
1335 : 13635333 : assertToTheory(
1336 : : literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
1337 : : }
1338 : : }
1339 : : else
1340 : : {
1341 : : // Just send off to the SAT solver
1342 [ - + ][ - + ]: 8718175 : Assert(d_propEngine->isSatLiteral(literal));
[ - - ]
1343 : 8718175 : assertToTheory(
1344 : : literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1345 : : }
1346 : :
1347 : 63918110 : return !d_inConflict;
1348 : 31959055 : }
1349 : :
1350 : 2160243 : theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b)
1351 : : {
1352 [ - + ][ - + ]: 6480729 : AssertEqual(a.getType(), b.getType());
[ - - ]
1353 : 2160243 : return d_sharedSolver->getEqualityStatus(a, b);
1354 : : }
1355 : :
1356 : 454 : void TheoryEngine::getDifficultyMap(std::map<Node, Node>& dmap,
1357 : : bool includeLemmas)
1358 : : {
1359 [ - + ][ - + ]: 454 : Assert(d_relManager != nullptr);
[ - - ]
1360 : 454 : d_relManager->getDifficultyMap(dmap, includeLemmas);
1361 : 454 : }
1362 : :
1363 : 1765 : theory::IncompleteId TheoryEngine::getModelUnsoundId() const
1364 : : {
1365 : 1765 : return d_modelUnsoundId.get();
1366 : : }
1367 : 23 : theory::IncompleteId TheoryEngine::getRefutationUnsoundId() const
1368 : : {
1369 : 23 : return d_refutationUnsoundId.get();
1370 : : }
1371 : :
1372 : 12493 : Node TheoryEngine::getCandidateModelValue(TNode var)
1373 : : {
1374 [ + + ]: 12493 : if (var.isConst())
1375 : : {
1376 : : // the model value of a constant must be itself
1377 : 18 : return var;
1378 : : }
1379 [ - + ][ - - ]: 24950 : Assert(d_sharedSolver->isShared(var))
1380 [ - + ][ - + ]: 12475 : << "node " << var << " is not shared" << std::endl;
[ - - ]
1381 : 12475 : return theoryOf(d_env.theoryOf(var.getType()))->getCandidateModelValue(var);
1382 : : }
1383 : :
1384 : 0 : std::unordered_set<TNode> TheoryEngine::getRelevantAssertions(bool& success)
1385 : : {
1386 : : // if there is no relevance manager, we fail
1387 [ - - ]: 0 : if (d_relManager == nullptr)
1388 : : {
1389 : 0 : success = false;
1390 : : // return empty set
1391 : 0 : return std::unordered_set<TNode>();
1392 : : }
1393 : 0 : return d_relManager->getRelevantAssertions(success);
1394 : : }
1395 : :
1396 : 251983 : TrustNode TheoryEngine::getExplanation(TNode node)
1397 : : {
1398 [ + - ]: 503966 : Trace("theory::explain") << "TheoryEngine::getExplanation(" << node
1399 : 0 : << "): current propagation index = "
1400 : 251983 : << d_propagationMapTimestamp << endl;
1401 : 251983 : bool polarity = node.getKind() != Kind::NOT;
1402 [ + + ]: 251983 : TNode atom = polarity ? node : node[0];
1403 : :
1404 : : // If we're not in shared mode, explanations are simple
1405 : 251983 : TrustNode texplanation;
1406 [ + + ]: 251983 : if (!logicInfo().isSharingEnabled())
1407 : : {
1408 [ + - ]: 171360 : Trace("theory::explain")
1409 : 0 : << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1410 [ - + ][ - - ]: 85680 : << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl;
1411 : :
1412 : 85680 : texplanation = theoryOf(atom)->explain(node);
1413 : 85680 : Node explanation = texplanation.getNode();
1414 [ + - ]: 171360 : Trace("theory::explain") << "TheoryEngine::getExplanation(" << node
1415 : 85680 : << ") => " << explanation << endl;
1416 [ + + ]: 85680 : if (isProofEnabled())
1417 : : {
1418 : 40162 : texplanation.debugCheckClosed(
1419 : : options(), "te-proof-exp", "texplanation no share", false);
1420 : : // check if no generator, if so, add THEORY_LEMMA
1421 [ - + ]: 40162 : if (texplanation.getGenerator() == nullptr)
1422 : : {
1423 : 0 : Node proven = texplanation.getProven();
1424 : 0 : TheoryId tid = theoryOf(atom)->getId();
1425 : : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(
1426 : 0 : nodeManager(), tid);
1427 : 0 : d_lazyProof->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn});
1428 : : texplanation =
1429 [ - - ]: 0 : TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get());
1430 : 0 : }
1431 : : }
1432 : 85680 : }
1433 : : else
1434 : : {
1435 [ + - ]: 332606 : Trace("theory::explain")
1436 : 166303 : << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
1437 : :
1438 : : // Initial thing to explain
1439 : : NodeTheoryPair toExplain(
1440 : 166303 : node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
1441 [ - + ][ - + ]: 166303 : Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
[ - - ]
1442 : :
1443 : 166303 : NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
1444 [ + - ]: 332606 : Trace("theory::explain")
1445 : 0 : << "TheoryEngine::getExplanation: explainer for node "
1446 : 0 : << nodeExplainerPair.d_node
1447 : 166303 : << " is theory: " << nodeExplainerPair.d_theory << std::endl;
1448 : :
1449 : : // Create the workplace for explanations
1450 : 498909 : std::vector<NodeTheoryPair> vec{d_propagationMap[toExplain]};
1451 : : // Process the explanation
1452 : 166303 : texplanation = getExplanation(vec);
1453 [ + - ]: 332606 : Trace("theory::explain") << "TheoryEngine::getExplanation(" << node
1454 [ - + ][ - - ]: 166303 : << ") => " << texplanation.getNode() << endl;
1455 : 166303 : }
1456 : : // notify the conflict as a lemma
1457 [ + + ]: 252019 : for (TheoryEngineModule* tem : d_modules)
1458 : : {
1459 : 36 : tem->notifyLemma(texplanation.getProven(),
1460 : : InferenceId::EXPLAINED_PROPAGATION,
1461 : : LemmaProperty::NONE,
1462 : : {},
1463 : : {});
1464 : : }
1465 : 503966 : return texplanation;
1466 : 251983 : }
1467 : :
1468 : : struct AtomsCollect
1469 : : {
1470 : : std::vector<TNode> d_atoms;
1471 : : std::unordered_set<TNode> d_visited;
1472 : :
1473 : : public:
1474 : : typedef void return_type;
1475 : :
1476 : 1013408 : bool alreadyVisited(TNode current, CVC5_UNUSED TNode parent)
1477 : : {
1478 : : // Check if already visited
1479 [ + + ]: 1013408 : if (d_visited.find(current) != d_visited.end()) return true;
1480 : : // Don't visit non-boolean
1481 [ + + ]: 930452 : if (!current.getType().isBoolean()) return true;
1482 : : // New node
1483 : 760718 : return false;
1484 : : }
1485 : :
1486 : 254010 : void visit(TNode current, CVC5_UNUSED TNode parent)
1487 : : {
1488 [ + + ]: 254010 : if (Theory::theoryOf(current) != theory::THEORY_BOOL)
1489 : : {
1490 : 86780 : d_atoms.push_back(current);
1491 : : }
1492 : 254010 : d_visited.insert(current);
1493 : 254010 : }
1494 : :
1495 : 84268 : void start(CVC5_UNUSED TNode node) {}
1496 : 84268 : void done(CVC5_UNUSED TNode node) {}
1497 : :
1498 : 84268 : std::vector<TNode> getAtoms() const { return d_atoms; }
1499 : : };
1500 : :
1501 : 84268 : void TheoryEngine::ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo)
1502 : : {
1503 [ - + ][ - + ]: 84268 : Assert(atomsTo != THEORY_LAST);
[ - - ]
1504 [ + - ]: 168536 : Trace("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(" << n << ", "
1505 : 84268 : << atomsTo << ")" << endl;
1506 : 84268 : AtomsCollect collectAtoms;
1507 : 84268 : NodeVisitor<AtomsCollect>::run(collectAtoms, n);
1508 : 84268 : ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
1509 : 84268 : }
1510 : :
1511 : 84268 : void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms,
1512 : : theory::TheoryId atomsTo)
1513 : : {
1514 [ + + ]: 171048 : for (unsigned i = 0; i < atoms.size(); ++i)
1515 : : {
1516 : : // Non-equality atoms are either owned by theory or they don't make sense
1517 [ + + ]: 86780 : if (atoms[i].getKind() != Kind::EQUAL)
1518 : : {
1519 : 71167 : continue;
1520 : : }
1521 : :
1522 : : // The equality
1523 : 82954 : Node eq = atoms[i];
1524 : : // Simple normalization to not repeat stuff
1525 [ - + ]: 82954 : if (eq[0] > eq[1])
1526 : : {
1527 : 0 : eq = eq[1].eqNode(eq[0]);
1528 : : }
1529 : :
1530 : : // Rewrite the equality
1531 : 82954 : Node eqNormalized = rewrite(atoms[i]);
1532 : :
1533 [ + - ]: 165908 : Trace("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
1534 : 82954 : << " with nf " << eqNormalized << endl;
1535 : :
1536 : : // If the equality is a boolean constant, we send immediately
1537 [ + + ]: 82954 : if (eqNormalized.isConst())
1538 : : {
1539 [ - + ]: 2 : if (eqNormalized.getConst<bool>())
1540 : : {
1541 : 0 : assertToTheory(eq,
1542 : : eqNormalized,
1543 : : /** to */ atomsTo,
1544 : : /** Sat solver */ theory::THEORY_SAT_SOLVER);
1545 : : }
1546 : : else
1547 : : {
1548 : : // Use notEq and notEqNormalized to ensure deterministic node ID
1549 : : // assignments
1550 : 2 : Node notEq = eq.notNode();
1551 : 2 : Node notEqNormalized = eqNormalized.notNode();
1552 : 2 : assertToTheory(notEq,
1553 : : notEqNormalized,
1554 : : /** to */ atomsTo,
1555 : : /** Sat solver */ theory::THEORY_SAT_SOLVER);
1556 : 2 : }
1557 : 2 : continue;
1558 : 2 : }
1559 [ - + ]: 82952 : else if (eqNormalized.getKind() != Kind::EQUAL)
1560 : : {
1561 : 0 : Assert(eqNormalized.getKind() == Kind::SKOLEM
1562 : : || (eqNormalized.getKind() == Kind::NOT
1563 : : && eqNormalized[0].getKind() == Kind::SKOLEM));
1564 : : // this happens for Boolean term equalities V = true that are rewritten to
1565 : : // V, we should skip
1566 : : // TODO : revisit this
1567 : 0 : continue;
1568 : : }
1569 : :
1570 : : // If the normalization did the just flips, keep the flip
1571 : 82952 : if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0])
1572 : : {
1573 : 1619 : eq = eqNormalized;
1574 : : }
1575 : :
1576 : : // Check if the equality is already known by the sat solver
1577 [ + + ]: 82952 : if (d_propEngine->isSatLiteral(eqNormalized))
1578 : : {
1579 : : bool value;
1580 [ + + ]: 69606 : if (d_propEngine->hasValue(eqNormalized, value))
1581 : : {
1582 [ + + ]: 67339 : if (value)
1583 : : {
1584 : 66534 : assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1585 : 67339 : continue;
1586 : : }
1587 : : else
1588 : : {
1589 : : // Use notEq and notEqNormalized to ensure deterministic node ID
1590 : : // assignments
1591 : 805 : Node notEq = eq.notNode();
1592 : 805 : Node notEqNormalized = eqNormalized.notNode();
1593 : 805 : assertToTheory(
1594 : : notEq, notEqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1595 : 805 : continue;
1596 : 805 : }
1597 : : }
1598 : : }
1599 : :
1600 : : // If the theory is asking about a different form, or the form is ok but if
1601 : : // will go to a different theory then we must figure it out
1602 [ + + ][ + + ]: 15613 : if (eqNormalized != eq || d_env.theoryOf(eq) != atomsTo)
[ + + ][ + + ]
[ - - ]
1603 : : {
1604 : : // If you get eqNormalized, send atoms[i] to atomsTo
1605 : 12923 : d_atomRequests.add(eqNormalized, eq, atomsTo);
1606 : : }
1607 [ + + ][ + + ]: 150295 : }
1608 : 84268 : }
1609 : :
1610 : 911559 : void TheoryEngine::lemma(TrustNode tlemma,
1611 : : InferenceId id,
1612 : : LemmaProperty p,
1613 : : TheoryId from)
1614 : : {
1615 : : // For resource-limiting (also does a time check).
1616 : : // spendResource();
1617 [ + + ][ + - ]: 911559 : Assert(tlemma.getKind() == TrustNodeKind::LEMMA
[ - + ][ - + ]
[ - - ]
1618 : : || tlemma.getKind() == TrustNodeKind::CONFLICT);
1619 : :
1620 : : // minimize or generalize conflict
1621 [ + + ]: 911559 : if (d_cp)
1622 : : {
1623 : 135 : TrustNode tproc = d_cp->processLemma(tlemma);
1624 [ + + ]: 135 : if (!tproc.isNull())
1625 : : {
1626 : 7 : tlemma = tproc;
1627 : : }
1628 : 135 : }
1629 : :
1630 : : // get the node
1631 : 911559 : Node node = tlemma.getNode();
1632 : 911559 : Node lemma = tlemma.getProven();
1633 : :
1634 : : // must rewrite when checking here since we may have shadowing in rare cases,
1635 : : // e.g. lazy lambda lifting lemmas
1636 [ - + ][ - - ]: 1823118 : Assert(!expr::hasFreeVar(rewrite(lemma)))
1637 [ - + ][ - + ]: 911559 : << "Lemma " << lemma << " from " << from << " has a free variable";
[ - - ]
1638 : :
1639 : : // when proofs are enabled, we ensure the trust node has a generator by
1640 : : // adding a trust step to the lazy proof maintained by this class
1641 [ + + ]: 911559 : if (isProofEnabled())
1642 : : {
1643 : : // ensure proof: set THEORY_LEMMA if no generator is provided
1644 [ + + ]: 392955 : if (tlemma.getGenerator() == nullptr)
1645 : : {
1646 : : // add theory lemma step to proof
1647 : : Node tidn =
1648 : 46473 : builtin::BuiltinProofRuleChecker::mkTheoryIdNode(nodeManager(), from);
1649 : 92946 : d_lazyProof->addTrustedStep(lemma, TrustId::THEORY_LEMMA, {}, {tidn});
1650 : : // update the trust node
1651 [ + - ]: 46473 : tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
1652 : 46473 : }
1653 : : // ensure closed
1654 : 392955 : tlemma.debugCheckClosed(
1655 : : options(), "te-proof-debug", "TheoryEngine::lemma_initial");
1656 : : }
1657 : :
1658 : : // assert the lemma
1659 : 911560 : d_propEngine->assertLemma(id, tlemma, p);
1660 : :
1661 : : // If specified, we must add this lemma to the set of those that need to be
1662 : : // justified, where note we pass all auxiliary lemmas in skAsserts as well,
1663 : : // since these by extension must be justified as well.
1664 [ + + ]: 911558 : if (!d_modules.empty())
1665 : : {
1666 : 945 : std::vector<Node> skAsserts;
1667 : 945 : std::vector<Node> sks;
1668 : : Node retLemma =
1669 : 1890 : d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
1670 : :
1671 : : // notify the modules of the lemma
1672 [ + + ]: 1890 : for (TheoryEngineModule* tem : d_modules)
1673 : : {
1674 : : // don't notify theory modules of their own lemmas
1675 [ + + ]: 945 : if (tem->getId() != from)
1676 : : {
1677 : 932 : tem->notifyLemma(retLemma, id, p, skAsserts, sks);
1678 : : }
1679 : : }
1680 : 945 : }
1681 : :
1682 : : // Mark that we added some lemmas
1683 : 911558 : d_lemmasAdded = true;
1684 : 911560 : }
1685 : :
1686 : 368545 : void TheoryEngine::markInConflict()
1687 : : {
1688 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
1689 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
1690 : : #endif
1691 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
1692 : : theoryOf(THEORY)->notifyInConflict();
1693 : 368545 : CVC5_FOR_EACH_THEORY;
1694 : 368545 : d_inConflict = true;
1695 : 368545 : }
1696 : :
1697 : 198211 : void TheoryEngine::conflict(TrustNode tconflict,
1698 : : InferenceId id,
1699 : : TheoryId theoryId)
1700 : : {
1701 [ - + ][ - + ]: 198211 : Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
[ - - ]
1702 : :
1703 : 198211 : TNode conflict = tconflict.getNode();
1704 [ + - ]: 396422 : Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", "
1705 : 198211 : << id << ", " << theoryId << ")" << endl;
1706 [ + - ]: 198211 : Trace("te-proof-debug") << "Check closed conflict" << std::endl;
1707 : : // doesn't require proof generator, yet, since THEORY_LEMMA is added below
1708 : 198211 : tconflict.debugCheckClosed(
1709 : : options(), "te-proof-debug", "TheoryEngine::conflict_initial", false);
1710 : :
1711 [ + - ]: 198211 : Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
1712 : :
1713 : : // Mark that we are in conflict
1714 : 198211 : markInConflict();
1715 : :
1716 : : // In the multiple-theories case, we need to reconstruct the conflict
1717 [ + + ]: 198211 : if (logicInfo().isSharingEnabled())
1718 : : {
1719 : : // Create the workplace for explanations
1720 : 162984 : std::vector<NodeTheoryPair> vec;
1721 : 162984 : vec.push_back(
1722 : 325968 : NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
1723 : :
1724 : : // Process the explanation
1725 : 162984 : TrustNode tncExp = getExplanation(vec);
1726 : 162984 : Node fullConflict = tncExp.getNode();
1727 : :
1728 [ + + ]: 162984 : if (isProofEnabled())
1729 : : {
1730 [ + - ]: 139884 : Trace("te-proof-debug")
1731 : 69942 : << "Check closed conflict explained with sharing" << std::endl;
1732 : 69942 : tncExp.debugCheckClosed(options(),
1733 : : "te-proof-debug",
1734 : : "TheoryEngine::conflict_explained_sharing");
1735 [ + - ]: 69942 : Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
1736 [ + - ]: 139884 : Trace("te-proof-debug") << "Conflict " << tconflict << " from "
1737 [ - + ][ - - ]: 69942 : << tconflict.identifyGenerator() << std::endl;
1738 [ + - ]: 139884 : Trace("te-proof-debug") << "Explanation " << tncExp << " from "
1739 [ - + ][ - - ]: 69942 : << tncExp.identifyGenerator() << std::endl;
1740 [ - + ][ - + ]: 69942 : Assert(d_lazyProof != nullptr);
[ - - ]
1741 [ + + ]: 69942 : if (tconflict.getGenerator() != nullptr)
1742 : : {
1743 : 68620 : d_lazyProof->addLazyStep(tconflict.getProven(),
1744 : : tconflict.getGenerator());
1745 : : }
1746 : : else
1747 : : {
1748 : : // add theory lemma step
1749 : : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(
1750 : 1322 : nodeManager(), theoryId);
1751 : 1322 : Node conf = tconflict.getProven();
1752 : 2644 : d_lazyProof->addTrustedStep(conf, TrustId::THEORY_LEMMA, {}, {tidn});
1753 : 1322 : }
1754 : : // store the explicit step, which should come from a different
1755 : : // generator, e.g. d_tepg.
1756 : 69942 : Node proven = tncExp.getProven();
1757 [ + - ][ - + ]: 69942 : Assert(tncExp.getGenerator() != d_lazyProof.get());
[ - + ][ - - ]
1758 [ + - ][ - + ]: 139884 : Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
[ - - ]
1759 : 69942 : << " for " << proven << std::endl;
1760 : 69942 : d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
1761 [ + - ]: 69942 : pfgEnsureClosed(options(),
1762 : : proven,
1763 : 69942 : d_lazyProof.get(),
1764 : : "te-proof-debug",
1765 : : "TheoryEngine::conflict_during");
1766 : 69942 : Node fullConflictNeg = fullConflict.notNode();
1767 : 69942 : std::vector<Node> children;
1768 : 69942 : children.push_back(proven);
1769 : 69942 : std::vector<Node> args;
1770 : 69942 : args.push_back(fullConflictNeg);
1771 [ + + ]: 69942 : if (conflict == d_false)
1772 : : {
1773 [ - + ][ - + ]: 598 : AlwaysAssert(proven == fullConflictNeg);
[ - - ]
1774 : : }
1775 : : else
1776 : : {
1777 [ + + ]: 69344 : if (!CDProof::isSame(fullConflict, conflict))
1778 : : {
1779 : : // ------------------------- explained
1780 : : // fullConflict => conflict
1781 : : // ------------------------- IMPLIES_ELIM ---------- from theory
1782 : : // ~fullConflict V conflict ~conflict
1783 : : // -------------------------------------------------- RESOLUTION
1784 : : // ~fullConflict
1785 : : Node provenOr =
1786 : 131072 : nodeManager()->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
1787 : 131072 : d_lazyProof->addStep(provenOr, ProofRule::IMPLIES_ELIM, {proven}, {});
1788 : 393216 : d_lazyProof->addStep(fullConflictNeg,
1789 : : ProofRule::RESOLUTION,
1790 : : {provenOr, conflict.notNode()},
1791 : 65536 : {d_true, conflict});
1792 : 65536 : }
1793 : : }
1794 : 69942 : }
1795 : : // pass the processed trust node
1796 : : TrustNode tconf =
1797 [ + + ]: 162984 : TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get());
1798 [ + - ]: 325968 : Trace("theory::conflict")
1799 : 0 : << "TheoryEngine::conflict(" << conflict << ", " << theoryId
1800 : 162984 : << "): full = " << fullConflict << endl;
1801 [ - + ][ - + ]: 162984 : Assert(properConflict(fullConflict));
[ - - ]
1802 [ + - ]: 325968 : Trace("te-proof-debug")
1803 : 162984 : << "Check closed conflict with sharing" << std::endl;
1804 [ + + ]: 162984 : if (isProofEnabled())
1805 : : {
1806 : 69942 : tconf.debugCheckClosed(
1807 : : options(), "te-proof-debug", "TheoryEngine::conflict:sharing");
1808 : : }
1809 : 162984 : lemma(tconf, id, LemmaProperty::NONE, theoryId);
1810 : 162984 : }
1811 : : else
1812 : : {
1813 : : // When only one theory, the conflict should need no processing
1814 [ - + ][ - + ]: 35227 : Assert(properConflict(conflict));
[ - - ]
1815 : : // pass the trust node that was sent from the theory
1816 : 35227 : lemma(tconflict, id, LemmaProperty::NONE, theoryId);
1817 : : }
1818 : 198211 : }
1819 : :
1820 : 0 : void TheoryEngine::setModelUnsound(theory::IncompleteId id)
1821 : : {
1822 : 0 : setModelUnsound(TheoryId::THEORY_NONE, id);
1823 : 0 : }
1824 : :
1825 : 43 : void TheoryEngine::setRefutationUnsound(theory::IncompleteId id)
1826 : : {
1827 : 43 : setRefutationUnsound(TheoryId::THEORY_NONE, id);
1828 : 43 : }
1829 : :
1830 : 3421 : void TheoryEngine::setModelUnsound(theory::TheoryId theory,
1831 : : theory::IncompleteId id)
1832 : : {
1833 : 3421 : d_modelUnsound = true;
1834 : 3421 : d_modelUnsoundTheory = theory;
1835 : 3421 : d_modelUnsoundId = id;
1836 : 3421 : }
1837 : :
1838 : 176 : void TheoryEngine::setRefutationUnsound(theory::TheoryId theory,
1839 : : theory::IncompleteId id)
1840 : : {
1841 : 176 : d_refutationUnsound = true;
1842 : 176 : d_refutationUnsoundTheory = theory;
1843 : 176 : d_refutationUnsoundId = id;
1844 : 176 : }
1845 : :
1846 : 329287 : TrustNode TheoryEngine::getExplanation(
1847 : : std::vector<NodeTheoryPair>& explanationVector)
1848 : : {
1849 [ - + ][ - + ]: 329287 : Assert(explanationVector.size() == 1);
[ - - ]
1850 : 329287 : Node conclusion = explanationVector[0].d_node;
1851 : : // if the theory explains using the central equality engine, we always start
1852 : : // with THEORY_BUILTIN.
1853 : 658574 : explanationVector[0].d_theory =
1854 : 329287 : theoryExpPropagation(explanationVector[0].d_theory);
1855 : 329287 : std::shared_ptr<LazyCDProof> lcp;
1856 [ + + ]: 329287 : if (isProofEnabled())
1857 : : {
1858 [ + - ]: 241032 : Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion
1859 : 120516 : << std::endl;
1860 : : // We do not use auto-symmetry in this proof, since in very rare cases, it
1861 : : // is possible that the proof of explanations is cyclic when considering
1862 : : // (dis)equalities modulo symmetry, where such a proof looks like:
1863 : : // x = y
1864 : : // -----
1865 : : // A ...
1866 : : // ----------
1867 : : // y = x
1868 : : // Notice that this complication arises since propagations consider
1869 : : // equalities that are not in rewritten form. This complication would not
1870 : : // exist otherwise. It is the shared term database that introduces these
1871 : : // unrewritten equalities; it must do so since theory combination requires
1872 : : // communicating arrangements between shared terms, and the rewriter
1873 : : // for arithmetic equalities does not preserve terms, e.g. x=y may become
1874 : : // x+-1*y=0.
1875 : 241032 : lcp.reset(new LazyCDProof(d_env,
1876 : : nullptr,
1877 : : nullptr,
1878 : : "TheoryEngine::LazyCDProof::getExplanation",
1879 : 120516 : false));
1880 : : }
1881 : 329287 : unsigned i = 0; // Index of the current literal we are processing
1882 : :
1883 : 329287 : std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
1884 : : // the overall explanation
1885 : 329287 : std::set<TNode> exp;
1886 : : // vector of trust nodes to explain at the end
1887 : 329287 : std::vector<std::pair<TheoryId, TrustNode>> texplains;
1888 : : // cache of nodes we have already explained by some theory
1889 : 329287 : std::unordered_map<Node, size_t> cache;
1890 : :
1891 [ + + ]: 8539280 : while (i < explanationVector.size())
1892 : : {
1893 : : // Get the current literal to explain
1894 : 8209993 : NodeTheoryPair toExplain = explanationVector[i];
1895 : :
1896 [ + - ]: 16419986 : Trace("theory::explain")
1897 : 0 : << "[i=" << i << "] TheoryEngine::explain(): processing ["
1898 : 0 : << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
1899 : 8209993 : << toExplain.d_theory << endl;
1900 : :
1901 : 8209993 : if (cache.find(toExplain.d_node) != cache.end()
1902 [ + + ][ + + ]: 8209993 : && cache[toExplain.d_node] < toExplain.d_timestamp)
[ + + ]
1903 : : {
1904 : 258868 : ++i;
1905 : 258868 : continue;
1906 : : }
1907 : 7951125 : cache[toExplain.d_node] = toExplain.d_timestamp;
1908 : :
1909 : : // If a true constant or a negation of a false constant we can ignore it
1910 [ + + ]: 30947 : if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
1911 [ + + ][ + + ]: 8658762 : || (toExplain.d_node.getKind() == Kind::NOT
1912 [ - + ][ + + ]: 8627815 : && toExplain.d_node[0].isConst()
[ - - ]
1913 [ - - ][ - + ]: 7951125 : && !toExplain.d_node[0].getConst<bool>()))
[ + + ][ - - ]
1914 : : {
1915 : 29910 : ++i;
1916 : : // if we are building a proof
1917 [ + + ]: 29910 : if (lcp != nullptr)
1918 : : {
1919 [ + - ]: 6422 : Trace("te-proof-exp")
1920 : 3211 : << "- explain " << toExplain.d_node << " trivially..." << std::endl;
1921 : : // ------------------MACRO_SR_PRED_INTRO
1922 : : // toExplain.d_node
1923 : 3211 : std::vector<Node> children;
1924 : 3211 : std::vector<Node> args;
1925 : 3211 : args.push_back(toExplain.d_node);
1926 : 3211 : lcp->addStep(
1927 : : toExplain.d_node, ProofRule::MACRO_SR_PRED_INTRO, children, args);
1928 : 3211 : }
1929 : 29910 : continue;
1930 : 29910 : }
1931 : :
1932 : : // If from the SAT solver, keep it
1933 [ + + ]: 7921215 : if (toExplain.d_theory == THEORY_SAT_SOLVER)
1934 : : {
1935 [ + - ]: 5816036 : Trace("theory::explain")
1936 : 2908018 : << "\tLiteral came from THEORY_SAT_SOLVER. Keeping it." << endl;
1937 : 2908018 : exp.insert(explanationVector[i++].d_node);
1938 : : // it will be a free assumption in the proof
1939 [ + - ]: 2908018 : Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl;
1940 : 2908018 : continue;
1941 : : }
1942 : :
1943 : : // If an and, expand it
1944 [ + + ]: 5013197 : if (toExplain.d_node.getKind() == Kind::AND)
1945 : : {
1946 [ + - ]: 1366204 : Trace("theory::explain")
1947 : 0 : << "TheoryEngine::explain(): expanding " << toExplain.d_node
1948 : 683102 : << " got from " << toExplain.d_theory << endl;
1949 : 683102 : size_t nchild = toExplain.d_node.getNumChildren();
1950 [ + + ]: 4233713 : for (size_t k = 0; k < nchild; ++k)
1951 : : {
1952 : : NodeTheoryPair newExplain(
1953 : 7101222 : toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
1954 : 3550611 : explanationVector.push_back(newExplain);
1955 : 3550611 : }
1956 [ + + ]: 683102 : if (lcp != nullptr)
1957 : : {
1958 [ + - ]: 536906 : Trace("te-proof-exp")
1959 : 268453 : << "- AND expand " << toExplain.d_node << std::endl;
1960 : : // delay explanation, use a dummy trust node
1961 : : TrustNode tnAndExp = TrustNode::mkTrustPropExp(
1962 : 536906 : toExplain.d_node, toExplain.d_node, nullptr);
1963 : 268453 : texplains.push_back(
1964 : 536906 : std::pair<TheoryId, TrustNode>(THEORY_LAST, tnAndExp));
1965 : 268453 : }
1966 : 683102 : ++i;
1967 : 683102 : continue;
1968 : 683102 : }
1969 : :
1970 : : // See if it was sent to the theory by another theory
1971 : 4330095 : PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
1972 [ + + ]: 4330095 : if (find != d_propagationMap.end())
1973 : : {
1974 [ + - ]: 8216314 : Trace("theory::explain")
1975 : 0 : << "\tTerm was propagated by another theory (theory = "
1976 [ - + ][ - - ]: 4108157 : << getTheoryString((*find).second.d_theory) << ")" << std::endl;
1977 : : // There is some propagation, check if its a timely one
1978 [ + + ]: 4108157 : if ((*find).second.d_timestamp < toExplain.d_timestamp)
1979 : : {
1980 [ + - ]: 7373300 : Trace("theory::explain")
1981 : 0 : << "\tRelevant timetsamp, pushing " << (*find).second.d_node
1982 : 3686650 : << "to index = " << explanationVector.size() << std::endl;
1983 : 3686650 : explanationVector.push_back((*find).second);
1984 : 3686650 : ++i;
1985 : :
1986 [ + + ]: 3686650 : if (lcp != nullptr)
1987 : : {
1988 [ + + ]: 1465433 : if (toExplain.d_node != (*find).second.d_node)
1989 : : {
1990 [ + - ]: 22714 : Trace("te-proof-exp")
1991 : 0 : << "- t-explained cached: " << toExplain.d_node << " by "
1992 : 11357 : << (*find).second.d_node << std::endl;
1993 : : // delay explanation, use a dummy trust node that says that
1994 : : // (*find).second.d_node explains toExplain.d_node.
1995 : : TrustNode tnRewExp = TrustNode::mkTrustPropExp(
1996 : 22714 : toExplain.d_node, (*find).second.d_node, nullptr);
1997 : 11357 : texplains.push_back(
1998 : 22714 : std::pair<TheoryId, TrustNode>(THEORY_LAST, tnRewExp));
1999 : 11357 : }
2000 : : }
2001 : 3686650 : continue;
2002 : 3686650 : }
2003 : : }
2004 : : // It was produced by the theory, so ask for an explanation
2005 : : TrustNode texplanation =
2006 : 643445 : d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
2007 [ + + ]: 643445 : if (lcp != nullptr)
2008 : : {
2009 : 255067 : texplanation.debugCheckClosed(
2010 : : options(), "te-proof-exp", "texplanation", false);
2011 [ + - ]: 510134 : Trace("te-proof-exp")
2012 : 0 : << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
2013 [ - + ][ - - ]: 255067 : << " by " << texplanation.getNode() << std::endl;
2014 : : // should prove the propagation we asked for
2015 : 255067 : Assert(texplanation.getKind() == TrustNodeKind::PROP_EXP
2016 : : && texplanation.getProven()[1] == toExplain.d_node);
2017 : : // We add it to the list of theory explanations, to be processed at
2018 : : // the end of this method. We wait to explain here because it may
2019 : : // be that a later explanation may preempt the need for proving this
2020 : : // step. For instance, if the conclusion lit is later added as an
2021 : : // assumption in the final explanation. This avoids cyclic proofs.
2022 : 255067 : texplains.push_back(
2023 : 510134 : std::pair<TheoryId, TrustNode>(toExplain.d_theory, texplanation));
2024 : : }
2025 : 643445 : Node explanation = texplanation.getNode();
2026 : :
2027 [ + - ]: 1286890 : Trace("theory::explain")
2028 : 0 : << "TheoryEngine::explain(): got explanation " << explanation
2029 : 643445 : << " got from " << toExplain.d_theory << endl;
2030 : 643445 : Assert(explanation != toExplain.d_node)
2031 : : << "wasn't sent to you, so why are you explaining it trivially, for "
2032 : 0 : "fact "
2033 : : << explanation;
2034 : : // Mark the explanation
2035 : : NodeTheoryPair newExplain(
2036 : 643445 : explanation, toExplain.d_theory, toExplain.d_timestamp);
2037 : 643445 : explanationVector.push_back(newExplain);
2038 : :
2039 : 643445 : ++i;
2040 [ + + ]: 8209993 : }
2041 : :
2042 : : // make the explanation node
2043 : 329287 : Node expNode;
2044 [ + + ]: 329287 : if (exp.size() == 0)
2045 : : {
2046 : : // Normalize to true
2047 : 72 : expNode = nodeManager()->mkConst<bool>(true);
2048 : : }
2049 [ + + ]: 329215 : else if (exp.size() == 1)
2050 : : {
2051 : : // All the same, or just one
2052 : 12249 : expNode = *exp.begin();
2053 : : }
2054 : : else
2055 : : {
2056 : 316966 : NodeBuilder conjunction(nodeManager(), Kind::AND);
2057 : 316966 : std::set<TNode>::const_iterator it = exp.begin();
2058 : 316966 : std::set<TNode>::const_iterator it_end = exp.end();
2059 [ + + ]: 3132385 : while (it != it_end)
2060 : : {
2061 : 2815419 : conjunction << *it;
2062 : 2815419 : ++it;
2063 : : }
2064 : 316966 : expNode = conjunction;
2065 : 316966 : }
2066 : : // if we are building a proof, go back through the explanations and
2067 : : // build the proof
2068 [ + + ]: 329287 : if (lcp != nullptr)
2069 : : {
2070 [ - + ]: 120516 : if (TraceIsOn("te-proof-exp"))
2071 : : {
2072 [ - - ]: 0 : Trace("te-proof-exp") << "Explanation is:" << std::endl;
2073 [ - - ]: 0 : for (TNode e : exp)
2074 : : {
2075 [ - - ]: 0 : Trace("te-proof-exp") << " " << e << std::endl;
2076 : 0 : }
2077 [ - - ]: 0 : Trace("te-proof-exp") << "=== Replay explanations..." << std::endl;
2078 : : }
2079 : : // Now, go back and add the necessary steps of theory explanations, i.e.
2080 : : // add those that prove things that aren't in the final explanation. We
2081 : : // iterate in reverse order so that most recent steps take priority. This
2082 : : // avoids cyclic proofs in the lazy proof we are building (lcp).
2083 : 120516 : for (std::vector<std::pair<TheoryId, TrustNode>>::reverse_iterator
2084 : 120516 : it = texplains.rbegin(),
2085 : 120516 : itEnd = texplains.rend();
2086 [ + + ]: 655393 : it != itEnd;
2087 : 534877 : ++it)
2088 : : {
2089 : 534877 : TrustNode trn = it->second;
2090 [ - + ][ - + ]: 534877 : Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
[ - - ]
2091 : 534877 : Node proven = trn.getProven();
2092 [ - + ][ - + ]: 534877 : Assert(proven.getKind() == Kind::IMPLIES);
[ - - ]
2093 : 534877 : Node tConc = proven[1];
2094 [ + - ]: 534877 : Trace("te-proof-exp") << "- Process " << trn << std::endl;
2095 [ + + ]: 534877 : if (exp.find(tConc) != exp.end())
2096 : : {
2097 : : // already added to proof
2098 [ + - ]: 20249 : Trace("te-proof-exp") << "...already added" << std::endl;
2099 : 20249 : continue;
2100 : : }
2101 : : // remember that we've explained this formula, to avoid cycles in lcp
2102 : 514628 : exp.insert(tConc);
2103 : 514628 : TheoryId ttid = it->first;
2104 : 514628 : Node tExp = proven[0];
2105 [ + + ]: 514628 : if (ttid == THEORY_LAST)
2106 : : {
2107 [ + + ]: 269193 : if (tConc == tExp)
2108 : : {
2109 : : // dummy trust node, do AND expansion
2110 [ - + ][ - + ]: 261424 : Assert(tConc.getKind() == Kind::AND);
[ - - ]
2111 : : // tConc[0] ... tConc[n]
2112 : : // ---------------------- AND_INTRO
2113 : : // tConc
2114 : 261424 : std::vector<Node> pfChildren;
2115 : 261424 : pfChildren.insert(pfChildren.end(), tConc.begin(), tConc.end());
2116 : 261424 : lcp->addStep(tConc, ProofRule::AND_INTRO, pfChildren, {});
2117 [ + - ]: 261424 : Trace("te-proof-exp") << "...via AND_INTRO" << std::endl;
2118 : 261424 : continue;
2119 : 261424 : }
2120 : : // otherwise should hold by rewriting
2121 [ - + ][ - + ]: 38845 : AssertEqual(rewrite(tConc), rewrite(tExp));
[ - - ]
2122 : : // tExp
2123 : : // ---- MACRO_SR_PRED_TRANSFORM
2124 : : // tConc
2125 : 23307 : lcp->addStep(
2126 : : tConc, ProofRule::MACRO_SR_PRED_TRANSFORM, {tExp}, {tConc});
2127 [ + - ]: 7769 : Trace("te-proof-exp") << "...via MACRO_SR_PRED_TRANSFORM" << std::endl;
2128 : 7769 : continue;
2129 : 7769 : }
2130 [ - + ]: 245435 : if (tExp == tConc)
2131 : : {
2132 : : // trivial
2133 [ - - ]: 0 : Trace("te-proof-exp") << "...trivial" << std::endl;
2134 : 0 : continue;
2135 : : }
2136 : : // ------------- Via theory
2137 : : // tExp tExp => tConc
2138 : : // ---------------------------------MODUS_PONENS
2139 : : // tConc
2140 [ + - ]: 245435 : if (trn.getGenerator() != nullptr)
2141 : : {
2142 [ + - ]: 245435 : Trace("te-proof-exp") << "...via theory generator" << std::endl;
2143 : 245435 : lcp->addLazyStep(proven, trn.getGenerator());
2144 : : }
2145 : : else
2146 : : {
2147 [ - - ]: 0 : Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl;
2148 : : // otherwise, trusted theory lemma
2149 : : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(
2150 : 0 : nodeManager(), ttid);
2151 : 0 : lcp->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn});
2152 : 0 : }
2153 : 245435 : std::vector<Node> pfChildren;
2154 : 245435 : pfChildren.push_back(trn.getNode());
2155 : 245435 : pfChildren.push_back(proven);
2156 : 245435 : lcp->addStep(tConc, ProofRule::MODUS_PONENS, pfChildren, {});
2157 [ + + ][ + + ]: 1382954 : }
[ + + ][ + + ]
2158 : : // If we don't have a step and the conclusion is not part of the
2159 : : // explanation (for unit T-conflicts), it must be by symmetry. We must do
2160 : : // this manually since lcp does not have auto-symmetry enabled due to the
2161 : : // complication mentioned above.
2162 : 120516 : if (!lcp->hasStep(conclusion) && exp.find(conclusion) == exp.end())
2163 : : {
2164 : 0 : Node sconc = CDProof::getSymmFact(conclusion);
2165 [ - - ]: 0 : if (!sconc.isNull())
2166 : : {
2167 : 0 : lcp->addStep(conclusion, ProofRule::SYMM, {sconc}, {});
2168 : : }
2169 : : else
2170 : : {
2171 : 0 : DebugUnhandled()
2172 : 0 : << "TheoryEngine::getExplanation: no step found for conclusion "
2173 : : << conclusion;
2174 : : }
2175 : 0 : }
2176 : : // store in the proof generator
2177 : 241032 : TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp);
2178 : : // return the trust node
2179 : 120516 : return trn;
2180 : 120516 : }
2181 : :
2182 : 208771 : return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
2183 : 329287 : }
2184 : :
2185 : 6419935 : bool TheoryEngine::isProofEnabled() const
2186 : : {
2187 : 6419935 : return d_env.isTheoryProofProducing();
2188 : : }
2189 : :
2190 : 2898 : void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure)
2191 : : {
2192 : 2898 : bool hasFailure = false;
2193 : 2898 : std::stringstream serror;
2194 : : // If possible, get the list of relevant assertions. Those that are not
2195 : : // relevant will be skipped.
2196 : 2898 : std::unordered_set<TNode> relevantAssertions;
2197 : 2898 : bool hasRelevantAssertions = false;
2198 [ + + ]: 2898 : if (d_relManager != nullptr)
2199 : : {
2200 : : relevantAssertions =
2201 : 11 : d_relManager->getRelevantAssertions(hasRelevantAssertions);
2202 : : }
2203 [ + + ]: 43470 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
2204 : : {
2205 : 40572 : Theory* theory = d_theoryTable[theoryId];
2206 [ + - ][ + + ]: 40572 : if (theory && isTheoryEnabled(theoryId))
[ + + ]
2207 : : {
2208 : 21238 : for (context::CDList<Assertion>::const_iterator
2209 : 21238 : it = theory->facts_begin(),
2210 : 21238 : it_end = theory->facts_end();
2211 [ + + ]: 157779 : it != it_end;
2212 : 136541 : ++it)
2213 : : {
2214 : 136541 : Node assertion = (*it).d_assertion;
2215 : 136776 : if (hasRelevantAssertions
2216 [ + + ][ + + ]: 136541 : && relevantAssertions.find(assertion) == relevantAssertions.end())
[ + + ][ + + ]
[ - - ]
2217 : : {
2218 : : // not relevant, skip
2219 : 235 : continue;
2220 : : }
2221 : 136306 : Node val = d_tc->getModel()->getValue(assertion);
2222 [ + + ]: 136306 : if (val != d_true)
2223 : : {
2224 : 357 : std::stringstream ss;
2225 [ + + ]: 930 : for (Node child : assertion)
2226 : : {
2227 : 573 : Node value = d_tc->getModel()->getValue(child);
2228 : 573 : ss << "getValue(" << child << "): " << value << std::endl;
2229 : 573 : }
2230 : 357 : ss << " " << theoryId << " has an asserted fact that";
2231 [ - + ]: 357 : if (val == d_false)
2232 : : {
2233 : 0 : ss << " the model doesn't satisfy." << std::endl;
2234 : : }
2235 : : else
2236 : : {
2237 : 357 : ss << " the model may not satisfy." << std::endl;
2238 : : }
2239 : 357 : ss << "The fact: " << assertion << std::endl
2240 : 357 : << "Model value: " << val << std::endl;
2241 [ + - ]: 357 : if (hardFailure)
2242 : : {
2243 [ - + ]: 357 : if (val == d_false)
2244 : : {
2245 : : // Always an error if it is false
2246 : 0 : hasFailure = true;
2247 : 0 : serror << ss.str();
2248 : : }
2249 : : else
2250 : : {
2251 : : // Otherwise just a warning. Notice this case may happen for
2252 : : // assertions with unevaluable operators, e.g. transcendental
2253 : : // functions. It also may happen for separation logic, where
2254 : : // check-model support is limited.
2255 : 357 : warning() << ss.str();
2256 : : }
2257 : : }
2258 : 357 : }
2259 [ + + ]: 136541 : }
2260 : : }
2261 : : }
2262 [ - + ]: 2898 : if (hasFailure)
2263 : : {
2264 : 0 : InternalError() << serror.str();
2265 : : }
2266 : 2898 : }
2267 : :
2268 : 11517 : std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
2269 : : TNode lit)
2270 : : {
2271 [ + + ]: 11517 : TNode atom = (lit.getKind() == Kind::NOT) ? lit[0] : lit;
2272 [ + + ]: 23030 : if (atom.getKind() == Kind::AND || atom.getKind() == Kind::OR
2273 [ + + ][ + + ]: 23030 : || atom.getKind() == Kind::IMPLIES)
[ + + ]
2274 : : {
2275 : : // Boolean connective, recurse
2276 : 18 : std::vector<Node> children;
2277 : 18 : bool pol = (lit.getKind() != Kind::NOT);
2278 : 18 : bool is_conjunction = pol == (lit.getKind() == Kind::AND);
2279 [ + - ]: 18 : for (unsigned i = 0; i < atom.getNumChildren(); i++)
2280 : : {
2281 : 18 : Node ch = atom[i];
2282 [ - + ][ - - ]: 18 : if (pol == (lit.getKind() == Kind::IMPLIES && i == 0))
[ + - ]
2283 : : {
2284 : 18 : ch = atom[i].negate();
2285 : : }
2286 : 18 : std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2287 [ - + ]: 18 : if (chres.first)
2288 : : {
2289 [ - - ]: 0 : if (!is_conjunction)
2290 : : {
2291 : 0 : return chres;
2292 : : }
2293 : : else
2294 : : {
2295 : 0 : children.push_back(chres.second);
2296 : : }
2297 : : }
2298 [ + - ][ + - ]: 18 : else if (!chres.first && is_conjunction)
2299 : : {
2300 : 18 : return std::pair<bool, Node>(false, Node::null());
2301 : : }
2302 [ - + ][ - + ]: 36 : }
2303 [ - - ]: 0 : if (is_conjunction)
2304 : : {
2305 : : return std::pair<bool, Node>(true,
2306 : 0 : nodeManager()->mkNode(Kind::AND, children));
2307 : : }
2308 : : else
2309 : : {
2310 : 0 : return std::pair<bool, Node>(false, Node::null());
2311 : : }
2312 : 18 : }
2313 : 34497 : else if (atom.getKind() == Kind::ITE
2314 : 11499 : || (atom.getKind() == Kind::EQUAL && atom[0].getType().isBoolean()))
2315 : : {
2316 : 0 : bool pol = (lit.getKind() != Kind::NOT);
2317 [ - - ]: 0 : for (unsigned r = 0; r < 2; r++)
2318 : : {
2319 : 0 : Node ch = atom[0];
2320 [ - - ]: 0 : if (r == 1)
2321 : : {
2322 : 0 : ch = ch.negate();
2323 : : }
2324 : 0 : std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2325 [ - - ]: 0 : if (chres.first)
2326 : : {
2327 [ - - ]: 0 : Node ch2 = atom[atom.getKind() == Kind::ITE ? r + 1 : 1];
2328 : 0 : if (pol == (atom.getKind() == Kind::ITE ? true : r == 1))
2329 : : {
2330 : 0 : ch2 = ch2.negate();
2331 : : }
2332 : 0 : std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
2333 [ - - ]: 0 : if (chres2.first)
2334 : : {
2335 : : return std::pair<bool, Node>(
2336 : : true,
2337 : 0 : NodeManager::mkNode(Kind::AND, chres.second, chres2.second));
2338 : : }
2339 : : else
2340 : : {
2341 : 0 : break;
2342 : : }
2343 [ - - ][ - - ]: 0 : }
2344 [ - - ][ - - ]: 0 : }
[ - - ]
2345 : 0 : return std::pair<bool, Node>(false, Node::null());
2346 : : }
2347 : : else
2348 : : {
2349 : : // it is a theory atom
2350 : 11499 : theory::TheoryId tid = Theory::theoryOf(atom, mode);
2351 : 11499 : theory::Theory* th = theoryOf(tid);
2352 : :
2353 [ - + ][ - + ]: 11499 : Assert(th != nullptr);
[ - - ]
2354 [ + - ]: 11499 : Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
2355 : :
2356 : 11499 : std::pair<bool, Node> chres = th->entailmentCheck(lit);
2357 : 11499 : return chres;
2358 : 11499 : }
2359 : 11517 : }
2360 : :
2361 : 22369364 : void TheoryEngine::spendResource(Resource r)
2362 : : {
2363 : 22369364 : d_env.getResourceManager()->spendResource(r);
2364 : 22369364 : }
2365 : :
2366 : 20031 : void TheoryEngine::initializeProofChecker(ProofChecker* pc)
2367 : : {
2368 [ + + ]: 300465 : for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
2369 : 280434 : ++id)
2370 : : {
2371 : 280434 : ProofRuleChecker* prc = d_theoryTable[id]->getProofChecker();
2372 [ + + ]: 280434 : if (prc)
2373 : : {
2374 : 200310 : prc->registerTo(pc);
2375 : : }
2376 : : }
2377 : 20031 : }
2378 : :
2379 : 719114 : theory::Rewriter* TheoryEngine::getRewriter() { return d_env.getRewriter(); }
2380 : :
2381 : : } // namespace cvc5::internal
|
