1 /********************* */
3 ** Original author: mdeters
4 ** Major contributors: none
5 ** Minor contributors (to current version): dejan, taking
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** Base of the theory interface.
16 #include "cvc4_private.h"
18 #ifndef __CVC4__THEORY__THEORY_H
19 #define __CVC4__THEORY__THEORY_H
21 #include "expr/node.h"
22 #include "expr/attribute.h"
23 #include "theory/output_channel.h"
24 #include "context/context.h"
38 * Base class for T-solvers. Abstract DPLL(T).
40 * This is essentially an interface class. The TheoryEngine has
41 * pointers to Theory. But each individual theory implementation T
42 * should inherit from TheoryImpl<T>, which specializes a few things
49 friend class TheoryImpl
;
54 Theory(context::Context
* ctxt
, OutputChannel
& out
) throw() :
60 * Disallow default construction.
67 * The output channel for the Theory.
69 context::Context
* d_context
;
72 * The output channel for the Theory.
77 * The assertFact() queue.
79 // FIXME CD: on backjump we clear the facts IFF the queue gets
80 // emptied on every DL. In general I guess we need a CDQueue<>?
81 // Perhaps one that asserts it's empty at each push?
82 std::queue
<Node
> d_facts
;
85 * Return whether a node is shared or not. Used by setup().
87 bool isShared(TNode n
) throw();
90 * Returns true if the assertFact queue is empty
93 return d_facts
.empty();
99 * Destructs a Theory. This implementation does nothing, but we
100 * need a virtual destructor for safety in case subclasses have a
107 * Subclasses of Theory may add additional efforts. DO NOT CHECK
108 * equality with one of these values (e.g. if STANDARD xxx) but
109 * rather use range checks (or use the helper functions below).
110 * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
120 // TODO add compiler annotation "constant function" here
121 static bool minEffortOnly(Effort e
) { return e
== MIN_EFFORT
; }
122 static bool quickCheckOrMore(Effort e
) { return e
>= QUICK_CHECK
; }
123 static bool quickCheckOnly(Effort e
) { return e
>= QUICK_CHECK
&& e
< STANDARD
; }
124 static bool standardEffortOrMore(Effort e
) { return e
>= STANDARD
; }
125 static bool standardEffortOnly(Effort e
) { return e
>= STANDARD
&& e
< FULL_EFFORT
; }
126 static bool fullEffort(Effort e
) { return e
>= FULL_EFFORT
; }
129 * Set the output channel associated to this theory.
131 void setOutputChannel(OutputChannel
& out
) {
136 * Get the output channel associated to this theory.
138 OutputChannel
& getOutputChannel() {
143 * Get the output channel associated to this theory [const].
145 const OutputChannel
& getOutputChannel() const {
150 * Pre-register a term. Done one time for a Node, ever.
153 virtual void preRegisterTerm(TNode
) = 0;
158 * When get() is called to get the next thing off the theory queue,
159 * setup() is called on its subterms (in TheoryEngine). Then setup()
160 * is called on this node.
162 * This is done in a "context escape" -- that is, at context level 0.
163 * setup() MUST NOT MODIFY context-dependent objects that it hasn't
164 * itself just created.
166 virtual void registerTerm(TNode
) = 0;
169 * Assert a fact in the current context.
171 void assertFact(TNode n
) {
176 * Check the current assignment's consistency.
178 virtual void check(Effort level
= FULL_EFFORT
) = 0;
181 * T-propagate new literal assignments in the current context.
183 virtual void propagate(Effort level
= FULL_EFFORT
) = 0;
186 * Return an explanation for the literal represented by parameter n
187 * (which was previously propagated by this theory). Report
188 * explanations to an output channel.
190 virtual void explain(TNode n
, Effort level
= FULL_EFFORT
) = 0;
193 // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
197 * Different states at which invariants are checked.
202 };/* enum ReadyState */
205 * Public invariant checker. Assert that this theory is in a valid
206 * state for the (external) system state. This implementation
207 * checks base invariants and then calls theoryReady(). This
208 * function may abort in the case of a failed assert, or return
209 * false (the caller should assert that the return value is true).
211 * @param s the state about which to check invariants
213 bool ready(ReadyState s
) {
214 if(s
== ABOUT_TO_PUSH
) {
215 Assert(d_facts
.empty(), "Theory base code invariant broken: "
216 "fact queue is nonempty on context push");
219 return theoryReady(s
);
225 * Check any invariants at the ReadyState given. Only called by
226 * Theory class, and then only with CVC4_ASSERTIONS enabled. This
227 * function may abort in the case of a failed assert, or return
228 * false (the caller should assert that the return value is true).
230 * @param s the state about which to check invariants
232 virtual bool theoryReady(ReadyState s
) {
240 * Base class for T-solver implementations. Each individual
241 * implementation T of the Theory interface should inherit from
242 * TheoryImpl<T>. This class specializes some things for a particular
243 * theory implementation.
245 * The problem with this is that Theory implementations cannot be
246 * further subclassed without designing all non-children in the type
247 * DAG to play the same trick as here (be template-polymorphic in their
248 * most-derived child), linearizing the inheritance hierarchy (viewing
249 * each instantiation separately).
252 class TheoryImpl
: public Theory
{
257 * Construct a Theory.
259 TheoryImpl(context::Context
* ctxt
, OutputChannel
& out
) :
261 /* FIXME: assert here that a TheoryImpl<T> doesn't already exist
262 * for this NodeManager?? If it does, we're hosed because they'll
263 * share per-theory node attributes. */
266 /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
267 struct Registered
{};
268 /** The "registerTerm()-has-been-called" flag on Nodes */
269 typedef CVC4::expr::CDAttribute
<Registered
, bool> RegisteredAttr
;
271 /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
272 struct PreRegistered
{};
273 /** The "preRegisterTerm()-has-been-called" flag on Nodes */
274 typedef CVC4::expr::Attribute
<PreRegistered
, bool> PreRegisteredAttr
;
277 * Returns the next atom in the assertFact() queue. Guarantees that
278 * registerTerm() has been called on the theory specific subterms.
280 * @return the next atom in the assertFact() queue.
283 };/* class TheoryImpl<T> */
286 Node TheoryImpl
<T
>::get() {
287 Assert(typeid(*this) == typeid(T
),
288 "Improper Theory inheritance chain detected.");
290 Assert( !d_facts
.empty(),
291 "Theory::get() called with assertion queue empty!" );
293 Node fact
= d_facts
.front();
296 if(! fact
.getAttribute(RegisteredAttr())) {
297 std::list
<TNode
> toReg
;
298 toReg
.push_back(fact
);
300 /* Essentially this is doing a breadth-first numbering of
301 * non-registered subterms with children. Any non-registered
302 * leaves are immediately registered. */
303 for(std::list
<TNode
>::iterator workp
= toReg
.begin();
304 workp
!= toReg
.end();
309 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
312 if(! c
.getAttribute(RegisteredAttr())) {
313 if(c
.getNumChildren() == 0) {
314 c
.setAttribute(RegisteredAttr(), true);
323 /* Now register the list of terms in reverse order. Between this
324 * and the above registration of leaves, this should ensure that
325 * all subterms in the entire tree were registered in
326 * reverse-topological order. */
327 for(std::list
<TNode
>::reverse_iterator i
= toReg
.rend();
333 /* Note that a shared TNode in the DAG rooted at "fact" could
334 * appear twice on the list, so we have to avoid hitting it
336 // FIXME when ExprSets are online, use one of those to avoid
337 // duplicates in the above?
338 if(! n
.getAttribute(RegisteredAttr())) {
339 n
.setAttribute(RegisteredAttr(), true);
348 }/* CVC4::theory namespace */
349 }/* CVC4 namespace */
351 #endif /* __CVC4__THEORY__THEORY_H */