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