1 /********************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Dejan Jovanovic, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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/logic_info.h"
43 #include "theory/output_channel.h"
44 #include "theory/theory_id.h"
45 #include "theory/theory_rewriter.h"
46 #include "theory/valuation.h"
47 #include "util/statistics_registry.h"
55 class QuantifiersEngine
;
57 class SubstitutionMap
;
60 class EntailmentCheckParameters
;
61 class EntailmentCheckSideEffects
;
64 class CandidateGenerator
;
65 }/* CVC4::theory::rrinst namespace */
69 }/* CVC4::theory::eq namespace */
72 * Base class for T-solvers. Abstract DPLL(T).
74 * This is essentially an interface class. The TheoryEngine has
75 * pointers to Theory. Note that only one specific Theory type (e.g.,
76 * TheoryUF) can exist per NodeManager, because of how the
77 * RegisteredAttr works. (If you need multiple instances of the same
78 * theory, you'll have to write a multiplexed theory that dispatches
85 friend class ::CVC4::TheoryEngine
;
87 // Disallow default construction, copy, assignment.
89 Theory(const Theory
&) = delete;
90 Theory
& operator=(const Theory
&) = delete;
92 /** An integer identifying the type of the theory. */
95 /** Name of this theory instance. Along with the TheoryId this should provide
96 * an unique string identifier for each instance of a Theory class. We need
97 * this to ensure unique statistics names over multiple theory instances. */
98 std::string d_instanceName
;
100 /** The SAT search context for the Theory. */
101 context::Context
* d_satContext
;
103 /** The user level assertion context for the Theory. */
104 context::UserContext
* d_userContext
;
106 /** Information about the logic we're operating within. */
107 const LogicInfo
& d_logicInfo
;
110 * The assertFact() queue.
112 * These can not be TNodes as some atoms (such as equalities) are sent
113 * across theories without being stored in a global map.
115 context::CDList
<Assertion
> d_facts
;
117 /** Index into the head of the facts list */
118 context::CDO
<unsigned> d_factsHead
;
120 /** Add shared term to the theory. */
121 void addSharedTermInternal(TNode node
);
123 /** Indices for splitting on the shared terms. */
124 context::CDO
<unsigned> d_sharedTermsIndex
;
126 /** The care graph the theory will use during combination. */
127 CareGraph
* d_careGraph
;
130 * Pointer to the quantifiers engine (or NULL, if quantifiers are not
131 * supported or not enabled). Not owned by the theory.
133 QuantifiersEngine
* d_quantEngine
;
135 /** Pointer to the decision manager. */
136 DecisionManager
* d_decManager
;
138 /** Extended theory module or NULL. Owned by the theory. */
139 ExtTheory
* d_extTheory
;
144 // === STATISTICS ===
145 /** time spent in check calls */
146 TimerStat d_checkTime
;
147 /** time spent in theory combination */
148 TimerStat d_computeCareGraphTime
;
151 * The only method to add suff to the care graph.
153 void addCarePair(TNode t1
, TNode t2
);
156 * The function should compute the care graph over the shared terms.
157 * The default function returns all the pairs among the shared variables.
159 virtual void computeCareGraph();
162 * A list of shared terms that the theory has.
164 context::CDList
<TNode
> d_sharedTerms
;
167 * Helper function for computeRelevantTerms
169 void collectTerms(TNode n
,
170 std::set
<Kind
>& irrKinds
,
171 std::set
<Node
>& termSet
) const;
174 * Scans the current set of assertions and shared terms top-down
175 * until a theory-leaf is reached, and adds all terms found to
176 * termSet. This is used by collectModelInfo to delimit the set of
177 * terms that should be used when constructing a model.
179 * irrKinds: The kinds of terms that appear in assertions that should *not*
180 * be included in termSet. Note that the kinds EQUAL and NOT are always
181 * treated as irrelevant kinds.
183 * includeShared: Whether to include shared terms in termSet. Notice that
184 * shared terms are not influenced by irrKinds.
186 void computeRelevantTerms(std::set
<Node
>& termSet
,
187 std::set
<Kind
>& irrKinds
,
188 bool includeShared
= true) const;
189 /** same as above, but with empty irrKinds */
190 void computeRelevantTerms(std::set
<Node
>& termSet
, bool includeShared
= true) const;
193 * Construct a Theory.
195 * The pair <id, instance> is assumed to uniquely identify this Theory
196 * w.r.t. the SmtEngine.
199 context::Context
* satContext
,
200 context::UserContext
* userContext
,
203 const LogicInfo
& logicInfo
,
204 std::string instance
= ""); // taking : No default.
207 * This is called at shutdown time by the TheoryEngine, just before
208 * destruction. It is important because there are destruction
209 * ordering issues between PropEngine and Theory (based on what
210 * hard-links to Nodes are outstanding). As the fact queue might be
211 * nonempty, we ensure here that it's clear. If you overload this,
212 * you must make an explicit call here to this->Theory::shutdown()
215 virtual void shutdown() { }
218 * The output channel for the Theory.
220 OutputChannel
* d_out
;
223 * The valuation proxy for the Theory to communicate back with the
224 * theory engine (and other theories).
226 Valuation d_valuation
;
229 * Whether proofs are enabled
232 bool d_proofsEnabled
;
235 * Returns the next assertion in the assertFact() queue.
237 * @return the next assertion in the assertFact() queue
239 inline Assertion
get();
241 const LogicInfo
& getLogicInfo() const {
246 * The theory that owns the uninterpreted sort.
248 static TheoryId s_uninterpretedSortOwner
;
250 void printFacts(std::ostream
& os
) const;
251 void debugPrintFacts() const;
256 * Return the ID of the theory responsible for the given type.
258 static inline TheoryId
theoryOf(TypeNode typeNode
) {
259 Trace("theory::internal") << "theoryOf(" << typeNode
<< ")" << std::endl
;
261 if (typeNode
.getKind() == kind::TYPE_CONSTANT
) {
262 id
= typeConstantToTheoryId(typeNode
.getConst
<TypeConstant
>());
264 id
= kindToTheoryId(typeNode
.getKind());
266 if (id
== THEORY_BUILTIN
) {
267 Trace("theory::internal") << "theoryOf(" << typeNode
<< ") == " << s_uninterpretedSortOwner
<< std::endl
;
268 return s_uninterpretedSortOwner
;
274 * Returns the ID of the theory responsible for the given node.
276 static TheoryId
theoryOf(options::TheoryOfMode mode
, TNode node
);
279 * Returns the ID of the theory responsible for the given node.
281 static inline TheoryId
theoryOf(TNode node
) {
282 return theoryOf(options::theoryOfMode(), node
);
286 * Set the owner of the uninterpreted sort.
288 static void setUninterpretedSortOwner(TheoryId theory
) {
289 s_uninterpretedSortOwner
= theory
;
293 * Get the owner of the uninterpreted sort.
295 static TheoryId
getUninterpretedSortOwner() {
296 return s_uninterpretedSortOwner
;
300 * Checks if the node is a leaf node of this theory
302 inline bool isLeaf(TNode node
) const {
303 return node
.getNumChildren() == 0 || theoryOf(node
) != d_id
;
307 * Checks if the node is a leaf node of a theory.
309 inline static bool isLeafOf(TNode node
, TheoryId theoryId
) {
310 return node
.getNumChildren() == 0 || theoryOf(node
) != theoryId
;
313 /** Returns true if the assertFact queue is empty*/
314 bool done() const { return d_factsHead
== d_facts
.size(); }
316 * Destructs a Theory.
321 * Creates a new theory rewriter for the theory.
323 virtual std::unique_ptr
<TheoryRewriter
> mkTheoryRewriter() = 0;
326 * Subclasses of Theory may add additional efforts. DO NOT CHECK
327 * equality with one of these values (e.g. if STANDARD xxx) but
328 * rather use range checks (or use the helper functions below).
329 * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
334 * Standard effort where theory need not do anything
336 EFFORT_STANDARD
= 50,
338 * Full effort requires the theory make sure its assertions are satisfiable or not
342 * Combination effort means that the individual theories are already satisfied, and
343 * it is time to put some effort into propagation of shared term equalities
345 EFFORT_COMBINATION
= 150,
347 * Last call effort, reserved for quantifiers.
349 EFFORT_LAST_CALL
= 200
352 static inline bool standardEffortOrMore(Effort e
) CVC4_CONST_FUNCTION
353 { return e
>= EFFORT_STANDARD
; }
354 static inline bool standardEffortOnly(Effort e
) CVC4_CONST_FUNCTION
355 { return e
>= EFFORT_STANDARD
&& e
< EFFORT_FULL
; }
356 static inline bool fullEffort(Effort e
) CVC4_CONST_FUNCTION
357 { return e
== EFFORT_FULL
; }
358 static inline bool combination(Effort e
) CVC4_CONST_FUNCTION
359 { return e
== EFFORT_COMBINATION
; }
362 * Get the id for this Theory.
364 TheoryId
getId() const {
369 * Get the SAT context associated to this Theory.
371 context::Context
* getSatContext() const {
376 * Get the context associated to this Theory.
378 context::UserContext
* getUserContext() const {
379 return d_userContext
;
383 * Set the output channel associated to this theory.
385 void setOutputChannel(OutputChannel
& out
) {
390 * Get the output channel associated to this theory.
392 OutputChannel
& getOutputChannel() {
397 * Get the valuation associated to this theory.
399 Valuation
& getValuation() {
404 * Get the quantifiers engine associated to this theory.
406 QuantifiersEngine
* getQuantifiersEngine() {
407 return d_quantEngine
;
411 * Get the quantifiers engine associated to this theory (const version).
413 const QuantifiersEngine
* getQuantifiersEngine() const {
414 return d_quantEngine
;
417 /** Get the decision manager associated to this theory. */
418 DecisionManager
* getDecisionManager() { return d_decManager
; }
421 * Finish theory initialization. At this point, options and the logic
422 * setting are final, and the master equality engine and quantifiers
423 * engine (if any) are initialized. This base class implementation
426 virtual void finishInit() { }
429 * Some theories have kinds that are effectively definitions and
430 * should be expanded before they are handled. Definitions allow
431 * a much wider range of actions than the normal forms given by the
432 * rewriter; they can enable other theories and create new terms.
433 * However no assumptions can be made about subterms having been
434 * expanded or rewritten. Where possible rewrite rules should be
435 * used, definitions should only be used when rewrites are not
436 * possible, for example in handling under-specified operations
437 * using partially defined functions.
439 * Some theories like sets use expandDefinition as a "context
440 * independent preRegisterTerm". This is required for cases where
441 * a theory wants to be notified about a term before preprocessing
442 * and simplification but doesn't necessarily want to rewrite it.
444 virtual Node
expandDefinition(LogicRequest
&logicRequest
, Node node
) {
445 // by default, do nothing
450 * Pre-register a term. Done one time for a Node per SAT context level.
452 virtual void preRegisterTerm(TNode
) { }
455 * Assert a fact in the current context.
457 void assertFact(TNode assertion
, bool isPreregistered
) {
458 Trace("theory") << "Theory<" << getId() << ">::assertFact["
459 << d_satContext
->getLevel() << "](" << assertion
<< ", "
460 << (isPreregistered
? "true" : "false") << ")" << std::endl
;
461 d_facts
.push_back(Assertion(assertion
, isPreregistered
));
465 * This method is called to notify a theory that the node n should
466 * be considered a "shared term" by this theory
468 virtual void addSharedTerm(TNode n
) { }
471 * Called to set the master equality engine.
473 virtual void setMasterEqualityEngine(eq::EqualityEngine
* eq
) { }
475 /** Called to set the quantifiers engine. */
476 void setQuantifiersEngine(QuantifiersEngine
* qe
);
477 /** Called to set the decision manager. */
478 void setDecisionManager(DecisionManager
* dm
);
480 /** Setup an ExtTheory module for this Theory. Can only be called once. */
481 void setupExtTheory();
484 * Return the current theory care graph. Theories should overload
485 * computeCareGraph to do the actual computation, and use addCarePair to add
486 * pairs to the care graph.
488 void getCareGraph(CareGraph
* careGraph
);
491 * Return the status of two terms in the current context. Should be
492 * implemented in sub-theories to enable more efficient theory-combination.
494 virtual EqualityStatus
getEqualityStatus(TNode a
, TNode b
) {
495 return EQUALITY_UNKNOWN
;
499 * Return the model value of the give shared term (or null if not available).
501 virtual Node
getModelValue(TNode var
) { return Node::null(); }
504 * Check the current assignment's consistency.
506 * An implementation of check() is required to either:
507 * - return a conflict on the output channel,
509 * - throw an exception
510 * - or call get() until done() is true.
512 virtual void check(Effort level
= EFFORT_FULL
) { }
514 /** Needs last effort check? */
515 virtual bool needsCheckLastEffort() { return false; }
517 /** T-propagate new literal assignments in the current context. */
518 virtual void propagate(Effort level
= EFFORT_FULL
) { }
521 * Return an explanation for the literal represented by parameter n
522 * (which was previously propagated by this theory).
524 virtual Node
explain(TNode n
) {
525 Unimplemented() << "Theory " << identify()
526 << " propagated a node but doesn't implement the "
527 "Theory::explain() interface!";
531 * Get all relevant information in this theory regarding the current
532 * model. This should be called after a call to check( FULL_EFFORT )
533 * for all theories with no conflicts and no lemmas added.
535 * This method returns true if and only if the equality engine of m is
536 * consistent as a result of this call.
538 virtual bool collectModelInfo(TheoryModel
* m
) { return true; }
539 /** if theories want to do something with model after building, do it here */
540 virtual void postProcessModel( TheoryModel
* m
){ }
542 * Statically learn from assertion "in," which has been asserted
543 * true at the top level. The theory should only add (via
544 * ::operator<< or ::append()) to the "learned" builder---it should
545 * *never* clear it. It is a conjunction to add to the formula at
546 * the top-level and may contain other theories' contributions.
548 virtual void ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) { }
550 enum PPAssertStatus
{
551 /** Atom has been solved */
552 PP_ASSERT_STATUS_SOLVED
,
553 /** Atom has not been solved */
554 PP_ASSERT_STATUS_UNSOLVED
,
555 /** Atom is inconsistent */
556 PP_ASSERT_STATUS_CONFLICT
560 * Given a literal, add the solved substitutions to the map, if any.
561 * The method should return true if the literal can be safely removed.
563 virtual PPAssertStatus
ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
);
566 * Given an atom of the theory coming from the input formula, this
567 * method can be overridden in a theory implementation to rewrite
568 * the atom into an equivalent form. This is only called just
569 * before an input atom to the engine.
571 virtual Node
ppRewrite(TNode atom
) { return atom
; }
574 * Notify preprocessed assertions. Called on new assertions after
575 * preprocessing before they are asserted to theory engine.
577 virtual void ppNotifyAssertions(const std::vector
<Node
>& assertions
) {}
580 * A Theory is called with presolve exactly one time per user
581 * check-sat. presolve() is called after preregistration,
582 * rewriting, and Boolean propagation, (other theories'
583 * propagation?), but the notified Theory has not yet had its
584 * check() or propagate() method called. A Theory may empty its
585 * assertFact() queue using get(). A Theory can raise conflicts,
586 * add lemmas, and propagate literals during presolve().
588 * NOTE: The presolve property must be added to the kinds file for
591 virtual void presolve() { }
594 * A Theory is called with postsolve exactly one time per user
595 * check-sat. postsolve() is called after the query has completed
596 * (regardless of whether sat, unsat, or unknown), and after any
597 * model-querying related to the query has been performed.
598 * After this call, the theory will not get another check() or
599 * propagate() call until presolve() is called again. A Theory
600 * cannot raise conflicts, add lemmas, or propagate literals during
603 virtual void postsolve() { }
606 * Notification sent to the theory wheneven the search restarts.
607 * Serves as a good time to do some clean-up work, and you can
608 * assume you're at DL 0 for the purposes of Contexts. This function
609 * should not use the output channel.
611 virtual void notifyRestart() { }
614 * Identify this theory (for debugging, dynamic configuration,
617 virtual std::string
identify() const = 0;
619 /** Set user attribute
620 * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
621 * via the syntax (! n :attr)
623 virtual void setUserAttribute(const std::string
& attr
, Node n
, std::vector
<Node
> node_values
, std::string str_value
) {
624 Unimplemented() << "Theory " << identify()
625 << " doesn't support Theory::setUserAttribute interface";
628 /** A set of theories */
629 typedef uint32_t Set
;
631 /** A set of all theories */
632 static const Set AllTheories
= (1 << theory::THEORY_LAST
) - 1;
634 /** Pops a first theory off the set */
635 static inline TheoryId
setPop(Set
& set
) {
636 uint32_t i
= ffs(set
); // Find First Set (bit)
637 if (i
== 0) { return THEORY_LAST
; }
638 TheoryId id
= (TheoryId
)(i
-1);
639 set
= setRemove(id
, set
);
643 /** Returns the size of a set of theories */
644 static inline size_t setSize(Set set
) {
646 while (setPop(set
) != THEORY_LAST
) {
652 /** Returns the index size of a set of theories */
653 static inline size_t setIndex(TheoryId id
, Set set
) {
654 Assert(setContains(id
, set
));
656 while (setPop(set
) != id
) {
662 /** Add the theory to the set. If no set specified, just returns a singleton set */
663 static inline Set
setInsert(TheoryId theory
, Set set
= 0) {
664 return set
| (1 << theory
);
667 /** Add the theory to the set. If no set specified, just returns a singleton set */
668 static inline Set
setRemove(TheoryId theory
, Set set
= 0) {
669 return setDifference(set
, setInsert(theory
));
672 /** Check if the set contains the theory */
673 static inline bool setContains(TheoryId theory
, Set set
) {
674 return set
& (1 << theory
);
677 static inline Set
setComplement(Set a
) {
678 return (~a
) & AllTheories
;
681 static inline Set
setIntersection(Set a
, Set b
) {
685 static inline Set
setUnion(Set a
, Set b
) {
690 static inline Set
setDifference(Set a
, Set b
) {
694 static inline std::string
setToString(theory::Theory::Set theorySet
) {
695 std::stringstream ss
;
697 for(unsigned theoryId
= 0; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
698 if (theory::Theory::setContains((theory::TheoryId
)theoryId
, theorySet
)) {
699 ss
<< (theory::TheoryId
) theoryId
<< " ";
706 typedef context::CDList
<Assertion
>::const_iterator assertions_iterator
;
709 * Provides access to the facts queue, primarily intended for theory
710 * debugging purposes.
712 * @return the iterator to the beginning of the fact queue
714 assertions_iterator
facts_begin() const {
715 return d_facts
.begin();
719 * Provides access to the facts queue, primarily intended for theory
720 * debugging purposes.
722 * @return the iterator to the end of the fact queue
724 assertions_iterator
facts_end() const {
725 return d_facts
.end();
728 * Whether facts have been asserted to this theory.
730 * @return true iff facts have been asserted to this theory.
733 return !d_facts
.empty();
736 /** Return total number of facts asserted to this theory */
737 size_t numAssertions() {
738 return d_facts
.size();
741 typedef context::CDList
<TNode
>::const_iterator shared_terms_iterator
;
744 * Provides access to the shared terms, primarily intended for theory
745 * debugging purposes.
747 * @return the iterator to the beginning of the shared terms list
749 shared_terms_iterator
shared_terms_begin() const {
750 return d_sharedTerms
.begin();
754 * Provides access to the facts queue, primarily intended for theory
755 * debugging purposes.
757 * @return the iterator to the end of the shared terms list
759 shared_terms_iterator
shared_terms_end() const {
760 return d_sharedTerms
.end();
765 * This is a utility function for constructing a copy of the currently shared terms
766 * in a queriable form. As this is
768 std::unordered_set
<TNode
, TNodeHashFunction
> currentlySharedTerms() const;
771 * This allows the theory to be queried for whether a literal, lit, is
772 * entailed by the theory. This returns a pair of a Boolean and a node E.
774 * If the Boolean is true, then E is a formula that entails lit and E is propositionally
775 * entailed by the assertions to the theory.
777 * If the Boolean is false, it is "unknown" if lit is entailed and E may be
780 * The literal lit is either an atom a or (not a), which must belong to the theory:
781 * There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
783 * There are NO assumptions that a or the subterms of a have been
784 * preprocessed in any form. This includes ppRewrite, rewriting,
785 * preregistering, registering, definition expansion or ITE removal!
787 * Theories are free to limit the amount of effort they use and so may
788 * always opt to return "unknown". Both "unknown" and "not entailed",
789 * may return for E a non-boolean Node (e.g. Node::null()). (There is no explicit output
790 * for the negation of lit is entailed.)
792 * If lit is theory valid, the return result may be the Boolean constant
795 * If lit is entailed by multiple assertions on the theory's getFact()
796 * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
797 * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
799 * If lit is entailed by a single assertion on the theory's getFact()
800 * queue, say a, this may return E=a.
802 * The theory may always return false!
804 * The search is controlled by the parameter params. For default behavior,
805 * this may be left NULL.
807 * Theories that want parameters extend the virtual EntailmentCheckParameters
808 * class. Users ask the theory for an appropriate subclass from the theory
809 * and configure that. How this is implemented is on a per theory basis.
811 * The search may provide additional output to guide the user of
812 * this function. This output is stored in a EntailmentCheckSideEffects*
813 * output parameter. The implementation of this is theory specific. For
814 * no output, this is NULL.
816 * Theories may not touch their output stream during an entailment check.
818 * @param lit a literal belonging to the theory.
819 * @param params the control parameters for the entailment check.
820 * @param out a theory specific output object of the entailment search.
821 * @return a pair <b,E> s.t. if b is true, then a formula E such that
822 * E |= lit in the theory.
824 virtual std::pair
<bool, Node
> entailmentCheck(
825 TNode lit
, const EntailmentCheckParameters
* params
= NULL
,
826 EntailmentCheckSideEffects
* out
= NULL
);
828 /* equality engine TODO: use? */
829 virtual eq::EqualityEngine
* getEqualityEngine() { return NULL
; }
831 /* Get extended theory if one has been installed. */
832 ExtTheory
* getExtTheory();
834 /* get current substitution at an effort
837 * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
839 virtual bool getCurrentSubstitution(int effort
, std::vector
<Node
>& vars
,
840 std::vector
<Node
>& subs
,
841 std::map
<Node
, std::vector
<Node
> >& exp
) {
845 /* is extended function reduced */
846 virtual bool isExtfReduced( int effort
, Node n
, Node on
, std::vector
< Node
>& exp
) { return n
.isConst(); }
849 * Get reduction for node
850 * If return value is not 0, then n is reduced.
851 * If return value <0 then n is reduced SAT-context-independently (e.g. by a
852 * lemma that persists at this user-context level).
853 * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
854 * and return value should be <0.
856 virtual int getReduction( int effort
, Node n
, Node
& nr
) { return 0; }
858 /** Turn on proof-production mode. */
859 void produceProofs() { d_proofsEnabled
= true; }
863 std::ostream
& operator<<(std::ostream
& os
, theory::Theory::Effort level
);
866 inline theory::Assertion
Theory::get() {
867 Assert(!done()) << "Theory::get() called with assertion queue empty!";
870 Assertion fact
= d_facts
[d_factsHead
];
871 d_factsHead
= d_factsHead
+ 1;
873 Trace("theory") << "Theory::get() => " << fact
<< " (" << d_facts
.size() - d_factsHead
<< " left)" << std::endl
;
875 if(Dump
.isOn("state")) {
876 Dump("state") << AssertCommand(fact
.d_assertion
.toExpr());
882 inline std::ostream
& operator<<(std::ostream
& out
,
883 const CVC4::theory::Theory
& theory
) {
884 return out
<< theory
.identify();
887 inline std::ostream
& operator << (std::ostream
& out
, theory::Theory::PPAssertStatus status
) {
889 case theory::Theory::PP_ASSERT_STATUS_SOLVED
:
890 out
<< "SOLVE_STATUS_SOLVED"; break;
891 case theory::Theory::PP_ASSERT_STATUS_UNSOLVED
:
892 out
<< "SOLVE_STATUS_UNSOLVED"; break;
893 case theory::Theory::PP_ASSERT_STATUS_CONFLICT
:
894 out
<< "SOLVE_STATUS_CONFLICT"; break;
901 class EntailmentCheckParameters
{
905 EntailmentCheckParameters(TheoryId tid
);
907 TheoryId
getTheoryId() const;
908 virtual ~EntailmentCheckParameters();
909 };/* class EntailmentCheckParameters */
911 class EntailmentCheckSideEffects
{
915 EntailmentCheckSideEffects(TheoryId tid
);
917 TheoryId
getTheoryId() const;
918 virtual ~EntailmentCheckSideEffects();
919 };/* class EntailmentCheckSideEffects */
921 }/* CVC4::theory namespace */
922 }/* CVC4 namespace */
924 #endif /* CVC4__THEORY__THEORY_H */