summaryrefslogtreecommitdiff
path: root/src/theory/theory.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r--src/theory/theory.h274
1 files changed, 244 insertions, 30 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 76b9697dc..e079d67bd 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -17,25 +17,91 @@
#define __CVC4__THEORY__THEORY_H
#include "expr/node.h"
+#include "expr/attribute.h"
#include "theory/output_channel.h"
#include "context/context.h"
+#include <queue>
+#include <vector>
+
+#include <typeinfo>
+
namespace CVC4 {
namespace theory {
+template <class T>
+class TheoryImpl;
+
/**
* Base class for T-solvers. Abstract DPLL(T).
+ *
+ * This is essentially an interface class. The TheoryEngine has
+ * pointers to Theory. But each individual theory implementation T
+ * should inherit from TheoryImpl<T>, which specializes a few things
+ * for that theory.
*/
class Theory {
+private:
+
+ template <class T>
+ friend class TheoryImpl;
+
+ /**
+ * Construct a Theory.
+ */
+ Theory(context::Context* ctxt, OutputChannel& out) throw() :
+ d_context(ctxt),
+ d_out(&out) {
+ }
+
+ /**
+ * Disallow default construction.
+ */
+ Theory();
+
+protected:
+
+ /**
+ * The output channel for the Theory.
+ */
+ context::Context* d_context;
+
+ /**
+ * The output channel for the Theory.
+ */
+ OutputChannel* d_out;
+
+ /**
+ * The assertFact() queue.
+ */
+ // FIXME CD: on backjump we clear the facts IFF the queue gets
+ // emptied on every DL. In general I guess we need a CDQueue<>?
+ // Perhaps one that asserts it's empty at each push?
+ std::queue<Node> d_facts;
/**
* Return whether a node is shared or not. Used by setup().
*/
- bool isShared(const Node& n);
+ bool isShared(TNode n) throw();
+
+ /**
+ * Returns true if the assertFact queue is empty
+ */
+ bool done() throw() {
+ return d_facts.empty();
+ }
public:
/**
+ * Destructs a Theory. This implementation does nothing, but we
+ * need a virtual destructor for safety in case subclasses have a
+ * destructor.
+ */
+ virtual ~Theory() {
+ }
+
+ /**
* Subclasses of Theory may add additional efforts. DO NOT CHECK
* equality with one of these values (e.g. if STANDARD xxx) but
* rather use range checks (or use the helper functions below).
@@ -58,20 +124,34 @@ public:
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
- * Construct a Theory.
+ * Set the output channel associated to this theory.
*/
- Theory(context::Context* c) : d_assertions(c), d_nextAssertion(c, 0){}
+ void setOutputChannel(OutputChannel& out) {
+ d_out = &out;
+ }
/**
- * Destructs a Theory. This implementation does nothing, but we
- * need a virtual destructor for safety in case subclasses have a
- * destructor.
+ * Get the output channel associated to this theory.
*/
- virtual ~Theory() {
+ OutputChannel& getOutputChannel() {
+ return *d_out;
+ }
+
+ /**
+ * Get the output channel associated to this theory [const].
+ */
+ const OutputChannel& getOutputChannel() const {
+ return *d_out;
}
/**
- * Prepare for a Node.
+ * Pre-register a term. Done one time for a Node, ever.
+ *
+ */
+ virtual void preRegisterTerm(TNode) = 0;
+
+ /**
+ * Register a term.
*
* When get() is called to get the next thing off the theory queue,
* setup() is called on its subterms (in TheoryEngine). Then setup()
@@ -81,55 +161,189 @@ public:
* setup() MUST NOT MODIFY context-dependent objects that it hasn't
* itself just created.
*/
-
- /*virtual void setup(const Node& n) = 0;*/
-
- virtual void registerTerm(TNode n) = 0;
+ virtual void registerTerm(TNode) = 0;
/**
* Assert a fact in the current context.
*/
- void assertFact(const Node& n);
+ void assertFact(TNode n) {
+ d_facts.push(n);
+ }
/**
* Check the current assignment's consistency.
*/
- virtual void check(OutputChannel& out,
- Effort level = FULL_EFFORT) = 0;
+ virtual void check(Effort level = FULL_EFFORT) = 0;
/**
* T-propagate new literal assignments in the current context.
*/
- virtual void propagate(OutputChannel& out,
- Effort level = FULL_EFFORT) = 0;
+ virtual void propagate(Effort level = FULL_EFFORT) = 0;
/**
* Return an explanation for the literal represented by parameter n
* (which was previously propagated by this theory). Report
* explanations to an output channel.
*/
- virtual void explain(OutputChannel& out,
- const Node& n,
- Effort level = FULL_EFFORT) = 0;
-private:
- context::CDList<Node> d_assertions;
- context::CDO<unsigned> d_nextAssertion;
+ virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
+
+ //
+ // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
+ //
-protected:
/**
- * Returns the next atom in the assertFact() queue.
- * Guarentees that registerTerm is called on the theory specific subterms.
- * @return the next atom in the assertFact() queue.
+ * Different states at which invariants are checked.
*/
- Node get();
+ enum ReadyState {
+ ABOUT_TO_PUSH,
+ ABOUT_TO_POP
+ };/* enum ReadyState */
/**
- * Returns true if the assertFactQueue is empty
+ * Public invariant checker. Assert that this theory is in a valid
+ * state for the (external) system state. This implementation
+ * checks base invariants and then calls theoryReady(). This
+ * function may abort in the case of a failed assert, or return
+ * false (the caller should assert that the return value is true).
+ *
+ * @param s the state about which to check invariants
*/
- bool done();
+ bool ready(ReadyState s) {
+ if(s == ABOUT_TO_PUSH) {
+ Assert(d_facts.empty(), "Theory base code invariant broken: "
+ "fact queue is nonempty on context push");
+ }
+
+ return theoryReady(s);
+ }
+
+protected:
+
+ /**
+ * Check any invariants at the ReadyState given. Only called by
+ * Theory class, and then only with CVC4_ASSERTIONS enabled. This
+ * function may abort in the case of a failed assert, or return
+ * false (the caller should assert that the return value is true).
+ *
+ * @param s the state about which to check invariants
+ */
+ virtual bool theoryReady(ReadyState s) {
+ return true;
+ }
};/* class Theory */
+
+/**
+ * Base class for T-solver implementations. Each individual
+ * implementation T of the Theory interface should inherit from
+ * TheoryImpl<T>. This class specializes some things for a particular
+ * theory implementation.
+ *
+ * The problem with this is that Theory implementations cannot be
+ * further subclassed without designing all non-children in the type
+ * DAG to play the same trick as here (be template-polymorphic in their
+ * most-derived child), linearizing the inheritance hierarchy (viewing
+ * each instantiation separately).
+ */
+template <class T>
+class TheoryImpl : public Theory {
+
+protected:
+
+ /**
+ * Construct a Theory.
+ */
+ TheoryImpl(context::Context* ctxt, OutputChannel& out) :
+ Theory(ctxt, out) {
+ /* FIXME: assert here that a TheoryImpl<T> doesn't already exist
+ * for this NodeManager?? If it does, we're hosed because they'll
+ * share per-theory node attributes. */
+ }
+
+ /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
+ struct Registered {};
+ /** The "registerTerm()-has-been-called" flag on Nodes */
+ typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
+
+ /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
+ struct PreRegistered {};
+ /** The "preRegisterTerm()-has-been-called" flag on Nodes */
+ typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
+
+ /**
+ * Returns the next atom in the assertFact() queue. Guarantees that
+ * registerTerm() has been called on the theory specific subterms.
+ *
+ * @return the next atom in the assertFact() queue.
+ */
+ Node get();
+};/* class TheoryImpl<T> */
+
+template <class T>
+Node TheoryImpl<T>::get() {
+ Warning.printf("testing %s == %s\n", typeid(*this).name(), typeid(T).name());
+ /*Assert(typeid(*this) == typeid(T),
+ "Improper Theory inheritance chain detected.");*/
+
+ Assert( !d_facts.empty(),
+ "Theory::get() called with assertion queue empty!" );
+
+ Node fact = d_facts.front();
+ d_facts.pop();
+
+ if(! fact.getAttribute(RegisteredAttr())) {
+ std::vector<TNode> toReg;
+ toReg.push_back(fact);
+
+ /* Essentially this is doing a breadth-first numbering of
+ * non-registered subterms with children. Any non-registered
+ * leaves are immediately registered. */
+ for(std::vector<TNode>::iterator workp = toReg.begin();
+ workp != toReg.end();
+ ++workp) {
+
+ TNode n = *workp;
+
+ for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+ TNode c = *i;
+
+ if(! c.getAttribute(RegisteredAttr())) {
+ if(c.getNumChildren() == 0) {
+ c.setAttribute(RegisteredAttr(), true);
+ registerTerm(c);
+ } else {
+ toReg.push_back(c);
+ }
+ }
+ }
+ }
+
+ /* Now register the list of terms in reverse order. Between this
+ * and the above registration of leaves, this should ensure that
+ * all subterms in the entire tree were registered in
+ * reverse-topological order. */
+ for(std::vector<TNode>::reverse_iterator i = toReg.rend();
+ i != toReg.rbegin();
+ ++i) {
+
+ TNode n = *i;
+
+ /* Note that a shared TNode in the DAG rooted at "fact" could
+ * appear twice on the list, so we have to avoid hitting it
+ * twice. */
+ // FIXME when ExprSets are online, use one of those to avoid
+ // duplicates in the above?
+ if(! n.getAttribute(RegisteredAttr())) {
+ n.setAttribute(RegisteredAttr(), true);
+ registerTerm(n);
+ }
+ }
+ }
+
+ return fact;
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback