diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-10 22:22:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-10 22:22:14 +0000 |
commit | 4f0961923bdefbc36377ed37022594fde57be513 (patch) | |
tree | 4b8a119f2aee64a6dae565f6b2440d88a5434508 /src/theory | |
parent | c449010208acb1f7a98e2eee722e71b7db472547 (diff) |
note on setup(); for discussion at 2010.02.11 meeting
Diffstat (limited to 'src/theory')
-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; |