diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 13:01:02 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 13:02:46 -0400 |
commit | 7f13c0713accdefa46ce2a43dbeae8c46255bea1 (patch) | |
tree | 13110353d5a45c0970e1fc4928f863e45c732e50 /src/theory/term_registration_visitor.h | |
parent | 315eb7e44cada64fd9b8a2b4ab9b9cac66758769 (diff) |
Fix erroneous results when the logic was incorrectly specified (by throwing LogicException). Also correct a case where sharing was doing some work during pure theory solving.
Diffstat (limited to 'src/theory/term_registration_visitor.h')
-rw-r--r-- | src/theory/term_registration_visitor.h | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 768508d2c..478e82d19 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -55,25 +55,19 @@ class PreRegisterVisitor { theory::Theory::Set d_theories; /** - * Is true if the term we're traversing involves multiple theories. - */ - bool d_multipleTheories; - - /** * String representation of the visited map, for debugging purposes. */ std::string toString() const; public: - /** Return type tells us if there are more than one theory or not */ - typedef bool return_type; + /** Returned set tells us which theories there are */ + typedef theory::Theory::Set return_type; PreRegisterVisitor(TheoryEngine* engine, context::Context* context) : d_engine(engine) , d_visited(context) , d_theories(0) - , d_multipleTheories(false) {} /** @@ -89,13 +83,12 @@ public: /** * Marks the node as the starting literal. */ - void start(TNode node); + void start(TNode node) { } /** * Notifies the engine of all the theories used. */ - bool done(TNode node); - + theory::Theory::Set done(TNode node) { return d_theories; } }; |