src/theory/output_channel.h

   1 /*********************                                                        */
   2 /*! \file output_channel.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: taking
   6  ** Minor contributors (to current version): barrett
   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 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    * Notify the OutputChannel that a new fact has been received by
  58    * the theory.
  59    */
  60   virtual void newFact(TNode n) { }
  61
  62   /**
  63    * With safePoint(), the theory signals that it is at a safe point
  64    * and can be interrupted.
  65    */
  66   virtual void safePoint() throw(Interrupted, AssertionException) {
  67   }
  68
  69   /**
  70    * Indicate a theory conflict has arisen.
  71    *
  72    * @param n - a conflict at the current decision level.  This should
  73    * be an AND-kinded node of literals that are TRUE in the current
  74    * assignment and are in conflict (i.e., at least one must be
  75    * assigned false).
  76    *
  77    * @param safe - whether it is safe to be interrupted
  78    */
  79   virtual void conflict(TNode n, bool safe = false)
  80     throw(Interrupted, AssertionException) = 0;
  81
  82   /**
  83    * Propagate a theory literal.
  84    *
  85    * @param n - a theory consequence at the current decision level.
  86    *
  87    * @param safe - whether it is safe to be interrupted
  88    */
  89   virtual void propagate(TNode n, bool safe = false)
  90     throw(Interrupted, AssertionException) = 0;
  91
  92   /**
  93    * Tell the core that a valid theory lemma at decision level 0 has
  94    * been detected.  (This request a split.)
  95    *
  96    * @param n - a theory lemma valid at decision level 0
  97    * @param safe - whether it is safe to be interrupted
  98    */
  99   virtual void lemma(TNode n, bool safe = false)
 100     throw(Interrupted, AssertionException) = 0;
 101
 102   /**
 103    * Provide an explanation in response to an explanation request.
 104    *
 105    * @param n - an explanation
 106    * @param safe - whether it is safe to be interrupted
 107    */
 108   virtual void explanation(TNode n, bool safe = false)
 109     throw(Interrupted, AssertionException) = 0;
 110
 111   /**
 112    * Notification from a theory that it realizes it is incomplete at
 113    * this context level.  If SAT is later determined by the
 114    * TheoryEngine, it should actually return an UNKNOWN result.
 115    */
 116   virtual void setIncomplete()
 117     throw(Interrupted, AssertionException) = 0;
 118
 119 };/* class OutputChannel */
 120
 121 }/* CVC4::theory namespace */
 122 }/* CVC4 namespace */
 123
 124 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */