Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Morgan Deters, Tim King
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 : : * Base of the theory interface.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__THEORY_H
19 : : #define CVC5__THEORY__THEORY_H
20 : :
21 : : #include <iosfwd>
22 : : #include <set>
23 : : #include <string>
24 : : #include <unordered_set>
25 : :
26 : : #include "context/cdlist.h"
27 : : #include "context/cdo.h"
28 : : #include "context/context.h"
29 : : #include "expr/node.h"
30 : : #include "options/theory_options.h"
31 : : #include "proof/trust_node.h"
32 : : #include "smt/env.h"
33 : : #include "smt/env_obj.h"
34 : : #include "theory/assertion.h"
35 : : #include "theory/care_graph.h"
36 : : #include "theory/logic_info.h"
37 : : #include "theory/skolem_lemma.h"
38 : : #include "theory/theory_id.h"
39 : : #include "theory/valuation.h"
40 : : #include "util/statistics_stats.h"
41 : :
42 : : namespace cvc5::internal {
43 : :
44 : : class ProofNodeManager;
45 : : class TheoryEngine;
46 : : class ProofRuleChecker;
47 : :
48 : : namespace theory {
49 : :
50 : : class CarePairArgumentCallback;
51 : : class DecisionManager;
52 : : struct EeSetupInfo;
53 : : class OutputChannel;
54 : : class QuantifiersEngine;
55 : : class TheoryInferenceManager;
56 : : class TheoryModel;
57 : : class TheoryRewriter;
58 : : class TheoryState;
59 : : class TrustSubstitutionMap;
60 : :
61 : : namespace eq {
62 : : class EqualityEngine;
63 : : } // namespace eq
64 : :
65 : : /**
66 : : * Base class for T-solvers. Abstract DPLL(T).
67 : : *
68 : : * This is essentially an interface class. The TheoryEngine has
69 : : * pointers to Theory. Note that only one specific Theory type (e.g.,
70 : : * TheoryUF) can exist per NodeManager, because of how the
71 : : * RegisteredAttr works. (If you need multiple instances of the same
72 : : * theory, you'll have to write a multiplexed theory that dispatches
73 : : * all calls to them.)
74 : : *
75 : : * NOTE: A Theory has a special way of being initialized. The owner of a Theory
76 : : * is either:
77 : : *
78 : : * (A) Using Theory as a standalone object, not associated with a TheoryEngine.
79 : : * In this case, simply call the public initialization method
80 : : * (Theory::finishInitStandalone).
81 : : *
82 : : * (B) TheoryEngine, which determines how the Theory acts in accordance with
83 : : * its theory combination policy. We require the following steps in order:
84 : : * (B.1) Get information about whether the theory wishes to use an equality
85 : : * eninge, and more specifically which equality engine notifications the Theory
86 : : * would like to be notified of (Theory::needsEqualityEngine).
87 : : * (B.2) Set the equality engine of the theory (Theory::setEqualityEngine),
88 : : * which we refer to as the "official equality engine" of this Theory. The
89 : : * equality engine passed to the theory must respect the contract(s) specified
90 : : * by the equality engine setup information (EeSetupInfo) returned in the
91 : : * previous step.
92 : : * (B.3) Set the other required utilities including setQuantifiersEngine and
93 : : * setDecisionManager.
94 : : * (B.4) Call the private initialization method (Theory::finishInit).
95 : : *
96 : : * Initialization of the second form happens during TheoryEngine::finishInit,
97 : : * after the quantifiers engine and model objects have been set up.
98 : : */
99 : : class Theory : protected EnvObj
100 : : {
101 : : friend class CarePairArgumentCallback;
102 : : friend class internal::TheoryEngine;
103 : :
104 : : protected:
105 : : /** Name of this theory instance. Along with the TheoryId this should
106 : : * provide an unique string identifier for each instance of a Theory class.
107 : : * We need this to ensure unique statistics names over multiple theory
108 : : * instances. */
109 : : std::string d_instanceName;
110 : :
111 : : // === STATISTICS ===
112 : : /** time spent in check calls */
113 : : TimerStat d_checkTime;
114 : : /** time spent in theory combination */
115 : : TimerStat d_computeCareGraphTime;
116 : :
117 : : /** Add (t1, t2) to the care graph */
118 : : void addCarePair(TNode t1, TNode t2);
119 : : /**
120 : : * Assuming a is f(a1, ..., an) and b is f(b1, ..., bn), this method adds
121 : : * (ai, bi) to the care graph for each i where ai is not equal to bi.
122 : : */
123 : : void addCarePairArgs(TNode a, TNode b);
124 : : /**
125 : : * Process care pair arguments for a and b. By default, this calls the
126 : : * method above if a and b are not equal according to the equality engine
127 : : * of this theory.
128 : : */
129 : : virtual void processCarePairArgs(TNode a, TNode b);
130 : : /**
131 : : * Are care disequal? Return true if x and y are distinct constants, shared
132 : : * terms that are disequal according to the valuation, or otherwise
133 : : * disequal according to the equality engine of this theory.
134 : : */
135 : : virtual bool areCareDisequal(TNode x, TNode y);
136 : :
137 : : /**
138 : : * The function should compute the care graph over the shared terms.
139 : : * The default function returns all the pairs among the shared variables.
140 : : */
141 : : virtual void computeCareGraph();
142 : :
143 : : /**
144 : : * Construct a Theory.
145 : : *
146 : : * The pair <id, instance> is assumed to uniquely identify this Theory
147 : : * w.r.t. the SolverEngine.
148 : : */
149 : : Theory(TheoryId id,
150 : : Env& env,
151 : : OutputChannel& out,
152 : : Valuation valuation,
153 : : std::string instance = ""); // taking : No default.
154 : :
155 : : /**
156 : : * The output channel for the Theory.
157 : : */
158 : : OutputChannel* d_out;
159 : :
160 : : /**
161 : : * The valuation proxy for the Theory to communicate back with the
162 : : * theory engine (and other theories).
163 : : */
164 : : Valuation d_valuation;
165 : : /**
166 : : * Pointer to the official equality engine of this theory, which is owned by
167 : : * the equality engine manager of TheoryEngine.
168 : : */
169 : : eq::EqualityEngine* d_equalityEngine;
170 : : /**
171 : : * The official equality engine, if we allocated it.
172 : : */
173 : : std::unique_ptr<eq::EqualityEngine> d_allocEqualityEngine;
174 : : /**
175 : : * The theory state, which contains contexts, valuation, and equality
176 : : * engine. Notice the theory is responsible for memory management of this
177 : : * class.
178 : : */
179 : : TheoryState* d_theoryState;
180 : : /**
181 : : * The theory inference manager. This is a wrapper around the equality
182 : : * engine and the output channel. It ensures that the output channel and
183 : : * the equality engine are used properly.
184 : : */
185 : : TheoryInferenceManager* d_inferManager;
186 : :
187 : : /**
188 : : * Pointer to the quantifiers engine (or NULL, if quantifiers are not
189 : : * supported or not enabled). Not owned by the theory.
190 : : */
191 : : QuantifiersEngine* d_quantEngine;
192 : :
193 : : /** Pointer to proof node manager */
194 : : ProofNodeManager* d_pnm;
195 : : /**
196 : : * Are proofs enabled?
197 : : *
198 : : * They are considered enabled if the ProofNodeManager is non-null.
199 : : */
200 : : bool proofsEnabled() const;
201 : :
202 : : void printFacts(std::ostream& os) const;
203 : : void debugPrintFacts() const;
204 : :
205 : : //--------------------------------- private initialization
206 : : /**
207 : : * Called to set the official equality engine. This should be done by
208 : : * TheoryEngine only.
209 : : */
210 : : void setEqualityEngine(eq::EqualityEngine* ee);
211 : : /** Called to set the quantifiers engine. */
212 : : void setQuantifiersEngine(QuantifiersEngine* qe);
213 : : /** Called to set the decision manager. */
214 : : void setDecisionManager(DecisionManager* dm);
215 : : /**
216 : : * Finish theory initialization. At this point, options and the logic
217 : : * setting are final, the master equality engine and quantifiers
218 : : * engine (if any) are initialized, and the official equality engine of this
219 : : * theory has been assigned. This base class implementation
220 : : * does nothing. This should be called by TheoryEngine only.
221 : : */
222 : 49903 : virtual void finishInit() {}
223 : : //--------------------------------- end private initialization
224 : :
225 : : /**
226 : : * This method is called to notify a theory that the node n should
227 : : * be considered a "shared term" by this theory. This does anything
228 : : * theory-specific concerning the fact that n is now marked as a shared
229 : : * term, which is done in addition to explicitly storing n as a shared
230 : : * term and adding it as a trigger term in the equality engine of this
231 : : * class (see addSharedTerm).
232 : : */
233 : : virtual void notifySharedTerm(TNode n);
234 : : /**
235 : : * Notify in conflict, called when a conflict clause is added to
236 : : * TheoryEngine by any theory (not necessarily this one). This signals that
237 : : * the theory should suspend what it is currently doing and wait for
238 : : * backtracking.
239 : : */
240 : : virtual void notifyInConflict();
241 : :
242 : : public:
243 : : //--------------------------------- initialization
244 : : /**
245 : : * @return The theory rewriter associated with this theory.
246 : : */
247 : : virtual TheoryRewriter* getTheoryRewriter() = 0;
248 : : /**
249 : : * @return The proof checker associated with this theory.
250 : : */
251 : : virtual ProofRuleChecker* getProofChecker() = 0;
252 : : /**
253 : : * Returns true if this theory needs an equality engine for checking
254 : : * satisfiability.
255 : : *
256 : : * If this method returns true, then the equality engine manager will
257 : : * initialize its equality engine field via setEqualityEngine above during
258 : : * TheoryEngine::finishInit, prior to calling finishInit for this theory.
259 : : *
260 : : * Additionally, if this method returns true, then this method is required
261 : : * to update the argument esi with instructions for initializing and setting
262 : : * up notifications from its equality engine, which is commonly done with a
263 : : * notifications class (eq::EqualityEngineNotify).
264 : : */
265 : : virtual bool needsEqualityEngine(EeSetupInfo& esi);
266 : : /**
267 : : * Finish theory initialization, standalone version. This is used to
268 : : * initialize this class if it is not associated with a theory engine.
269 : : * This allocates the official equality engine of this Theory and then
270 : : * calls the finishInit method above.
271 : : */
272 : : void finishInitStandalone();
273 : : //--------------------------------- end initialization
274 : :
275 : : /**
276 : : * Return the ID of the theory responsible for the given type.
277 : : */
278 : 100952000 : static inline TheoryId theoryOf(TypeNode typeNode,
279 : : TheoryId usortOwner = theory::THEORY_UF)
280 : : {
281 : : TheoryId id;
282 [ + + ]: 100952000 : if (typeNode.getKind() == Kind::TYPE_CONSTANT)
283 : : {
284 : 73049800 : id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
285 : : }
286 : : else
287 : : {
288 : 27902500 : id = kindToTheoryId(typeNode.getKind());
289 : : }
290 [ + + ]: 100952000 : if (id == THEORY_BUILTIN)
291 : : {
292 : 4317350 : return usortOwner;
293 : : }
294 : 96635000 : return id;
295 : : }
296 : :
297 : : /**
298 : : * Returns the ID of the theory responsible for the given node.
299 : : *
300 : : * Note this method does not take into account "Boolean term skolem". Boolean
301 : : * term skolems always belong to THEORY_UF. This case is handled in
302 : : * Env::theoryOf.
303 : : *
304 : : * @param node The node in question.
305 : : * @param mdoe The theoryof mode, which impacts which theory owns e.g.
306 : : * variables.
307 : : * @param usortOwner The theory that owns uninterpreted sorts.
308 : : * @return The theory that owns node.
309 : : */
310 : : static TheoryId theoryOf(
311 : : TNode node,
312 : : options::TheoryOfMode mode = options::TheoryOfMode::THEORY_OF_TYPE_BASED,
313 : : TheoryId usortOwner = theory::THEORY_UF);
314 : :
315 : : /**
316 : : * Checks if the node is a leaf node of this theory.
317 : : */
318 : 9101 : inline bool isLeaf(TNode node) const
319 : : {
320 : : // variables have 0 children thus theoryOf is not impacted by whether
321 : : // node is a Boolean term skolem.
322 : 18202 : return node.getNumChildren() == 0
323 [ + + ][ + + ]: 9101 : || theoryOf(node, options().theory.theoryOfMode) != d_id;
[ + + ][ - - ]
324 : : }
325 : :
326 : : /**
327 : : * Checks if the node is a leaf node of a theory.
328 : : */
329 : 161952000 : inline static bool isLeafOf(
330 : : TNode node,
331 : : TheoryId theoryId,
332 : : options::TheoryOfMode mode = options::TheoryOfMode::THEORY_OF_TYPE_BASED)
333 : : {
334 : : // variables have 0 children thus theoryOf is not impacted by whether
335 : : // node is a Boolean term skolem.
336 [ + + ][ + + ]: 161952000 : return node.getNumChildren() == 0 || theoryOf(node, mode) != theoryId;
[ + + ][ - - ]
337 : : }
338 : :
339 : : /** Returns true if the assertFact queue is empty*/
340 : 117469009 : bool done() const { return d_factsHead == d_facts.size(); }
341 : : /**
342 : : * Destructs a Theory.
343 : : */
344 : : virtual ~Theory();
345 : :
346 : : /**
347 : : * Subclasses of Theory may add additional efforts. DO NOT CHECK
348 : : * equality with one of these values (e.g. if STANDARD xxx) but
349 : : * rather use range checks (or use the helper functions below).
350 : : * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
351 : : * with FULL_EFFORT.
352 : : */
353 : : enum Effort
354 : : {
355 : : /**
356 : : * Standard effort where theory need not do anything
357 : : */
358 : : EFFORT_STANDARD = 50,
359 : : /**
360 : : * Full effort requires the theory make sure its assertions are
361 : : * satisfiable or not
362 : : */
363 : : EFFORT_FULL = 100,
364 : : /**
365 : : * Last call effort, called after theory combination has completed with
366 : : * no lemmas and a model is available.
367 : : */
368 : : EFFORT_LAST_CALL = 200
369 : : }; /* enum Effort */
370 : :
371 : 80310902 : static bool fullEffort(Effort e) { return e == EFFORT_FULL; }
372 : :
373 : : /**
374 : : * Get the id for this Theory.
375 : : */
376 : 715 : TheoryId getId() const { return d_id; }
377 : :
378 : : /**
379 : : * Get the output channel associated to this theory.
380 : : */
381 : 705271 : OutputChannel& getOutputChannel() { return *d_out; }
382 : :
383 : : /**
384 : : * Get the valuation associated to this theory.
385 : : */
386 : 115715 : Valuation& getValuation() { return d_valuation; }
387 : :
388 : : /** Get the equality engine being used by this theory. */
389 : : eq::EqualityEngine* getEqualityEngine();
390 : :
391 : : /**
392 : : * Get the quantifiers engine associated to this theory.
393 : : */
394 : 691523 : QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
395 : :
396 : : /**
397 : : * @return The theory state associated with this theory.
398 : : */
399 : 673063 : TheoryState* getTheoryState() { return d_theoryState; }
400 : :
401 : : /**
402 : : * @return The theory inference manager associated with this theory.
403 : : */
404 : 49903 : TheoryInferenceManager* getInferenceManager() { return d_inferManager; }
405 : :
406 : : /**
407 : : * Pre-register a term. Done one time for a Node per SAT context level.
408 : : */
409 : : virtual void preRegisterTerm(TNode);
410 : :
411 : : /**
412 : : * Assert a fact in the current context.
413 : : */
414 : 35029703 : void assertFact(TNode assertion, bool isPreregistered)
415 : : {
416 [ + - ]: 70059406 : Trace("theory") << "Theory<" << getId() << ">::assertFact["
417 : 0 : << context()->getLevel() << "](" << assertion << ", "
418 [ - - ]: 35029703 : << (isPreregistered ? "true" : "false") << ")" << std::endl;
419 : 35029703 : d_facts.push_back(Assertion(assertion, isPreregistered));
420 : 35029703 : }
421 : :
422 : : /** Add shared term to the theory. */
423 : : void addSharedTerm(TNode node);
424 : :
425 : : /**
426 : : * Return the current theory care graph. Theories should overload
427 : : * computeCareGraph to do the actual computation, and use addCarePair to add
428 : : * pairs to the care graph.
429 : : */
430 : : void getCareGraph(CareGraph* careGraph);
431 : :
432 : : /**
433 : : * Return the status of two terms in the current context. Should be
434 : : * implemented in sub-theories to enable more efficient theory-combination.
435 : : */
436 : : virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
437 : :
438 : : /**
439 : : * Return the candidate model value of the give shared term (or null if not
440 : : * available). A candidate model value is one computed at full effort,
441 : : * prior to running theory combination and final model construction.
442 : : * Typically only non-parametric theories are able to implement this method,
443 : : * since model construction for parametric theories involves running final
444 : : * model construction.
445 : : */
446 : 2711 : virtual Node getCandidateModelValue(TNode var) { return Node::null(); }
447 : :
448 : : /** T-propagate new literal assignments in the current context. */
449 : 0 : virtual void propagate(Effort level = EFFORT_FULL) {}
450 : :
451 : : /**
452 : : * Return an explanation for the literal represented by parameter n
453 : : * (which was previously propagated by this theory).
454 : : */
455 : 0 : virtual TrustNode explain(TNode n)
456 : : {
457 : 0 : Unimplemented() << "Theory " << identify()
458 : : << " propagated a node but doesn't implement the "
459 : 0 : "Theory::explain() interface!";
460 : : return TrustNode::null();
461 : : }
462 : :
463 : : //--------------------------------- check
464 : : /**
465 : : * Does this theory wish to be called to check at last call effort? This is
466 : : * the case for any theory that wishes to run when a model is available.
467 : : */
468 : 209755 : virtual bool needsCheckLastEffort() { return false; }
469 : : /**
470 : : * Check the current assignment's consistency.
471 : : *
472 : : * An implementation of check() is required to either:
473 : : * - return a conflict on the output channel,
474 : : * - be interrupted,
475 : : * - throw an exception
476 : : * - or call get() until done() is true.
477 : : *
478 : : * The standard method for check consists of a loop that processes the
479 : : * entire fact queue when preCheck returns false. It makes four
480 : : * theory-specific callbacks, (preCheck, postCheck, preNotifyFact,
481 : : * notifyFact) as described below. It asserts each fact to the official
482 : : * equality engine when preNotifyFact returns false.
483 : : *
484 : : * Theories that use this check method must use an official theory
485 : : * state object (d_theoryState).
486 : : */
487 : : void check(Effort level = EFFORT_FULL);
488 : : /**
489 : : * Pre-check, called before the fact queue of the theory is processed.
490 : : * If this method returns false, then the theory will process its fact
491 : : * queue. If this method returns true, then the theory has indicated
492 : : * its check method should finish immediately.
493 : : */
494 : : virtual bool preCheck(Effort level = EFFORT_FULL);
495 : : /**
496 : : * Post-check, called after the fact queue of the theory is processed.
497 : : */
498 : : virtual void postCheck(Effort level = EFFORT_FULL);
499 : : /**
500 : : * Pre-notify fact, return true if the theory processed it. If this
501 : : * method returns false, then the atom will be added to the equality engine
502 : : * of the theory and notifyFact will be called with isInternal=false.
503 : : *
504 : : * Theories that implement check but do not use official equality
505 : : * engines should always return true for this method.
506 : : *
507 : : * @param atom The atom
508 : : * @param polarity Its polarity
509 : : * @param fact The original literal that was asserted
510 : : * @param isPrereg Whether the assertion is preregistered
511 : : * @param isInternal Whether the origin of the fact was internal. If this
512 : : * is false, the fact was asserted via the fact queue of the theory.
513 : : * @return true if the theory completely processed this fact, i.e. it does
514 : : * not need to assert the fact to its equality engine.
515 : : */
516 : : virtual bool preNotifyFact(
517 : : TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal);
518 : : /**
519 : : * Notify fact, called immediately after the fact was pushed into the
520 : : * equality engine.
521 : : *
522 : : * @param atom The atom
523 : : * @param polarity Its polarity
524 : : * @param fact The original literal that was asserted.
525 : : * @param isInternal Whether the origin of the fact was internal. If this
526 : : * is false, the fact was asserted via the fact queue of the theory.
527 : : */
528 : : virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal);
529 : : //--------------------------------- end check
530 : :
531 : : //--------------------------------- collect model info
532 : : /**
533 : : * Get all relevant information in this theory regarding the current
534 : : * model. This should be called after a call to check( FULL_EFFORT )
535 : : * for all theories with no conflicts and no lemmas added.
536 : : *
537 : : * This method returns true if and only if the equality engine of m is
538 : : * consistent as a result of this call.
539 : : *
540 : : * The standard method for collectModelInfo computes the relevant terms,
541 : : * asserts the theory's equality engine to the model (if necessary) and
542 : : * then calls computeModelValues.
543 : : *
544 : : * TODO (project #39): this method should be non-virtual, once all theories
545 : : * conform to the new standard, delete, move to model manager distributed.
546 : : */
547 : : virtual bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet);
548 : : /**
549 : : * Compute terms that are not necessarily part of the assertions or
550 : : * shared terms that should be considered relevant, add them to termSet.
551 : : */
552 : : virtual void computeRelevantTerms(std::set<Node>& termSet);
553 : : /**
554 : : * Collect asserted terms for this theory and add them to termSet.
555 : : *
556 : : * @param termSet The set to add terms to
557 : : * @param includeShared Whether to include the shared terms of the theory
558 : : * @param irrKind The kinds
559 : : */
560 : : void collectAssertedTerms(std::set<Node>& termSet,
561 : : bool includeShared,
562 : : const std::set<Kind>& irrKinds) const;
563 : : /** Same as above, using the irrelevant model kinds for irrKinds.*/
564 : : void collectAssertedTermsForModel(std::set<Node>& termSet,
565 : : bool includeShared = true) const;
566 : : /**
567 : : * Helper function for collectAssertedTerms, adds all subterms
568 : : * belonging to this theory to termSet.
569 : : */
570 : : void collectTerms(TNode n,
571 : : std::set<Node>& termSet,
572 : : const std::set<Kind>& irrKinds) const;
573 : : /**
574 : : * Collect model values, after equality information is added to the model.
575 : : * The argument termSet is the set of relevant terms returned by
576 : : * computeRelevantTerms.
577 : : */
578 : : virtual bool collectModelValues(TheoryModel* m,
579 : : const std::set<Node>& termSet);
580 : : /** if theories want to do something with model after building, do it here
581 : : */
582 : 52650 : virtual void postProcessModel(TheoryModel* m) {}
583 : : //--------------------------------- end collect model info
584 : :
585 : : //--------------------------------- preprocessing
586 : : /**
587 : : * Statically learn from assertion "in," which has been asserted
588 : : * true at the top level.
589 : : */
590 : 0 : virtual void ppStaticLearn(TNode in, std::vector<TrustNode>& learned) {}
591 : :
592 : : /**
593 : : * Given a literal and its proof generator (encapsulated by trust node tin),
594 : : * add the solved substitutions to the map, if any. The method should return
595 : : * true if the literal can be safely removed from the input problem.
596 : : *
597 : : * Note that tin has trust node kind LEMMA. Its proof generator should be
598 : : * taken into account when adding a substitution to outSubstitutions when
599 : : * proofs are enabled.
600 : : *
601 : : * @param tin The literal and its proof generator.
602 : : * @param outSubstitutions The substitution map to add to, if applicable.
603 : : * @return true iff the literal can be removed from the input, e.g. when
604 : : * the substitution it entails is added to outSubstitutions.
605 : : */
606 : : virtual bool ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions);
607 : :
608 : : /**
609 : : * Given a term of the theory coming from the input formula or
610 : : * from a lemma generated during solving, this method can be overridden in a
611 : : * theory implementation to rewrite the term into an equivalent form.
612 : : *
613 : : * This method returns a TrustNode of kind TrustNodeKind::REWRITE, which
614 : : * carries information about the proof generator for the rewrite, which can
615 : : * be the null TrustNode if n is unchanged.
616 : : *
617 : : * Notice this method is only in theory preprocessing. It is called on all
618 : : * (non-equality) terms n that occur in the input formula or in lemmas. We
619 : : * do not pass equality terms to this method, since they should never be
620 : : * preprocessed in lemmas. Instead, equalities may be prepreocessed in
621 : : * the ppStaticRewrite method below.
622 : : *
623 : : * @param n the node to preprocess-rewrite.
624 : : * @param lems a set of lemmas that should be added as a consequence of
625 : : * preprocessing n. These are in the form of "skolem lemmas". For example,
626 : : * calling this method on (div x n), we return a trust node proving:
627 : : * (= (div x n) k_div)
628 : : * for fresh skolem k, and add the skolem lemma for k that indicates that
629 : : * it is the division of x and n.
630 : : *
631 : : * Note that ppRewrite should not return WITNESS terms, since the internal
632 : : * calculus works in "original forms" and not "witness forms".
633 : : */
634 : 2600070 : virtual TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
635 : : {
636 : 2600070 : return TrustNode::null();
637 : : }
638 : : /**
639 : : * Similar to the above method, given a term of the theory coming from the
640 : : * input formula, this method can be overridden in a theory implementation to
641 : : * rewrite the term into an equivalent form. This method returns a TrustNode
642 : : * of kind TrustNodeKind::REWRITE, as in ppRewrite.
643 : : *
644 : : * Notice this method is used in the "static preprocess rewrite"
645 : : * preprocessing pass, where n is a term from the input formula.
646 : : * It is not called on lemmas generated during solving.
647 : : *
648 : : * @param n the node to preprocess-rewrite.
649 : : *
650 : : * Note that ppRewrite should not return WITNESS terms, since the internal
651 : : * calculus works in "original forms" and not "witness forms".
652 : : */
653 : 1976020 : virtual TrustNode ppStaticRewrite(TNode n) { return TrustNode::null(); }
654 : :
655 : : /**
656 : : * Notify preprocessed assertions. Called on new assertions after
657 : : * preprocessing before they are asserted to theory engine.
658 : : */
659 : 773652 : virtual void ppNotifyAssertions(const std::vector<Node>& assertions) {}
660 : : //--------------------------------- end preprocessing
661 : :
662 : : /**
663 : : * A Theory is called with presolve exactly one time per user
664 : : * check-sat. presolve() is called after preregistration,
665 : : * rewriting, and Boolean propagation, (other theories'
666 : : * propagation?), but the notified Theory has not yet had its
667 : : * check() or propagate() method called. A Theory may empty its
668 : : * assertFact() queue using get(). A Theory can raise conflicts,
669 : : * add lemmas, and propagate literals during presolve().
670 : : *
671 : : * NOTE: The presolve property must be added to the kinds file for
672 : : * the theory.
673 : : */
674 : 0 : virtual void presolve() {}
675 : :
676 : : /**
677 : : * Notification sent to the theory wheneven the search restarts.
678 : : * Serves as a good time to do some clean-up work, and you can
679 : : * assume you're at DL 0 for the purposes of Contexts. This function
680 : : * should not use the output channel.
681 : : */
682 : 0 : virtual void notifyRestart() {}
683 : :
684 : : /**
685 : : * Identify this theory (for debugging, dynamic configuration,
686 : : * etc..)
687 : : */
688 : : virtual std::string identify() const = 0;
689 : :
690 : : typedef context::CDList<Assertion>::const_iterator assertions_iterator;
691 : :
692 : : /**
693 : : * Provides access to the facts queue, primarily intended for theory
694 : : * debugging purposes.
695 : : *
696 : : * @return the iterator to the beginning of the fact queue
697 : : */
698 : 1214420 : assertions_iterator facts_begin() const { return d_facts.begin(); }
699 : :
700 : : /**
701 : : * Provides access to the facts queue, primarily intended for theory
702 : : * debugging purposes.
703 : : *
704 : : * @return the iterator to the end of the fact queue
705 : : */
706 : 3678040 : assertions_iterator facts_end() const { return d_facts.end(); }
707 : : /**
708 : : * Whether facts have been asserted to this theory.
709 : : *
710 : : * @return true iff facts have been asserted to this theory.
711 : : */
712 : : bool hasFacts() { return !d_facts.empty(); }
713 : :
714 : : /** Return total number of facts asserted to this theory */
715 : 0 : size_t numAssertions() { return d_facts.size(); }
716 : :
717 : : typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
718 : :
719 : : /**
720 : : * This allows the theory to be queried for whether a literal, lit, is
721 : : * entailed by the theory. This returns a pair of a Boolean and a node E.
722 : : *
723 : : * If the Boolean is true, then E is a formula that entails lit and E is
724 : : * propositionally entailed by the assertions to the theory.
725 : : *
726 : : * If the Boolean is false, it is "unknown" if lit is entailed and E may be
727 : : * any node.
728 : : *
729 : : * The literal lit is either an atom a or (not a), which must belong to the
730 : : * theory: There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) ==
731 : : * this->getId().
732 : : *
733 : : * There are NO assumptions that a or the subterms of a have been
734 : : * preprocessed in any form. This includes ppRewrite, rewriting,
735 : : * preregistering, registering, definition expansion or ITE removal!
736 : : *
737 : : * Theories are free to limit the amount of effort they use and so may
738 : : * always opt to return "unknown". Both "unknown" and "not entailed",
739 : : * may return for E a non-boolean Node (e.g. Node::null()). (There is no
740 : : * explicit output for the negation of lit is entailed.)
741 : : *
742 : : * If lit is theory valid, the return result may be the Boolean constant
743 : : * true for E.
744 : : *
745 : : * If lit is entailed by multiple assertions on the theory's getFact()
746 : : * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
747 : : * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ...
748 : : * a_k)
749 : : *
750 : : * If lit is entailed by a single assertion on the theory's getFact()
751 : : * queue, say a, this may return E=a.
752 : : *
753 : : * The theory may always return false!
754 : : *
755 : : * Theories may not touch their output stream during an entailment check.
756 : : *
757 : : * @param lit a literal belonging to the theory.
758 : : * @return a pair <b,E> s.t. if b is true, then a formula E such
759 : : * that E |= lit in the theory.
760 : : */
761 : : virtual std::pair<bool, Node> entailmentCheck(TNode lit);
762 : :
763 : : /**
764 : : * Return true if this theory explains and propagates via central equality
765 : : * engine only when the theory uses the central equality engine.
766 : : */
767 : : static bool expUsingCentralEqualityEngine(TheoryId id);
768 : :
769 : : private:
770 : : // Disallow default construction, copy, assignment.
771 : : Theory() = delete;
772 : : Theory(const Theory&) = delete;
773 : : Theory& operator=(const Theory&) = delete;
774 : :
775 : : /**
776 : : * Returns the next assertion in the assertFact() queue.
777 : : *
778 : : * @return the next assertion in the assertFact() queue
779 : : */
780 : : Assertion get();
781 : :
782 : : /** An integer identifying the type of the theory. */
783 : : TheoryId d_id;
784 : :
785 : : /**
786 : : * The assertFact() queue.
787 : : *
788 : : * These can not be TNodes as some atoms (such as equalities) are sent
789 : : * across theories without being stored in a global map.
790 : : */
791 : : context::CDList<Assertion> d_facts;
792 : :
793 : : /** Index into the head of the facts list */
794 : : context::CDO<unsigned> d_factsHead;
795 : :
796 : : /** The care graph the theory will use during combination. */
797 : : CareGraph* d_careGraph;
798 : :
799 : : /** Pointer to the decision manager. */
800 : : DecisionManager* d_decManager;
801 : : }; /* class Theory */
802 : :
803 : : std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
804 : :
805 : : inline std::ostream& operator<<(std::ostream& out,
806 : : const cvc5::internal::theory::Theory& theory)
807 : : {
808 : : return out << theory.identify();
809 : : }
810 : :
811 : : } // namespace theory
812 : : } // namespace cvc5::internal
813 : :
814 : : #endif /* CVC5__THEORY__THEORY_H */
|
