Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Dejan Jovanovic, Morgan Deters
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * The theory engine.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY_ENGINE_H
19 : : #define CVC5__THEORY_ENGINE_H
20 : :
21 : : #include <memory>
22 : : #include <vector>
23 : :
24 : : #include "base/check.h"
25 : : #include "context/cdhashmap.h"
26 : : #include "expr/node.h"
27 : : #include "options/theory_options.h"
28 : : #include "proof/trust_node.h"
29 : : #include "prop/sat_solver_types.h"
30 : : #include "smt/env_obj.h"
31 : : #include "theory/atom_requests.h"
32 : : #include "theory/inference_id.h"
33 : : #include "theory/interrupted.h"
34 : : #include "theory/output_channel.h"
35 : : #include "theory/partition_generator.h"
36 : : #include "theory/rewriter.h"
37 : : #include "theory/sort_inference.h"
38 : : #include "theory/theory.h"
39 : : #include "theory/theory_engine_module.h"
40 : : #include "theory/theory_engine_statistics.h"
41 : : #include "theory/theory_preprocessor.h"
42 : : #include "theory/trust_substitutions.h"
43 : : #include "theory/uf/equality_engine.h"
44 : : #include "theory/valuation.h"
45 : : #include "util/hash.h"
46 : : #include "util/statistics_stats.h"
47 : :
48 : : namespace cvc5::internal {
49 : :
50 : : class Env;
51 : : class ResourceManager;
52 : : class TheoryEngineProofGenerator;
53 : : class Plugin;
54 : : class ProofChecker;
55 : :
56 : : /**
57 : : * A pair of a theory and a node. This is used to mark the flow of
58 : : * propagations between theories.
59 : : */
60 : : struct NodeTheoryPair {
61 : : Node d_node;
62 : : theory::TheoryId d_theory;
63 : : size_t d_timestamp;
64 : 159197000 : NodeTheoryPair(TNode n, theory::TheoryId t, size_t ts = 0)
65 : 159197000 : : d_node(n), d_theory(t), d_timestamp(ts)
66 : : {
67 : 159197000 : }
68 : 109303000 : NodeTheoryPair() : d_theory(theory::THEORY_LAST), d_timestamp() {}
69 : : // Comparison doesn't take into account the timestamp
70 : 191861000 : bool operator == (const NodeTheoryPair& pair) const {
71 [ + - ][ + - ]: 191861000 : return d_node == pair.d_node && d_theory == pair.d_theory;
72 : : }
73 : : };/* struct NodeTheoryPair */
74 : :
75 : : struct NodeTheoryPairHashFunction {
76 : : std::hash<Node> hashFunction;
77 : : // Hash doesn't take into account the timestamp
78 : 301427000 : size_t operator()(const NodeTheoryPair& pair) const {
79 : 301427000 : uint64_t hash = fnv1a::fnv1a_64(std::hash<Node>()(pair.d_node));
80 : 301427000 : return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash));
81 : : }
82 : : };/* struct NodeTheoryPairHashFunction */
83 : :
84 : :
85 : : /* Forward declarations */
86 : : namespace theory {
87 : :
88 : : class CombinationEngine;
89 : : class DecisionManager;
90 : : class PluginModule;
91 : : class RelevanceManager;
92 : : class Rewriter;
93 : : class SharedSolver;
94 : : class TheoryModel;
95 : : class ConflictProcessor;
96 : :
97 : : } // namespace theory
98 : :
99 : : namespace prop {
100 : : class PropEngine;
101 : : }
102 : :
103 : : /**
104 : : * This is essentially an abstraction for a collection of theories. A
105 : : * TheoryEngine provides services to a PropEngine, making various
106 : : * T-solvers look like a single unit to the propositional part of
107 : : * cvc5.
108 : : */
109 : : class TheoryEngine : protected EnvObj
110 : : {
111 : : /** Shared terms database can use the internals notify the theories */
112 : : friend class SharedTermsDatabase;
113 : : friend class theory::OutputChannel;
114 : : friend class theory::CombinationEngine;
115 : : friend class theory::SharedSolver;
116 : :
117 : : public:
118 : : /** Constructs a theory engine */
119 : : TheoryEngine(Env& env);
120 : :
121 : : /** Destroys a theory engine */
122 : : ~TheoryEngine();
123 : :
124 : : void interrupt();
125 : :
126 : : /** "Spend" a resource during a search or preprocessing.*/
127 : : void spendResource(Resource r);
128 : :
129 : : /**
130 : : * Adds a theory. Only one theory per TheoryId can be present, so if
131 : : * there is another theory it will be deleted.
132 : : */
133 : : template <class TheoryClass>
134 : 719450 : void addTheory(theory::TheoryId theoryId)
135 : : {
136 [ + - ][ + - ]: 1438900 : Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
[ - + ][ - - ]
137 : 719450 : d_theoryOut[theoryId] =
138 : 719450 : new theory::OutputChannel(statisticsRegistry(), this, theoryId);
139 : 873614 : d_theoryTable[theoryId] =
140 : 719450 : new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this));
141 : 1438900 : getRewriter()->registerTheoryRewriter(
142 : 719450 : theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
143 : 719450 : }
144 : :
145 : : /** Register theory proof rule checkers to the given proof checker */
146 : : void initializeProofChecker(ProofChecker* pc);
147 : :
148 : 51985 : void setPropEngine(prop::PropEngine* propEngine)
149 : : {
150 : 51985 : d_propEngine = propEngine;
151 : 51985 : }
152 : :
153 : : /**
154 : : * Called when all initialization of options/logic is done, after theory
155 : : * objects have been created.
156 : : *
157 : : * This initializes the quantifiers engine, the "official" equality engines
158 : : * of each theory as required, and the model and model builder utilities.
159 : : */
160 : : void finishInit();
161 : :
162 : : /**
163 : : * Get a pointer to the underlying propositional engine.
164 : : */
165 : 3384980 : prop::PropEngine* getPropEngine() const { return d_propEngine; }
166 : :
167 : : /**
168 : : * Get a pointer to the underlying quantifiers engine.
169 : : */
170 : 92809 : theory::QuantifiersEngine* getQuantifiersEngine() const
171 : : {
172 : 92809 : return d_quantEngine;
173 : : }
174 : : /**
175 : : * Get a pointer to the underlying decision manager.
176 : : */
177 : : theory::DecisionManager* getDecisionManager() const
178 : : {
179 : : return d_decManager.get();
180 : : }
181 : :
182 : : /**
183 : : * Preprocess rewrite, called:
184 : : * (1) on equalities by the preprocessor to rewrite equalities appearing in
185 : : * the input,
186 : : * (2) on non-equalities by the theory preprocessor.
187 : : *
188 : : * Calls the ppRewrite of the theory of term and adds the associated skolem
189 : : * lemmas to lems, for details see Theory::ppRewrite.
190 : : */
191 : : TrustNode ppRewrite(TNode term, std::vector<theory::SkolemLemma>& lems);
192 : : /**
193 : : * Same as above, but applied only at preprocess time.
194 : : */
195 : : TrustNode ppStaticRewrite(TNode term);
196 : : /** Notify (preprocessed) assertions. */
197 : : void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
198 : :
199 : : /**
200 : : * Return whether or not we are model unsound (in the current SAT context).
201 : : * For details, see theory_inference_manager.
202 : : */
203 : 24361 : bool isModelUnsound() const { return d_modelUnsound; }
204 : : /**
205 : : * Return whether or not we are refutation unsound (in the current user
206 : : * context). For details, see theory_inference_manager.
207 : : */
208 : 26796 : bool isRefutationUnsound() const { return d_refutationUnsound; }
209 : :
210 : : /**
211 : : * Returns true if we need another round of checking. If this
212 : : * returns true, check(FULL_EFFORT) _must_ be called by the
213 : : * propositional layer before reporting SAT.
214 : : *
215 : : * This is especially necessary for incomplete theories that lazily
216 : : * output some lemmas on FULL_EFFORT check (e.g. quantifier reasoning
217 : : * outputing quantifier instantiations). In such a case, a lemma can
218 : : * be asserted that is simplified away (perhaps it's already true).
219 : : * However, we must maintain the invariant that, if a theory uses the
220 : : * OutputChannel, it implicitly requests that another check(FULL_EFFORT)
221 : : * be performed before exit, even if no new facts are on its fact queue,
222 : : * as it might decide to further instantiate some lemmas, precluding
223 : : * a SAT response.
224 : : */
225 [ + + ][ - + ]: 1602370 : bool needCheck() const { return d_outputChannelUsed || d_lemmasAdded; }
226 : : /**
227 : : * Is the literal lit (possibly) critical for satisfying the input formula in
228 : : * the current context? This call is applicable only during collectModelInfo
229 : : * or during LAST_CALL effort.
230 : : */
231 : : bool isRelevant(Node lit) const;
232 : : /** is legal elimination
233 : : *
234 : : * Returns true if x -> val is a legal elimination of variable x. This is
235 : : * useful for ppAssert, when x = val is an entailed equality. This function
236 : : * determines whether indeed x can be eliminated from the problem via the
237 : : * substitution x -> val.
238 : : *
239 : : * The following criteria imply that x -> val is *not* a legal elimination:
240 : : * (1) If x is contained in val,
241 : : * (2) If the type of val is not the same as the type of x,
242 : : * (3) If val contains an operator that cannot be evaluated, and
243 : : * produceModels is true. For example, x -> sqrt(2) is not a legal
244 : : * elimination if we are producing models. This is because we care about the
245 : : * value of x, and its value must be computed (approximated) by the
246 : : * non-linear solver.
247 : : */
248 : : bool isLegalElimination(TNode x, TNode val);
249 : : /**
250 : : * Returns true if the node has a current SAT assignment. If yes, the
251 : : * argument "value" is set to its value.
252 : : *
253 : : * @return true if the literal has a current assignment, and returns the
254 : : * value in the "value" argument; otherwise false and the "value"
255 : : * argument is unmodified.
256 : : */
257 : : bool hasSatValue(TNode n, bool& value) const;
258 : : /**
259 : : * Same as above, without setting the value.
260 : : */
261 : : bool hasSatValue(TNode n) const;
262 : : /**
263 : : * Solve the given literal with a theory that owns it. The proof of tliteral
264 : : * is carried in the trust node. The proof added to substitutionOut should
265 : : * take this proof into account (when proofs are enabled).
266 : : *
267 : : * @param tin The literal and its proof generator.
268 : : * @param outSubstitutions The substitution map to add to, if applicable.
269 : : * @return true iff the literal can be removed from the input, e.g. when
270 : : * the substitution it entails is added to outSubstitutions.
271 : : */
272 : : bool solve(TrustNode tliteral, theory::TrustSubstitutionMap& substitutionOut);
273 : :
274 : : /**
275 : : * Preregister a Theory atom with the responsible theory (or
276 : : * theories).
277 : : */
278 : : void preRegister(TNode preprocessed);
279 : :
280 : : /**
281 : : * Assert the formula to the appropriate theory.
282 : : * @param node the assertion
283 : : */
284 : : void assertFact(TNode node);
285 : :
286 : : /**
287 : : * Check all (currently-active) theories for conflicts.
288 : : * @param effort the effort level to use
289 : : */
290 : : void check(theory::Theory::Effort effort);
291 : :
292 : : /**
293 : : * Calls ppStaticLearn() on all theories.
294 : : * Adds any new lemmas learned to the learned vector.
295 : : * @param in The formula that holds.
296 : : * @param learned The vector storing the new lemmas learned.
297 : : */
298 : : void ppStaticLearn(TNode in, std::vector<TrustNode>& learned);
299 : :
300 : : /**
301 : : * Calls presolve() on all theories and returns true
302 : : * if one of the theories discovers a conflict.
303 : : */
304 : : bool presolve();
305 : :
306 : : /**
307 : : * Resets the internal state.
308 : : */
309 : : void postsolve(prop::SatValue result);
310 : :
311 : : /**
312 : : * Calls notifyRestart() on all active theories.
313 : : */
314 : : void notifyRestart();
315 : :
316 : 34472900 : void getPropagatedLiterals(std::vector<TNode>& literals)
317 : : {
318 [ + + ]: 34472900 : for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size();
319 : 17218000 : d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1)
320 : : {
321 [ + - ]: 34435900 : Trace("getPropagatedLiterals")
322 : 0 : << "TheoryEngine::getPropagatedLiterals: propagating: "
323 : 17218000 : << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl;
324 : 17218000 : literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]);
325 : : }
326 : 17254900 : }
327 : :
328 : : /**
329 : : * Returns the next decision request, or null if none exist. The next
330 : : * decision request is a literal that this theory engine prefers the SAT
331 : : * solver to make as its next decision. Decision requests are managed by
332 : : * the decision manager d_decManager.
333 : : */
334 : : Node getNextDecisionRequest();
335 : :
336 : : bool properConflict(TNode conflict) const;
337 : :
338 : : /**
339 : : * Returns an explanation of the node propagated to the SAT solver.
340 : : */
341 : : TrustNode getExplanation(TNode node);
342 : :
343 : : /**
344 : : * Get the pointer to the model object used by this theory engine.
345 : : */
346 : : theory::TheoryModel* getModel();
347 : : /**
348 : : * Get the current model for the current set of assertions. This method
349 : : * should only be called immediately after a satisfiable response to a
350 : : * check-sat call, and only if produceModels is true.
351 : : *
352 : : * If the model is not already built, this will cause this theory engine to
353 : : * build the model.
354 : : *
355 : : * If the model cannot be built, then this returns the null pointer.
356 : : */
357 : : theory::TheoryModel* getBuiltModel();
358 : : /**
359 : : * This forces the model maintained by the combination engine to be built
360 : : * if it has not been done so already. This should be called only during a
361 : : * last call effort check after theory combination is run.
362 : : *
363 : : * @return true if the model was successfully built (possibly prior to this
364 : : * call).
365 : : */
366 : : bool buildModel();
367 : :
368 : : /**
369 : : * Get the theory associated to a given Node.
370 : : *
371 : : * @returns the theory, or NULL if the TNode is
372 : : * of built-in type.
373 : : */
374 : 94844 : theory::Theory* theoryOf(TNode node) const
375 : : {
376 : 94844 : return d_theoryTable[d_env.theoryOf(node)];
377 : : }
378 : :
379 : : /**
380 : : * Get the theory associated to a the given theory id.
381 : : *
382 : : * @returns the theory
383 : : */
384 : 147366000 : theory::Theory* theoryOf(theory::TheoryId theoryId) const
385 : : {
386 [ - + ][ - + ]: 147366000 : Assert(theoryId < theory::THEORY_LAST);
[ - - ]
387 : 147366000 : return d_theoryTable[theoryId];
388 : : }
389 : :
390 : : bool isTheoryEnabled(theory::TheoryId theoryId) const;
391 : : /** return the theory that should explain a propagation from TheoryId */
392 : : theory::TheoryId theoryExpPropagation(theory::TheoryId tid) const;
393 : :
394 : : /**
395 : : * Returns the equality status of the two terms, from the theory
396 : : * that owns the domain type. The types of a and b must be the same.
397 : : */
398 : : theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
399 : :
400 : : /**
401 : : * Returns the value that a theory that owns the type of var currently
402 : : * has (or null if none);
403 : : */
404 : : Node getCandidateModelValue(TNode var);
405 : :
406 : : /**
407 : : * Get relevant assertions. This returns a set of assertions that are
408 : : * currently asserted to this TheoryEngine that propositionally entail the
409 : : * (preprocessed) input formula and all theory lemmas that have been marked
410 : : * NEEDS_JUSTIFY. For more details on this, see relevance_manager.h.
411 : : *
412 : : * This method updates success to false if the set of relevant assertions
413 : : * is not available. This may occur if we are not in SAT mode, if the
414 : : * relevance manager is disabled (see option::relevanceFilter) or if the
415 : : * relevance manager failed to compute relevant assertions due to an internal
416 : : * error.
417 : : */
418 : : std::unordered_set<TNode> getRelevantAssertions(bool& success);
419 : :
420 : : /**
421 : : * Get difficulty map, which populates dmap, mapping preprocessed assertions
422 : : * to a value that estimates their difficulty for solving the current problem.
423 : : *
424 : : * For details, see theory/difficuly_manager.h.
425 : : */
426 : : void getDifficultyMap(std::map<Node, Node>& dmap, bool includeLemmas = false);
427 : :
428 : : /** Get incomplete id, valid when isModelUnsound is true. */
429 : : theory::IncompleteId getModelUnsoundId() const;
430 : : /** Get unsound id, valid when isRefutationUnsound is true. */
431 : : theory::IncompleteId getRefutationUnsoundId() const;
432 : :
433 : : /**
434 : : * Forwards an entailment check according to the given theoryOfMode.
435 : : * See theory.h for documentation on entailmentCheck().
436 : : */
437 : : std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
438 : :
439 : 8361 : theory::SortInference* getSortInference() { return d_sortInfer.get(); }
440 : :
441 : : /** Prints the assertions to the debug stream */
442 : : void printAssertions(const char* tag);
443 : :
444 : : /**
445 : : * Check that the theory assertions are satisfied in the model.
446 : : * This function is called from the smt engine's checkModel routine.
447 : : */
448 : : void checkTheoryAssertionsWithModel(bool hardFailure);
449 : :
450 : : /** Called externally to notify that the current branch is incomplete. */
451 : : void setModelUnsound(theory::IncompleteId id);
452 : : /** Called externally that we are unsound (user-context). */
453 : : void setRefutationUnsound(theory::IncompleteId id);
454 : :
455 : : private:
456 : : typedef context::
457 : : CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction>
458 : : PropagationMap;
459 : :
460 : : /**
461 : : * Called by the theories to notify of a conflict.
462 : : *
463 : : * @param conflict The trust node containing the conflict and its proof
464 : : * generator (if it exists),
465 : : * @param id The inference identifier for the conflict.
466 : : * @param theoryId The theory that sent the conflict
467 : : */
468 : : void conflict(TrustNode conflict,
469 : : theory::InferenceId id,
470 : : theory::TheoryId theoryId);
471 : :
472 : : /** set in conflict */
473 : : void markInConflict();
474 : :
475 : : /** Called by the theories to notify that the current branch is incomplete. */
476 : : void setModelUnsound(theory::TheoryId theory, theory::IncompleteId id);
477 : : /** Called by the theories to notify that we are unsound (user-context). */
478 : : void setRefutationUnsound(theory::TheoryId theory, theory::IncompleteId id);
479 : :
480 : : /**
481 : : * Called by the output channel to propagate literals and facts
482 : : * @return false if immediate conflict
483 : : */
484 : : bool propagate(TNode literal, theory::TheoryId theory);
485 : :
486 : : /**
487 : : * Internal method to call the propagation routines and collect the
488 : : * propagated literals.
489 : : */
490 : : void propagate(theory::Theory::Effort effort);
491 : :
492 : : /**
493 : : * Assert the formula to the given theory.
494 : : * @param assertion the assertion to send (not necesserily normalized)
495 : : * @param original the assertion as it was sent in from the propagating theory
496 : : * @param toTheoryId the theory to assert to
497 : : * @param fromTheoryId the theory that sent it
498 : : */
499 : : void assertToTheory(TNode assertion,
500 : : TNode originalAssertion,
501 : : theory::TheoryId toTheoryId,
502 : : theory::TheoryId fromTheoryId);
503 : :
504 : : /**
505 : : * Marks a theory propagation from a theory to a theory where a
506 : : * theory could be the THEORY_SAT_SOLVER for literals coming from
507 : : * or being propagated to the SAT solver. If the receiving theory
508 : : * already recieved the literal, the method returns false, otherwise
509 : : * it returns true.
510 : : *
511 : : * @param assertion the normalized assertion being sent
512 : : * @param originalAssertion the actual assertion that was sent
513 : : * @param toTheoryId the theory that is on the receiving end
514 : : * @param fromTheoryId the theory that sent the assertion
515 : : * @return true if a new assertion, false if theory already got it
516 : : */
517 : : bool markPropagation(TNode assertion,
518 : : TNode originalAssertions,
519 : : theory::TheoryId toTheoryId,
520 : : theory::TheoryId fromTheoryId);
521 : :
522 : : /**
523 : : * Computes the explanation by traversing the propagation graph and
524 : : * asking relevant theories to explain the propagations. Initially
525 : : * the explanation vector should contain only the element (node, theory)
526 : : * where the node is the one to be explained, and the theory is the
527 : : * theory that sent the literal.
528 : : */
529 : : TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector);
530 : :
531 : : /** Are proofs enabled? */
532 : : bool isProofEnabled() const;
533 : :
534 : : /**
535 : : * Get a pointer to the rewriter owned by the associated Env.
536 : : */
537 : : theory::Rewriter* getRewriter();
538 : :
539 : : /**
540 : : * Adds a new lemma, returning its status.
541 : : * @param node The lemma
542 : : * @param id The inference identifier for the lemma
543 : : * @param p The properties of the lemma.
544 : : * @param atomsTo The theory that atoms of the lemma should be sent to
545 : : * @param from The theory that sent the lemma.
546 : : */
547 : : void lemma(TrustNode node,
548 : : theory::InferenceId id,
549 : : theory::LemmaProperty p,
550 : : theory::TheoryId from = theory::THEORY_LAST);
551 : :
552 : : /** Ensure atoms from the given node are sent to the given theory */
553 : : void ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo);
554 : : /** Ensure that the given atoms are sent to the given theory */
555 : : void ensureLemmaAtoms(const std::vector<TNode>& atoms,
556 : : theory::TheoryId atomsTo);
557 : :
558 : : /** Associated PropEngine engine */
559 : : prop::PropEngine* d_propEngine;
560 : :
561 : : /**
562 : : * A table of from theory IDs to theory pointers. Never use this table
563 : : * directly, use theoryOf() instead.
564 : : */
565 : : theory::Theory* d_theoryTable[theory::THEORY_LAST];
566 : :
567 : : //--------------------------------- proofs
568 : : /** The lazy proof object
569 : : *
570 : : * This stores instructions for how to construct proofs for all theory lemmas.
571 : : */
572 : : std::shared_ptr<LazyCDProof> d_lazyProof;
573 : : /** The proof generator */
574 : : std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
575 : : //--------------------------------- end proofs
576 : : /** The combination manager we are using */
577 : : std::unique_ptr<theory::CombinationEngine> d_tc;
578 : : /** The shared solver of the above combination engine. */
579 : : theory::SharedSolver* d_sharedSolver;
580 : : /** The quantifiers engine, which is owned by the quantifiers theory */
581 : : theory::QuantifiersEngine* d_quantEngine;
582 : : /**
583 : : * The decision manager
584 : : */
585 : : std::unique_ptr<theory::DecisionManager> d_decManager;
586 : : /** The relevance manager */
587 : : std::unique_ptr<theory::RelevanceManager> d_relManager;
588 : :
589 : : /**
590 : : * Output channels for individual theories.
591 : : */
592 : : theory::OutputChannel* d_theoryOut[theory::THEORY_LAST];
593 : :
594 : : /**
595 : : * Are we in conflict.
596 : : */
597 : : context::CDO<bool> d_inConflict;
598 : :
599 : : /**
600 : : * True if a theory has notified us of model unsoundness (at this SAT
601 : : * context level or below). For details, see theory_inference_manager.
602 : : */
603 : : context::CDO<bool> d_modelUnsound;
604 : : /** The theory and identifier that (most recently) set model unsound */
605 : : context::CDO<theory::TheoryId> d_modelUnsoundTheory;
606 : : context::CDO<theory::IncompleteId> d_modelUnsoundId;
607 : : /**
608 : : * True if a theory has notified us of refutation unsoundness (at this user
609 : : * context level or below).
610 : : */
611 : : context::CDO<bool> d_refutationUnsound;
612 : : /** The theory and identifier that (most recently) set incomplete */
613 : : context::CDO<theory::TheoryId> d_refutationUnsoundTheory;
614 : : context::CDO<theory::IncompleteId> d_refutationUnsoundId;
615 : :
616 : : /**
617 : : * Mapping of propagations from recievers to senders.
618 : : */
619 : : PropagationMap d_propagationMap;
620 : :
621 : : /**
622 : : * Timestamp of propagations
623 : : */
624 : : context::CDO<size_t> d_propagationMapTimestamp;
625 : :
626 : : /**
627 : : * Literals that are propagated by the theory. Note that these are TNodes.
628 : : * The theory can only propagate nodes that have an assigned literal in the
629 : : * SAT solver and are hence referenced in the SAT solver.
630 : : */
631 : : context::CDList<TNode> d_propagatedLiterals;
632 : :
633 : : /**
634 : : * The index of the next literal to be propagated by a theory.
635 : : */
636 : : context::CDO<unsigned> d_propagatedLiteralsIndex;
637 : :
638 : : /**
639 : : * A variable to mark if we added any lemmas.
640 : : */
641 : : bool d_lemmasAdded;
642 : :
643 : : /**
644 : : * A variable to mark if the OutputChannel was "used" by any theory
645 : : * since the start of the last check. If it has been, we require
646 : : * a FULL_EFFORT check before exiting and reporting SAT.
647 : : *
648 : : * See the documentation for the needCheck() function, below.
649 : : */
650 : : bool d_outputChannelUsed;
651 : :
652 : : /** Atom requests from lemmas */
653 : : AtomRequests d_atomRequests;
654 : :
655 : : /** sort inference module */
656 : : std::unique_ptr<theory::SortInference> d_sortInfer;
657 : :
658 : : /** Statistics */
659 : : theory::TheoryEngineStatistics d_stats;
660 : :
661 : : Node d_true;
662 : : Node d_false;
663 : :
664 : : /** Whether we were just interrupted (or not) */
665 : : bool d_interrupted;
666 : :
667 : : /**
668 : : * Queue of nodes for pre-registration.
669 : : */
670 : : std::queue<TNode> d_preregisterQueue;
671 : :
672 : : /**
673 : : * Boolean flag denoting we are in pre-registration.
674 : : */
675 : : bool d_inPreregister;
676 : :
677 : : /**
678 : : * Did the theories get any new facts since the last time we called
679 : : * check()
680 : : */
681 : : context::CDO<bool> d_factsAsserted;
682 : :
683 : : /**
684 : : * The splitter produces partitions when the compute-partitions option is
685 : : * used.
686 : : */
687 : : std::unique_ptr<theory::PartitionGenerator> d_partitionGen;
688 : : /** The list of modules */
689 : : std::vector<theory::TheoryEngineModule*> d_modules;
690 : : /** Conflict processor */
691 : : std::unique_ptr<theory::ConflictProcessor> d_cp;
692 : : /** User plugin modules */
693 : : std::vector<std::unique_ptr<theory::PluginModule>> d_userPlugins;
694 : :
695 : : }; /* class TheoryEngine */
696 : :
697 : : } // namespace cvc5::internal
698 : :
699 : : #endif /* CVC5__THEORY_ENGINE_H */
|
