note on setup(); for discussion at 2010.02.11 meeting

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index ad89a2aaa..8aa76ea81 100644
--- 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;