From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 10 Feb 2010 22:22:14 +0000 (+0000)
Subject: note on setup(); for discussion at 2010.02.11 meeting
X-Git-Tag: cvc5-1.0.0~9261
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f0961923bdefbc36377ed37022594fde57be513;p=cvc5.git

note on setup(); for discussion at 2010.02.11 meeting
---

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;