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