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