1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: Tim King, Dejan Jovanovic
6 ** Minor contributors (to current version): Francois Bobot, Kshitij Bansal, Martin Brain <>, Clark Barrett, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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
22 #include "expr/node.h"
23 //#include "expr/attribute.h"
24 #include "expr/command.h"
25 #include "smt/logic_request.h"
26 #include "theory/valuation.h"
27 #include "theory/output_channel.h"
28 #include "theory/logic_info.h"
29 #include "theory/options.h"
30 #include "theory/theoryof_mode.h"
31 #include "context/context.h"
32 #include "context/cdlist.h"
33 #include "context/cdo.h"
34 #include "options/options.h"
35 #include "util/statistics_registry.h"
36 #include "util/dump.h"
43 #include <ext/hash_set>
51 class QuantifiersEngine
;
53 class SubstitutionMap
;
55 class EntailmentCheckParameters
;
56 class EntailmentCheckSideEffects
;
59 class CandidateGenerator
;
60 }/* CVC4::theory::rrinst namespace */
64 }/* CVC4::theory::eq namespace */
67 * Information about an assertion for the theories.
73 /** Has this assertion been preregistered with this theory */
76 Assertion(TNode assertion
, bool isPreregistered
)
77 : assertion(assertion
), isPreregistered(isPreregistered
) {}
80 * Convert the assertion to a TNode.
82 operator TNode () const {
87 * Convert the assertion to a Node.
89 operator Node () const {
93 };/* struct Assertion */
96 * A (oredered) pair of terms a theory cares about.
105 CarePair(TNode a
, TNode b
, TheoryId theory
)
106 : a(a
< b
? a
: b
), b(a
< b
? b
: a
), theory(theory
) {}
108 bool operator == (const CarePair
& other
) const {
109 return (theory
== other
.theory
) && (a
== other
.a
) && (b
== other
.b
);
112 bool operator < (const CarePair
& other
) const {
113 if (theory
< other
.theory
) return true;
114 if (theory
> other
.theory
) return false;
115 if (a
< other
.a
) return true;
116 if (a
> other
.a
) return false;
120 };/* struct CarePair */
123 * A set of care pairs.
125 typedef std::set
<CarePair
> CareGraph
;
128 * Base class for T-solvers. Abstract DPLL(T).
130 * This is essentially an interface class. The TheoryEngine has
131 * pointers to Theory. Note that only one specific Theory type (e.g.,
132 * TheoryUF) can exist per NodeManager, because of how the
133 * RegisteredAttr works. (If you need multiple instances of the same
134 * theory, you'll have to write a multiplexed theory that dispatches
135 * all calls to them.)
141 friend class ::CVC4::TheoryEngine
;
143 // Disallow default construction, copy, assignment.
144 Theory() CVC4_UNUSED
;
145 Theory(const Theory
&) CVC4_UNUSED
;
146 Theory
& operator=(const Theory
&) CVC4_UNUSED
;
149 * An integer identifying the type of the theory
154 * The SAT search context for the Theory.
156 context::Context
* d_satContext
;
159 * The user level assertion context for the Theory.
161 context::UserContext
* d_userContext
;
164 * Information about the logic we're operating within.
166 const LogicInfo
& d_logicInfo
;
169 * The assertFact() queue.
171 * These can not be TNodes as some atoms (such as equalities) are sent
172 * across theories without being stored in a global map.
174 context::CDList
<Assertion
> d_facts
;
176 /** Index into the head of the facts list */
177 context::CDO
<unsigned> d_factsHead
;
180 * Add shared term to the theory.
182 void addSharedTermInternal(TNode node
);
185 * Indices for splitting on the shared terms.
187 context::CDO
<unsigned> d_sharedTermsIndex
;
190 * The care graph the theory will use during combination.
192 CareGraph
* d_careGraph
;
195 * Reference to the quantifiers engine (or NULL, if quantifiers are
196 * not supported or not enabled).
198 QuantifiersEngine
* d_quantEngine
;
200 // === STATISTICS ===
201 /** time spent in theory combination */
202 TimerStat d_computeCareGraphTime
;
204 static std::string
statName(TheoryId id
, const char* statName
) {
205 std::stringstream ss
;
206 ss
<< "theory<" << id
<< ">::" << statName
;
213 * The only method to add suff to the care graph.
215 void addCarePair(TNode t1
, TNode t2
) {
217 d_careGraph
->insert(CarePair(t1
, t2
, d_id
));
222 * The function should compute the care graph over the shared terms.
223 * The default function returns all the pairs among the shared variables.
225 virtual void computeCareGraph();
228 * A list of shared terms that the theory has.
230 context::CDList
<TNode
> d_sharedTerms
;
233 * Helper function for computeRelevantTerms
235 void collectTerms(TNode n
, std::set
<Node
>& termSet
) const;
237 * Scans the current set of assertions and shared terms top-down
238 * until a theory-leaf is reached, and adds all terms found to
239 * termSet. This is used by collectModelInfo to delimit the set of
240 * terms that should be used when constructing a model
242 void computeRelevantTerms(std::set
<Node
>& termSet
) const;
245 * Construct a Theory.
247 Theory(TheoryId id
, context::Context
* satContext
, context::UserContext
* userContext
,
248 OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
) throw()
250 , d_satContext(satContext
)
251 , d_userContext(userContext
)
252 , d_logicInfo(logicInfo
)
253 , d_facts(satContext
)
254 , d_factsHead(satContext
, 0)
255 , d_sharedTermsIndex(satContext
, 0)
257 , d_quantEngine(NULL
)
258 , d_computeCareGraphTime(statName(id
, "computeCareGraphTime"))
259 , d_sharedTerms(satContext
)
261 , d_valuation(valuation
)
262 , d_proofEnabled(false)
264 StatisticsRegistry::registerStat(&d_computeCareGraphTime
);
268 * This is called at shutdown time by the TheoryEngine, just before
269 * destruction. It is important because there are destruction
270 * ordering issues between PropEngine and Theory (based on what
271 * hard-links to Nodes are outstanding). As the fact queue might be
272 * nonempty, we ensure here that it's clear. If you overload this,
273 * you must make an explicit call here to this->Theory::shutdown()
276 virtual void shutdown() { }
279 * The output channel for the Theory.
281 OutputChannel
* d_out
;
284 * The valuation proxy for the Theory to communicate back with the
285 * theory engine (and other theories).
287 Valuation d_valuation
;
290 * Returns the next assertion in the assertFact() queue.
292 * @return the next assertion in the assertFact() queue
294 inline Assertion
get();
296 const LogicInfo
& getLogicInfo() const {
301 * The theory that owns the uninterpreted sort.
303 static TheoryId s_uninterpretedSortOwner
;
305 void printFacts(std::ostream
& os
) const;
306 void debugPrintFacts() const;
309 * Whether proofs are enabled
317 * Return the ID of the theory responsible for the given type.
319 static inline TheoryId
theoryOf(TypeNode typeNode
) {
320 Trace("theory::internal") << "theoryOf(" << typeNode
<< ")" << std::endl
;
322 while (typeNode
.isPredicateSubtype()) {
323 typeNode
= typeNode
.getSubtypeParentType();
325 if (typeNode
.getKind() == kind::TYPE_CONSTANT
) {
326 id
= typeConstantToTheoryId(typeNode
.getConst
<TypeConstant
>());
328 id
= kindToTheoryId(typeNode
.getKind());
330 if (id
== THEORY_BUILTIN
) {
331 Trace("theory::internal") << "theoryOf(" << typeNode
<< ") == " << s_uninterpretedSortOwner
<< std::endl
;
332 return s_uninterpretedSortOwner
;
338 * Returns the ID of the theory responsible for the given node.
340 static TheoryId
theoryOf(TheoryOfMode mode
, TNode node
);
343 * Returns the ID of the theory responsible for the given node.
345 static inline TheoryId
theoryOf(TNode node
) {
346 return theoryOf(options::theoryOfMode(), node
);
350 * Set the owner of the uninterpreted sort.
352 static void setUninterpretedSortOwner(TheoryId theory
) {
353 s_uninterpretedSortOwner
= theory
;
357 * Get the owner of the uninterpreted sort.
359 static TheoryId
getUninterpretedSortOwner() {
360 return s_uninterpretedSortOwner
;
364 * Checks if the node is a leaf node of this theory
366 inline bool isLeaf(TNode node
) const {
367 return node
.getNumChildren() == 0 || theoryOf(node
) != d_id
;
371 * Checks if the node is a leaf node of a theory.
373 inline static bool isLeafOf(TNode node
, TheoryId theoryId
) {
374 return node
.getNumChildren() == 0 || theoryOf(node
) != theoryId
;
378 * Returns true if the assertFact queue is empty
380 bool done() const throw() {
381 return d_factsHead
== d_facts
.size();
385 * Destructs a Theory.
390 * Subclasses of Theory may add additional efforts. DO NOT CHECK
391 * equality with one of these values (e.g. if STANDARD xxx) but
392 * rather use range checks (or use the helper functions below).
393 * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
398 * Standard effort where theory need not do anything
400 EFFORT_STANDARD
= 50,
402 * Full effort requires the theory make sure its assertions are satisfiable or not
406 * Combination effort means that the individual theories are already satisfied, and
407 * it is time to put some effort into propagation of shared term equalities
409 EFFORT_COMBINATION
= 150,
411 * Last call effort, reserved for quantifiers.
413 EFFORT_LAST_CALL
= 200
416 static inline bool standardEffortOrMore(Effort e
) CVC4_CONST_FUNCTION
417 { return e
>= EFFORT_STANDARD
; }
418 static inline bool standardEffortOnly(Effort e
) CVC4_CONST_FUNCTION
419 { return e
>= EFFORT_STANDARD
&& e
< EFFORT_FULL
; }
420 static inline bool fullEffort(Effort e
) CVC4_CONST_FUNCTION
421 { return e
== EFFORT_FULL
; }
422 static inline bool combination(Effort e
) CVC4_CONST_FUNCTION
423 { return e
== EFFORT_COMBINATION
; }
426 * Get the id for this Theory.
428 TheoryId
getId() const {
433 * Get the SAT context associated to this Theory.
435 context::Context
* getSatContext() const {
440 * Get the context associated to this Theory.
442 context::UserContext
* getUserContext() const {
443 return d_userContext
;
447 * Set the output channel associated to this theory.
449 void setOutputChannel(OutputChannel
& out
) {
454 * Get the output channel associated to this theory.
456 OutputChannel
& getOutputChannel() {
461 * Get the valuation associated to this theory.
463 Valuation
& getValuation() {
468 * Get the quantifiers engine associated to this theory.
470 QuantifiersEngine
* getQuantifiersEngine() {
471 return d_quantEngine
;
475 * Get the quantifiers engine associated to this theory (const version).
477 const QuantifiersEngine
* getQuantifiersEngine() const {
478 return d_quantEngine
;
482 * Finish theory initialization. At this point, options and the logic
483 * setting are final, and the master equality engine and quantifiers
484 * engine (if any) are initialized. This base class implementation
487 virtual void finishInit() { }
490 * Some theories have kinds that are effectively definitions and
491 * should be expanded before they are handled. Definitions allow
492 * a much wider range of actions than the normal forms given by the
493 * rewriter; they can enable other theories and create new terms.
494 * However no assumptions can be made about subterms having been
495 * expanded or rewritten. Where possible rewrite rules should be
496 * used, definitions should only be used when rewrites are not
497 * possible, for example in handling under-specified operations
498 * using partially defined functions.
500 virtual Node
expandDefinition(LogicRequest
&logicRequest
, Node node
) {
501 // by default, do nothing
506 * Pre-register a term. Done one time for a Node per SAT context level.
508 virtual void preRegisterTerm(TNode
) { }
511 * Assert a fact in the current context.
513 void assertFact(TNode assertion
, bool isPreregistered
) {
514 Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_satContext
->getLevel() << "](" << assertion
<< ", " << (isPreregistered
? "true" : "false") << ")" << std::endl
;
515 d_facts
.push_back(Assertion(assertion
, isPreregistered
));
519 * This method is called to notify a theory that the node n should
520 * be considered a "shared term" by this theory
522 virtual void addSharedTerm(TNode n
) { }
525 * Called to set the master equality engine.
527 virtual void setMasterEqualityEngine(eq::EqualityEngine
* eq
) { }
530 * Called to set the quantifiers engine.
532 virtual void setQuantifiersEngine(QuantifiersEngine
* qe
) {
537 * Return the current theory care graph. Theories should overload computeCareGraph to do
538 * the actual computation, and use addCarePair to add pairs to the care graph.
540 void getCareGraph(CareGraph
& careGraph
) {
541 Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl
;
542 TimerStat::CodeTimer
computeCareGraphTime(d_computeCareGraphTime
);
543 d_careGraph
= &careGraph
;
549 * Return the status of two terms in the current context. Should be implemented in
550 * sub-theories to enable more efficient theory-combination.
552 virtual EqualityStatus
getEqualityStatus(TNode a
, TNode b
) { return EQUALITY_UNKNOWN
; }
555 * Return the model value of the give shared term (or null if not available).
557 virtual Node
getModelValue(TNode var
) { return Node::null(); }
560 * Check the current assignment's consistency.
562 * An implementation of check() is required to either:
563 * - return a conflict on the output channel,
565 * - throw an exception
566 * - or call get() until done() is true.
568 virtual void check(Effort level
= EFFORT_FULL
) { }
571 * T-propagate new literal assignments in the current context.
573 virtual void propagate(Effort level
= EFFORT_FULL
) { }
576 * Return an explanation for the literal represented by parameter n
577 * (which was previously propagated by this theory).
579 virtual Node
explain(TNode n
) {
580 Unimplemented("Theory %s propagated a node but doesn't implement the "
581 "Theory::explain() interface!", identify().c_str());
585 * Get all relevant information in this theory regarding the current
586 * model. This should be called after a call to check( FULL_EFFORT )
587 * for all theories with no conflicts and no lemmas added.
588 * If fullModel is true, then we must specify sufficient information for
589 * the model class to construct constant representatives for each equivalence
592 virtual void collectModelInfo( TheoryModel
* m
, bool fullModel
){ }
595 * Return a decision request, if the theory has one, or the NULL node
598 virtual Node
getNextDecisionRequest() { return Node(); }
601 * Statically learn from assertion "in," which has been asserted
602 * true at the top level. The theory should only add (via
603 * ::operator<< or ::append()) to the "learned" builder---it should
604 * *never* clear it. It is a conjunction to add to the formula at
605 * the top-level and may contain other theories' contributions.
607 virtual void ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) { }
609 enum PPAssertStatus
{
610 /** Atom has been solved */
611 PP_ASSERT_STATUS_SOLVED
,
612 /** Atom has not been solved */
613 PP_ASSERT_STATUS_UNSOLVED
,
614 /** Atom is inconsistent */
615 PP_ASSERT_STATUS_CONFLICT
619 * Given a literal, add the solved substitutions to the map, if any.
620 * The method should return true if the literal can be safely removed.
622 virtual PPAssertStatus
ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
);
625 * Given an atom of the theory coming from the input formula, this
626 * method can be overridden in a theory implementation to rewrite
627 * the atom into an equivalent form. This is only called just
628 * before an input atom to the engine.
630 virtual Node
ppRewrite(TNode atom
) { return atom
; }
633 * Don't preprocess subterm of this term
635 virtual bool ppDontRewriteSubterm(TNode atom
) { return false; }
638 * A Theory is called with presolve exactly one time per user
639 * check-sat. presolve() is called after preregistration,
640 * rewriting, and Boolean propagation, (other theories'
641 * propagation?), but the notified Theory has not yet had its
642 * check() or propagate() method called. A Theory may empty its
643 * assertFact() queue using get(). A Theory can raise conflicts,
644 * add lemmas, and propagate literals during presolve().
646 * NOTE: The presolve property must be added to the kinds file for
649 virtual void presolve() { }
652 * A Theory is called with postsolve exactly one time per user
653 * check-sat. postsolve() is called after the query has completed
654 * (regardless of whether sat, unsat, or unknown), and after any
655 * model-querying related to the query has been performed.
656 * After this call, the theory will not get another check() or
657 * propagate() call until presolve() is called again. A Theory
658 * cannot raise conflicts, add lemmas, or propagate literals during
661 virtual void postsolve() { }
664 * Notification sent to the theory wheneven the search restarts.
665 * Serves as a good time to do some clean-up work, and you can
666 * assume you're at DL 0 for the purposes of Contexts. This function
667 * should not use the output channel.
669 virtual void notifyRestart() { }
672 * Identify this theory (for debugging, dynamic configuration,
675 virtual std::string
identify() const = 0;
677 /** Set user attribute
678 * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
679 * via the syntax (! n :attr)
681 virtual void setUserAttribute(const std::string
& attr
, Node n
, std::vector
<Node
> node_values
, std::string str_value
) {
682 Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface",
686 /** A set of theories */
687 typedef uint32_t Set
;
689 /** A set of all theories */
690 static const Set AllTheories
= (1 << theory::THEORY_LAST
) - 1;
692 /** Pops a first theory off the set */
693 static inline TheoryId
setPop(Set
& set
) {
694 uint32_t i
= ffs(set
); // Find First Set (bit)
695 if (i
== 0) { return THEORY_LAST
; }
696 TheoryId id
= (TheoryId
)(i
-1);
697 set
= setRemove(id
, set
);
701 /** Returns the size of a set of theories */
702 static inline size_t setSize(Set set
) {
704 while (setPop(set
) != THEORY_LAST
) {
710 /** Returns the index size of a set of theories */
711 static inline size_t setIndex(TheoryId id
, Set set
) {
712 Assert (setContains(id
, set
));
714 while (setPop(set
) != id
) {
720 /** Add the theory to the set. If no set specified, just returns a singleton set */
721 static inline Set
setInsert(TheoryId theory
, Set set
= 0) {
722 return set
| (1 << theory
);
725 /** Add the theory to the set. If no set specified, just returns a singleton set */
726 static inline Set
setRemove(TheoryId theory
, Set set
= 0) {
727 return setDifference(set
, setInsert(theory
));
730 /** Check if the set contains the theory */
731 static inline bool setContains(TheoryId theory
, Set set
) {
732 return set
& (1 << theory
);
735 static inline Set
setComplement(Set a
) {
736 return (~a
) & AllTheories
;
739 static inline Set
setIntersection(Set a
, Set b
) {
743 static inline Set
setUnion(Set a
, Set b
) {
748 static inline Set
setDifference(Set a
, Set b
) {
752 static inline std::string
setToString(theory::Theory::Set theorySet
) {
753 std::stringstream ss
;
755 for(unsigned theoryId
= 0; theoryId
< theory::THEORY_LAST
; ++theoryId
) {
756 if (theory::Theory::setContains((theory::TheoryId
)theoryId
, theorySet
)) {
757 ss
<< (theory::TheoryId
) theoryId
<< " ";
764 typedef context::CDList
<Assertion
>::const_iterator assertions_iterator
;
767 * Provides access to the facts queue, primarily intended for theory
768 * debugging purposes.
770 * @return the iterator to the beginning of the fact queue
772 assertions_iterator
facts_begin() const {
773 return d_facts
.begin();
777 * Provides access to the facts queue, primarily intended for theory
778 * debugging purposes.
780 * @return the iterator to the end of the fact queue
782 assertions_iterator
facts_end() const {
783 return d_facts
.end();
786 typedef context::CDList
<TNode
>::const_iterator shared_terms_iterator
;
789 * Provides access to the shared terms, primarily intended for theory
790 * debugging purposes.
792 * @return the iterator to the beginning of the shared terms list
794 shared_terms_iterator
shared_terms_begin() const {
795 return d_sharedTerms
.begin();
799 * Provides access to the facts queue, primarily intended for theory
800 * debugging purposes.
802 * @return the iterator to the end of the shared terms list
804 shared_terms_iterator
shared_terms_end() const {
805 return d_sharedTerms
.end();
810 * This is a utility function for constructing a copy of the currently shared terms
811 * in a queriable form. As this is
813 std::hash_set
<TNode
, TNodeHashFunction
> currentlySharedTerms() const;
816 * This allows the theory to be queried for whether a literal, lit, is
817 * entailed by the theory. This returns a pair of a Boolean and a node E.
819 * If the Boolean is true, then E is a formula that entails lit and E is propositionally
820 * entailed by the assertions to the theory.
822 * If the Boolean is false, it is "unknown" if lit is entailed and E may be
825 * The literal lit is either an atom a or (not a), which must belong to the theory:
826 * There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
828 * There are NO assumptions that a or the subterms of a have been
829 * preprocessed in any form. This includes ppRewrite, rewriting,
830 * preregistering, registering, definition expansion or ITE removal!
832 * Theories are free to limit the amount of effort they use and so may
833 * always opt to return "unknown". Both "unknown" and "not entailed",
834 * may return for E a non-boolean Node (e.g. Node::null()). (There is no explicit output
835 * for the negation of lit is entailed.)
837 * If lit is theory valid, the return result may be the Boolean constant
840 * If lit is entailed by multiple assertions on the theory's getFact()
841 * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
842 * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
844 * If lit is entailed by a single assertion on the theory's getFact()
845 * queue, say a, this may return E=a.
847 * The theory may always return false!
849 * The search is controlled by the parameter params. For default behavior,
850 * this may be left NULL.
852 * Theories that want parameters extend the virtual EntailmentCheckParameters
853 * class. Users ask the theory for an appropriate subclass from the theory
854 * and configure that. How this is implemented is on a per theory basis.
856 * The search may provide additional output to guide the user of
857 * this function. This output is stored in a EntailmentCheckSideEffects*
858 * output parameter. The implementation of this is theory specific. For
859 * no output, this is NULL.
861 * Theories may not touch their output stream during an entailment check.
863 * @param lit a literal belonging to the theory.
864 * @param params the control parameters for the entailment check.
865 * @param out a theory specific output object of the entailment search.
866 * @return a pair <b,E> s.t. if b is true, then a formula E such that
867 * E |= lit in the theory.
869 virtual std::pair
<bool, Node
> entailmentCheck(TNode lit
, const EntailmentCheckParameters
* params
= NULL
, EntailmentCheckSideEffects
* out
= NULL
);
873 std::ostream
& operator<<(std::ostream
& os
, theory::Theory::Effort level
);
874 inline std::ostream
& operator<<(std::ostream
& out
, const theory::Assertion
& a
);
876 inline theory::Assertion
Theory::get() {
877 Assert( !done(), "Theory::get() called with assertion queue empty!" );
880 Assertion fact
= d_facts
[d_factsHead
];
881 d_factsHead
= d_factsHead
+ 1;
883 Trace("theory") << "Theory::get() => " << fact
<< " (" << d_facts
.size() - d_factsHead
<< " left)" << std::endl
;
885 if(Dump
.isOn("state")) {
886 Dump("state") << AssertCommand(fact
.assertion
.toExpr());
892 inline std::ostream
& operator<<(std::ostream
& out
, const theory::Assertion
& a
) {
893 return out
<< a
.assertion
;
896 inline std::ostream
& operator<<(std::ostream
& out
,
897 const CVC4::theory::Theory
& theory
) {
898 return out
<< theory
.identify();
901 inline std::ostream
& operator << (std::ostream
& out
, theory::Theory::PPAssertStatus status
) {
903 case theory::Theory::PP_ASSERT_STATUS_SOLVED
:
904 out
<< "SOLVE_STATUS_SOLVED"; break;
905 case theory::Theory::PP_ASSERT_STATUS_UNSOLVED
:
906 out
<< "SOLVE_STATUS_UNSOLVED"; break;
907 case theory::Theory::PP_ASSERT_STATUS_CONFLICT
:
908 out
<< "SOLVE_STATUS_CONFLICT"; break;
915 class EntailmentCheckParameters
{
919 EntailmentCheckParameters(TheoryId tid
);
921 TheoryId
getTheoryId() const;
922 virtual ~EntailmentCheckParameters();
923 };/* class EntailmentCheckParameters */
925 class EntailmentCheckSideEffects
{
929 EntailmentCheckSideEffects(TheoryId tid
);
931 TheoryId
getTheoryId() const;
932 virtual ~EntailmentCheckSideEffects();
933 };/* class EntailmentCheckSideEffects */
935 }/* CVC4::theory namespace */
936 }/* CVC4 namespace */
938 #endif /* __CVC4__THEORY__THEORY_H */