src/theory/output_channel.h

   1 /*********************                                                        */
   2 /** output_channel.h
   3  ** Original author: mdeters
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): none
   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  ** The theory output channel interface.
  14  **/
  15
  16 #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
  17 #define __CVC4__THEORY__OUTPUT_CHANNEL_H
  18
  19 #include "theory/interrupted.h"
  20
  21 namespace CVC4 {
  22 namespace theory {
  23
  24 /**
  25  * Generic "theory output channel" interface.
  26  */
  27 class OutputChannel {
  28 public:
  29
  30   /**
  31    * Destructs an OutputChannel.  This implementation does nothing,
  32    * but we need a virtual destructor for safety in case subclasses
  33    * have a destructor.
  34    */
  35   virtual ~OutputChannel() {
  36   }
  37
  38   /**
  39    * With safePoint(), the theory signals that it is at a safe point
  40    * and can be interrupted.
  41    */
  42   virtual void safePoint() throw(Interrupted&) {
  43   }
  44
  45   /**
  46    * Indicate a theory conflict has arisen.
  47    *
  48    * @param n - a conflict at the current decision level
  49    * @param safe - whether it is safe to be interrupted
  50    */
  51   virtual void conflict(Node n, bool safe = false) throw(Interrupted&) = 0;
  52
  53   /**
  54    * Propagate a theory literal.
  55    *
  56    * @param n - a theory consequence at the current decision level
  57    * @param safe - whether it is safe to be interrupted
  58    */
  59   virtual void propagate(Node n, bool safe = false) throw(Interrupted&) = 0;
  60
  61   /**
  62    * Tell the core that a valid theory lemma at decision level 0 has
  63    * been detected.  (This request a split.)
  64    *
  65    * @param n - a theory lemma valid at decision level 0
  66    * @param safe - whether it is safe to be interrupted
  67    */
  68   virtual void lemma(Node n, bool safe = false) throw(Interrupted&) = 0;
  69
  70 };/* class OutputChannel */
  71
  72 /**
  73  * Generic "theory output channel" interface for explanations.
  74  */
  75 class ExplainOutputChannel {
  76 public:
  77
  78   /**
  79    * Destructs an ExplainOutputChannel.  This implementation does
  80    * nothing, but we need a virtual destructor for safety in case
  81    * subclasses have a destructor.
  82    */
  83   virtual ~ExplainOutputChannel() {
  84   }
  85
  86   /**
  87    * With safePoint(), the theory signals that it is at a safe point
  88    * and can be interrupted.  The default implementation never
  89    * interrupts.
  90    */
  91   virtual void safePoint() throw(Interrupted&) {
  92   }
  93
  94   /**
  95    * Provide an explanation in response to an explanation request.
  96    *
  97    * @param n - an explanation
  98    * @param safe - whether it is safe to be interrupted
  99    */
 100   virtual void explanation(Node n, bool safe = false) throw(Interrupted&) = 0;
 101 };/* class ExplainOutputChannel */
 102
 103 }/* CVC4::theory namespace */
 104 }/* CVC4 namespace */
 105
 106 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */