1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): dejan, taking
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Base of the theory interface.
16 ** Base of the theory interface.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__THEORY_H
22 #define __CVC4__THEORY__THEORY_H
24 #include "expr/node.h"
25 #include "expr/attribute.h"
26 #include "theory/output_channel.h"
27 #include "context/context.h"
40 // rewrite cache support
41 struct RewriteCacheTag
{};
42 typedef expr::Attribute
<RewriteCacheTag
, TNode
> RewriteCache
;
45 * Base class for T-solvers. Abstract DPLL(T).
47 * This is essentially an interface class. The TheoryEngine has
48 * pointers to Theory. Note that only one specific Theory type (e.g.,
49 * TheoryUF) can exist per NodeManager, because of how the
50 * RegisteredAttr works. (If you need multiple instances of the same
51 * theory, you'll have to write a multiplexed theory that dispatches
57 friend class ::CVC4::TheoryEngine
;
60 * Disallow default construction.
65 * The context for the Theory.
67 context::Context
* d_context
;
70 * The assertFact() queue.
72 * This queue MUST be emptied by ANY call to check() at ANY effort
73 * level. In debug builds, this is checked. On backjump we clear
74 * the fact queue (see FactsResetter, below).
76 * These can safely be TNodes because the literal map maintained in
77 * the SAT solver keeps them live. As an added benefit, if we have
78 * them as TNodes, dtors are cheap (optimized away?).
80 std::deque
<TNode
> d_facts
;
82 /** Helper class to reset the fact queue on pop(). */
83 class FactsResetter
: public context::ContextNotifyObj
{
87 FactsResetter(Theory
& thy
) :
88 context::ContextNotifyObj(thy
.d_context
),
93 d_thy
.d_facts
.clear();
97 friend class FactsResetter
;
102 * Construct a Theory.
104 Theory(context::Context
* ctxt
, OutputChannel
& out
) throw() :
107 d_factsResetter(*this),
112 * This is called at shutdown time by the TheoryEngine, just before
113 * destruction. It is important because there are destruction
114 * ordering issues between PropEngine and Theory (based on what
115 * hard-links to Nodes are outstanding). As the fact queue might be
116 * nonempty, we ensure here that it's clear. If you overload this,
117 * you must make an explicit call here to this->Theory::shutdown()
120 virtual void shutdown() {
124 context::Context
* getContext() const {
129 * The output channel for the Theory.
131 OutputChannel
* d_out
;
134 * Returns true if the assertFact queue is empty
136 bool done() throw() {
137 return d_facts
.empty();
141 * Return whether a node is shared or not. Used by setup().
143 bool isShared(TNode n
) throw();
146 * Check whether a node is in the rewrite cache or not.
148 static bool inRewriteCache(TNode n
) throw() {
149 return n
.hasAttribute(RewriteCache());
153 * Get the value of the rewrite cache (or Node::null()) if there is
156 static Node
getRewriteCache(TNode n
) throw() {
157 return n
.getAttribute(RewriteCache());
160 /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
161 struct Registered
{};
162 /** The "registerTerm()-has-been-called" flag on Nodes */
163 typedef CVC4::expr::CDAttribute
<Registered
, bool> RegisteredAttr
;
165 /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
166 struct PreRegistered
{};
167 /** The "preRegisterTerm()-has-been-called" flag on Nodes */
168 typedef CVC4::expr::Attribute
<PreRegistered
, bool> PreRegisteredAttr
;
171 * Returns the next atom in the assertFact() queue. Guarantees that
172 * registerTerm() has been called on the theory specific subterms.
174 * @return the next atom in the assertFact() queue.
181 * Destructs a Theory. This implementation does nothing, but we
182 * need a virtual destructor for safety in case subclasses have a
189 * Subclasses of Theory may add additional efforts. DO NOT CHECK
190 * equality with one of these values (e.g. if STANDARD xxx) but
191 * rather use range checks (or use the helper functions below).
192 * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
202 // TODO add compiler annotation "constant function" here
203 static bool minEffortOnly(Effort e
) { return e
== MIN_EFFORT
; }
204 static bool quickCheckOrMore(Effort e
) { return e
>= QUICK_CHECK
; }
205 static bool quickCheckOnly(Effort e
) { return e
>= QUICK_CHECK
&& e
< STANDARD
; }
206 static bool standardEffortOrMore(Effort e
) { return e
>= STANDARD
; }
207 static bool standardEffortOnly(Effort e
) { return e
>= STANDARD
&& e
< FULL_EFFORT
; }
208 static bool fullEffort(Effort e
) { return e
>= FULL_EFFORT
; }
211 * Set the output channel associated to this theory.
213 void setOutputChannel(OutputChannel
& out
) {
218 * Get the output channel associated to this theory.
220 OutputChannel
& getOutputChannel() {
225 * Get the output channel associated to this theory [const].
227 const OutputChannel
& getOutputChannel() const {
232 * Pre-register a term. Done one time for a Node, ever.
235 virtual void preRegisterTerm(TNode
) = 0;
238 * Rewrite a term. Done one time for a Node, ever.
240 virtual Node
rewrite(TNode n
) {
247 * When get() is called to get the next thing off the theory queue,
248 * setup() is called on its subterms (in TheoryEngine). Then setup()
249 * is called on this node.
251 * This is done in a "context escape" -- that is, at context level 0.
252 * setup() MUST NOT MODIFY context-dependent objects that it hasn't
253 * itself just created.
255 virtual void registerTerm(TNode
) = 0;
258 * Assert a fact in the current context.
260 void assertFact(TNode n
) {
261 Debug("theory") << "Theory::assertFact(" << n
<< ")" << std::endl
;
262 d_facts
.push_back(n
);
266 * Check the current assignment's consistency.
268 * An implementation of check() is required to either:
269 * - return a conflict on the output channel,
271 * - throw an exception
272 * - or call get() until done() is true.
274 virtual void check(Effort level
= FULL_EFFORT
) = 0;
277 * T-propagate new literal assignments in the current context.
279 virtual void propagate(Effort level
= FULL_EFFORT
) = 0;
282 * Return an explanation for the literal represented by parameter n
283 * (which was previously propagated by this theory). Report
284 * explanations to an output channel.
286 virtual void explain(TNode n
, Effort level
= FULL_EFFORT
) = 0;
289 // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
293 * Different states at which invariants are checked.
298 };/* enum ReadyState */
301 * Public invariant checker. Assert that this theory is in a valid
302 * state for the (external) system state. This implementation
303 * checks base invariants and then calls theoryReady(). This
304 * function may abort in the case of a failed assert, or return
305 * false (the caller should assert that the return value is true).
307 * @param s the state about which to check invariants
309 bool ready(ReadyState s
) {
310 if(s
== ABOUT_TO_PUSH
) {
311 Assert(d_facts
.empty(), "Theory base code invariant broken: "
312 "fact queue is nonempty on context push");
315 return theoryReady(s
);
321 * Check any invariants at the ReadyState given. Only called by
322 * Theory class, and then only with CVC4_ASSERTIONS enabled. This
323 * function may abort in the case of a failed assert, or return
324 * false (the caller should assert that the return value is true).
326 * @param s the state about which to check invariants
328 virtual bool theoryReady(ReadyState s
) {
334 std::ostream
& operator<<(std::ostream
& os
, Theory::Effort level
);
336 }/* CVC4::theory namespace */
337 }/* CVC4 namespace */
339 #endif /* __CVC4__THEORY__THEORY_H */