diff options
Diffstat (limited to 'src/theory/term_registration_visitor.h')
-rw-r--r-- | src/theory/term_registration_visitor.h | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 11a56ec1e..ac3494193 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -26,7 +26,15 @@ namespace CVC4 { class TheoryEngine; /** - * Visitor that calls the apropriate theory to preregister the term. + * Visitor that calls the appropriate theory to pre-register the term. The visitor also keeps track + * of the sets of theories that are involved in the terms, so that it can say if there are multiple + * theories involved. + * + * A sub-term has been visited if the theories of both the parent and the term itself have already + * visited this term. + * + * Computation of the set of theories in the original term are computed in the alreadyVisited method + * so as no to skip any theories. */ class PreRegisterVisitor { @@ -41,9 +49,9 @@ class PreRegisterVisitor { TNodeToTheorySetMap d_visited; /** - * Map from terms to the theories that have have a sub-term in it. + * A set of all theories in the term */ - TNodeToTheorySetMap d_theories; + theory::Theory::Set d_theories; /** * Is true if the term we're traversing involves multiple theories. @@ -63,7 +71,7 @@ public: PreRegisterVisitor(TheoryEngine* engine, context::Context* context) : d_engine(engine) , d_visited(context) - , d_theories(context) + , d_theories(0) , d_multipleTheories(false) {} |