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