note on setup(); for discussion at 2010.02.11 meeting

diff --git a/src/theory/theory.h b/src/theory/theory.h
index ad89a2aaaba7db62222b797a1f89e6689fe4ff3b..8aa76ea810cf2432ff907b79c99519b607f04421 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -64,6 +64,14 @@ public:
 
   /**
    * Prepare for a Node.
+   *
+   * When get() is called to get the next thing off the theory queue,
+   * setup() is called on its subterms (in TheoryEngine).  Then setup()
+   * is called on this node.
+   *
+   * This is done in a "context escape" -- that is, at context level 0.
+   * setup() MUST NOT MODIFY context-dependent objects that it hasn't
+   * itself just created.
    */
   virtual void setup(const Node& n) = 0;