From 4f0961923bdefbc36377ed37022594fde57be513 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 10 Feb 2010 22:22:14 +0000
Subject: note on setup(); for discussion at 2010.02.11 meeting

---
 src/theory/theory.h | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src')

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;
 
-- 
cgit v1.2.3