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