diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-15 16:36:49 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-15 16:36:49 +0000 |
commit | e9339ddd445c657fb6ebdd074cdb6091a80825bf (patch) | |
tree | 94c923c8693d39ffe907fd2ad9f531c808413a77 | |
parent | 672c02a79ba691c33955cd7e7c62f932671e845c (diff) |
I made a documentation change to get() to make explicit the contract requirements for 'slurping the queue'. Closes bug 154
-rw-r--r-- | src/theory/theory.h | 6 |
1 files changed, 6 insertions, 0 deletions
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; |