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   /** Disallow copying: private constructor */
  29   OutputChannel(const OutputChannel&);
  30
  31   /** Disallow assignment: private operator=() */
  32   OutputChannel& operator=(const OutputChannel&);
  33
  34 public:
  35
  36   /**
  37    * Construct an OutputChannel.
  38    */
  39   OutputChannel() {
  40   }
  41
  42   /**
  43    * Destructs an OutputChannel.  This implementation does nothing,
  44    * but we need a virtual destructor for safety in case subclasses
  45    * have a destructor.
  46    */
  47   virtual ~OutputChannel() {
  48   }
  49
  50   /**
  51    * With safePoint(), the theory signals that it is at a safe point
  52    * and can be interrupted.
  53    */
  54   virtual void safePoint() throw(Interrupted) {
  55   }
  56
  57   /**
  58    * Indicate a theory conflict has arisen.
  59    *
  60    * @param n - a conflict at the current decision level.  This should
  61    * be an AND-kinded node of literals that are TRUE in the current
  62    * assignment and are in conflict (i.e., at least one must be
  63    * assigned false).
  64    *
  65    * @param safe - whether it is safe to be interrupted
  66    */
  67   virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0;
  68
  69   /**
  70    * Propagate a theory literal.
  71    *
  72    * @param n - a theory consequence at the current decision level.
  73    *
  74    * @param safe - whether it is safe to be interrupted
  75    */
  76   virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0;
  77
  78   /**
  79    * Tell the core that a valid theory lemma at decision level 0 has
  80    * been detected.  (This request a split.)
  81    *
  82    * @param n - a theory lemma valid at decision level 0
  83    * @param safe - whether it is safe to be interrupted
  84    */
  85   virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0;
  86
  87   /**
  88    * Provide an explanation in response to an explanation request.
  89    *
  90    * @param n - an explanation
  91    * @param safe - whether it is safe to be interrupted
  92    */
  93   virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0;
  94
  95 };/* class OutputChannel */
  96
  97 }/* CVC4::theory namespace */
  98 }/* CVC4 namespace */
  99
 100 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */