src/theory/theory.h

   1 /*********************                                                        */
   2 /** theory.h
   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
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Base of the theory interface.
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef __CVC4__THEORY__THEORY_H
  19 #define __CVC4__THEORY__THEORY_H
  20
  21 #include "expr/node.h"
  22 #include "expr/attribute.h"
  23 #include "theory/output_channel.h"
  24 #include "context/context.h"
  25
  26 #include <queue>
  27 #include <list>
  28
  29 #include <typeinfo>
  30
  31 namespace CVC4 {
  32 namespace theory {
  33
  34 template <class T>
  35 class TheoryImpl;
  36
  37 /**
  38  * Base class for T-solvers.  Abstract DPLL(T).
  39  *
  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
  43  * for that theory.
  44  */
  45 class Theory {
  46 private:
  47
  48   template <class T>
  49   friend class TheoryImpl;
  50
  51   /**
  52    * Construct a Theory.
  53    */
  54   Theory(context::Context* ctxt, OutputChannel& out) throw() :
  55     d_context(ctxt),
  56     d_out(&out) {
  57   }
  58
  59   /**
  60    * Disallow default construction.
  61    */
  62   Theory();
  63
  64 protected:
  65
  66   /**
  67    * The output channel for the Theory.
  68    */
  69   context::Context* d_context;
  70
  71   /**
  72    * The output channel for the Theory.
  73    */
  74   OutputChannel* d_out;
  75
  76   /**
  77    * The assertFact() queue.
  78    */
  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;
  83
  84   /**
  85    * Return whether a node is shared or not.  Used by setup().
  86    */
  87   bool isShared(TNode n) throw();
  88
  89   /**
  90    * Returns true if the assertFact queue is empty
  91    */
  92   bool done() throw() {
  93     return d_facts.empty();
  94   }
  95
  96 public:
  97
  98   /**
  99    * Destructs a Theory.  This implementation does nothing, but we
 100    * need a virtual destructor for safety in case subclasses have a
 101    * destructor.
 102    */
 103   virtual ~Theory() {
 104   }
 105
 106   /**
 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
 111    * with MAX_EFFORT.
 112    */
 113   enum Effort {
 114     MIN_EFFORT = 0,
 115     QUICK_CHECK = 10,
 116     STANDARD = 50,
 117     FULL_EFFORT = 100
 118   };/* enum Effort */
 119
 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; }
 127
 128   /**
 129    * Set the output channel associated to this theory.
 130    */
 131   void setOutputChannel(OutputChannel& out) {
 132     d_out = &out;
 133   }
 134
 135   /**
 136    * Get the output channel associated to this theory.
 137    */
 138   OutputChannel& getOutputChannel() {
 139     return *d_out;
 140   }
 141
 142   /**
 143    * Get the output channel associated to this theory [const].
 144    */
 145   const OutputChannel& getOutputChannel() const {
 146     return *d_out;
 147   }
 148
 149   /**
 150    * Pre-register a term.  Done one time for a Node, ever.
 151    *
 152    */
 153   virtual void preRegisterTerm(TNode) = 0;
 154
 155   /**
 156    * Register a term.
 157    *
 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.
 161    *
 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.
 165    */
 166   virtual void registerTerm(TNode) = 0;
 167
 168   /**
 169    * Assert a fact in the current context.
 170    */
 171   void assertFact(TNode n) {
 172     Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl;
 173     d_facts.push(n);
 174   }
 175
 176   /**
 177    * Check the current assignment's consistency.
 178    */
 179   virtual void check(Effort level = FULL_EFFORT) = 0;
 180
 181   /**
 182    * T-propagate new literal assignments in the current context.
 183    */
 184   virtual void propagate(Effort level = FULL_EFFORT) = 0;
 185
 186   /**
 187    * Return an explanation for the literal represented by parameter n
 188    * (which was previously propagated by this theory).  Report
 189    * explanations to an output channel.
 190    */
 191   virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
 192
 193   //
 194   // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
 195   //
 196
 197   /**
 198    * Different states at which invariants are checked.
 199    */
 200   enum ReadyState {
 201     ABOUT_TO_PUSH,
 202     ABOUT_TO_POP
 203   };/* enum ReadyState */
 204
 205   /**
 206    * Public invariant checker.  Assert that this theory is in a valid
 207    * state for the (external) system state.  This implementation
 208    * checks base invariants and then calls theoryReady().  This
 209    * function may abort in the case of a failed assert, or return
 210    * false (the caller should assert that the return value is true).
 211    *
 212    * @param s the state about which to check invariants
 213    */
 214   bool ready(ReadyState s) {
 215     if(s == ABOUT_TO_PUSH) {
 216       Assert(d_facts.empty(), "Theory base code invariant broken: "
 217              "fact queue is nonempty on context push");
 218     }
 219
 220     return theoryReady(s);
 221   }
 222
 223 protected:
 224
 225   /**
 226    * Check any invariants at the ReadyState given.  Only called by
 227    * Theory class, and then only with CVC4_ASSERTIONS enabled.  This
 228    * function may abort in the case of a failed assert, or return
 229    * false (the caller should assert that the return value is true).
 230    *
 231    * @param s the state about which to check invariants
 232    */
 233   virtual bool theoryReady(ReadyState s) {
 234     return true;
 235   }
 236
 237 };/* class Theory */
 238
 239
 240 /**
 241  * Base class for T-solver implementations.  Each individual
 242  * implementation T of the Theory interface should inherit from
 243  * TheoryImpl<T>.  This class specializes some things for a particular
 244  * theory implementation.
 245  *
 246  * The problem with this is that Theory implementations cannot be
 247  * further subclassed without designing all non-children in the type
 248  * DAG to play the same trick as here (be template-polymorphic in their
 249  * most-derived child), linearizing the inheritance hierarchy (viewing
 250  * each instantiation separately).
 251  */
 252 template <class T>
 253 class TheoryImpl : public Theory {
 254
 255 protected:
 256
 257   /**
 258    * Construct a Theory.
 259    */
 260   TheoryImpl(context::Context* ctxt, OutputChannel& out) :
 261     Theory(ctxt, out) {
 262     /* FIXME: assert here that a TheoryImpl<T> doesn't already exist
 263      * for this NodeManager??  If it does, we're hosed because they'll
 264      * share per-theory node attributes. */
 265   }
 266
 267   /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
 268   struct Registered {};
 269   /** The "registerTerm()-has-been-called" flag on Nodes */
 270   typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
 271
 272   /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
 273   struct PreRegistered {};
 274   /** The "preRegisterTerm()-has-been-called" flag on Nodes */
 275   typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
 276
 277   /**
 278    * Returns the next atom in the assertFact() queue.  Guarantees that
 279    * registerTerm() has been called on the theory specific subterms.
 280    *
 281    * @return the next atom in the assertFact() queue.
 282    */
 283   Node get();
 284 };/* class TheoryImpl<T> */
 285
 286 template <class T>
 287 Node TheoryImpl<T>::get() {
 288   Assert(typeid(*this) == typeid(T),
 289          "Improper Theory inheritance chain detected.");
 290
 291   Assert( !d_facts.empty(),
 292           "Theory::get() called with assertion queue empty!" );
 293
 294   Node fact = d_facts.front();
 295   d_facts.pop();
 296
 297   Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl;
 298
 299   if(! fact.getAttribute(RegisteredAttr())) {
 300     std::list<TNode> toReg;
 301     toReg.push_back(fact);
 302
 303     Debug("theory") << "Theory::get(): registering new atom" << std::endl;
 304
 305     /* Essentially this is doing a breadth-first numbering of
 306      * non-registered subterms with children.  Any non-registered
 307      * leaves are immediately registered. */
 308     for(std::list<TNode>::iterator workp = toReg.begin();
 309         workp != toReg.end();
 310         ++workp) {
 311
 312       TNode n = *workp;
 313
 314       for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
 315         TNode c = *i;
 316
 317         if(! c.getAttribute(RegisteredAttr())) {
 318           if(c.getNumChildren() == 0) {
 319             c.setAttribute(RegisteredAttr(), true);
 320             registerTerm(c);
 321           } else {
 322             toReg.push_back(c);
 323           }
 324         }
 325       }
 326     }
 327
 328     /* Now register the list of terms in reverse order.  Between this
 329      * and the above registration of leaves, this should ensure that
 330      * all subterms in the entire tree were registered in
 331      * reverse-topological order. */
 332     for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
 333         i != toReg.rend();
 334         ++i) {
 335
 336       TNode n = *i;
 337
 338       /* Note that a shared TNode in the DAG rooted at "fact" could
 339        * appear twice on the list, so we have to avoid hitting it
 340        * twice. */
 341       // FIXME when ExprSets are online, use one of those to avoid
 342       // duplicates in the above?
 343       if(! n.getAttribute(RegisteredAttr())) {
 344         n.setAttribute(RegisteredAttr(), true);
 345         registerTerm(n);
 346       }
 347     }
 348   }
 349
 350   return fact;
 351 }
 352
 353 }/* CVC4::theory namespace */
 354 }/* CVC4 namespace */
 355
 356 #endif /* __CVC4__THEORY__THEORY_H */