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 : 49172 : void TheoryEngine::finishInit()
136 : : {
137 : 49172 : d_modules.clear();
138 [ + - ]: 49172 : 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 : 98344 : 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 [ + + ][ + + ]: 49172 : CVC5_FOR_EACH_THEORY;
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
155 : :
156 : : // Initialize the theory combination architecture
157 [ + - ]: 49172 : if (options().theory.tcMode == options::TcMode::CARE_GRAPH)
158 : : {
159 : 49172 : 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 [ + + ][ + + ]: 49172 : 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 [ + + ]: 49172 : if (logicInfo().isQuantified())
175 : : {
176 : : // get the quantifiers engine, which is initialized by the quantifiers
177 : : // theory
178 : 42052 : d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
179 [ - + ][ - + ]: 42052 : 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 [ + + ]: 49172 : if (logicInfo().isQuantified())
185 : : {
186 : 42052 : 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 : 49172 : d_tc->finishInit();
191 : : // get pointer to the shared solver
192 : 49172 : 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 [ + + ]: 737580 : for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
197 : 688408 : Theory* t = d_theoryTable[theoryId];
198 [ - + ]: 688408 : if (t == nullptr)
199 : : {
200 : 0 : continue;
201 : : }
202 : : // setup the pointers to the utilities
203 : 688408 : const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
204 [ - + ][ - + ]: 688408 : Assert(eeti != nullptr);
[ - - ]
205 : : // the theory's official equality engine is the one specified by the
206 : : // equality engine manager
207 : 688408 : t->setEqualityEngine(eeti->d_usedEe);
208 : : // set the quantifiers engine
209 : 688408 : t->setQuantifiersEngine(d_quantEngine);
210 : : // set the decision manager for the theory
211 : 688408 : t->setDecisionManager(d_decManager.get());
212 : : // finish initializing the theory
213 : 688408 : t->finishInit();
214 : : }
215 : :
216 [ - + ]: 49172 : 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 : 49172 : const std::vector<Plugin*> plugins = d_env.getPlugins();
225 [ + - ]: 98344 : Trace("theory") << "initialize with " << plugins.size()
226 : 49172 : << " user-provided plugins" << std::endl;
227 [ + + ]: 49199 : for (Plugin* p : plugins)
228 : : {
229 : 27 : d_userPlugins.push_back(
230 : 54 : std::unique_ptr<PluginModule>(new PluginModule(d_env, this, p)));
231 : 27 : d_modules.push_back(d_userPlugins.back().get());
232 : : }
233 [ + - ]: 49172 : Trace("theory") << "End TheoryEngine::finishInit" << std::endl;
234 : 49172 : }
235 : :
236 : 49172 : TheoryEngine::TheoryEngine(Env& env)
237 : : : EnvObj(env),
238 : : d_propEngine(nullptr),
239 : : d_lazyProof(
240 : 98344 : env.isTheoryProofProducing()
241 : : ? new LazyCDProof(
242 : 20882 : env, nullptr, userContext(), "TheoryEngine::LazyCDProof")
243 : : : nullptr),
244 : 49172 : d_tepg(new TheoryEngineProofGenerator(env, userContext())),
245 : : d_tc(nullptr),
246 : : d_sharedSolver(nullptr),
247 : : d_quantEngine(nullptr),
248 : 49172 : 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 : 168398 : d_cp(nullptr)
269 : : {
270 [ + + ]: 737580 : for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
271 : 688408 : ++ theoryId)
272 : : {
273 : 688408 : d_theoryTable[theoryId] = NULL;
274 : 688408 : d_theoryOut[theoryId] = NULL;
275 : : }
276 : :
277 [ + + ]: 49172 : if (options().smt.sortInference)
278 : : {
279 : 35 : d_sortInfer.reset(new SortInference(env));
280 : : }
281 : 49172 : if (options().theory.conflictProcessMode
282 [ + + ]: 49172 : != 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 : 49172 : d_true = NodeManager::currentNM()->mkConst<bool>(true);
290 : 49172 : d_false = NodeManager::currentNM()->mkConst<bool>(false);
291 : 49172 : }
292 : :
293 : 97832 : TheoryEngine::~TheoryEngine() {
294 : :
295 [ + + ]: 733740 : for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
296 [ + + ]: 684824 : if(d_theoryTable[theoryId] != NULL) {
297 [ + - ]: 684797 : delete d_theoryTable[theoryId];
298 [ + - ]: 684797 : delete d_theoryOut[theoryId];
299 : : }
300 : : }
301 : 97832 : }
302 : :
303 : 692153 : void TheoryEngine::interrupt() { d_interrupted = true; }
304 : 2147970 : void TheoryEngine::preRegister(TNode preprocessed) {
305 [ + - ]: 4295930 : Trace("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
306 : 2147970 : << std::endl;
307 : 2147970 : d_preregisterQueue.push(preprocessed);
308 : :
309 [ + + ]: 2147970 : if (!d_inPreregister) {
310 : : // We're in pre-register
311 : 2011650 : d_inPreregister = true;
312 : :
313 : : // Process the pre-registration queue
314 [ + + ]: 4159600 : while (!d_preregisterQueue.empty()) {
315 : : // Get the next atom to pre-register
316 : 2147970 : preprocessed = d_preregisterQueue.front();
317 : 2147970 : d_preregisterQueue.pop();
318 : :
319 : : // the atom should not have free variables
320 [ + - ]: 4295930 : Trace("theory") << "TheoryEngine::preRegister: " << preprocessed
321 : 2147970 : << std::endl;
322 [ + - ]: 2147970 : if (Configuration::isAssertionBuild())
323 : : {
324 : 4295930 : std::unordered_set<Node> fvs;
325 : 2147970 : expr::getFreeVariables(preprocessed, fvs);
326 [ - + ]: 2147970 : 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 [ - + ][ - + ]: 2147970 : 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 [ - + ][ - + ]: 2147970 : Assert(d_sharedSolver != nullptr);
[ - - ]
339 : 2147970 : d_sharedSolver->preRegister(preprocessed);
340 : : }
341 : :
342 : : // Leaving pre-register
343 : 2011640 : d_inPreregister = false;
344 : : }
345 : 2147950 : }
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 : 15807000 : void TheoryEngine::check(Theory::Effort effort) {
399 : : // spendResource();
400 : :
401 : : // Reset the interrupt flag
402 : 15807000 : 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 : 15807000 : d_outputChannelUsed = false;
429 : :
430 : : // Mark the lemmas flag (no lemmas added)
431 : 15807000 : d_lemmasAdded = false;
432 : :
433 [ + - ][ - - ]: 15807000 : 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 [ + + ]: 15807000 : if (Theory::fullEffort(effort)) {
437 : 159947 : spendResource(Resource::TheoryFullCheckStep);
438 : 159947 : d_factsAsserted = true;
439 : 159947 : d_tc->resetRound();
440 : : }
441 : :
442 : : // check with the theory modules
443 [ + + ]: 15808500 : for (TheoryEngineModule* tem : d_modules)
444 : : {
445 : 1516 : tem->check(effort);
446 : : }
447 : :
448 : 15807000 : auto rm = d_env.getResourceManager();
449 : :
450 : : // Check until done
451 [ + + ][ + + ]: 29258400 : while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
[ + + ][ + + ]
452 : :
453 [ + - ]: 13721900 : Trace("theory") << "TheoryEngine::check(" << effort << "): running check" << endl;
454 : :
455 [ + - ]: 13721900 : Trace("theory::assertions") << endl;
456 [ - + ]: 13721900 : if (TraceIsOn("theory::assertions")) {
457 : 0 : printAssertions("theory::assertions");
458 : : }
459 : :
460 [ + + ]: 13721900 : if(Theory::fullEffort(effort)) {
461 [ + - ]: 175761 : Trace("theory::assertions::fulleffort") << endl;
462 [ - + ]: 175761 : if (TraceIsOn("theory::assertions::fulleffort")) {
463 : 0 : printAssertions("theory::assertions::fulleffort");
464 : : }
465 : : }
466 : :
467 : : // Note that we've discharged all the facts
468 : 13721900 : d_factsAsserted = false;
469 : :
470 : : // Do the checking
471 [ + + ][ + + ]: 13721900 : CVC5_FOR_EACH_THEORY;
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + + ][ - + ]
[ - - ][ - + ]
472 : :
473 [ + - ]: 13451400 : Trace("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
474 : :
475 : : // We are still satisfiable, propagate as much as possible
476 : 13451400 : propagate(effort);
477 : :
478 : : // Interrupt in case we reached a resource limit.
479 [ - + ]: 13451400 : if (rm->out())
480 : : {
481 : 0 : interrupt();
482 : 0 : return;
483 : : }
484 : :
485 [ + + ]: 13451400 : if (Theory::fullEffort(effort))
486 : : {
487 : 128026 : d_stats.d_fullEffortChecks++;
488 : : // We do combination if all has been processed and we are in fullcheck
489 [ + + ][ + + ]: 246075 : if (logicInfo().isSharingEnabled() && !d_factsAsserted && !needCheck()
490 [ + + ][ + - ]: 246075 : && !d_inConflict)
[ + + ]
491 : : {
492 : 64937 : d_stats.d_combineTheoriesCalls++;
493 : : // Do the combination
494 [ + - ]: 129874 : Trace("theory") << "TheoryEngine::check(" << effort
495 : 64937 : << "): running combination" << endl;
496 : : {
497 : : TimerStat::CodeTimer combineTheoriesTimer(
498 : 129874 : d_stats.d_combineTheoriesTime);
499 : 64937 : d_tc->combineTheories();
500 : : }
501 [ + + ]: 64937 : if (logicInfo().isQuantified())
502 : : {
503 : 44663 : d_quantEngine->notifyCombineTheories();
504 : : }
505 : : }
506 : : }
507 : : else
508 : : {
509 [ - + ][ - + ]: 13323400 : Assert(effort == Theory::EFFORT_STANDARD);
[ - - ]
510 : 13323400 : d_stats.d_stdEffortChecks++;
511 : : }
512 : :
513 : : // Interrupt in case we reached a resource limit.
514 [ - + ]: 13451400 : 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 [ + + ][ + + ]: 15807000 : if( Theory::fullEffort(effort) && ! d_inConflict && ! needCheck() ) {
[ + + ][ + + ]
523 : 56034 : d_stats.d_lcEffortChecks++;
524 [ + - ]: 56034 : Trace("theory::assertions-model") << endl;
525 [ - + ]: 56034 : if (TraceIsOn("theory::assertions-model")) {
526 : 0 : printAssertions("theory::assertions-model");
527 : : }
528 : : // reset the model in the combination engine
529 : 56034 : d_tc->resetModel();
530 : : //checks for theories requiring the model go at last call
531 [ + + ]: 840506 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
532 : : {
533 [ + + ]: 784474 : if (theoryId != THEORY_QUANTIFIERS)
534 : : {
535 : 728442 : Theory* theory = d_theoryTable[theoryId];
536 [ + - ][ + + ]: 728442 : if (theory && isTheoryEnabled(theoryId))
[ + + ]
537 : : {
538 [ + + ]: 443434 : if (theory->needsCheckLastEffort())
539 : : {
540 [ + + ]: 28834 : if (!d_tc->buildModel())
541 : : {
542 : 2 : break;
543 : : }
544 : 28832 : theory->check(Theory::EFFORT_LAST_CALL);
545 : : }
546 : : }
547 : : }
548 : : }
549 [ + - ]: 56034 : if (!d_inConflict)
550 : : {
551 [ + + ]: 56034 : if (logicInfo().isQuantified())
552 : : {
553 : : // quantifiers engine must check at last call effort
554 : 45916 : d_quantEngine->check(Theory::EFFORT_LAST_CALL);
555 : : }
556 : : // notify the theory modules of the model
557 [ + + ]: 56364 : for (TheoryEngineModule* tem : d_modules)
558 : : {
559 [ + + ]: 335 : if (!tem->needsCandidateModel())
560 : : {
561 : : // module does not need candidate model
562 : 302 : continue;
563 : : }
564 [ - + ]: 33 : if (!d_tc->buildModel())
565 : : {
566 : : // model failed to build, we are done
567 : 0 : break;
568 : : }
569 : 33 : tem->notifyCandidateModel(getModel());
570 : : }
571 : : }
572 : : }
573 : :
574 : 15807000 : Trace("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
575 [ + - ][ - - ]: 15807000 : Trace("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
576 : :
577 : : // post check with the theory modules
578 [ + + ]: 15808500 : for (TheoryEngineModule* tem : d_modules)
579 : : {
580 : 1516 : tem->postCheck(effort);
581 : : }
582 [ + + ]: 15807000 : if (Theory::fullEffort(effort))
583 : : {
584 [ + + ][ + + ]: 159937 : if (!d_inConflict && !needCheck())
[ + + ]
585 : : {
586 : : // if some theory believes there is a conflict, but it is was not
587 : : // processed, we mark incomplete.
588 [ + + ]: 363465 : for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST;
589 : 339234 : ++theoryId)
590 : : {
591 : 339234 : Theory* theory = d_theoryTable[theoryId];
592 [ + - ][ + + ]: 339234 : if (theory && theory->getTheoryState() != nullptr)
[ + + ]
593 : : {
594 [ - + ]: 315003 : if (theory->getTheoryState()->isInConflict())
595 : : {
596 : 0 : setModelUnsound(theoryId,
597 : : IncompleteId::UNPROCESSED_THEORY_CONFLICT);
598 : 0 : Assert(false) << "Unprocessed theory conflict from " << theoryId;
599 : : break;
600 : : }
601 : : }
602 : : }
603 : : // Do post-processing of model from the theories (e.g. used for
604 : : // THEORY_SEP to construct heap model)
605 : 24231 : d_tc->postProcessModel(d_modelUnsound.get());
606 : : }
607 : : }
608 : 0 : } catch(const theory::Interrupted&) {
609 [ - - ]: 0 : Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
610 : : }
611 : : }
612 : :
613 : 13451400 : void TheoryEngine::propagate(Theory::Effort effort)
614 : : {
615 : : // Reset the interrupt flag
616 : 13451400 : d_interrupted = false;
617 : :
618 : : // Definition of the statement that is to be run by every theory
619 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
620 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
621 : : #endif
622 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
623 : : if (theory::TheoryTraits<THEORY>::hasPropagate \
624 : : && isTheoryEnabled(THEORY)) \
625 : : { \
626 : : theoryOf(THEORY)->propagate(effort); \
627 : : }
628 : :
629 : : // Reset the interrupt flag
630 : 13451400 : d_interrupted = false;
631 : :
632 : : // Propagate for each theory using the statement above
633 [ + + ][ + + ]: 13451400 : CVC5_FOR_EACH_THEORY;
634 : 13451400 : }
635 : :
636 : 11984900 : Node TheoryEngine::getNextDecisionRequest()
637 : : {
638 : 11984900 : return d_decManager->getNextDecisionRequest();
639 : : }
640 : :
641 : 240891 : bool TheoryEngine::properConflict(TNode conflict) const {
642 : : bool value;
643 [ + + ]: 240891 : if (conflict.getKind() == Kind::AND)
644 : : {
645 [ + + ]: 2785590 : for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
646 [ - + ]: 2546180 : if (! getPropEngine()->hasValue(conflict[i], value)) {
647 [ - - ]: 0 : Trace("properConflict") << "Bad conflict is due to unassigned atom: "
648 : 0 : << conflict[i] << endl;
649 : 0 : return false;
650 : : }
651 [ - + ]: 2546180 : if (! value) {
652 [ - - ]: 0 : Trace("properConflict") << "Bad conflict is due to false atom: "
653 : 0 : << conflict[i] << endl;
654 : 0 : return false;
655 : : }
656 [ - + ]: 2546180 : if (conflict[i] != rewrite(conflict[i]))
657 : : {
658 [ - - ]: 0 : Trace("properConflict")
659 [ - - ]: 0 : << "Bad conflict is due to atom not in normal form: " << conflict[i]
660 : 0 : << " vs " << rewrite(conflict[i]) << endl;
661 : 0 : return false;
662 : : }
663 : : }
664 : : }
665 : : else
666 : : {
667 [ - + ]: 1478 : if (! getPropEngine()->hasValue(conflict, value)) {
668 [ - - ]: 0 : Trace("properConflict") << "Bad conflict is due to unassigned atom: "
669 : 0 : << conflict << endl;
670 : 0 : return false;
671 : : }
672 [ - + ]: 1478 : if(! value) {
673 [ - - ]: 0 : Trace("properConflict") << "Bad conflict is due to false atom: "
674 : 0 : << conflict << endl;
675 : 0 : return false;
676 : : }
677 [ - + ]: 1478 : if (conflict != rewrite(conflict))
678 : : {
679 [ - - ]: 0 : Trace("properConflict")
680 : 0 : << "Bad conflict is due to atom not in normal form: " << conflict
681 : 0 : << " vs " << rewrite(conflict) << endl;
682 : 0 : return false;
683 : : }
684 : : }
685 : 240891 : return true;
686 : : }
687 : :
688 : 1725240 : TheoryModel* TheoryEngine::getModel()
689 : : {
690 [ - + ][ - + ]: 1725240 : Assert(d_tc != nullptr);
[ - - ]
691 : 1725240 : TheoryModel* m = d_tc->getModel();
692 [ - + ][ - + ]: 1725240 : Assert(m != nullptr);
[ - - ]
693 : 1725240 : return m;
694 : : }
695 : :
696 : 20520 : TheoryModel* TheoryEngine::getBuiltModel()
697 : : {
698 [ - + ][ - + ]: 20520 : Assert(d_tc != nullptr);
[ - - ]
699 : : // If this method was called, produceModels should be true.
700 [ - + ][ - + ]: 20520 : AlwaysAssert(options().smt.produceModels);
[ - - ]
701 : : // we must build model at this point
702 [ - + ]: 20520 : if (!d_tc->buildModel())
703 : : {
704 : 0 : return nullptr;
705 : : }
706 : 20520 : return d_tc->getModel();
707 : : }
708 : :
709 : 24758 : bool TheoryEngine::buildModel()
710 : : {
711 [ - + ][ - + ]: 24758 : Assert(d_tc != nullptr);
[ - - ]
712 : 24758 : return d_tc->buildModel();
713 : : }
714 : :
715 : 279650000 : bool TheoryEngine::isTheoryEnabled(theory::TheoryId theoryId) const
716 : : {
717 : 279650000 : return logicInfo().isTheoryEnabled(theoryId);
718 : : }
719 : :
720 : 60368500 : theory::TheoryId TheoryEngine::theoryExpPropagation(theory::TheoryId tid) const
721 : : {
722 [ + + ]: 60368500 : if (options().theory.eeMode == options::EqEngineMode::CENTRAL)
723 : : {
724 : 13738 : if (EqEngineManagerCentral::usesCentralEqualityEngine(options(), tid)
725 [ + + ][ + + ]: 13738 : && Theory::expUsingCentralEqualityEngine(tid))
[ + + ]
726 : : {
727 : 5865 : return THEORY_BUILTIN;
728 : : }
729 : : }
730 : 60362600 : return tid;
731 : : }
732 : :
733 : 49226 : bool TheoryEngine::presolve() {
734 : : // Reset the interrupt flag
735 : 49226 : d_interrupted = false;
736 : :
737 : : // Reset the decision manager. This clears its decision strategies that are
738 : : // no longer valid in this user context.
739 : 49226 : d_decManager->presolve();
740 : :
741 : : try {
742 : : // Definition of the statement that is to be run by every theory
743 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
744 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
745 : : #endif
746 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
747 : : if (theory::TheoryTraits<THEORY>::hasPresolve) \
748 : : { \
749 : : theoryOf(THEORY)->presolve(); \
750 : : if (d_inConflict) \
751 : : { \
752 : : return true; \
753 : : } \
754 : : }
755 : :
756 : : // Presolve for each theory using the statement above
757 [ - + ][ - + ]: 49226 : CVC5_FOR_EACH_THEORY;
[ - + ][ - + ]
[ - + ][ - + ]
[ - + ][ - + ]
[ - + ]
758 : 0 : } catch(const theory::Interrupted&) {
759 [ - - ]: 0 : Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
760 : : }
761 : : // presolve with the theory engine modules as well
762 [ + + ]: 49666 : for (TheoryEngineModule* tem : d_modules)
763 : : {
764 : 440 : tem->presolve();
765 : : }
766 : :
767 : : // return whether we have a conflict
768 : 49226 : return false;
769 : : }/* TheoryEngine::presolve() */
770 : :
771 : 49213 : void TheoryEngine::postsolve(prop::SatValue result)
772 : : {
773 : : // postsolve with the theory engine modules as well
774 [ + + ]: 49653 : for (TheoryEngineModule* tem : d_modules)
775 : : {
776 : 440 : tem->postsolve(result);
777 : : }
778 : :
779 : : // Reset the interrupt flag
780 : 49213 : d_interrupted = false;
781 : 49213 : }
782 : :
783 : 5185 : void TheoryEngine::notifyRestart() {
784 : : // Reset the interrupt flag
785 : 5185 : d_interrupted = false;
786 : :
787 : : // Definition of the statement that is to be run by every theory
788 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
789 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
790 : : #endif
791 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
792 : : if (theory::TheoryTraits<THEORY>::hasNotifyRestart \
793 : : && isTheoryEnabled(THEORY)) \
794 : : { \
795 : : theoryOf(THEORY)->notifyRestart(); \
796 : : }
797 : :
798 : : // notify each theory using the statement above
799 [ + + ]: 5185 : CVC5_FOR_EACH_THEORY;
800 : 5185 : }
801 : :
802 : 445220 : void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder& learned)
803 : : {
804 : : // Reset the interrupt flag
805 : 445220 : d_interrupted = false;
806 : :
807 : : // Definition of the statement that is to be run by every theory
808 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
809 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
810 : : #endif
811 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
812 : : if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) \
813 : : { \
814 : : theoryOf(THEORY)->ppStaticLearn(in, learned); \
815 : : }
816 : :
817 : : // static learning for each theory using the statement above
818 : 445220 : CVC5_FOR_EACH_THEORY;
819 : 445220 : }
820 : :
821 : 290403 : bool TheoryEngine::hasSatValue(TNode n, bool& value) const
822 : : {
823 [ + + ]: 290403 : if (d_propEngine->isSatLiteral(n))
824 : : {
825 : 290250 : return d_propEngine->hasValue(n, value);
826 : : }
827 : 153 : return false;
828 : : }
829 : :
830 : 1733460 : bool TheoryEngine::hasSatValue(TNode n) const
831 : : {
832 [ + + ]: 1733460 : if (d_propEngine->isSatLiteral(n))
833 : : {
834 : : bool value;
835 : 1732540 : return d_propEngine->hasValue(n, value);
836 : : }
837 : 924 : return false;
838 : : }
839 : :
840 : 1052 : bool TheoryEngine::isRelevant(Node lit) const
841 : : {
842 [ + - ]: 1052 : if (d_relManager != nullptr)
843 : : {
844 : 1052 : return d_relManager->isRelevant(lit);
845 : : }
846 : : // otherwise must assume its relevant
847 : 0 : return true;
848 : : }
849 : :
850 : 57933 : bool TheoryEngine::isLegalElimination(TNode x, TNode val)
851 : : {
852 [ - + ][ - + ]: 57933 : Assert(x.isVar());
[ - - ]
853 [ + + ]: 57933 : if (expr::hasSubterm(val, x))
854 : : {
855 : 14695 : return false;
856 : : }
857 [ + + ]: 43238 : if (val.getType() != x.getType())
858 : : {
859 : 4 : return false;
860 : : }
861 [ + + ][ + - ]: 43234 : if (!options().smt.produceModels || options().smt.modelVarElimUneval)
[ + - ]
862 : : {
863 : : // Don't care about the model, or we allow variables to be eliminated by
864 : : // unevaluatable terms, we can eliminate. Notice that when
865 : : // options().smt.modelVarElimUneval is true, val may contain unevaluatable
866 : : // kinds. This means that e.g. a Boolean variable may be eliminated based on
867 : : // an equality (= b (forall ((x)) (P x))), where its model value is (forall
868 : : // ((x)) (P x)).
869 : 43234 : return true;
870 : : }
871 : : // If models are enabled, then it depends on whether the term contains any
872 : : // unevaluable operators like FORALL, SINE, etc. Having such operators makes
873 : : // model construction contain non-constant values for variables, which is
874 : : // not ideal from a user perspective.
875 : : // We also insist on this check since the term to eliminate should never
876 : : // contain quantifiers, or else variable shadowing issues may arise.
877 : : // there should be a model object
878 : 0 : TheoryModel* tm = getModel();
879 : 0 : Assert(tm != nullptr);
880 : 0 : return tm->isLegalElimination(x, val);
881 : : }
882 : :
883 : 292520 : theory::Theory::PPAssertStatus TheoryEngine::solve(
884 : : TrustNode tliteral, TrustSubstitutionMap& substitutionOut)
885 : : {
886 [ - + ][ - + ]: 292520 : Assert(tliteral.getKind() == TrustNodeKind::LEMMA);
[ - - ]
887 : : // Reset the interrupt flag
888 : 292520 : d_interrupted = false;
889 : :
890 : 585040 : TNode literal = tliteral.getNode();
891 [ + + ]: 292521 : TNode atom = literal.getKind() == Kind::NOT ? literal[0] : literal;
892 [ + - ][ - + ]: 292520 : Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
[ - - ]
893 : :
894 : 292520 : TheoryId tid = d_env.theoryOf(atom);
895 : : // Note that ppAssert is called before ppRewrite.
896 [ + + ][ + - ]: 292520 : if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
[ + + ]
897 : : {
898 : 2 : stringstream ss;
899 : 1 : ss << "The logic was specified as " << logicInfo().getLogicString()
900 : 2 : << ", which doesn't include " << tid
901 : 1 : << ", but got a theory atom for that theory." << std::endl
902 : 1 : << "The atom:" << std::endl
903 : 1 : << atom;
904 : 1 : throw LogicException(ss.str());
905 : : }
906 : :
907 : : Theory::PPAssertStatus solveStatus =
908 : 292519 : d_theoryTable[tid]->ppAssert(tliteral, substitutionOut);
909 [ + - ]: 292519 : Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
910 : 585038 : return solveStatus;
911 : : }
912 : :
913 : 4694660 : TrustNode TheoryEngine::ppRewrite(TNode term,
914 : : std::vector<theory::SkolemLemma>& lems)
915 : : {
916 [ - + ][ - + ]: 4694660 : Assert(lems.empty());
[ - - ]
917 : 4694660 : TheoryId tid = d_env.theoryOf(term);
918 : : // We check whether the theory is enabled here (instead of only during solve),
919 : : // since there are corner cases where facts may involve terms that belong
920 : : // to other theories, e.g. equalities between variables belong to UF when
921 : : // theoryof-mode is `term`.
922 [ - + ][ - - ]: 4694660 : if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
[ - + ]
923 : : {
924 : 0 : stringstream ss;
925 : 0 : ss << "The logic was specified as " << logicInfo().getLogicString()
926 : 0 : << ", which doesn't include " << tid
927 : 0 : << ", but got a term for that theory during solving." << std::endl
928 : 0 : << "The term:" << std::endl
929 : 0 : << term;
930 : 0 : throw LogicException(ss.str());
931 : : }
932 : 4694670 : TrustNode trn = d_theoryTable[tid]->ppRewrite(term, lems);
933 : : // should never introduce a skolem to eliminate an equality
934 [ + + ][ - + ]: 4694650 : Assert(lems.empty() || term.getKind() != Kind::EQUAL);
[ - + ][ - - ]
935 [ + + ]: 4694650 : if (!isProofEnabled())
936 : : {
937 : 2496520 : return trn;
938 : : }
939 [ - + ][ - + ]: 2198130 : Assert(d_lazyProof != nullptr);
[ - - ]
940 : : // if proofs are enabled, must ensure we have proofs for all the skolem lemmas
941 [ + + ]: 2200970 : for (SkolemLemma& skl : lems)
942 : : {
943 : 5688 : TrustNode tskl = skl.d_lemma;
944 [ - + ][ - + ]: 2844 : Assert(tskl.getKind() == TrustNodeKind::LEMMA);
[ - - ]
945 [ + + ]: 2844 : if (tskl.getGenerator() == nullptr)
946 : : {
947 : 1790 : Node proven = tskl.getProven();
948 : 895 : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
949 : 1790 : d_lazyProof->addTrustedStep(
950 : 895 : proven, TrustId::THEORY_PREPROCESS_LEMMA, {}, {tidn});
951 [ + - ]: 895 : skl.d_lemma = TrustNode::mkTrustLemma(proven, d_lazyProof.get());
952 : : }
953 : : }
954 : : // notice that we don't ensure proofs are processed for the returned (rewrite)
955 : : // trust node, this is the responsibility of the caller, i.e. theory
956 : : // preprocessor.
957 : 2198130 : return trn;
958 : : }
959 : :
960 : 4343090 : TrustNode TheoryEngine::ppStaticRewrite(TNode term)
961 : : {
962 : 4343090 : TheoryId tid = d_env.theoryOf(term);
963 [ + + ][ + - ]: 4343090 : if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
[ + + ]
964 : : {
965 : 4 : stringstream ss;
966 : 2 : ss << "The logic was specified as " << logicInfo().getLogicString()
967 : 4 : << ", which doesn't include " << tid
968 : 2 : << ", but got a preprocessing-time term for that theory."
969 : 2 : << std::endl
970 : 2 : << "The term:" << std::endl
971 : 2 : << term;
972 : 2 : throw LogicException(ss.str());
973 : : }
974 : 4343090 : return d_theoryTable[tid]->ppStaticRewrite(term);
975 : : }
976 : :
977 : 66088 : void TheoryEngine::notifyPreprocessedAssertions(
978 : : const std::vector<Node>& assertions) {
979 : : // call all the theories
980 [ + + ]: 991320 : for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
981 : 925232 : ++theoryId) {
982 [ + - ]: 925232 : if (d_theoryTable[theoryId]) {
983 : 925232 : theoryOf(theoryId)->ppNotifyAssertions(assertions);
984 : : }
985 : : }
986 [ + + ]: 66088 : if (d_relManager != nullptr)
987 : : {
988 : 413 : d_relManager->notifyPreprocessedAssertions(assertions, true);
989 : : }
990 : 66088 : }
991 : :
992 : 60053200 : bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
993 : : // What and where we are asserting
994 : 120106000 : NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
995 : : // What and where it came from
996 : 120106000 : NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp);
997 : :
998 : : // See if the theory already got this literal
999 : 60053200 : PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
1000 [ + + ]: 60053200 : if (find != d_propagationMap.end()) {
1001 : : // The theory already knows this
1002 [ + - ]: 16487600 : Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl;
1003 : 16487600 : return false;
1004 : : }
1005 : :
1006 [ + - ]: 43565600 : Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << endl;
1007 : :
1008 : : // Mark the propagation
1009 : 43565600 : d_propagationMap[toAssert] = toExplain;
1010 : 43565600 : d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
1011 : :
1012 : 43565600 : return true;
1013 : : }
1014 : :
1015 : :
1016 : 100635000 : void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
1017 [ + - ]: 100635000 : Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
1018 : :
1019 [ - + ][ - + ]: 100635000 : Assert(toTheoryId != fromTheoryId);
[ - - ]
1020 : 201270000 : if (toTheoryId != THEORY_SAT_SOLVER
1021 [ + + ][ - + ]: 100635000 : && !isTheoryEnabled(toTheoryId))
[ - + ]
1022 : : {
1023 : 0 : stringstream ss;
1024 : 0 : ss << "The logic was specified as " << logicInfo().getLogicString()
1025 : 0 : << ", which doesn't include " << toTheoryId
1026 : 0 : << ", but got an asserted fact to that theory." << endl
1027 : 0 : << "The fact:" << endl
1028 : 0 : << assertion;
1029 : 0 : throw LogicException(ss.str());
1030 : : }
1031 : :
1032 [ + + ]: 100635000 : if (d_inConflict) {
1033 : 172109 : return;
1034 : : }
1035 : :
1036 : : // If sharing is disabled, things are easy
1037 [ + + ]: 100463000 : if (!logicInfo().isSharingEnabled())
1038 : : {
1039 [ - + ][ - + ]: 40409700 : Assert(assertion == originalAssertion);
[ - - ]
1040 [ + + ]: 40409700 : if (fromTheoryId == THEORY_SAT_SOLVER) {
1041 : : // Send to the apropriate theory
1042 : 35458100 : theory::Theory* toTheory = theoryOf(toTheoryId);
1043 : : // We assert it, and we know it's preregistereed
1044 : 35458100 : toTheory->assertFact(assertion, true);
1045 : : // Mark that we have more information
1046 : 35458100 : d_factsAsserted = true;
1047 : : } else {
1048 [ - + ][ - + ]: 4951600 : Assert(toTheoryId == THEORY_SAT_SOLVER);
[ - - ]
1049 : : // Check for propositional conflict
1050 : : bool value;
1051 [ + + ]: 4951600 : if (d_propEngine->hasValue(assertion, value)) {
1052 [ + + ]: 3476860 : if (!value) {
1053 [ + - ]: 73811 : Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
1054 [ + - ]: 147622 : Trace("dtview::conflict")
1055 : 73811 : << ":THEORY-CONFLICT: " << assertion << std::endl;
1056 : 73811 : markInConflict();
1057 : : } else {
1058 : 3403050 : return;
1059 : : }
1060 : : }
1061 : 1548560 : d_propagatedLiterals.push_back(assertion);
1062 : : }
1063 : 37006700 : return;
1064 : : }
1065 : :
1066 : : // determine the actual theory that will process/explain the fact, which is
1067 : : // THEORY_BUILTIN if the theory uses the central equality engine
1068 : 60053200 : TheoryId toTheoryIdProp = theoryExpPropagation(toTheoryId);
1069 : : // If sending to the shared solver, it's also simple
1070 [ + + ]: 60053200 : if (toTheoryId == THEORY_BUILTIN) {
1071 [ + + ]: 19114800 : if (markPropagation(
1072 : : assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
1073 : : {
1074 : : // assert to the shared solver
1075 : 10652200 : bool polarity = assertion.getKind() != Kind::NOT;
1076 [ + + ]: 10652200 : TNode atom = polarity ? assertion : assertion[0];
1077 : 10652200 : d_sharedSolver->assertShared(atom, polarity, assertion);
1078 : : }
1079 : 19114800 : return;
1080 : : }
1081 : :
1082 : : // Things from the SAT solver are already normalized, so they go
1083 : : // directly to the apropriate theory
1084 [ + + ]: 40938400 : if (fromTheoryId == THEORY_SAT_SOLVER) {
1085 : : // We know that this is normalized, so just send it off to the theory
1086 [ + + ]: 15637200 : if (markPropagation(
1087 : : assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
1088 : : {
1089 : : // Is it preregistered
1090 [ - - ]: 15530700 : bool preregistered = d_propEngine->isSatLiteral(assertion)
1091 [ + + ][ + + ]: 15530700 : && d_env.theoryOf(assertion) == toTheoryId;
[ + + ][ + - ]
[ - - ]
1092 : : // We assert it
1093 : 15530700 : theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1094 : : // Mark that we have more information
1095 : 15530700 : d_factsAsserted = true;
1096 : : }
1097 : 15637200 : return;
1098 : : }
1099 : :
1100 : : // Propagations to the SAT solver are just enqueued for pickup by
1101 : : // the SAT solver later
1102 [ + + ]: 25301300 : if (toTheoryId == THEORY_SAT_SOLVER) {
1103 [ - + ][ - + ]: 19307600 : Assert(toTheoryIdProp == toTheoryId);
[ - - ]
1104 [ + + ]: 19307600 : if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1105 : : // Enqueue for propagation to the SAT solver
1106 : 12000700 : d_propagatedLiterals.push_back(assertion);
1107 : : // Check for propositional conflicts
1108 : : bool value;
1109 [ + + ][ + + ]: 12000700 : if (d_propEngine->hasValue(assertion, value) && !value) {
[ + - ][ + + ]
[ - - ]
1110 [ + - ]: 150914 : Trace("theory::propagate")
1111 : 0 : << "TheoryEngine::assertToTheory(" << assertion << ", "
1112 : 0 : << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)"
1113 : 75457 : << endl;
1114 [ + - ]: 150914 : Trace("dtview::conflict")
1115 : 75457 : << ":THEORY-CONFLICT: " << assertion << std::endl;
1116 : 75457 : markInConflict();
1117 : : }
1118 : : }
1119 : 19307600 : return;
1120 : : }
1121 : :
1122 : 7882200 : Assert(assertion.getKind() == Kind::EQUAL
1123 : : || (assertion.getKind() == Kind::NOT
1124 : : && assertion[0].getKind() == Kind::EQUAL));
1125 : :
1126 : : // Normalize
1127 : 11987200 : Node normalizedLiteral = rewrite(assertion);
1128 : :
1129 : : // See if it rewrites false directly -> conflict
1130 [ + + ]: 5993620 : if (normalizedLiteral.isConst()) {
1131 [ + + ]: 49614 : if (!normalizedLiteral.getConst<bool>()) {
1132 : : // Mark the propagation for explanations
1133 [ + - ]: 884 : if (markPropagation(normalizedLiteral,
1134 : : originalAssertion,
1135 : : toTheoryIdProp,
1136 : : fromTheoryId))
1137 : : {
1138 : : // special case, trust node has no proof generator
1139 : 884 : TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
1140 : : // Get the explanation (conflict will figure out where it came from)
1141 : 884 : conflict(trnn, InferenceId::CONFLICT_REWRITE_LIT, toTheoryId);
1142 : : } else {
1143 : 0 : Unreachable();
1144 : : }
1145 : 884 : return;
1146 : : }
1147 : : }
1148 : :
1149 : : // Try and assert (note that we assert the non-normalized one)
1150 [ + + ]: 5992740 : if (markPropagation(
1151 : : assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
1152 : : {
1153 : : // Check if has been pre-registered with the theory
1154 [ - - ]: 5381160 : bool preregistered = d_propEngine->isSatLiteral(assertion)
1155 [ + + ][ + + ]: 5381160 : && d_env.theoryOf(assertion) == toTheoryId;
[ + + ][ + - ]
[ - - ]
1156 : : // Assert away
1157 : 5381160 : theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1158 : 5381160 : d_factsAsserted = true;
1159 : : }
1160 : :
1161 : 5992740 : return;
1162 : : }
1163 : :
1164 : 51005400 : void TheoryEngine::assertFact(TNode literal)
1165 : : {
1166 [ + - ]: 51005400 : Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
1167 : :
1168 : : // spendResource();
1169 : :
1170 : : // If we're in conflict, nothing to do
1171 [ + + ]: 51005400 : if (d_inConflict) {
1172 : 32118 : return;
1173 : : }
1174 : :
1175 : : // Get the atom
1176 : 50973300 : bool polarity = literal.getKind() != Kind::NOT;
1177 [ + + ]: 101947000 : TNode atom = polarity ? literal : literal[0];
1178 : :
1179 [ + + ]: 50973300 : if (logicInfo().isSharingEnabled())
1180 : : {
1181 : : // If any shared terms, it's time to do sharing work
1182 : 15515200 : d_sharedSolver->preNotifySharedFact(atom);
1183 : :
1184 : : // If it's an equality, assert it to the shared term manager, even though the terms are not
1185 : : // yet shared. As the terms become shared later, the shared terms manager will then add them
1186 : : // to the assert the equality to the interested theories
1187 [ + + ]: 15515200 : if (atom.getKind() == Kind::EQUAL)
1188 : : {
1189 : : // Assert it to the the owning theory
1190 : 7941010 : assertToTheory(literal,
1191 : : literal,
1192 : 7941010 : /* to */ d_env.theoryOf(atom),
1193 : : /* from */ THEORY_SAT_SOLVER);
1194 : : // Shared terms manager will assert to interested theories directly, as
1195 : : // the terms become shared
1196 : 7941010 : assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
1197 : :
1198 : : // Now, let's check for any atom triggers from lemmas
1199 : 7941010 : AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
1200 [ + + ]: 7988810 : while (!it.done()) {
1201 : 47801 : const AtomRequests::Request& request = it.get();
1202 : : Node toAssert =
1203 [ + + ]: 95602 : polarity ? (Node)request.d_atom : request.d_atom.notNode();
1204 [ + - ]: 95602 : Trace("theory::atoms") << "TheoryEngine::assertFact(" << literal
1205 : 47801 : << "): sending requested " << toAssert << endl;
1206 : 47801 : assertToTheory(
1207 : 47801 : toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
1208 : 47801 : it.next();
1209 : : }
1210 : : }
1211 : : else
1212 : : {
1213 : : // Not an equality, just assert to the appropriate theory
1214 : 7574160 : assertToTheory(literal,
1215 : : literal,
1216 : 7574160 : /* to */ d_env.theoryOf(atom),
1217 : : /* from */ THEORY_SAT_SOLVER);
1218 : : }
1219 : : }
1220 : : else
1221 : : {
1222 : : // Assert the fact to the appropriate theory directly
1223 : 35458100 : assertToTheory(literal,
1224 : : literal,
1225 : 35458100 : /* to */ d_env.theoryOf(atom),
1226 : : /* from */ THEORY_SAT_SOLVER);
1227 : : }
1228 : : }
1229 : :
1230 : 28233500 : bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
1231 [ + - ]: 56467000 : Trace("theory::propagate")
1232 : 28233500 : << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
1233 : :
1234 : 56467000 : Trace("dtview::prop") << std::string(context()->getLevel(), ' ')
1235 : 28233500 : << ":THEORY-PROP: " << literal << endl;
1236 : :
1237 : : // spendResource();
1238 : :
1239 : : // Get the atom
1240 : 28233500 : bool polarity = literal.getKind() != Kind::NOT;
1241 [ + + ]: 28233500 : TNode atom = polarity ? literal : literal[0];
1242 : :
1243 [ + + ][ + + ]: 28233500 : if (logicInfo().isSharingEnabled() && atom.getKind() == Kind::EQUAL)
[ + + ]
1244 : : {
1245 [ + + ]: 19441100 : if (d_propEngine->isSatLiteral(literal)) {
1246 : : // We propagate SAT literals to SAT
1247 : 15580900 : assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1248 : : }
1249 [ + + ]: 19441100 : if (theory != THEORY_BUILTIN) {
1250 : : // Assert to the shared terms database
1251 : 11223700 : assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
1252 : : }
1253 : : }
1254 : : else
1255 : : {
1256 : : // Just send off to the SAT solver
1257 [ - + ][ - + ]: 8792410 : Assert(d_propEngine->isSatLiteral(literal));
[ - - ]
1258 : 8792410 : assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1259 : : }
1260 : :
1261 : 56467000 : return !d_inConflict;
1262 : : }
1263 : :
1264 : 2068660 : theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b)
1265 : : {
1266 [ - + ][ - + ]: 2068660 : Assert(a.getType() == b.getType());
[ - - ]
1267 : 2068660 : return d_sharedSolver->getEqualityStatus(a, b);
1268 : : }
1269 : :
1270 : 395 : void TheoryEngine::getDifficultyMap(std::map<Node, Node>& dmap,
1271 : : bool includeLemmas)
1272 : : {
1273 [ - + ][ - + ]: 395 : Assert(d_relManager != nullptr);
[ - - ]
1274 : 395 : d_relManager->getDifficultyMap(dmap, includeLemmas);
1275 : 395 : }
1276 : :
1277 : 2034 : theory::IncompleteId TheoryEngine::getModelUnsoundId() const
1278 : : {
1279 : 2034 : return d_modelUnsoundId.get();
1280 : : }
1281 : 14 : theory::IncompleteId TheoryEngine::getRefutationUnsoundId() const
1282 : : {
1283 : 14 : return d_refutationUnsoundId.get();
1284 : : }
1285 : :
1286 : 10732 : Node TheoryEngine::getCandidateModelValue(TNode var)
1287 : : {
1288 [ + + ]: 10732 : if (var.isConst())
1289 : : {
1290 : : // the model value of a constant must be itself
1291 : 174 : return var;
1292 : : }
1293 [ - + ][ - - ]: 21116 : Assert(d_sharedSolver->isShared(var))
1294 [ - + ][ - + ]: 10558 : << "node " << var << " is not shared" << std::endl;
[ - - ]
1295 : 10558 : return theoryOf(d_env.theoryOf(var.getType()))->getCandidateModelValue(var);
1296 : : }
1297 : :
1298 : 0 : std::unordered_set<TNode> TheoryEngine::getRelevantAssertions(bool& success)
1299 : : {
1300 : : // if there is no relevance manager, we fail
1301 [ - - ]: 0 : if (d_relManager == nullptr)
1302 : : {
1303 : 0 : success = false;
1304 : : // return empty set
1305 : 0 : return std::unordered_set<TNode>();
1306 : : }
1307 : 0 : return d_relManager->getRelevantAssertions(success);
1308 : : }
1309 : :
1310 : 212664 : TrustNode TheoryEngine::getExplanation(TNode node)
1311 : : {
1312 [ + - ]: 425328 : Trace("theory::explain") << "TheoryEngine::getExplanation(" << node
1313 : 0 : << "): current propagation index = "
1314 : 212664 : << d_propagationMapTimestamp << endl;
1315 : 212664 : bool polarity = node.getKind() != Kind::NOT;
1316 [ + + ]: 425328 : TNode atom = polarity ? node : node[0];
1317 : :
1318 : : // If we're not in shared mode, explanations are simple
1319 : 212664 : TrustNode texplanation;
1320 [ + + ]: 212664 : if (!logicInfo().isSharingEnabled())
1321 : : {
1322 [ + - ]: 189696 : Trace("theory::explain")
1323 : 0 : << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1324 [ - + ][ - - ]: 94848 : << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl;
1325 : :
1326 : 94848 : texplanation = theoryOf(atom)->explain(node);
1327 : 189696 : Node explanation = texplanation.getNode();
1328 [ + - ]: 189696 : Trace("theory::explain") << "TheoryEngine::getExplanation(" << node
1329 : 94848 : << ") => " << explanation << endl;
1330 [ + + ]: 94848 : if (isProofEnabled())
1331 : : {
1332 : 50095 : texplanation.debugCheckClosed(
1333 : : options(), "te-proof-exp", "texplanation no share", false);
1334 : : // check if no generator, if so, add THEORY_LEMMA
1335 [ - + ]: 50095 : if (texplanation.getGenerator() == nullptr)
1336 : : {
1337 : 0 : Node proven = texplanation.getProven();
1338 : 0 : TheoryId tid = theoryOf(atom)->getId();
1339 : 0 : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
1340 : 0 : d_lazyProof->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn});
1341 : : texplanation =
1342 [ - - ]: 0 : TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get());
1343 : : }
1344 : : }
1345 : : }
1346 : : else
1347 : : {
1348 [ + - ]: 235632 : Trace("theory::explain")
1349 : 117816 : << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
1350 : :
1351 : : // Initial thing to explain
1352 : : NodeTheoryPair toExplain(
1353 : 235632 : node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
1354 [ - + ][ - + ]: 117816 : Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
[ - - ]
1355 : :
1356 : 235632 : NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
1357 [ + - ]: 235632 : Trace("theory::explain")
1358 : 0 : << "TheoryEngine::getExplanation: explainer for node "
1359 : 0 : << nodeExplainerPair.d_node
1360 : 117816 : << " is theory: " << nodeExplainerPair.d_theory << std::endl;
1361 : :
1362 : : // Create the workplace for explanations
1363 : 353448 : std::vector<NodeTheoryPair> vec{d_propagationMap[toExplain]};
1364 : : // Process the explanation
1365 : 117816 : texplanation = getExplanation(vec);
1366 [ + - ]: 235632 : Trace("theory::explain") << "TheoryEngine::getExplanation(" << node
1367 [ - + ][ - - ]: 117816 : << ") => " << texplanation.getNode() << endl;
1368 : : }
1369 : : // notify the conflict as a lemma
1370 [ + + ]: 212697 : for (TheoryEngineModule* tem : d_modules)
1371 : : {
1372 : 33 : tem->notifyLemma(texplanation.getProven(),
1373 : : InferenceId::EXPLAINED_PROPAGATION,
1374 : : LemmaProperty::NONE,
1375 : : {},
1376 : 33 : {});
1377 : : }
1378 : 425328 : return texplanation;
1379 : : }
1380 : :
1381 : : struct AtomsCollect {
1382 : :
1383 : : std::vector<TNode> d_atoms;
1384 : : std::unordered_set<TNode> d_visited;
1385 : :
1386 : : public:
1387 : : typedef void return_type;
1388 : :
1389 : 1133060 : bool alreadyVisited(TNode current, TNode parent) {
1390 : : // Check if already visited
1391 [ + + ]: 1133060 : if (d_visited.find(current) != d_visited.end()) return true;
1392 : : // Don't visit non-boolean
1393 [ + + ]: 1039850 : if (!current.getType().isBoolean()) return true;
1394 : : // New node
1395 : 850283 : return false;
1396 : : }
1397 : :
1398 : 283750 : void visit(TNode current, TNode parent) {
1399 [ + + ]: 283750 : if (Theory::theoryOf(current) != theory::THEORY_BOOL) {
1400 : 96363 : d_atoms.push_back(current);
1401 : : }
1402 : 283750 : d_visited.insert(current);
1403 : 283750 : }
1404 : :
1405 : 94174 : void start(TNode node) {}
1406 : 94174 : void done(TNode node) {}
1407 : :
1408 : 94174 : std::vector<TNode> getAtoms() const {
1409 : 94174 : return d_atoms;
1410 : : }
1411 : : };
1412 : :
1413 : 94174 : void TheoryEngine::ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo)
1414 : : {
1415 [ - + ][ - + ]: 94174 : Assert(atomsTo != THEORY_LAST);
[ - - ]
1416 [ + - ]: 188348 : Trace("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(" << n << ", "
1417 : 94174 : << atomsTo << ")" << endl;
1418 : 94174 : AtomsCollect collectAtoms;
1419 : 94174 : NodeVisitor<AtomsCollect>::run(collectAtoms, n);
1420 : 94174 : ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
1421 : 94174 : }
1422 : :
1423 : 94174 : void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId atomsTo) {
1424 [ + + ]: 190537 : for (unsigned i = 0; i < atoms.size(); ++ i) {
1425 : :
1426 : : // Non-equality atoms are either owned by theory or they don't make sense
1427 [ + + ]: 96363 : if (atoms[i].getKind() != Kind::EQUAL)
1428 : : {
1429 : 81075 : continue;
1430 : : }
1431 : :
1432 : : // The equality
1433 : 93205 : Node eq = atoms[i];
1434 : : // Simple normalization to not repeat stuff
1435 [ - + ]: 93205 : if (eq[0] > eq[1]) {
1436 : 0 : eq = eq[1].eqNode(eq[0]);
1437 : : }
1438 : :
1439 : : // Rewrite the equality
1440 : 93205 : Node eqNormalized = rewrite(atoms[i]);
1441 : :
1442 [ + - ]: 186410 : Trace("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq
1443 : 93205 : << " with nf " << eqNormalized << endl;
1444 : :
1445 : : // If the equality is a boolean constant, we send immediately
1446 [ + + ]: 93205 : if (eqNormalized.isConst()) {
1447 [ - + ]: 2 : if (eqNormalized.getConst<bool>()) {
1448 : 0 : assertToTheory(eq, eqNormalized, /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1449 : : } else {
1450 : 2 : assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1451 : : }
1452 : 2 : continue;
1453 : : }
1454 [ - + ]: 93203 : else if (eqNormalized.getKind() != Kind::EQUAL)
1455 : : {
1456 : 0 : Assert(eqNormalized.getKind() == Kind::SKOLEM
1457 : : || (eqNormalized.getKind() == Kind::NOT
1458 : : && eqNormalized[0].getKind() == Kind::SKOLEM));
1459 : : // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1460 : : // TODO : revisit this
1461 : 0 : continue;
1462 : : }
1463 : :
1464 : : // If the normalization did the just flips, keep the flip
1465 : 93203 : if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) {
1466 : 2315 : eq = eqNormalized;
1467 : : }
1468 : :
1469 : : // Check if the equality is already known by the sat solver
1470 [ + + ]: 93203 : if (d_propEngine->isSatLiteral(eqNormalized)) {
1471 : : bool value;
1472 [ + + ]: 80199 : if (d_propEngine->hasValue(eqNormalized, value)) {
1473 [ + + ]: 77915 : if (value) {
1474 : 75078 : assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1475 : 77915 : continue;
1476 : : } else {
1477 : 2837 : assertToTheory(eq.notNode(), eqNormalized.notNode(), atomsTo, theory::THEORY_SAT_SOLVER);
1478 : 2837 : continue;
1479 : : }
1480 : : }
1481 : : }
1482 : :
1483 : : // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1484 : : // then we must figure it out
1485 [ + + ][ + + ]: 15288 : if (eqNormalized != eq || d_env.theoryOf(eq) != atomsTo)
[ + + ][ + + ]
[ - - ]
1486 : : {
1487 : : // If you get eqNormalized, send atoms[i] to atomsTo
1488 : 12701 : d_atomRequests.add(eqNormalized, eq, atomsTo);
1489 : : }
1490 : : }
1491 : 94174 : }
1492 : :
1493 : 899149 : void TheoryEngine::lemma(TrustNode tlemma,
1494 : : InferenceId id,
1495 : : LemmaProperty p,
1496 : : TheoryId from)
1497 : : {
1498 : : // For resource-limiting (also does a time check).
1499 : : // spendResource();
1500 [ + + ][ - + ]: 899149 : Assert(tlemma.getKind() == TrustNodeKind::LEMMA
[ - + ][ - - ]
1501 : : || tlemma.getKind() == TrustNodeKind::CONFLICT);
1502 : :
1503 : : // minimize or generalize conflict
1504 [ + + ]: 899149 : if (d_cp)
1505 : : {
1506 : 308 : TrustNode tproc = d_cp->processLemma(tlemma);
1507 [ + + ]: 154 : if (!tproc.isNull())
1508 : : {
1509 : 8 : tlemma = tproc;
1510 : : }
1511 : : }
1512 : :
1513 : : // get the node
1514 : 1798300 : Node node = tlemma.getNode();
1515 : 899150 : Node lemma = tlemma.getProven();
1516 : :
1517 : : // must rewrite when checking here since we may have shadowing in rare cases,
1518 : : // e.g. lazy lambda lifting lemmas
1519 [ - + ][ - - ]: 1798300 : Assert(!expr::hasFreeVar(rewrite(lemma)))
1520 [ - + ][ - + ]: 899149 : << "Lemma " << lemma << " from " << from << " has a free variable";
[ - - ]
1521 : :
1522 : : // when proofs are enabled, we ensure the trust node has a generator by
1523 : : // adding a trust step to the lazy proof maintained by this class
1524 [ + + ]: 899149 : if (isProofEnabled())
1525 : : {
1526 : : // ensure proof: set THEORY_LEMMA if no generator is provided
1527 [ + + ]: 421610 : if (tlemma.getGenerator() == nullptr)
1528 : : {
1529 : : // add theory lemma step to proof
1530 : 47731 : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from);
1531 : 95462 : d_lazyProof->addTrustedStep(lemma, TrustId::THEORY_LEMMA, {}, {tidn});
1532 : : // update the trust node
1533 [ + - ]: 47731 : tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
1534 : : }
1535 : : // ensure closed
1536 : 421610 : tlemma.debugCheckClosed(
1537 : : options(), "te-proof-debug", "TheoryEngine::lemma_initial");
1538 : : }
1539 : :
1540 : : // assert the lemma
1541 : 899150 : d_propEngine->assertLemma(id, tlemma, p);
1542 : :
1543 : : // If specified, we must add this lemma to the set of those that need to be
1544 : : // justified, where note we pass all auxiliary lemmas in skAsserts as well,
1545 : : // since these by extension must be justified as well.
1546 [ + + ]: 899148 : if (!d_modules.empty())
1547 : : {
1548 : 1682 : std::vector<Node> skAsserts;
1549 : 1682 : std::vector<Node> sks;
1550 : : Node retLemma =
1551 : 2523 : d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
1552 : :
1553 : : // notify the modules of the lemma
1554 [ + + ]: 1682 : for (TheoryEngineModule* tem : d_modules)
1555 : : {
1556 : : // don't notify theory modules of their own lemmas
1557 [ + + ]: 841 : if (tem->getId() != from)
1558 : : {
1559 : 828 : tem->notifyLemma(retLemma, id, p, skAsserts, sks);
1560 : : }
1561 : : }
1562 : : }
1563 : :
1564 : : // Mark that we added some lemmas
1565 : 899148 : d_lemmasAdded = true;
1566 : 899148 : }
1567 : :
1568 : 390159 : void TheoryEngine::markInConflict()
1569 : : {
1570 : : #ifdef CVC5_FOR_EACH_THEORY_STATEMENT
1571 : : #undef CVC5_FOR_EACH_THEORY_STATEMENT
1572 : : #endif
1573 : : #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
1574 : : theoryOf(THEORY)->notifyInConflict();
1575 : 390159 : CVC5_FOR_EACH_THEORY;
1576 : 390159 : d_inConflict = true;
1577 : 390159 : }
1578 : :
1579 : 240891 : void TheoryEngine::conflict(TrustNode tconflict,
1580 : : InferenceId id,
1581 : : TheoryId theoryId)
1582 : : {
1583 [ - + ][ - + ]: 240891 : Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
[ - - ]
1584 : :
1585 : 481782 : TNode conflict = tconflict.getNode();
1586 [ + - ]: 481782 : Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", "
1587 : 240891 : << id << ", " << theoryId << ")" << endl;
1588 [ + - ]: 240891 : Trace("te-proof-debug") << "Check closed conflict" << std::endl;
1589 : : // doesn't require proof generator, yet, since THEORY_LEMMA is added below
1590 : 240891 : tconflict.debugCheckClosed(
1591 : : options(), "te-proof-debug", "TheoryEngine::conflict_initial", false);
1592 : :
1593 [ + - ]: 240891 : Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
1594 : :
1595 : : // Mark that we are in conflict
1596 : 240891 : markInConflict();
1597 : :
1598 : : // In the multiple-theories case, we need to reconstruct the conflict
1599 [ + + ]: 240891 : if (logicInfo().isSharingEnabled())
1600 : : {
1601 : : // Create the workplace for explanations
1602 : 394930 : std::vector<NodeTheoryPair> vec;
1603 : 197465 : vec.push_back(
1604 : 394930 : NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
1605 : :
1606 : : // Process the explanation
1607 : 394930 : TrustNode tncExp = getExplanation(vec);
1608 : 394930 : Node fullConflict = tncExp.getNode();
1609 : :
1610 [ + + ]: 197465 : if (isProofEnabled())
1611 : : {
1612 [ + - ]: 206484 : Trace("te-proof-debug")
1613 : 103242 : << "Check closed conflict explained with sharing" << std::endl;
1614 : 103242 : tncExp.debugCheckClosed(options(),
1615 : : "te-proof-debug",
1616 : : "TheoryEngine::conflict_explained_sharing");
1617 [ + - ]: 103242 : Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
1618 [ + - ]: 206484 : Trace("te-proof-debug") << "Conflict " << tconflict << " from "
1619 [ - + ][ - - ]: 103242 : << tconflict.identifyGenerator() << std::endl;
1620 [ + - ]: 206484 : Trace("te-proof-debug") << "Explanation " << tncExp << " from "
1621 [ - + ][ - - ]: 103242 : << tncExp.identifyGenerator() << std::endl;
1622 [ - + ][ - + ]: 103242 : Assert(d_lazyProof != nullptr);
[ - - ]
1623 [ + + ]: 103242 : if (tconflict.getGenerator() != nullptr)
1624 : : {
1625 : 100816 : d_lazyProof->addLazyStep(tconflict.getProven(),
1626 : : tconflict.getGenerator());
1627 : : }
1628 : : else
1629 : : {
1630 : : // add theory lemma step
1631 : 4852 : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
1632 : 2426 : Node conf = tconflict.getProven();
1633 : 4852 : d_lazyProof->addTrustedStep(conf, TrustId::THEORY_LEMMA, {}, {tidn});
1634 : : }
1635 : : // store the explicit step, which should come from a different
1636 : : // generator, e.g. d_tepg.
1637 : 206484 : Node proven = tncExp.getProven();
1638 [ + - ][ - + ]: 103242 : Assert(tncExp.getGenerator() != d_lazyProof.get());
[ - + ][ - - ]
1639 [ + - ][ - + ]: 206484 : Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
[ - - ]
1640 : 103242 : << " for " << proven << std::endl;
1641 : 103242 : d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
1642 [ + - ]: 103242 : pfgEnsureClosed(options(),
1643 : : proven,
1644 : 103242 : d_lazyProof.get(),
1645 : : "te-proof-debug",
1646 : : "TheoryEngine::conflict_during");
1647 : 206484 : Node fullConflictNeg = fullConflict.notNode();
1648 : 206484 : std::vector<Node> children;
1649 : 103242 : children.push_back(proven);
1650 : 206484 : std::vector<Node> args;
1651 : 103242 : args.push_back(fullConflictNeg);
1652 [ + + ]: 103242 : if (conflict == d_false)
1653 : : {
1654 [ - + ][ - + ]: 496 : AlwaysAssert(proven == fullConflictNeg);
[ - - ]
1655 : : }
1656 : : else
1657 : : {
1658 [ + + ]: 102746 : if (!CDProof::isSame(fullConflict, conflict))
1659 : : {
1660 : : // ------------------------- explained
1661 : : // fullConflict => conflict
1662 : : // ------------------------- IMPLIES_ELIM ---------- from theory
1663 : : // ~fullConflict V conflict ~conflict
1664 : : // -------------------------------------------------- RESOLUTION
1665 : : // ~fullConflict
1666 : 197818 : Node provenOr = nodeManager()->mkNode(Kind::OR, proven[0].notNode(), proven[1]);
1667 : 197818 : d_lazyProof->addStep(provenOr,
1668 : : ProofRule::IMPLIES_ELIM,
1669 : : {proven},
1670 : 98909 : {});
1671 : 593454 : d_lazyProof->addStep(fullConflictNeg,
1672 : : ProofRule::RESOLUTION,
1673 : : {provenOr, conflict.notNode()},
1674 : 494545 : {d_true, conflict});
1675 : : }
1676 : : }
1677 : : }
1678 : : // pass the processed trust node
1679 : : TrustNode tconf =
1680 [ + + ]: 197465 : TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get());
1681 [ + - ]: 394930 : Trace("theory::conflict")
1682 : 0 : << "TheoryEngine::conflict(" << conflict << ", " << theoryId
1683 : 197465 : << "): full = " << fullConflict << endl;
1684 [ - + ][ - + ]: 197465 : Assert(properConflict(fullConflict));
[ - - ]
1685 [ + - ]: 394930 : Trace("te-proof-debug")
1686 : 197465 : << "Check closed conflict with sharing" << std::endl;
1687 [ + + ]: 197465 : if (isProofEnabled())
1688 : : {
1689 : 103242 : tconf.debugCheckClosed(
1690 : : options(), "te-proof-debug", "TheoryEngine::conflict:sharing");
1691 : : }
1692 : 197465 : lemma(tconf, id, LemmaProperty::NONE);
1693 : : }
1694 : : else
1695 : : {
1696 : : // When only one theory, the conflict should need no processing
1697 [ - + ][ - + ]: 43426 : Assert(properConflict(conflict));
[ - - ]
1698 : : // pass the trust node that was sent from the theory
1699 : 43426 : lemma(tconflict, id, LemmaProperty::NONE, theoryId);
1700 : : }
1701 : 240891 : }
1702 : :
1703 : 0 : void TheoryEngine::setModelUnsound(theory::IncompleteId id)
1704 : : {
1705 : 0 : setModelUnsound(TheoryId::THEORY_NONE, id);
1706 : 0 : }
1707 : :
1708 : 42 : void TheoryEngine::setRefutationUnsound(theory::IncompleteId id)
1709 : : {
1710 : 42 : setRefutationUnsound(TheoryId::THEORY_NONE, id);
1711 : 42 : }
1712 : :
1713 : 9169 : void TheoryEngine::setModelUnsound(theory::TheoryId theory,
1714 : : theory::IncompleteId id)
1715 : : {
1716 : 9169 : d_modelUnsound = true;
1717 : 9169 : d_modelUnsoundTheory = theory;
1718 : 9169 : d_modelUnsoundId = id;
1719 : 9169 : }
1720 : :
1721 : 160 : void TheoryEngine::setRefutationUnsound(theory::TheoryId theory,
1722 : : theory::IncompleteId id)
1723 : : {
1724 : 160 : d_refutationUnsound = true;
1725 : 160 : d_refutationUnsoundTheory = theory;
1726 : 160 : d_refutationUnsoundId = id;
1727 : 160 : }
1728 : :
1729 : 315281 : TrustNode TheoryEngine::getExplanation(
1730 : : std::vector<NodeTheoryPair>& explanationVector)
1731 : : {
1732 [ - + ][ - + ]: 315281 : Assert(explanationVector.size() == 1);
[ - - ]
1733 : 630562 : Node conclusion = explanationVector[0].d_node;
1734 : : // if the theory explains using the central equality engine, we always start
1735 : : // with THEORY_BUILTIN.
1736 : 630562 : explanationVector[0].d_theory =
1737 : 315281 : theoryExpPropagation(explanationVector[0].d_theory);
1738 : 315281 : std::shared_ptr<LazyCDProof> lcp;
1739 [ + + ]: 315281 : if (isProofEnabled())
1740 : : {
1741 [ + - ]: 266532 : Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion
1742 : 133266 : << std::endl;
1743 : : // We do not use auto-symmetry in this proof, since in very rare cases, it
1744 : : // is possible that the proof of explanations is cyclic when considering
1745 : : // (dis)equalities modulo symmetry, where such a proof looks like:
1746 : : // x = y
1747 : : // -----
1748 : : // A ...
1749 : : // ----------
1750 : : // y = x
1751 : : // Notice that this complication arises since propagations consider
1752 : : // equalities that are not in rewritten form. This complication would not
1753 : : // exist otherwise. It is the shared term database that introduces these
1754 : : // unrewritten equalities; it must do so since theory combination requires
1755 : : // communicating arrangements between shared terms, and the rewriter
1756 : : // for arithmetic equalities does not preserve terms, e.g. x=y may become
1757 : : // x+-1*y=0.
1758 : 266532 : lcp.reset(new LazyCDProof(d_env,
1759 : : nullptr,
1760 : : nullptr,
1761 : : "TheoryEngine::LazyCDProof::getExplanation",
1762 : 133266 : false));
1763 : : }
1764 : 315281 : unsigned i = 0; // Index of the current literal we are processing
1765 : :
1766 : 630562 : std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
1767 : : // the overall explanation
1768 : 630562 : std::set<TNode> exp;
1769 : : // vector of trust nodes to explain at the end
1770 : 630562 : std::vector<std::pair<TheoryId, TrustNode>> texplains;
1771 : : // cache of nodes we have already explained by some theory
1772 : 630562 : std::unordered_map<Node, size_t> cache;
1773 : :
1774 [ + + ]: 7080590 : while (i < explanationVector.size()) {
1775 : : // Get the current literal to explain
1776 : 6765310 : NodeTheoryPair toExplain = explanationVector[i];
1777 : :
1778 [ + - ]: 13530600 : Trace("theory::explain")
1779 : 0 : << "[i=" << i << "] TheoryEngine::explain(): processing ["
1780 : 0 : << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
1781 : 6765310 : << toExplain.d_theory << endl;
1782 : :
1783 : 6765310 : if (cache.find(toExplain.d_node) != cache.end()
1784 [ + + ][ + + ]: 6765310 : && cache[toExplain.d_node] < toExplain.d_timestamp)
[ + + ]
1785 : : {
1786 : 181210 : ++i;
1787 : 181210 : continue;
1788 : : }
1789 : 6584100 : cache[toExplain.d_node] = toExplain.d_timestamp;
1790 : :
1791 : : // If a true constant or a negation of a false constant we can ignore it
1792 [ + + ]: 12347 : if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
1793 [ + + ][ + + ]: 7412990 : || (toExplain.d_node.getKind() == Kind::NOT
1794 [ - + ][ + + ]: 7400650 : && toExplain.d_node[0].isConst()
[ - - ]
1795 [ - - ][ - + ]: 6584100 : && !toExplain.d_node[0].getConst<bool>()))
[ + + ][ - - ]
1796 : : {
1797 : 11463 : ++ i;
1798 : : // if we are building a proof
1799 [ + + ]: 11463 : if (lcp != nullptr)
1800 : : {
1801 [ + - ]: 8324 : Trace("te-proof-exp")
1802 : 4162 : << "- explain " << toExplain.d_node << " trivially..." << std::endl;
1803 : : // ------------------MACRO_SR_PRED_INTRO
1804 : : // toExplain.d_node
1805 : 8324 : std::vector<Node> children;
1806 : 4162 : std::vector<Node> args;
1807 : 4162 : args.push_back(toExplain.d_node);
1808 : 4162 : lcp->addStep(
1809 : : toExplain.d_node, ProofRule::MACRO_SR_PRED_INTRO, children, args);
1810 : : }
1811 : 11463 : continue;
1812 : : }
1813 : :
1814 : : // If from the SAT solver, keep it
1815 [ + + ]: 6572640 : if (toExplain.d_theory == THEORY_SAT_SOLVER)
1816 : : {
1817 [ + - ]: 4915830 : Trace("theory::explain")
1818 : 2457920 : << "\tLiteral came from THEORY_SAT_SOLVER. Keeping it." << endl;
1819 : 2457920 : exp.insert(explanationVector[i++].d_node);
1820 : : // it will be a free assumption in the proof
1821 [ + - ]: 2457920 : Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl;
1822 : 2457920 : continue;
1823 : : }
1824 : :
1825 : : // If an and, expand it
1826 [ + + ]: 4114720 : if (toExplain.d_node.getKind() == Kind::AND)
1827 : : {
1828 [ + - ]: 1174700 : Trace("theory::explain")
1829 : 0 : << "TheoryEngine::explain(): expanding " << toExplain.d_node
1830 : 587348 : << " got from " << toExplain.d_theory << endl;
1831 : 587348 : size_t nchild = toExplain.d_node.getNumChildren();
1832 [ + + ]: 3510000 : for (size_t k = 0; k < nchild; ++k)
1833 : : {
1834 : : NodeTheoryPair newExplain(
1835 : 8767960 : toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
1836 : 2922660 : explanationVector.push_back(newExplain);
1837 : : }
1838 [ + + ]: 587348 : if (lcp != nullptr)
1839 : : {
1840 [ + - ]: 514182 : Trace("te-proof-exp")
1841 : 257091 : << "- AND expand " << toExplain.d_node << std::endl;
1842 : : // delay explanation, use a dummy trust node
1843 : : TrustNode tnAndExp = TrustNode::mkTrustPropExp(
1844 : 514182 : toExplain.d_node, toExplain.d_node, nullptr);
1845 : 257091 : texplains.push_back(
1846 : 514182 : std::pair<TheoryId, TrustNode>(THEORY_LAST, tnAndExp));
1847 : : }
1848 : 587348 : ++ i;
1849 : 587348 : continue;
1850 : : }
1851 : :
1852 : : // See if it was sent to the theory by another theory
1853 : 3527380 : PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
1854 [ + + ]: 3527380 : if (find != d_propagationMap.end()) {
1855 [ + - ]: 6726130 : Trace("theory::explain")
1856 : 0 : << "\tTerm was propagated by another theory (theory = "
1857 [ - + ][ - - ]: 3363070 : << getTheoryString((*find).second.d_theory) << ")" << std::endl;
1858 : : // There is some propagation, check if its a timely one
1859 [ + + ]: 3363070 : if ((*find).second.d_timestamp < toExplain.d_timestamp)
1860 : : {
1861 [ + - ]: 6058020 : Trace("theory::explain")
1862 : 0 : << "\tRelevant timetsamp, pushing " << (*find).second.d_node
1863 : 3029010 : << "to index = " << explanationVector.size() << std::endl;
1864 : 3029010 : explanationVector.push_back((*find).second);
1865 : 3029010 : ++i;
1866 : :
1867 [ + + ]: 3029010 : if (lcp != nullptr)
1868 : : {
1869 [ + + ]: 1375940 : if (toExplain.d_node != (*find).second.d_node)
1870 : : {
1871 [ + - ]: 33882 : Trace("te-proof-exp")
1872 : 0 : << "- t-explained cached: " << toExplain.d_node << " by "
1873 : 16941 : << (*find).second.d_node << std::endl;
1874 : : // delay explanation, use a dummy trust node that says that
1875 : : // (*find).second.d_node explains toExplain.d_node.
1876 : : TrustNode tnRewExp = TrustNode::mkTrustPropExp(
1877 : 33882 : toExplain.d_node, (*find).second.d_node, nullptr);
1878 : 16941 : texplains.push_back(
1879 : 33882 : std::pair<TheoryId, TrustNode>(THEORY_LAST, tnRewExp));
1880 : : }
1881 : : }
1882 : 3029010 : continue;
1883 : : }
1884 : : }
1885 : : // It was produced by the theory, so ask for an explanation
1886 : : TrustNode texplanation =
1887 : 996730 : d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
1888 [ + + ]: 498365 : if (lcp != nullptr)
1889 : : {
1890 : 206663 : texplanation.debugCheckClosed(
1891 : : options(), "te-proof-exp", "texplanation", false);
1892 [ + - ]: 413326 : Trace("te-proof-exp")
1893 : 0 : << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
1894 [ - + ][ - - ]: 206663 : << " by " << texplanation.getNode() << std::endl;
1895 : : // should prove the propagation we asked for
1896 : 413326 : Assert(texplanation.getKind() == TrustNodeKind::PROP_EXP
1897 : : && texplanation.getProven()[1] == toExplain.d_node);
1898 : : // We add it to the list of theory explanations, to be processed at
1899 : : // the end of this method. We wait to explain here because it may
1900 : : // be that a later explanation may preempt the need for proving this
1901 : : // step. For instance, if the conclusion lit is later added as an
1902 : : // assumption in the final explanation. This avoids cyclic proofs.
1903 : 206663 : texplains.push_back(
1904 : 413326 : std::pair<TheoryId, TrustNode>(toExplain.d_theory, texplanation));
1905 : : }
1906 : 996730 : Node explanation = texplanation.getNode();
1907 : :
1908 [ + - ]: 996730 : Trace("theory::explain")
1909 : 0 : << "TheoryEngine::explain(): got explanation " << explanation
1910 : 498365 : << " got from " << toExplain.d_theory << endl;
1911 : 498365 : Assert(explanation != toExplain.d_node)
1912 : : << "wasn't sent to you, so why are you explaining it trivially, for "
1913 : 0 : "fact "
1914 : : << explanation;
1915 : : // Mark the explanation
1916 : : NodeTheoryPair newExplain(
1917 : 498365 : explanation, toExplain.d_theory, toExplain.d_timestamp);
1918 : 498365 : explanationVector.push_back(newExplain);
1919 : :
1920 : 498365 : ++ i;
1921 : : }
1922 : :
1923 : : // make the explanation node
1924 : 630562 : Node expNode;
1925 [ + + ]: 315281 : if (exp.size() == 0)
1926 : : {
1927 : : // Normalize to true
1928 : 81 : expNode = NodeManager::currentNM()->mkConst<bool>(true);
1929 : : }
1930 [ + + ]: 315200 : else if (exp.size() == 1)
1931 : : {
1932 : : // All the same, or just one
1933 : 11396 : expNode = *exp.begin();
1934 : : }
1935 : : else
1936 : : {
1937 : 303804 : NodeBuilder conjunction(Kind::AND);
1938 : 303804 : std::set<TNode>::const_iterator it = exp.begin();
1939 : 303804 : std::set<TNode>::const_iterator it_end = exp.end();
1940 [ + + ]: 2677450 : while (it != it_end)
1941 : : {
1942 : 2373640 : conjunction << *it;
1943 : 2373640 : ++it;
1944 : : }
1945 : 303804 : expNode = conjunction;
1946 : : }
1947 : : // if we are building a proof, go back through the explanations and
1948 : : // build the proof
1949 [ + + ]: 315281 : if (lcp != nullptr)
1950 : : {
1951 [ - + ]: 133266 : if (TraceIsOn("te-proof-exp"))
1952 : : {
1953 [ - - ]: 0 : Trace("te-proof-exp") << "Explanation is:" << std::endl;
1954 [ - - ]: 0 : for (TNode e : exp)
1955 : : {
1956 [ - - ]: 0 : Trace("te-proof-exp") << " " << e << std::endl;
1957 : : }
1958 [ - - ]: 0 : Trace("te-proof-exp") << "=== Replay explanations..." << std::endl;
1959 : : }
1960 : : // Now, go back and add the necessary steps of theory explanations, i.e.
1961 : : // add those that prove things that aren't in the final explanation. We
1962 : : // iterate in reverse order so that most recent steps take priority. This
1963 : : // avoids cyclic proofs in the lazy proof we are building (lcp).
1964 : 480695 : for (std::vector<std::pair<TheoryId, TrustNode>>::reverse_iterator
1965 : 133266 : it = texplains.rbegin(),
1966 : 133266 : itEnd = texplains.rend();
1967 [ + + ]: 613961 : it != itEnd;
1968 : 480695 : ++it)
1969 : : {
1970 : 480695 : TrustNode trn = it->second;
1971 [ - + ][ - + ]: 480695 : Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
[ - - ]
1972 : 480695 : Node proven = trn.getProven();
1973 [ - + ][ - + ]: 480695 : Assert(proven.getKind() == Kind::IMPLIES);
[ - - ]
1974 : 480695 : Node tConc = proven[1];
1975 [ + - ]: 480695 : Trace("te-proof-exp") << "- Process " << trn << std::endl;
1976 [ + + ]: 480695 : if (exp.find(tConc) != exp.end())
1977 : : {
1978 : : // already added to proof
1979 [ + - ]: 20093 : Trace("te-proof-exp") << "...already added" << std::endl;
1980 : 20093 : continue;
1981 : : }
1982 : : // remember that we've explained this formula, to avoid cycles in lcp
1983 : 460602 : exp.insert(tConc);
1984 : 460602 : TheoryId ttid = it->first;
1985 : 460602 : Node tExp = proven[0];
1986 [ + + ]: 460602 : if (ttid == THEORY_LAST)
1987 : : {
1988 [ + + ]: 260738 : if (tConc == tExp)
1989 : : {
1990 : : // dummy trust node, do AND expansion
1991 [ - + ][ - + ]: 251337 : Assert(tConc.getKind() == Kind::AND);
[ - - ]
1992 : : // tConc[0] ... tConc[n]
1993 : : // ---------------------- AND_INTRO
1994 : : // tConc
1995 : 502674 : std::vector<Node> pfChildren;
1996 : 251337 : pfChildren.insert(pfChildren.end(), tConc.begin(), tConc.end());
1997 : 251337 : lcp->addStep(tConc, ProofRule::AND_INTRO, pfChildren, {});
1998 [ + - ]: 251337 : Trace("te-proof-exp") << "...via AND_INTRO" << std::endl;
1999 : 251337 : continue;
2000 : : }
2001 : : // otherwise should hold by rewriting
2002 [ - + ][ - + ]: 9401 : Assert(rewrite(tConc) == rewrite(tExp));
[ - - ]
2003 : : // tExp
2004 : : // ---- MACRO_SR_PRED_TRANSFORM
2005 : : // tConc
2006 : 28203 : lcp->addStep(
2007 : 18802 : tConc, ProofRule::MACRO_SR_PRED_TRANSFORM, {tExp}, {tConc});
2008 [ + - ]: 9401 : Trace("te-proof-exp") << "...via MACRO_SR_PRED_TRANSFORM" << std::endl;
2009 : 9401 : continue;
2010 : : }
2011 [ - + ]: 199864 : if (tExp == tConc)
2012 : : {
2013 : : // trivial
2014 [ - - ]: 0 : Trace("te-proof-exp") << "...trivial" << std::endl;
2015 : 0 : continue;
2016 : : }
2017 : : // ------------- Via theory
2018 : : // tExp tExp => tConc
2019 : : // ---------------------------------MODUS_PONENS
2020 : : // tConc
2021 [ + - ]: 199864 : if (trn.getGenerator() != nullptr)
2022 : : {
2023 [ + - ]: 199864 : Trace("te-proof-exp") << "...via theory generator" << std::endl;
2024 : 199864 : lcp->addLazyStep(proven, trn.getGenerator());
2025 : : }
2026 : : else
2027 : : {
2028 [ - - ]: 0 : Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl;
2029 : : // otherwise, trusted theory lemma
2030 : 0 : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(ttid);
2031 : 0 : lcp->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn});
2032 : : }
2033 : 199864 : std::vector<Node> pfChildren;
2034 : 199864 : pfChildren.push_back(trn.getNode());
2035 : 199864 : pfChildren.push_back(proven);
2036 : 199864 : lcp->addStep(tConc, ProofRule::MODUS_PONENS, pfChildren, {});
2037 : : }
2038 : : // If we don't have a step and the conclusion is not part of the
2039 : : // explanation (for unit T-conflicts), it must be by symmetry. We must do
2040 : : // this manually since lcp does not have auto-symmetry enabled due to the
2041 : : // complication mentioned above.
2042 : 133266 : if (!lcp->hasStep(conclusion) && exp.find(conclusion) == exp.end())
2043 : : {
2044 : 0 : Node sconc = CDProof::getSymmFact(conclusion);
2045 [ - - ]: 0 : if (!sconc.isNull())
2046 : : {
2047 : 0 : lcp->addStep(conclusion, ProofRule::SYMM, {sconc}, {});
2048 : : }
2049 : : else
2050 : : {
2051 : 0 : Assert(false)
2052 : 0 : << "TheoryEngine::getExplanation: no step found for conclusion "
2053 : : << conclusion;
2054 : : }
2055 : : }
2056 : : // store in the proof generator
2057 : 399798 : TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp);
2058 : : // return the trust node
2059 : 133266 : return trn;
2060 : : }
2061 : :
2062 : 182015 : return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
2063 : : }
2064 : :
2065 : 6398850 : bool TheoryEngine::isProofEnabled() const
2066 : : {
2067 : 6398850 : return d_env.isTheoryProofProducing();
2068 : : }
2069 : :
2070 : 2757 : void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
2071 : 2757 : bool hasFailure = false;
2072 : 5514 : std::stringstream serror;
2073 : : // If possible, get the list of relevant assertions. Those that are not
2074 : : // relevant will be skipped.
2075 : 5514 : std::unordered_set<TNode> relevantAssertions;
2076 : 2757 : bool hasRelevantAssertions = false;
2077 [ + + ]: 2757 : if (d_relManager != nullptr)
2078 : : {
2079 : : relevantAssertions =
2080 : 11 : d_relManager->getRelevantAssertions(hasRelevantAssertions);
2081 : : }
2082 [ + + ]: 41355 : for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
2083 : 38598 : Theory* theory = d_theoryTable[theoryId];
2084 [ + - ][ + + ]: 38598 : if (theory && isTheoryEnabled(theoryId))
[ + + ]
2085 : : {
2086 : 128254 : for (context::CDList<Assertion>::const_iterator
2087 : 19904 : it = theory->facts_begin(),
2088 : 19904 : it_end = theory->facts_end();
2089 [ + + ]: 148158 : it != it_end;
2090 : 128254 : ++it)
2091 : : {
2092 : 128254 : Node assertion = (*it).d_assertion;
2093 : 128489 : if (hasRelevantAssertions
2094 [ + + ][ + + ]: 128254 : && relevantAssertions.find(assertion) == relevantAssertions.end())
[ + + ][ + + ]
[ - - ]
2095 : : {
2096 : : // not relevant, skip
2097 : 235 : continue;
2098 : : }
2099 : 256038 : Node val = d_tc->getModel()->getValue(assertion);
2100 [ + + ]: 128019 : if (val != d_true)
2101 : : {
2102 : 708 : std::stringstream ss;
2103 [ + + ]: 923 : for (Node child : assertion)
2104 : : {
2105 : 569 : Node value = d_tc->getModel()->getValue(child);
2106 : 569 : ss << "getValue(" << child << "): " << value << std::endl;
2107 : : }
2108 : 354 : ss << " " << theoryId << " has an asserted fact that";
2109 [ - + ]: 354 : if (val == d_false)
2110 : : {
2111 : 0 : ss << " the model doesn't satisfy." << std::endl;
2112 : : }
2113 : : else
2114 : : {
2115 : 354 : ss << " the model may not satisfy." << std::endl;
2116 : : }
2117 : 354 : ss << "The fact: " << assertion << std::endl
2118 : 354 : << "Model value: " << val << std::endl;
2119 [ + - ]: 354 : if (hardFailure)
2120 : : {
2121 [ - + ]: 354 : if (val == d_false)
2122 : : {
2123 : : // Always an error if it is false
2124 : 0 : hasFailure = true;
2125 : 0 : serror << ss.str();
2126 : : }
2127 : : else
2128 : : {
2129 : : // Otherwise just a warning. Notice this case may happen for
2130 : : // assertions with unevaluable operators, e.g. transcendental
2131 : : // functions. It also may happen for separation logic, where
2132 : : // check-model support is limited.
2133 : 354 : warning() << ss.str();
2134 : : }
2135 : : }
2136 : : }
2137 : : }
2138 : : }
2139 : : }
2140 [ - + ]: 2757 : if (hasFailure)
2141 : : {
2142 : 0 : InternalError() << serror.str();
2143 : : }
2144 : 2757 : }
2145 : :
2146 : 8916 : std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
2147 : : TNode lit)
2148 : : {
2149 [ + + ]: 17832 : TNode atom = (lit.getKind() == Kind::NOT) ? lit[0] : lit;
2150 [ + + ]: 17828 : if (atom.getKind() == Kind::AND || atom.getKind() == Kind::OR
2151 [ + + ][ + + ]: 17828 : || atom.getKind() == Kind::IMPLIES)
[ + + ]
2152 : : {
2153 : : //Boolean connective, recurse
2154 : 36 : std::vector< Node > children;
2155 : 18 : bool pol = (lit.getKind() != Kind::NOT);
2156 : 18 : bool is_conjunction = pol == (lit.getKind() == Kind::AND);
2157 [ + - ]: 18 : for( unsigned i=0; i<atom.getNumChildren(); i++ ){
2158 : 18 : Node ch = atom[i];
2159 [ - + ][ - - ]: 18 : if (pol == (lit.getKind() == Kind::IMPLIES && i == 0))
[ + - ]
2160 : : {
2161 : 18 : ch = atom[i].negate();
2162 : : }
2163 : 18 : std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2164 [ - + ]: 18 : if( chres.first ){
2165 [ - - ]: 0 : if( !is_conjunction ){
2166 : 0 : return chres;
2167 : : }else{
2168 : 0 : children.push_back( chres.second );
2169 : : }
2170 [ + - ][ + - ]: 18 : }else if( !chres.first && is_conjunction ){
2171 : 18 : return std::pair<bool, Node>(false, Node::null());
2172 : : }
2173 : : }
2174 [ - - ]: 0 : if( is_conjunction ){
2175 : : return std::pair<bool, Node>(
2176 : 0 : true, NodeManager::currentNM()->mkNode(Kind::AND, children));
2177 : : }else{
2178 : 0 : return std::pair<bool, Node>(false, Node::null());
2179 : : }
2180 : : }
2181 : 26694 : else if (atom.getKind() == Kind::ITE
2182 : 8898 : || (atom.getKind() == Kind::EQUAL && atom[0].getType().isBoolean()))
2183 : : {
2184 : 0 : bool pol = (lit.getKind() != Kind::NOT);
2185 [ - - ]: 0 : for( unsigned r=0; r<2; r++ ){
2186 : 0 : Node ch = atom[0];
2187 [ - - ]: 0 : if( r==1 ){
2188 : 0 : ch = ch.negate();
2189 : : }
2190 : 0 : std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2191 [ - - ]: 0 : if( chres.first ){
2192 [ - - ]: 0 : Node ch2 = atom[atom.getKind() == Kind::ITE ? r + 1 : 1];
2193 : 0 : if (pol == (atom.getKind() == Kind::ITE ? true : r == 1))
2194 : : {
2195 : 0 : ch2 = ch2.negate();
2196 : : }
2197 : 0 : std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
2198 [ - - ]: 0 : if( chres2.first ){
2199 : : return std::pair<bool, Node>(
2200 : : true,
2201 : 0 : NodeManager::currentNM()->mkNode(
2202 : 0 : Kind::AND, chres.second, chres2.second));
2203 : : }else{
2204 : 0 : break;
2205 : : }
2206 : : }
2207 : : }
2208 : 0 : return std::pair<bool, Node>(false, Node::null());
2209 : : }
2210 : : else
2211 : : {
2212 : : //it is a theory atom
2213 : 8898 : theory::TheoryId tid = Theory::theoryOf(atom, mode);
2214 : 8898 : theory::Theory* th = theoryOf(tid);
2215 : :
2216 [ - + ][ - + ]: 8898 : Assert(th != NULL);
[ - - ]
2217 [ + - ]: 8898 : Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
2218 : :
2219 : 17796 : std::pair<bool, Node> chres = th->entailmentCheck(lit);
2220 : 8898 : return chres;
2221 : : }
2222 : : }
2223 : :
2224 : 30917800 : void TheoryEngine::spendResource(Resource r)
2225 : : {
2226 : 30917800 : d_env.getResourceManager()->spendResource(r);
2227 : 30917800 : }
2228 : :
2229 : 18572 : void TheoryEngine::initializeProofChecker(ProofChecker* pc)
2230 : : {
2231 [ + + ]: 278580 : for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
2232 : 260008 : ++id)
2233 : : {
2234 : 260008 : ProofRuleChecker* prc = d_theoryTable[id]->getProofChecker();
2235 [ + + ]: 260008 : if (prc)
2236 : : {
2237 : 177587 : prc->registerTo(pc);
2238 : : }
2239 : : }
2240 : 18572 : }
2241 : :
2242 : 688426 : theory::Rewriter* TheoryEngine::getRewriter() { return d_env.getRewriter(); }
2243 : :
2244 : : } // namespace cvc5::internal
|
