diff options
-rw-r--r-- | src/theory/theory.h | 8 |
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; |