additional stuff for sharing,

1 files changed, 6 insertions, 24 deletions

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index bf928cb62..f5bf620bf 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -69,59 +69,41 @@ public:
    * assigned false), or else a literal by itself (in the case of a
    * unit conflict) which is assigned TRUE (and T-conflicting) in the
    * current assignment.
-   *
-   * @param safe - whether it is safe to be interrupted
    */
-  virtual void conflict(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) = 0;
+  virtual void conflict(TNode n) throw(AssertionException) = 0;
 
   /**
    * Propagate a theory literal.
    *
    * @param n - a theory consequence at the current decision level
-   * @param safe - whether it is safe to be interrupted
    */
-  virtual void propagate(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) = 0;
+  virtual void propagate(TNode n) throw(AssertionException) = 0;
 
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
    * been detected.  (This requests a split.)
    *
    * @param n - a theory lemma valid at decision level 0
-   * @param safe - whether it is safe to be interrupted
+   * @param removable - whether the lemma can be removed at any point
    */
-  virtual void lemma(TNode n, bool safe = false)
-    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
+  virtual void lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
 
   /**
    * Request a split on a new theory atom.  This is equivalent to
    * calling lemma({OR n (NOT n)}).
    *
    * @param n - a theory atom; must be of Boolean type
-   * @param safe - whether it is safe to be interrupted
    */
-  void split(TNode n, bool safe = false)
-    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) {
+  void split(TNode n) throw(TypeCheckingExceptionPrivate, AssertionException) {
     lemma(n.orNode(n.notNode()));
   }
 
   /**
-   * Provide an explanation in response to an explanation request.
-   *
-   * @param n - an explanation
-   * @param safe - whether it is safe to be interrupted
-   */
-  virtual void explanation(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) = 0;
-
-  /**
    * Notification from a theory that it realizes it is incomplete at
    * this context level.  If SAT is later determined by the
    * TheoryEngine, it should actually return an UNKNOWN result.
    */
-  virtual void setIncomplete()
-    throw(Interrupted, AssertionException) = 0;
+  virtual void setIncomplete() throw(AssertionException) = 0;
 
 };/* class OutputChannel */