precision in theoryskel

3 files changed, 10 insertions, 2 deletions

diff --git a/AUTHORS b/AUTHORS
index d6ce5a4ff..f5897d574 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,6 +1,7 @@
 The core authors and designers of CVC4 are:
 
   Clark Barrett <barrett@cs.nyu.edu>, New York University
+  François Bobot <bobot@lri.fr>, Paris-Sud University
   Christopher Conway <cconway@cs.nyu.edu>, New York University
   Morgan Deters <mdeters@cs.nyu.edu>, New York University
   Yeting Ge <yeting@cs.nyu.edu>, New York University
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT
index ce07eafb9..e860c5373 100644
--- a/contrib/theoryskel/README.WHATS-NEXT
+++ b/contrib/theoryskel/README.WHATS-NEXT
@@ -16,7 +16,14 @@ Your next steps will likely be:
 and finally:
 
 * to implement a decision procedure for your theory by implementing
-  Theory$camel::check() in theory_$dir.cpp
+  Theory$camel::check() in theory_$dir.cpp. Before writing the actual
+  code, you will need :
+
+  * to determine which datastructures are context dependent and use for them
+    context dependent datastructures (context/cd*.h)
+  * to choose which work will be done at QUICK_CHECK, STANDARD or at
+    FULL_EFFORT.
+
 
 Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance
 should you need it!
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 7441bbc4e..e6a2e2336 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -306,7 +306,7 @@ public:
    * equality with one of these values (e.g. if STANDARD xxx) but
    * rather use range checks (or use the helper functions below).
    * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
-   * with MAX_EFFORT.
+   * with FULL_EFFORT.
    */
   enum Effort {
     MIN_EFFORT = 0,