src/theory/output_channel.h

   1 /*********************                                                        */
   2 /*! \file output_channel.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): taking, barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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 The theory output channel interface
  15  **
  16  ** The theory output channel interface.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
  22 #define __CVC4__THEORY__OUTPUT_CHANNEL_H
  23
  24 #include "util/Assert.h"
  25 #include "theory/interrupted.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 /**
  31  * Generic "theory output channel" interface.
  32  */
  33 class OutputChannel {
  34   /** Disallow copying: private constructor */
  35   OutputChannel(const OutputChannel&) CVC4_UNDEFINED;
  36
  37   /** Disallow assignment: private operator=() */
  38   OutputChannel& operator=(const OutputChannel&) CVC4_UNDEFINED;
  39
  40 public:
  41
  42   /**
  43    * Construct an OutputChannel.
  44    */
  45   OutputChannel() {
  46   }
  47
  48   /**
  49    * Destructs an OutputChannel.  This implementation does nothing,
  50    * but we need a virtual destructor for safety in case subclasses
  51    * have a destructor.
  52    */
  53   virtual ~OutputChannel() {
  54   }
  55
  56   /**
  57    * With safePoint(), the theory signals that it is at a safe point
  58    * and can be interrupted.
  59    */
  60   virtual void safePoint() throw(Interrupted, AssertionException) {
  61   }
  62
  63   /**
  64    * Indicate a theory conflict has arisen.
  65    *
  66    * @param n - a conflict at the current decision level.  This should
  67    * be an AND-kinded node of literals that are TRUE in the current
  68    * assignment and are in conflict (i.e., at least one must be
  69    * assigned false), or else a literal by itself (in the case of a
  70    * unit conflict) which is assigned TRUE (and T-conflicting) in the
  71    * current assignment.
  72    */
  73   virtual void conflict(TNode n) throw(AssertionException) = 0;
  74
  75   /**
  76    * Propagate a theory literal.
  77    *
  78    * @param n - a theory consequence at the current decision level
  79    */
  80   virtual void propagate(TNode n) throw(AssertionException) = 0;
  81
  82   /**
  83    * Tell the core that a valid theory lemma at decision level 0 has
  84    * been detected.  (This requests a split.)
  85    *
  86    * @param n - a theory lemma valid at decision level 0
  87    * @param removable - whether the lemma can be removed at any point
  88    */
  89   virtual void lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
  90
  91   /**
  92    * Request a split on a new theory atom.  This is equivalent to
  93    * calling lemma({OR n (NOT n)}).
  94    *
  95    * @param n - a theory atom; must be of Boolean type
  96    */
  97   void split(TNode n) throw(TypeCheckingExceptionPrivate, AssertionException) {
  98     lemma(n.orNode(n.notNode()));
  99   }
 100
 101   /**
 102    * Notification from a theory that it realizes it is incomplete at
 103    * this context level.  If SAT is later determined by the
 104    * TheoryEngine, it should actually return an UNKNOWN result.
 105    */
 106   virtual void setIncomplete() throw(AssertionException) = 0;
 107
 108 };/* class OutputChannel */
 109
 110 }/* CVC4::theory namespace */
 111 }/* CVC4 namespace */
 112
 113 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */