From 4f0961923bdefbc36377ed37022594fde57be513 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 10 Feb 2010 22:22:14 +0000 Subject: [PATCH] note on setup(); for discussion at 2010.02.11 meeting --- src/theory/theory.h | 8 ++++++++ 1 file changed, 8 insertions(+) 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; -- 2.30.2