src/theory/theory.h

   1 /*********************                                                        */
   2 /** theory.h
   3  ** Original author: mdeters
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): dejan
   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 "theory/output_channel.h"
  21 #include "context/context.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 /**
  27  * Base class for T-solvers.  Abstract DPLL(T).
  28  */
  29 class Theory {
  30
  31   /**
  32    * Return whether a node is shared or not.  Used by setup().
  33    */
  34   bool isShared(const Node& n);
  35
  36 public:
  37
  38   /**
  39    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
  40    * equality with one of these values (e.g. if STANDARD xxx) but
  41    * rather use range checks (or use the helper functions below).
  42    * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
  43    * with MAX_EFFORT.
  44    */
  45   enum Effort {
  46     MIN_EFFORT = 0,
  47     QUICK_CHECK = 10,
  48     STANDARD = 50,
  49     FULL_EFFORT = 100
  50   };/* enum Effort */
  51
  52   // TODO add compiler annotation "constant function" here
  53   static bool minEffortOnly(Effort e)        { return e == MIN_EFFORT; }
  54   static bool quickCheckOrMore(Effort e)     { return e >= QUICK_CHECK; }
  55   static bool quickCheckOnly(Effort e)       { return e >= QUICK_CHECK && e < STANDARD; }
  56   static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
  57   static bool standardEffortOnly(Effort e)   { return e >= STANDARD && e < FULL_EFFORT; }
  58   static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
  59
  60   /**
  61    * Construct a Theory.
  62    */
  63   Theory() {
  64   }
  65
  66   /**
  67    * Destructs a Theory.  This implementation does nothing, but we
  68    * need a virtual destructor for safety in case subclasses have a
  69    * destructor.
  70    */
  71   virtual ~Theory() {
  72   }
  73
  74   /**
  75    * Prepare for a Node.
  76    *
  77    * When get() is called to get the next thing off the theory queue,
  78    * setup() is called on its subterms (in TheoryEngine).  Then setup()
  79    * is called on this node.
  80    *
  81    * This is done in a "context escape" -- that is, at context level 0.
  82    * setup() MUST NOT MODIFY context-dependent objects that it hasn't
  83    * itself just created.
  84    */
  85   virtual void setup(const Node& n) = 0;
  86
  87   /**
  88    * Assert a fact in the current context.
  89    */
  90   void assertFact(const Node& n);
  91
  92   /**
  93    * Check the current assignment's consistency.
  94    */
  95   virtual void check(OutputChannel& out,
  96                      Effort level = FULL_EFFORT) = 0;
  97
  98   /**
  99    * T-propagate new literal assignments in the current context.
 100    */
 101   virtual void propagate(OutputChannel& out,
 102                          Effort level = FULL_EFFORT) = 0;
 103
 104   /**
 105    * Return an explanation for the literal represented by parameter n
 106    * (which was previously propagated by this theory).  Report
 107    * explanations to an output channel.
 108    */
 109   virtual void explain(OutputChannel& out,
 110                        const Node& n,
 111                        Effort level = FULL_EFFORT) = 0;
 112
 113 protected:
 114   /**
 115    * Returns the next atom in the assertFact() queue.
 116    * Guarentees that registerTerm is called on the theory specific subterms.
 117    * @return the next atom in the assertFact() queue.
 118    */
 119   Node get();
 120
 121   /**
 122    * Returns true if the assertFactQueue is empty
 123    */
 124   bool done() { return true; }
 125
 126 };/* class Theory */
 127
 128 }/* CVC4::theory namespace */
 129 }/* CVC4 namespace */
 130
 131 #endif /* __CVC4__THEORY__THEORY_H */