From: Tim King <taking@cs.nyu.edu>
Date: Tue, 15 Jun 2010 16:36:49 +0000 (+0000)
Subject: I made a documentation change to get() to make explicit the contract requirements... 
X-Git-Tag: cvc5-1.0.0~8988
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e9339ddd445c657fb6ebdd074cdb6091a80825bf;p=cvc5.git

I made a documentation change to get() to make explicit the contract requirements for 'slurping the queue'. Closes bug 154
---

diff --git a/src/theory/theory.h b/src/theory/theory.h
index bdd695cdd..1bf6f660c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -264,6 +264,12 @@ public:
 
   /**
    * Check the current assignment's consistency.
+   *
+   * An implementation of check() is required to either:
+   * - return a conflict on the output channel,
+   * - be interrupted,
+   * - throw an exception
+   * - or call get() until done() is true.
    */
   virtual void check(Effort level = FULL_EFFORT) = 0;