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