1 /********************* */
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Base of the theory interface.
14 ** Base of the theory interface.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__THEORY_H
20 #define CVC4__THEORY__THEORY_H
26 #include <unordered_set>
28 #include "context/cdhashset.h"
29 #include "context/cdlist.h"
30 #include "context/cdo.h"
31 #include "context/context.h"
32 #include "expr/node.h"
34 #include "options/options.h"
35 #include "options/theory_options.h"
36 #include "smt/command.h"
38 #include "smt/logic_request.h"
39 #include "theory/assertion.h"
40 #include "theory/care_graph.h"
41 #include "theory/decision_manager.h"
42 #include "theory/ee_setup_info.h"
43 #include "theory/logic_info.h"
44 #include "theory/output_channel.h"
45 #include "theory/theory_id.h"
46 #include "theory/theory_rewriter.h"
47 #include "theory/theory_state.h"
48 #include "theory/trust_node.h"
49 #include "theory/valuation.h"
50 #include "util/statistics_registry.h"
55 class ProofNodeManager
;
59 class QuantifiersEngine
;
61 class SubstitutionMap
;
65 class CandidateGenerator
;
66 }/* CVC4::theory::rrinst namespace */
70 }/* CVC4::theory::eq namespace */
73 * Base class for T-solvers. Abstract DPLL(T).
75 * This is essentially an interface class. The TheoryEngine has
76 * pointers to Theory. Note that only one specific Theory type (e.g.,
77 * TheoryUF) can exist per NodeManager, because of how the
78 * RegisteredAttr works. (If you need multiple instances of the same
79 * theory, you'll have to write a multiplexed theory that dispatches
82 * NOTE: A Theory has a special way of being initialized. The owner of a Theory
85 * (A) Using Theory as a standalone object, not associated with a TheoryEngine.
86 * In this case, simply call the public initialization method
87 * (Theory::finishInitStandalone).
89 * (B) TheoryEngine, which determines how the Theory acts in accordance with
90 * its theory combination policy. We require the following steps in order:
91 * (B.1) Get information about whether the theory wishes to use an equality
92 * eninge, and more specifically which equality engine notifications the Theory
93 * would like to be notified of (Theory::needsEqualityEngine).
94 * (B.2) Set the equality engine of the theory (Theory::setEqualityEngine),
95 * which we refer to as the "official equality engine" of this Theory. The
96 * equality engine passed to the theory must respect the contract(s) specified
97 * by the equality engine setup information (EeSetupInfo) returned in the
99 * (B.3) Set the other required utilities including setQuantifiersEngine and
100 * setDecisionManager.
101 * (B.4) Call the private initialization method (Theory::finishInit).
103 * Initialization of the second form happens during TheoryEngine::finishInit,
104 * after the quantifiers engine and model objects have been set up.
107 friend class ::CVC4::TheoryEngine
;
110 // Disallow default construction, copy, assignment.
112 Theory(const Theory
&) = delete;
113 Theory
& operator=(const Theory
&) = delete;
115 /** An integer identifying the type of the theory. */
118 /** The SAT search context for the Theory. */
119 context::Context
* d_satContext
;
121 /** The user level assertion context for the Theory. */
122 context::UserContext
* d_userContext
;
124 /** Information about the logic we're operating within. */
125 const LogicInfo
& d_logicInfo
;
127 /** Pointer to proof node manager */
128 ProofNodeManager
* d_pnm
;
131 * The assertFact() queue.
133 * These can not be TNodes as some atoms (such as equalities) are sent
134 * across theories without being stored in a global map.
136 context::CDList
<Assertion
> d_facts
;
138 /** Index into the head of the facts list */
139 context::CDO
<unsigned> d_factsHead
;
141 /** Indices for splitting on the shared terms. */
142 context::CDO
<unsigned> d_sharedTermsIndex
;
144 /** The care graph the theory will use during combination. */
145 CareGraph
* d_careGraph
;
148 * Pointer to the quantifiers engine (or NULL, if quantifiers are not
149 * supported or not enabled). Not owned by the theory.
151 QuantifiersEngine
* d_quantEngine
;
153 /** Pointer to the decision manager. */
154 DecisionManager
* d_decManager
;
157 /** Name of this theory instance. Along with the TheoryId this should provide
158 * an unique string identifier for each instance of a Theory class. We need
159 * this to ensure unique statistics names over multiple theory instances. */
160 std::string d_instanceName
;
162 // === STATISTICS ===
163 /** time spent in check calls */
164 TimerStat d_checkTime
;
165 /** time spent in theory combination */
166 TimerStat d_computeCareGraphTime
;
169 * The only method to add suff to the care graph.
171 void addCarePair(TNode t1
, TNode t2
);
174 * The function should compute the care graph over the shared terms.
175 * The default function returns all the pairs among the shared variables.
177 virtual void computeCareGraph();
180 * A list of shared terms that the theory has.
182 context::CDList
<TNode
> d_sharedTerms
;
184 //---------------------------------- private collect model info
186 * Scans the current set of assertions and shared terms top-down
187 * until a theory-leaf is reached, and adds all terms found to
188 * termSet. This is used by collectModelInfo to delimit the set of
189 * terms that should be used when constructing a model.
191 * irrKinds: The kinds of terms that appear in assertions that should *not*
192 * be included in termSet. Note that the kinds EQUAL and NOT are always
193 * treated as irrelevant kinds.
195 * includeShared: Whether to include shared terms in termSet. Notice that
196 * shared terms are not influenced by irrKinds.
198 void computeRelevantTermsInternal(std::set
<Node
>& termSet
,
199 std::set
<Kind
>& irrKinds
,
200 bool includeShared
= true) const;
202 * Helper function for computeRelevantTerms
204 void collectTerms(TNode n
,
205 std::set
<Kind
>& irrKinds
,
206 std::set
<Node
>& termSet
) const;
207 //---------------------------------- end private collect model info
210 * Construct a Theory.
212 * The pair <id, instance> is assumed to uniquely identify this Theory
213 * w.r.t. the SmtEngine.
216 context::Context
* satContext
,
217 context::UserContext
* userContext
,
220 const LogicInfo
& logicInfo
,
221 ProofNodeManager
* pnm
,
222 std::string instance
= ""); // taking : No default.
225 * This is called at shutdown time by the TheoryEngine, just before
226 * destruction. It is important because there are destruction
227 * ordering issues between PropEngine and Theory (based on what
228 * hard-links to Nodes are outstanding). As the fact queue might be
229 * nonempty, we ensure here that it's clear. If you overload this,
230 * you must make an explicit call here to this->Theory::shutdown()
233 virtual void shutdown() { }
236 * The output channel for the Theory.
238 OutputChannel
* d_out
;
241 * The valuation proxy for the Theory to communicate back with the
242 * theory engine (and other theories).
244 Valuation d_valuation
;
246 * Pointer to the official equality engine of this theory, which is owned by
247 * the equality engine manager of TheoryEngine.
249 eq::EqualityEngine
* d_equalityEngine
;
251 * The official equality engine, if we allocated it.
253 std::unique_ptr
<eq::EqualityEngine
> d_allocEqualityEngine
;
255 * The theory state, which contains contexts, valuation, and equality engine.
256 * Notice the theory is responsible for memory management of this class.
258 TheoryState
* d_theoryState
;
260 * Whether proofs are enabled
263 bool d_proofsEnabled
;
266 * Returns the next assertion in the assertFact() queue.
268 * @return the next assertion in the assertFact() queue
270 inline Assertion
get();
272 const LogicInfo
& getLogicInfo() const {
277 * The theory that owns the uninterpreted sort.
279 static TheoryId s_uninterpretedSortOwner
;
281 void printFacts(std::ostream
& os
) const;
282 void debugPrintFacts() const;
284 /** is legal elimination
286 * Returns true if x -> val is a legal elimination of variable x. This is
287 * useful for ppAssert, when x = val is an entailed equality. This function
288 * determines whether indeed x can be eliminated from the problem via the
289 * substituion x -> val.
291 * The following criteria imply that x -> val is *not* a legal elimination:
292 * (1) If x is contained in val,
293 * (2) If the type of val is not a subtype of the type of x,
294 * (3) If val contains an operator that cannot be evaluated, and produceModels
295 * is true. For example, x -> sqrt(2) is not a legal elimination if we
296 * are producing models. This is because we care about the value of x, and
297 * its value must be computed (approximated) by the non-linear solver.
299 bool isLegalElimination(TNode x
, TNode val
);
300 //--------------------------------- private initialization
302 * Called to set the official equality engine. This should be done by
305 void setEqualityEngine(eq::EqualityEngine
* ee
);
306 /** Called to set the quantifiers engine. */
307 void setQuantifiersEngine(QuantifiersEngine
* qe
);
308 /** Called to set the decision manager. */
309 void setDecisionManager(DecisionManager
* dm
);
311 * Finish theory initialization. At this point, options and the logic
312 * setting are final, the master equality engine and quantifiers
313 * engine (if any) are initialized, and the official equality engine of this
314 * theory has been assigned. This base class implementation
315 * does nothing. This should be called by TheoryEngine only.
317 virtual void finishInit() {}
318 //--------------------------------- end private initialization
321 * This method is called to notify a theory that the node n should
322 * be considered a "shared term" by this theory. This does anything
323 * theory-specific concerning the fact that n is now marked as a shared
324 * term, which is done in addition to explicitly storing n as a shared
325 * term and adding it as a trigger term in the equality engine of this
326 * class (see addSharedTerm).
328 virtual void notifySharedTerm(TNode n
);
331 //--------------------------------- initialization
333 * @return The theory rewriter associated with this theory.
335 virtual TheoryRewriter
* getTheoryRewriter() = 0;
337 * Returns true if this theory needs an equality engine for checking
340 * If this method returns true, then the equality engine manager will
341 * initialize its equality engine field via setEqualityEngine above during
342 * TheoryEngine::finishInit, prior to calling finishInit for this theory.
344 * Additionally, if this method returns true, then this method is required to
345 * update the argument esi with instructions for initializing and setting up
346 * notifications from its equality engine, which is commonly done with
347 * a notifications class (eq::EqualityEngineNotify).
349 virtual bool needsEqualityEngine(EeSetupInfo
& esi
);
351 * Finish theory initialization, standalone version. This is used to
352 * initialize this class if it is not associated with a theory engine.
353 * This allocates the official equality engine of this Theory and then
354 * calls the finishInit method above.
356 void finishInitStandalone();
357 //--------------------------------- end initialization
360 * Return the ID of the theory responsible for the given type.
362 static inline TheoryId
theoryOf(TypeNode typeNode
) {
363 Trace("theory::internal") << "theoryOf(" << typeNode
<< ")" << std::endl
;
365 if (typeNode
.getKind() == kind::TYPE_CONSTANT
) {
366 id
= typeConstantToTheoryId(typeNode
.getConst
<TypeConstant
>());
368 id
= kindToTheoryId(typeNode
.getKind());
370 if (id
== THEORY_BUILTIN
) {
371 Trace("theory::internal") << "theoryOf(" << typeNode
<< ") == " << s_uninterpretedSortOwner
<< std::endl
;
372 return s_uninterpretedSortOwner
;
378 * Returns the ID of the theory responsible for the given node.
380 static TheoryId
theoryOf(options::TheoryOfMode mode
, TNode node
);
383 * Returns the ID of the theory responsible for the given node.
385 static inline TheoryId
theoryOf(TNode node
) {
386 return theoryOf(options::theoryOfMode(), node
);
390 * Set the owner of the uninterpreted sort.
392 static void setUninterpretedSortOwner(TheoryId theory
) {
393 s_uninterpretedSortOwner
= theory
;
397 * Get the owner of the uninterpreted sort.
399 static TheoryId
getUninterpretedSortOwner() {
400 return s_uninterpretedSortOwner
;
404 * Checks if the node is a leaf node of this theory
406 inline bool isLeaf(TNode node
) const {
407 return node
.getNumChildren() == 0 || theoryOf(node
) != d_id
;
411 * Checks if the node is a leaf node of a theory.
413 inline static bool isLeafOf(TNode node
, TheoryId theoryId
) {
414 return node
.getNumChildren() == 0 || theoryOf(node
) != theoryId
;
417 /** Returns true if the assertFact queue is empty*/
418 bool done() const { return d_factsHead
== d_facts
.size(); }
420 * Destructs a Theory.
425 * Subclasses of Theory may add additional efforts. DO NOT CHECK
426 * equality with one of these values (e.g. if STANDARD xxx) but
427 * rather use range checks (or use the helper functions below).
428 * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
434 * Standard effort where theory need not do anything
436 EFFORT_STANDARD
= 50,
438 * Full effort requires the theory make sure its assertions are satisfiable
443 * Last call effort, called after theory combination has completed with
444 * no lemmas and a model is available.
446 EFFORT_LAST_CALL
= 200
449 static inline bool standardEffortOrMore(Effort e
) CVC4_CONST_FUNCTION
450 { return e
>= EFFORT_STANDARD
; }
451 static inline bool standardEffortOnly(Effort e
) CVC4_CONST_FUNCTION
452 { return e
>= EFFORT_STANDARD
&& e
< EFFORT_FULL
; }
453 static inline bool fullEffort(Effort e
) CVC4_CONST_FUNCTION
454 { return e
== EFFORT_FULL
; }
457 * Get the id for this Theory.
459 TheoryId
getId() const {
464 * Get the SAT context associated to this Theory.
466 context::Context
* getSatContext() const {
471 * Get the context associated to this Theory.
473 context::UserContext
* getUserContext() const {
474 return d_userContext
;
478 * Set the output channel associated to this theory.
480 void setOutputChannel(OutputChannel
& out
) {
485 * Get the output channel associated to this theory.
487 OutputChannel
& getOutputChannel() {
492 * Get the valuation associated to this theory.
494 Valuation
& getValuation() {
498 /** Get the equality engine being used by this theory. */
499 eq::EqualityEngine
* getEqualityEngine();
502 * Get the quantifiers engine associated to this theory.
504 QuantifiersEngine
* getQuantifiersEngine() {
505 return d_quantEngine
;
508 /** Get the decision manager associated to this theory. */
509 DecisionManager
* getDecisionManager() { return d_decManager
; }
512 * Expand definitions in the term node. This returns a term that is
513 * equivalent to node. It wraps this term in a TrustNode of kind
514 * TrustNodeKind::REWRITE. If node is unchanged by this method, the
515 * null TrustNode may be returned. This is an optimization to avoid
516 * constructing the trivial equality (= node node) internally within
519 * The purpose of this method is typically to eliminate the operators in node
520 * that are syntax sugar that cannot otherwise be eliminated during rewriting.
521 * For example, division relies on the introduction of an uninterpreted
522 * function for the divide-by-zero case, which we do not introduce with
523 * the rewriter, since this function may be cached in a non-global fashion.
525 * Some theories have kinds that are effectively definitions and should be
526 * expanded before they are handled. Definitions allow a much wider range of
527 * actions than the normal forms given by the rewriter. However no
528 * assumptions can be made about subterms having been expanded or rewritten.
529 * Where possible rewrite rules should be used, definitions should only be
530 * used when rewrites are not possible, for example in handling
531 * under-specified operations using partially defined functions.
533 * Some theories like sets use expandDefinition as a "context
534 * independent preRegisterTerm". This is required for cases where
535 * a theory wants to be notified about a term before preprocessing
536 * and simplification but doesn't necessarily want to rewrite it.
538 virtual TrustNode
expandDefinition(Node node
)
540 // by default, do nothing
541 return TrustNode::null();
545 * Pre-register a term. Done one time for a Node per SAT context level.
547 virtual void preRegisterTerm(TNode
);
550 * Assert a fact in the current context.
552 void assertFact(TNode assertion
, bool isPreregistered
) {
553 Trace("theory") << "Theory<" << getId() << ">::assertFact["
554 << d_satContext
->getLevel() << "](" << assertion
<< ", "
555 << (isPreregistered
? "true" : "false") << ")" << std::endl
;
556 d_facts
.push_back(Assertion(assertion
, isPreregistered
));
559 /** Add shared term to the theory. */
560 void addSharedTerm(TNode node
);
563 * Return the current theory care graph. Theories should overload
564 * computeCareGraph to do the actual computation, and use addCarePair to add
565 * pairs to the care graph.
567 void getCareGraph(CareGraph
* careGraph
);
570 * Return the status of two terms in the current context. Should be
571 * implemented in sub-theories to enable more efficient theory-combination.
573 virtual EqualityStatus
getEqualityStatus(TNode a
, TNode b
);
576 * Return the model value of the give shared term (or null if not available).
578 * TODO (project #39): this method is likely to become deprecated.
580 virtual Node
getModelValue(TNode var
) { return Node::null(); }
582 /** T-propagate new literal assignments in the current context. */
583 virtual void propagate(Effort level
= EFFORT_FULL
) {}
586 * Return an explanation for the literal represented by parameter n
587 * (which was previously propagated by this theory).
589 virtual TrustNode
explain(TNode n
)
591 Unimplemented() << "Theory " << identify()
592 << " propagated a node but doesn't implement the "
593 "Theory::explain() interface!";
596 //--------------------------------- check
598 * Does this theory wish to be called to check at last call effort? This is
599 * the case for any theory that wishes to run when a model is available.
601 virtual bool needsCheckLastEffort() { return false; }
603 * Check the current assignment's consistency.
605 * An implementation of check() is required to either:
606 * - return a conflict on the output channel,
608 * - throw an exception
609 * - or call get() until done() is true.
611 * The standard method for check consists of a loop that processes the entire
612 * fact queue when preCheck returns false. It makes four theory-specific
613 * callbacks, (preCheck, postCheck, preNotifyFact, notifyFact) as described
614 * below. It asserts each fact to the official equality engine when
615 * preNotifyFact returns false.
617 * Theories that use this check method must use an official theory
618 * state object (d_theoryState).
620 * TODO (project #39): this method should be non-virtual, once all theories
621 * conform to the new standard
623 virtual void check(Effort level
= EFFORT_FULL
);
625 * Pre-check, called before the fact queue of the theory is processed.
626 * If this method returns false, then the theory will process its fact
627 * queue. If this method returns true, then the theory has indicated
628 * its check method should finish immediately.
630 virtual bool preCheck(Effort level
= EFFORT_FULL
);
632 * Post-check, called after the fact queue of the theory is processed.
634 virtual void postCheck(Effort level
= EFFORT_FULL
);
636 * Pre-notify fact, return true if the theory processed it. If this
637 * method returns false, then the atom will be added to the equality engine
638 * of the theory and notifyFact will be called with isInternal=false.
640 * Theories that implement check but do not use official equality
641 * engines should always return true for this method.
643 * @param atom The atom
644 * @param polarity Its polarity
645 * @param fact The original literal that was asserted
646 * @param isPrereg Whether the assertion is preregistered
647 * @param isInternal Whether the origin of the fact was internal. If this
648 * is false, the fact was asserted via the fact queue of the theory.
649 * @return true if the theory completely processed this fact, i.e. it does
650 * not need to assert the fact to its equality engine.
652 virtual bool preNotifyFact(
653 TNode atom
, bool pol
, TNode fact
, bool isPrereg
, bool isInternal
);
655 * Notify fact, called immediately after the fact was pushed into the
658 * @param atom The atom
659 * @param polarity Its polarity
660 * @param fact The original literal that was asserted.
661 * @param isInternal Whether the origin of the fact was internal. If this
662 * is false, the fact was asserted via the fact queue of the theory.
664 virtual void notifyFact(TNode atom
, bool pol
, TNode fact
, bool isInternal
);
665 //--------------------------------- end check
667 //--------------------------------- collect model info
669 * Get all relevant information in this theory regarding the current
670 * model. This should be called after a call to check( FULL_EFFORT )
671 * for all theories with no conflicts and no lemmas added.
673 * This method returns true if and only if the equality engine of m is
674 * consistent as a result of this call.
676 * The standard method for collectModelInfo computes the relevant terms,
677 * asserts the theory's equality engine to the model (if necessary) and
678 * then calls computeModelValues.
680 * TODO (project #39): this method should be non-virtual, once all theories
681 * conform to the new standard
683 virtual bool collectModelInfo(TheoryModel
* m
);
685 * Same as above, but with empty irrKinds. This version can be overridden
686 * by the theory, e.g. by restricting or extending the set of terms returned
687 * by computeRelevantTermsInternal, which is called by default with no
690 virtual void computeRelevantTerms(std::set
<Node
>& termSet
,
691 bool includeShared
= true);
693 * Collect model values, after equality information is added to the model.
694 * The argument termSet is the set of relevant terms returned by
695 * computeRelevantTerms.
697 virtual bool collectModelValues(TheoryModel
* m
,
698 const std::set
<Node
>& termSet
);
699 /** if theories want to do something with model after building, do it here */
700 virtual void postProcessModel( TheoryModel
* m
){ }
701 //--------------------------------- end collect model info
703 //--------------------------------- preprocessing
705 * Statically learn from assertion "in," which has been asserted
706 * true at the top level. The theory should only add (via
707 * ::operator<< or ::append()) to the "learned" builder---it should
708 * *never* clear it. It is a conjunction to add to the formula at
709 * the top-level and may contain other theories' contributions.
711 virtual void ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) { }
713 enum PPAssertStatus
{
714 /** Atom has been solved */
715 PP_ASSERT_STATUS_SOLVED
,
716 /** Atom has not been solved */
717 PP_ASSERT_STATUS_UNSOLVED
,
718 /** Atom is inconsistent */
719 PP_ASSERT_STATUS_CONFLICT
723 * Given a literal, add the solved substitutions to the map, if any.
724 * The method should return true if the literal can be safely removed.
726 virtual PPAssertStatus
ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
);
729 * Given an atom of the theory coming from the input formula, this
730 * method can be overridden in a theory implementation to rewrite
731 * the atom into an equivalent form. This is only called just
732 * before an input atom to the engine. This method returns a TrustNode of
733 * kind TrustNodeKind::REWRITE, which carries information about the proof
734 * generator for the rewrite. Similarly to expandDefinition, this method may
735 * return the null TrustNode if atom is unchanged.
737 virtual TrustNode
ppRewrite(TNode atom
) { return TrustNode::null(); }
740 * Notify preprocessed assertions. Called on new assertions after
741 * preprocessing before they are asserted to theory engine.
743 virtual void ppNotifyAssertions(const std::vector
<Node
>& assertions
) {}
744 //--------------------------------- end preprocessing
747 * A Theory is called with presolve exactly one time per user
748 * check-sat. presolve() is called after preregistration,
749 * rewriting, and Boolean propagation, (other theories'
750 * propagation?), but the notified Theory has not yet had its
751 * check() or propagate() method called. A Theory may empty its
752 * assertFact() queue using get(). A Theory can raise conflicts,
753 * add lemmas, and propagate literals during presolve().
755 * NOTE: The presolve property must be added to the kinds file for
758 virtual void presolve() { }
761 * A Theory is called with postsolve exactly one time per user
762 * check-sat. postsolve() is called after the query has completed
763 * (regardless of whether sat, unsat, or unknown), and after any
764 * model-querying related to the query has been performed.
765 * After this call, the theory will not get another check() or
766 * propagate() call until presolve() is called again. A Theory
767 * cannot raise conflicts, add lemmas, or propagate literals during
770 virtual void postsolve() { }
773 * Notification sent to the theory wheneven the search restarts.
774 * Serves as a good time to do some clean-up work, and you can
775 * assume you're at DL 0 for the purposes of Contexts. This function
776 * should not use the output channel.
778 virtual void notifyRestart() { }
781 * Identify this theory (for debugging, dynamic configuration,
784 virtual std::string
identify() const = 0;
786 /** Set user attribute
787 * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
788 * via the syntax (! n :attr)
790 virtual void setUserAttribute(const std::string
& attr
, Node n
, std::vector
<Node
> node_values
, std::string str_value
) {
791 Unimplemented() << "Theory " << identify()
792 << " doesn't support Theory::setUserAttribute interface";
795 /** A set of theories */
796 typedef uint32_t Set
;
798 /** A set of all theories */
799 static const Set AllTheories
= (1 << theory::THEORY_LAST
) - 1;
801 /** Pops a first theory off the set */
802 static inline TheoryId
setPop(Set
& set
) {
803 uint32_t i
= ffs(set
); // Find First Set (bit)
804 if (i
== 0) { return THEORY_LAST
; }
805 TheoryId id
= (TheoryId
)(i
-1);
806 set
= setRemove(id
, set
);
810 /** Returns the size of a set of theories */
811 static inline size_t setSize(Set set
) {
813 while (setPop(set
) != THEORY_LAST
) {
819 /** Returns the index size of a set of theories */
820 static inline size_t setIndex(TheoryId id
, Set set
) {
821 Assert(setContains(id
, set
));
823 while (setPop(set
) != id
) {
829 /** Add the theory to the set. If no set specified, just returns a singleton set */
830 static inline Set
setInsert(TheoryId theory
, Set set
= 0) {
831 return set
| (1 << theory
);
834 /** Add the theory to the set. If no set specified, just returns a singleton set */
835 static inline Set
setRemove(TheoryId theory
, Set set
= 0) {
836 return setDifference(set
, setInsert(theory
));
839 /** Check if the set contains the theory */
840 static inline bool setContains(TheoryId theory
, Set set
) {
841 return set
& (1 << theory
);
844 static inline Set
setComplement(Set a
) {
845 return (~a
) & AllTheories
;
848 static inline Set
setIntersection(Set a
, Set b
) {
852 static inline Set
setUnion(Set a
, Set b
) {
857 static inline Set
setDifference(Set a
, Set b
) {
861 static inline std::string
setToString(theory::Theory::Set theorySet
) {
862 std::stringstream ss
;
864 for(unsigned theoryId
= 0; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
865 if (theory::Theory::setContains((theory::TheoryId
)theoryId
, theorySet
)) {
866 ss
<< (theory::TheoryId
) theoryId
<< " ";
873 typedef context::CDList
<Assertion
>::const_iterator assertions_iterator
;
876 * Provides access to the facts queue, primarily intended for theory
877 * debugging purposes.
879 * @return the iterator to the beginning of the fact queue
881 assertions_iterator
facts_begin() const {
882 return d_facts
.begin();
886 * Provides access to the facts queue, primarily intended for theory
887 * debugging purposes.
889 * @return the iterator to the end of the fact queue
891 assertions_iterator
facts_end() const {
892 return d_facts
.end();
895 * Whether facts have been asserted to this theory.
897 * @return true iff facts have been asserted to this theory.
900 return !d_facts
.empty();
903 /** Return total number of facts asserted to this theory */
904 size_t numAssertions() {
905 return d_facts
.size();
908 typedef context::CDList
<TNode
>::const_iterator shared_terms_iterator
;
911 * Provides access to the shared terms, primarily intended for theory
912 * debugging purposes.
914 * @return the iterator to the beginning of the shared terms list
916 shared_terms_iterator
shared_terms_begin() const {
917 return d_sharedTerms
.begin();
921 * Provides access to the facts queue, primarily intended for theory
922 * debugging purposes.
924 * @return the iterator to the end of the shared terms list
926 shared_terms_iterator
shared_terms_end() const {
927 return d_sharedTerms
.end();
932 * This is a utility function for constructing a copy of the currently shared terms
933 * in a queriable form. As this is
935 std::unordered_set
<TNode
, TNodeHashFunction
> currentlySharedTerms() const;
938 * This allows the theory to be queried for whether a literal, lit, is
939 * entailed by the theory. This returns a pair of a Boolean and a node E.
941 * If the Boolean is true, then E is a formula that entails lit and E is propositionally
942 * entailed by the assertions to the theory.
944 * If the Boolean is false, it is "unknown" if lit is entailed and E may be
947 * The literal lit is either an atom a or (not a), which must belong to the theory:
948 * There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
950 * There are NO assumptions that a or the subterms of a have been
951 * preprocessed in any form. This includes ppRewrite, rewriting,
952 * preregistering, registering, definition expansion or ITE removal!
954 * Theories are free to limit the amount of effort they use and so may
955 * always opt to return "unknown". Both "unknown" and "not entailed",
956 * may return for E a non-boolean Node (e.g. Node::null()). (There is no explicit output
957 * for the negation of lit is entailed.)
959 * If lit is theory valid, the return result may be the Boolean constant
962 * If lit is entailed by multiple assertions on the theory's getFact()
963 * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
964 * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
966 * If lit is entailed by a single assertion on the theory's getFact()
967 * queue, say a, this may return E=a.
969 * The theory may always return false!
971 * Theories may not touch their output stream during an entailment check.
973 * @param lit a literal belonging to the theory.
974 * @return a pair <b,E> s.t. if b is true, then a formula E such that
975 * E |= lit in the theory.
977 virtual std::pair
<bool, Node
> entailmentCheck(TNode lit
);
979 /* get current substitution at an effort
982 * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
984 virtual bool getCurrentSubstitution(int effort
, std::vector
<Node
>& vars
,
985 std::vector
<Node
>& subs
,
986 std::map
<Node
, std::vector
<Node
> >& exp
) {
990 /* is extended function reduced */
991 virtual bool isExtfReduced( int effort
, Node n
, Node on
, std::vector
< Node
>& exp
) { return n
.isConst(); }
994 * Get reduction for node
995 * If return value is not 0, then n is reduced.
996 * If return value <0 then n is reduced SAT-context-independently (e.g. by a
997 * lemma that persists at this user-context level).
998 * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
999 * and return value should be <0.
1001 virtual int getReduction( int effort
, Node n
, Node
& nr
) { return 0; }
1003 /** Turn on proof-production mode. */
1004 void produceProofs() { d_proofsEnabled
= true; }
1005 };/* class Theory */
1007 std::ostream
& operator<<(std::ostream
& os
, theory::Theory::Effort level
);
1010 inline theory::Assertion
Theory::get() {
1011 Assert(!done()) << "Theory::get() called with assertion queue empty!";
1013 // Get the assertion
1014 Assertion fact
= d_facts
[d_factsHead
];
1015 d_factsHead
= d_factsHead
+ 1;
1017 Trace("theory") << "Theory::get() => " << fact
<< " (" << d_facts
.size() - d_factsHead
<< " left)" << std::endl
;
1019 if(Dump
.isOn("state")) {
1020 Dump("state") << AssertCommand(fact
.d_assertion
.toExpr());
1026 inline std::ostream
& operator<<(std::ostream
& out
,
1027 const CVC4::theory::Theory
& theory
) {
1028 return out
<< theory
.identify();
1031 inline std::ostream
& operator << (std::ostream
& out
, theory::Theory::PPAssertStatus status
) {
1033 case theory::Theory::PP_ASSERT_STATUS_SOLVED
:
1034 out
<< "SOLVE_STATUS_SOLVED"; break;
1035 case theory::Theory::PP_ASSERT_STATUS_UNSOLVED
:
1036 out
<< "SOLVE_STATUS_UNSOLVED"; break;
1037 case theory::Theory::PP_ASSERT_STATUS_CONFLICT
:
1038 out
<< "SOLVE_STATUS_CONFLICT"; break;
1045 }/* CVC4::theory namespace */
1046 }/* CVC4 namespace */
1048 #endif /* CVC4__THEORY__THEORY_H */