src/theory/theory.h

   1 /*********************                                                        */
   2 /*! \file theory.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief Base of the theory interface.
  15  **
  16  ** Base of the theory interface.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__THEORY_H
  22 #define __CVC4__THEORY__THEORY_H
  23
  24 #include "expr/node.h"
  25 #include "expr/attribute.h"
  26 #include "theory/output_channel.h"
  27 #include "context/context.h"
  28
  29 #include <deque>
  30 #include <list>
  31
  32 #include <typeinfo>
  33
  34 namespace CVC4 {
  35
  36 class TheoryEngine;
  37
  38 namespace theory {
  39
  40 // rewrite cache support
  41 struct RewriteCacheTag {};
  42 typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache;
  43
  44 /**
  45  * Base class for T-solvers.  Abstract DPLL(T).
  46  *
  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
  52  * all calls to them.)
  53  */
  54 class Theory {
  55 private:
  56
  57   friend class ::CVC4::TheoryEngine;
  58
  59   /**
  60    * Disallow default construction.
  61    */
  62   Theory();
  63
  64   /**
  65    * The context for the Theory.
  66    */
  67   context::Context* d_context;
  68
  69   /**
  70    * The assertFact() queue.
  71    *
  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).
  75    *
  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?).
  79    */
  80   std::deque<TNode> d_facts;
  81
  82   /** Helper class to reset the fact queue on pop(). */
  83   class FactsResetter : public context::ContextNotifyObj {
  84     Theory& d_thy;
  85
  86   public:
  87     FactsResetter(Theory& thy) :
  88       context::ContextNotifyObj(thy.d_context),
  89       d_thy(thy) {
  90     }
  91
  92     void notify() {
  93       d_thy.d_facts.clear();
  94     }
  95   } d_factsResetter;
  96
  97   friend class FactsResetter;
  98
  99 protected:
 100
 101   /**
 102    * Construct a Theory.
 103    */
 104   Theory(context::Context* ctxt, OutputChannel& out) throw() :
 105     d_context(ctxt),
 106     d_facts(),
 107     d_factsResetter(*this),
 108     d_out(&out) {
 109   }
 110
 111   /**
 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()
 118    * too.
 119    */
 120   virtual void shutdown() {
 121     d_facts.clear();
 122   }
 123
 124   context::Context* getContext() const {
 125     return d_context;
 126   }
 127
 128   /**
 129    * The output channel for the Theory.
 130    */
 131   OutputChannel* d_out;
 132
 133   /**
 134    * Returns true if the assertFact queue is empty
 135    */
 136   bool done() throw() {
 137     return d_facts.empty();
 138   }
 139
 140   /**
 141    * Return whether a node is shared or not.  Used by setup().
 142    */
 143   bool isShared(TNode n) throw();
 144
 145   /**
 146    * Check whether a node is in the rewrite cache or not.
 147    */
 148   static bool inRewriteCache(TNode n) throw() {
 149     return n.hasAttribute(RewriteCache());
 150   }
 151
 152   /**
 153    * Get the value of the rewrite cache (or Node::null()) if there is
 154    * none).
 155    */
 156   static Node getRewriteCache(TNode n) throw() {
 157     return n.getAttribute(RewriteCache());
 158   }
 159
 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;
 164
 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;
 169
 170   /**
 171    * Returns the next atom in the assertFact() queue.  Guarantees that
 172    * registerTerm() has been called on the theory specific subterms.
 173    *
 174    * @return the next atom in the assertFact() queue.
 175    */
 176   Node get();
 177
 178 public:
 179
 180   /**
 181    * Destructs a Theory.  This implementation does nothing, but we
 182    * need a virtual destructor for safety in case subclasses have a
 183    * destructor.
 184    */
 185   virtual ~Theory() {
 186   }
 187
 188   /**
 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
 193    * with MAX_EFFORT.
 194    */
 195   enum Effort {
 196     MIN_EFFORT = 0,
 197     QUICK_CHECK = 10,
 198     STANDARD = 50,
 199     FULL_EFFORT = 100
 200   };/* enum Effort */
 201
 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; }
 209
 210   /**
 211    * Set the output channel associated to this theory.
 212    */
 213   void setOutputChannel(OutputChannel& out) {
 214     d_out = &out;
 215   }
 216
 217   /**
 218    * Get the output channel associated to this theory.
 219    */
 220   OutputChannel& getOutputChannel() {
 221     return *d_out;
 222   }
 223
 224   /**
 225    * Get the output channel associated to this theory [const].
 226    */
 227   const OutputChannel& getOutputChannel() const {
 228     return *d_out;
 229   }
 230
 231   /**
 232    * Pre-register a term.  Done one time for a Node, ever.
 233    *
 234    */
 235   virtual void preRegisterTerm(TNode) = 0;
 236
 237   /**
 238    * Rewrite a term.  Done one time for a Node, ever.
 239    */
 240   virtual Node rewrite(TNode n) {
 241     return n;
 242   }
 243
 244   /**
 245    * Register a term.
 246    *
 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.
 250    *
 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.
 254    */
 255   virtual void registerTerm(TNode) = 0;
 256
 257   /**
 258    * Assert a fact in the current context.
 259    */
 260   void assertFact(TNode n) {
 261     Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl;
 262     d_facts.push_back(n);
 263   }
 264
 265   /**
 266    * Check the current assignment's consistency.
 267    *
 268    * An implementation of check() is required to either:
 269    * - return a conflict on the output channel,
 270    * - be interrupted,
 271    * - throw an exception
 272    * - or call get() until done() is true.
 273    */
 274   virtual void check(Effort level = FULL_EFFORT) = 0;
 275
 276   /**
 277    * T-propagate new literal assignments in the current context.
 278    */
 279   virtual void propagate(Effort level = FULL_EFFORT) = 0;
 280
 281   /**
 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.
 285    */
 286   virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
 287
 288   //
 289   // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
 290   //
 291
 292   /**
 293    * Different states at which invariants are checked.
 294    */
 295   enum ReadyState {
 296     ABOUT_TO_PUSH,
 297     ABOUT_TO_POP
 298   };/* enum ReadyState */
 299
 300   /**
 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).
 306    *
 307    * @param s the state about which to check invariants
 308    */
 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");
 313     }
 314
 315     return theoryReady(s);
 316   }
 317
 318 protected:
 319
 320   /**
 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).
 325    *
 326    * @param s the state about which to check invariants
 327    */
 328   virtual bool theoryReady(ReadyState s) {
 329     return true;
 330   }
 331
 332 };/* class Theory */
 333
 334 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
 335
 336 }/* CVC4::theory namespace */
 337 }/* CVC4 namespace */
 338
 339 #endif /* __CVC4__THEORY__THEORY_H */