Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : : #include "prop/theory_proxy.h"
16 : :
17 : : #include "context/context.h"
18 : : #include "decision/decision_engine.h"
19 : : #include "decision/justification_strategy.h"
20 : : #include "expr/node_algorithm.h"
21 : : #include "expr/plugin.h"
22 : : #include "expr/skolem_manager.h"
23 : : #include "options/base_options.h"
24 : : #include "options/decision_options.h"
25 : : #include "options/parallel_options.h"
26 : : #include "options/prop_options.h"
27 : : #include "options/smt_options.h"
28 : : #include "prop/cnf_stream.h"
29 : : #include "prop/proof_cnf_stream.h"
30 : : #include "prop/prop_engine.h"
31 : : #include "prop/skolem_def_manager.h"
32 : : #include "prop/zero_level_learner.h"
33 : : #include "smt/env.h"
34 : : #include "theory/rewriter.h"
35 : : #include "theory/theory_engine.h"
36 : : #include "util/statistics_stats.h"
37 : :
38 : : namespace cvc5::internal {
39 : : namespace prop {
40 : :
41 : 28707 : TheoryProxy::TheoryProxy(Env& env,
42 : : PropEngine* propEngine,
43 : : TheoryEngine* theoryEngine,
44 : 28707 : SkolemDefManager* skdm)
45 : : : EnvObj(env),
46 : 28707 : d_propEngine(propEngine),
47 : 28707 : d_cnfStream(nullptr),
48 : 28707 : d_decisionEngine(nullptr),
49 : 28707 : d_trackActiveSkDefs(false),
50 : 28707 : d_dmTrackActiveSkDefs(false),
51 : 28707 : d_inSolve(false),
52 : 28707 : d_theoryEngine(theoryEngine),
53 : 28707 : d_queue(context()),
54 : 28707 : d_tpp(env, *theoryEngine),
55 : 28707 : d_skdm(skdm),
56 : 28707 : d_zll(nullptr),
57 : 28707 : d_prr(nullptr),
58 : 28707 : d_stopSearch(userContext(), false),
59 : 57414 : d_activatedSkDefs(false)
60 : : {
61 : : bool trackZeroLevel =
62 : 28707 : options().smt.deepRestartMode != options::DeepRestartMode::NONE
63 [ + + ]: 28692 : || isOutputOn(OutputTag::LEARNED_LITS)
64 [ + + ]: 28690 : || options().smt.produceLearnedLiterals
65 [ + - ]: 28679 : || options().parallel.computePartitions > 0
66 [ + + ][ + + ]: 57399 : || options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE;
67 [ + + ]: 28707 : if (trackZeroLevel)
68 : : {
69 : 33 : d_zll = std::make_unique<ZeroLevelLearner>(env, theoryEngine);
70 : : }
71 : 28707 : }
72 : :
73 : 57388 : TheoryProxy::~TheoryProxy() { /* nothing to do for now */ }
74 : :
75 : 28707 : void TheoryProxy::finishInit(CDCLTSatSolver* ss, CnfStream* cs)
76 : : {
77 : : // make the decision engine, which requires pointers to the SAT solver and CNF
78 : : // stream
79 : 28707 : options::DecisionMode dmode = options().decision.decisionMode;
80 [ + + ]: 28707 : if (dmode == options::DecisionMode::JUSTIFICATION
81 [ + + ]: 8518 : || dmode == options::DecisionMode::STOPONLY)
82 : : {
83 : 20848 : d_decisionEngine.reset(new decision::JustificationStrategy(d_env, ss, cs));
84 : 20848 : if (options().decision.jhSkolemRlvMode
85 [ + - ]: 20848 : == options::JutificationSkolemRlvMode::ASSERT)
86 : : {
87 : 20848 : d_dmTrackActiveSkDefs = true;
88 : 20848 : d_trackActiveSkDefs = true;
89 : : }
90 : : }
91 : : else
92 : : {
93 : 7859 : d_decisionEngine.reset(new decision::DecisionEngineEmpty(d_env));
94 : : }
95 : : // make the theory preregistrar
96 : 28707 : d_prr.reset(new TheoryPreregistrar(d_env, d_theoryEngine, ss, cs));
97 : : // compute if we need to track skolem definitions
98 [ - + ]: 28707 : if (d_prr->needsActiveSkolemDefs())
99 : : {
100 : 0 : d_trackActiveSkDefs = true;
101 : : }
102 [ + + ]: 28707 : if (options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE)
103 : : {
104 : 5 : d_lemip.reset(new LemmaInprocess(d_env, cs, *d_zll.get()));
105 : : }
106 : 28707 : d_cnfStream = cs;
107 : 28707 : }
108 : :
109 : 32397 : void TheoryProxy::presolve()
110 : : {
111 [ + - ]: 32397 : Trace("theory-proxy") << "TheoryProxy::presolve: begin" << std::endl;
112 : 32397 : d_decisionEngine->presolve();
113 : 32397 : d_theoryEngine->presolve();
114 : 32397 : d_stopSearch = false;
115 [ + - ]: 32397 : Trace("theory-proxy") << "TheoryProxy::presolve: end" << std::endl;
116 : 32397 : d_inSolve = true;
117 : 32397 : }
118 : :
119 : 32381 : void TheoryProxy::postsolve(SatValue result)
120 : : {
121 : 32381 : d_theoryEngine->postsolve(result);
122 : 32381 : d_inSolve = false;
123 : 32381 : }
124 : :
125 : 52594 : void TheoryProxy::notifyTopLevelSubstitution(const Node& lhs,
126 : : const Node& rhs) const
127 : : {
128 [ + + ]: 52594 : if (d_zll != nullptr)
129 : : {
130 : 6 : d_zll->notifyTopLevelSubstitution(lhs, rhs);
131 : : }
132 : 52594 : }
133 : :
134 : 40607 : void TheoryProxy::notifyInputFormulas(
135 : : const std::vector<Node>& assertions,
136 : : std::unordered_map<size_t, Node>& skolemMap)
137 : : {
138 : : // notify the theory engine of preprocessed assertions
139 : 40607 : d_theoryEngine->notifyPreprocessedAssertions(assertions);
140 : : // Now, notify the theory proxy of the assertions and skolem definitions.
141 : : // Notice we do this before asserting the formulas to the CNF stream below,
142 : : // since (preregistration) lemmas may occur during calls to assertInternal.
143 : : // These lemmas we want to be notified about after the theory proxy has
144 : : // been notified about all input assertions.
145 : 40607 : std::unordered_map<size_t, Node>::iterator it;
146 [ + + ]: 504864 : for (size_t i = 0, asize = assertions.size(); i < asize; i++)
147 : : {
148 : : // is the assertion a skolem definition?
149 : 464257 : it = skolemMap.find(i);
150 : 464257 : Node skolem;
151 [ + + ]: 464257 : if (it != skolemMap.end())
152 : : {
153 : 26956 : skolem = it->second;
154 : : }
155 [ + + ]: 464257 : if (!skolem.isNull())
156 : : {
157 : 26956 : notifySkolemDefinition(assertions[i], skolem);
158 : : }
159 : 464257 : notifyAssertion(assertions[i], skolem, false);
160 : 464257 : }
161 : :
162 : : // the zero-level learner needs to be notified of the input assertions, to
163 : : // determine what is learnable
164 [ + + ]: 40607 : if (d_zll != nullptr)
165 : : {
166 : 32 : d_zll->notifyInputFormulas(assertions);
167 : : }
168 : 40607 : }
169 : :
170 : 62558 : void TheoryProxy::notifySkolemDefinition(Node a, TNode skolem)
171 : : {
172 [ - + ][ - + ]: 62558 : Assert(!skolem.isNull());
[ - - ]
173 : 62558 : d_skdm->notifySkolemDefinition(skolem, a);
174 : 62558 : }
175 : :
176 : 1384920 : void TheoryProxy::notifyAssertion(Node a,
177 : : TNode skolem,
178 : : bool isLemma,
179 : : bool local)
180 : : {
181 : : // ignore constants
182 [ + + ]: 1384920 : if (a.isConst())
183 : : {
184 : 123577 : return;
185 : : }
186 : : // notify the decision engine
187 [ - + ]: 1261343 : if (local)
188 : : {
189 : : // If it is marked local, add as local assertions.
190 : 0 : d_decisionEngine->addLocalAssertions({a});
191 : : }
192 [ + + ][ + + ]: 1261343 : else if (skolem.isNull() || !d_dmTrackActiveSkDefs)
[ + + ]
193 : : {
194 : : // Otherwise, if it is not a skolem definition, or we are treating
195 : : // skolem definitions as ordinary assertions, we add it now.
196 : 2441282 : d_decisionEngine->addAssertions({a});
197 : : }
198 : : // Otherwise, it is a skolem definition that will be activated dynamically
199 : : // in TheoryProxy::theoryCheck.
200 : :
201 : : // notify the preregistrar
202 : 1261343 : d_prr->addAssertion(a, skolem, isLemma);
203 : : }
204 : :
205 : 11067594 : void TheoryProxy::theoryCheck(theory::Theory::Effort effort)
206 : : {
207 [ + - ]: 11067594 : Trace("theory-proxy") << "TheoryProxy: check " << effort << std::endl;
208 : 11067594 : d_activatedSkDefs = false;
209 : : // check with the preregistrar
210 : 11067594 : d_prr->check();
211 : 11067594 : TNode assertion;
212 : : int32_t alevel;
213 [ + + ]: 38895067 : while (!d_queue.empty())
214 : : {
215 : 27827481 : std::tie(assertion, alevel) = d_queue.front();
216 : 27827481 : d_queue.pop();
217 [ + + ]: 27827481 : if (d_zll != nullptr)
218 : : {
219 [ - + ]: 391 : if (d_stopSearch.get())
220 : : {
221 : 0 : break;
222 : : }
223 [ + + ]: 391 : if (!d_zll->notifyAsserted(assertion, alevel))
224 : : {
225 : 7 : d_stopSearch = true;
226 : 7 : break;
227 : : }
228 : : }
229 : : // notify the preregister utility, which may trigger new preregistrations
230 [ - + ]: 27827474 : if (!d_prr->notifyAsserted(assertion))
231 : : {
232 : : // the preregistrar determined we should not assert this assertion, which
233 : : // can be the case for Boolean variables that we are notified about for
234 : : // the purposes of updating justification when using preregistration
235 : : // mode relevant.
236 : 0 : continue;
237 : : }
238 : : // now, assert to theory engine
239 [ + - ]: 27827474 : Trace("prereg") << "assert: " << assertion << std::endl;
240 : 27827475 : d_theoryEngine->assertFact(assertion);
241 [ + + ]: 27827473 : if (d_trackActiveSkDefs)
242 : : {
243 [ - + ][ - + ]: 12939678 : Assert(d_skdm != nullptr);
[ - - ]
244 : : // Assertion makes all skolems in assertion active,
245 : : // which triggers their definitions to becoming active.
246 : 12939678 : std::vector<TNode> activeSkolemDefs;
247 : 12939678 : d_skdm->notifyAsserted(assertion, activeSkolemDefs);
248 [ + + ]: 12939678 : if (!activeSkolemDefs.empty())
249 : : {
250 : : // notify the decision engine of the skolem definitions that have become
251 : : // active due to the assertion.
252 [ + - ]: 817893 : if (d_dmTrackActiveSkDefs)
253 : : {
254 : 817893 : d_decisionEngine->addLocalAssertions(activeSkolemDefs);
255 : : }
256 : 817893 : d_prr->notifyActiveSkolemDefs(activeSkolemDefs);
257 : : // if we are doing a FULL effort check (propagating with no remaining
258 : : // decisions) and a new skolem definition becomes active, then the SAT
259 : : // assignment is not complete.
260 [ + + ]: 817893 : if (effort == theory::Theory::EFFORT_FULL)
261 : : {
262 [ + - ]: 32 : Trace("theory-proxy") << "...change check to STANDARD!" << std::endl;
263 : 32 : effort = theory::Theory::EFFORT_STANDARD;
264 : : }
265 : 817893 : d_activatedSkDefs = true;
266 : : }
267 : 12939678 : }
268 : : }
269 [ + + ]: 11067593 : if (!d_stopSearch.get())
270 : : {
271 : 11067579 : d_theoryEngine->check(effort);
272 : : }
273 : 11067594 : }
274 : :
275 : 11067582 : void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output)
276 : : {
277 : : // Get the propagated literals
278 : 11067582 : std::vector<TNode> outputNodes;
279 : 11067582 : d_theoryEngine->getPropagatedLiterals(outputNodes);
280 [ + + ]: 25682613 : for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++i)
281 : : {
282 [ + - ]: 29230062 : Trace("prop-explain") << "theoryPropagate() => " << outputNodes[i]
283 : 14615031 : << std::endl;
284 : 14615031 : output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
285 : : }
286 : 11067582 : }
287 : :
288 : 250316 : void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation)
289 : : {
290 : 250316 : TNode lNode = d_cnfStream->getNode(l);
291 [ + - ]: 250316 : Trace("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
292 : :
293 : 250316 : TrustNode tte = d_theoryEngine->getExplanation(lNode);
294 : 250316 : Node theoryExplanation = tte.getNode();
295 [ + + ][ + - ]: 250316 : Assert(!d_env.isTheoryProofProducing() || tte.getGenerator());
[ - + ][ - + ]
[ - - ]
296 : : // notify the prop engine of the explanation, which is only relevant if
297 : : // we are proof producing for the purposes of storing the CNF of the
298 : : // explanation.
299 : 250316 : d_propEngine->notifyExplainedPropagation(tte);
300 [ + - ]: 500632 : Trace("prop-explain") << "explainPropagation() => " << theoryExplanation
301 : 250316 : << std::endl;
302 : 250316 : explanation.push_back(l);
303 [ + + ]: 250316 : if (theoryExplanation.getKind() == Kind::AND)
304 : : {
305 [ + + ]: 2419745 : for (const Node& n : theoryExplanation)
306 : : {
307 : 2181301 : explanation.push_back(~d_cnfStream->getLiteral(n));
308 : 2181301 : }
309 : : }
310 : : else
311 : : {
312 : 11872 : explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
313 : : }
314 [ - + ]: 250316 : if (TraceIsOn("sat-proof"))
315 : : {
316 : 0 : std::stringstream ss;
317 : 0 : ss << "TheoryProxy::explainPropagation: clause for lit is ";
318 [ - - ]: 0 : for (unsigned i = 0, size = explanation.size(); i < size; ++i)
319 : : {
320 : 0 : ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
321 : 0 : << "] ";
322 : : }
323 : 0 : Trace("sat-proof") << ss.str() << "\n";
324 : 0 : }
325 : 250316 : }
326 : :
327 : 821621 : void TheoryProxy::notifySatClause(const SatClause& clause)
328 : : {
329 : 821621 : const std::vector<Plugin*>& plugins = d_env.getPlugins();
330 [ + + ]: 821621 : if (plugins.empty())
331 : : {
332 : : // nothing to do if no plugins
333 : 821611 : return;
334 : : }
335 [ + + ][ - + ]: 10 : if (!d_inSolve && options().base.pluginNotifySatClauseInSolve)
[ - + ]
336 : : {
337 : : // We are not in solving mode. We do not inform plugins of SAT clauses
338 : : // if pluginNotifySatClauseInSolve is true (default).
339 : 0 : return;
340 : : }
341 : : // convert to node
342 : 10 : const auto& nodeCache = d_cnfStream->getNodeCache();
343 : 10 : std::vector<Node> clauseNodes;
344 [ + + ]: 20 : for (const SatLiteral& l : clause)
345 : : {
346 : 10 : auto it = nodeCache.find(l);
347 : : // This should only return null nodes with CaDiCaL when clauses contain
348 : : // activation literals, i.e., clauses learned at user level > 0.
349 [ + - ]: 10 : if (it != nodeCache.end())
350 : : {
351 : 10 : clauseNodes.push_back(it->second);
352 : : }
353 : : }
354 : 10 : Node cln = nodeManager()->mkOr(clauseNodes);
355 : : // get the sharable form of cln
356 : 10 : Node clns = d_env.getSharableFormula(cln);
357 [ + - ]: 10 : if (!clns.isNull())
358 : : {
359 [ + - ]: 20 : Trace("theory-proxy")
360 : 0 : << "TheoryProxy::notifySatClause: Clause from SAT solver: " << clns
361 : 10 : << std::endl;
362 : : // notify the plugins
363 [ + + ]: 20 : for (Plugin* p : plugins)
364 : : {
365 : 10 : p->notifySatClause(clns);
366 : : }
367 : : }
368 : 10 : }
369 : :
370 : 36127424 : void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l)
371 : : {
372 : 36127424 : Node literalNode = d_cnfStream->getNode(l);
373 [ + - ]: 72254848 : Trace("theory-proxy") << "enqueueing theory literal " << l << " "
374 : 36127424 : << literalNode << std::endl;
375 [ - + ][ - + ]: 36127424 : Assert(!literalNode.isNull());
[ - - ]
376 : : // Decision level = SAT context level - 1 due to global push().
377 : 36127424 : d_queue.push(std::make_pair(literalNode, context()->getLevel() - 1));
378 : 36127424 : }
379 : :
380 : 7282870 : SatLiteral TheoryProxy::getNextDecisionRequest(bool& requirePhase,
381 : : bool& stopSearch)
382 : : {
383 [ + - ]: 7282870 : Trace("theory-proxy") << "TheoryProxy: getNextDecisionRequest" << std::endl;
384 : 7282870 : requirePhase = false;
385 : 7282870 : stopSearch = false;
386 : 7282870 : SatLiteral res = undefSatLiteral;
387 : 7282870 : TNode n = d_theoryEngine->getNextDecisionRequest();
388 [ + + ]: 7282866 : if (!n.isNull())
389 : : {
390 [ + - ]: 165719 : Trace("theory-proxy") << "... return next theory decision" << std::endl;
391 : 165719 : requirePhase = true;
392 : 165719 : res = d_cnfStream->getLiteral(n);
393 : : }
394 : : else
395 : : {
396 [ - + ][ - + ]: 7117147 : Assert(d_decisionEngine != nullptr);
[ - - ]
397 [ - + ][ - + ]: 7117147 : Assert(stopSearch != true);
[ - - ]
398 : 7117147 : requirePhase = false;
399 [ + + ]: 7117147 : if (d_stopSearch.get())
400 : : {
401 [ + - ]: 7 : Trace("theory-proxy") << "...stop search, finished" << std::endl;
402 : 7 : stopSearch = true;
403 : : }
404 : : else
405 : : {
406 : 7117140 : res = d_decisionEngine->getNext(stopSearch);
407 [ + + ]: 7117140 : if (stopSearch)
408 : : {
409 [ + - ]: 223934 : Trace("theory-proxy")
410 : 111967 : << " *** Decision Engine stopped search *** " << std::endl;
411 : : }
412 : : else
413 : : {
414 [ + - ]: 7005173 : Trace("theory-proxy") << "...return next decision" << std::endl;
415 : : }
416 : : }
417 : : }
418 : 7282866 : return res;
419 : 7282866 : }
420 : :
421 : 31911 : bool TheoryProxy::theoryNeedCheck() const
422 : : {
423 [ + + ]: 31911 : if (d_stopSearch.get())
424 : : {
425 : 7 : return false;
426 : : }
427 [ + + ]: 31904 : else if (d_activatedSkDefs)
428 : : {
429 : : // a new skolem definition became active on the last call to theoryCheck
430 : 8 : return true;
431 : : }
432 : : // otherwise ask the theory engine, which will return true if its output
433 : : // channel was used.
434 : 31896 : bool needCheck = d_theoryEngine->needCheck();
435 [ + - ]: 63792 : Trace("theory-proxy") << "TheoryProxy: theoryNeedCheck returns " << needCheck
436 : 31896 : << std::endl;
437 : 31896 : return needCheck;
438 : : }
439 : :
440 : 13703 : bool TheoryProxy::isModelUnsound() const
441 : : {
442 [ + + ][ + + ]: 13703 : return d_stopSearch.get() || d_theoryEngine->isModelUnsound();
443 : : }
444 : :
445 : 18596 : bool TheoryProxy::isRefutationUnsound() const
446 : : {
447 : 18596 : return d_theoryEngine->isRefutationUnsound();
448 : : }
449 : :
450 : 832 : theory::IncompleteId TheoryProxy::getModelUnsoundId() const
451 : : {
452 [ + + ]: 832 : if (d_stopSearch.get())
453 : : {
454 : 7 : return theory::IncompleteId::STOP_SEARCH;
455 : : }
456 : 825 : return d_theoryEngine->getModelUnsoundId();
457 : : }
458 : :
459 : 20 : theory::IncompleteId TheoryProxy::getRefutationUnsoundId() const
460 : : {
461 : 20 : return d_theoryEngine->getRefutationUnsoundId();
462 : : }
463 : :
464 : 93404 : TNode TheoryProxy::getNode(SatLiteral lit) { return d_cnfStream->getNode(lit); }
465 : :
466 : 4728 : void TheoryProxy::notifyRestart()
467 : : {
468 : 4728 : d_propEngine->spendResource(Resource::RestartStep);
469 : 4728 : d_theoryEngine->notifyRestart();
470 : 4728 : }
471 : :
472 : 9297682 : void TheoryProxy::spendResource(Resource r)
473 : : {
474 : 9297682 : d_theoryEngine->spendResource(r);
475 : 9297682 : }
476 : :
477 : 128766 : bool TheoryProxy::isDecisionEngineDone()
478 : : {
479 [ + + ][ + + ]: 128766 : return d_decisionEngine->isDone() || d_stopSearch.get();
480 : : }
481 : :
482 : 15139 : CnfStream* TheoryProxy::getCnfStream() const { return d_cnfStream; }
483 : :
484 : 885062 : TrustNode TheoryProxy::preprocessLemma(
485 : : TrustNode trn, std::vector<theory::SkolemLemma>& newLemmas)
486 : : {
487 : 885062 : return d_tpp.preprocessLemma(trn, newLemmas);
488 : : }
489 : :
490 : 861401 : TrustNode TheoryProxy::preprocess(TNode node,
491 : : std::vector<theory::SkolemLemma>& newLemmas)
492 : : {
493 : 861401 : return d_tpp.preprocess(node, newLemmas);
494 : : }
495 : :
496 : 1342 : TrustNode TheoryProxy::removeItes(TNode node,
497 : : std::vector<theory::SkolemLemma>& newLemmas)
498 : : {
499 : 1342 : RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
500 : 1342 : return rtf.run(node, newLemmas, true);
501 : : }
502 : :
503 : 6215 : void TheoryProxy::getSkolems(TNode node,
504 : : std::vector<Node>& skAsserts,
505 : : std::vector<Node>& sks)
506 : : {
507 : 6215 : std::unordered_set<Node> skolems;
508 : 6215 : d_skdm->getSkolems(node, skolems);
509 [ + + ]: 10482 : for (const Node& k : skolems)
510 : : {
511 : 4267 : sks.push_back(k);
512 : 4267 : skAsserts.push_back(d_skdm->getDefinitionForSkolem(k));
513 : : }
514 : 6215 : }
515 : :
516 : 1226177 : void TheoryProxy::notifySatLiteral(Node n)
517 : : {
518 : : // notify the preregister utility, which may trigger new preregistrations
519 : 1226177 : d_prr->notifySatLiteral(n);
520 : 1226161 : }
521 : :
522 : 999129 : void TheoryProxy::notifyBacktrack()
523 : : {
524 : : // notify the preregistrar, which may trigger reregistrations
525 : 999129 : d_prr->notifyBacktrack();
526 : 999129 : }
527 : :
528 : 20 : std::vector<Node> TheoryProxy::getLearnedZeroLevelLiterals(
529 : : modes::LearnedLitType ltype) const
530 : : {
531 [ + - ]: 20 : if (d_zll != nullptr)
532 : : {
533 : 20 : return d_zll->getLearnedZeroLevelLiterals(ltype);
534 : : }
535 : 0 : return {};
536 : : }
537 : :
538 : 0 : modes::LearnedLitType TheoryProxy::getLiteralType(const Node& lit) const
539 : : {
540 [ - - ]: 0 : if (d_zll != nullptr)
541 : : {
542 : 0 : return d_zll->computeLearnedLiteralType(lit);
543 : : }
544 : 0 : return modes::LearnedLitType::UNKNOWN;
545 : : }
546 : :
547 : 7 : std::vector<Node> TheoryProxy::getLearnedZeroLevelLiteralsForRestart() const
548 : : {
549 [ + - ]: 7 : if (d_zll != nullptr)
550 : : {
551 : 7 : return d_zll->getLearnedZeroLevelLiteralsForRestart();
552 : : }
553 : 0 : return {};
554 : : }
555 : :
556 : 3 : TrustNode TheoryProxy::inprocessLemma(TrustNode& trn)
557 : : {
558 [ - + ][ - + ]: 3 : Assert(d_lemip != nullptr);
[ - - ]
559 : 3 : return d_lemip->inprocessLemma(trn);
560 : : }
561 : :
562 : : } // namespace prop
563 : : } // namespace cvc5::internal
|
