precision in theoryskel

diff --git a/AUTHORS b/AUTHORS
index d6ce5a4ff2407162807dfe12c9d20161e29f3277..f5897d574a5a475d0355e44d2827b8d163c926aa 100644 (file)
--- 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 ce07eafb9120fc794b255298a96721763c33520e..e860c5373d07405169a8df77851d0af5d0abd5b2 100644 (file)
--- 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 7441bbc4ebbda9974f79d0db7bdd9113261bd1c2..e6a2e2336f3b27b4c4c82e174a98f2ca9a96ac79 100644 (file)
--- 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,