src/theory/theory.h

   1 /*********************                                           -*- C++ -*-  */
   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 "util/literal.h"
  21 #include "theory/output_channel.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(Node);
  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    * Prepare for a Node.
  68    */
  69   virtual void setup(Node) = 0;
  70
  71   /**
  72    * Assert a literal in the current context.
  73    */
  74   void assertLiteral(Literal);
  75
  76   /**
  77    * Check the current assignment's consistency.
  78    */
  79   virtual void check(OutputChannel& out, Effort level = FULL_EFFORT) = 0;
  80
  81   /**
  82    * T-propagate new literal assignments in the current context.
  83    */
  84   virtual void propagate(OutputChannel& out, Effort level = FULL_EFFORT) = 0;
  85
  86   /**
  87    * Return an explanation for the literal represented by parameter n
  88    * (which was previously propagated by this theory).  Report
  89    * explanations to an output channel.
  90    */
  91   virtual void explain(OutputChannel& out, Node n, Effort level = FULL_EFFORT) = 0;
  92
  93 };/* class Theory */
  94
  95 }/* CVC4::theory namespace */
  96 }/* CVC4 namespace */
  97
  98 #endif /* __CVC4__THEORY__THEORY_H */