diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
commit | 1433806056059339dd16ae8e431feaae23553150 (patch) | |
tree | cf678baa687b1a19e479c28a1c01470bb2f120c7 /src/theory/term_registration_visitor.h | |
parent | 8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (diff) |
Some cleanup starting off from trying to understand the sharing code. Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor
Diffstat (limited to 'src/theory/term_registration_visitor.h')
-rw-r--r-- | src/theory/term_registration_visitor.h | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 74b756a03..11a56ec1e 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -33,26 +33,27 @@ class PreRegisterVisitor { /** The engine */ TheoryEngine* d_engine; + typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeToTheorySetMap; + /** - * Map from nodes to the theories that have already seen them. + * Map from terms to the theories that have already had this term pre-registered. */ - typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; - TNodeVisitedMap d_visited; + TNodeToTheorySetMap d_visited; /** - * All the theories of the visitation. + * Map from terms to the theories that have have a sub-term in it. */ - theory::Theory::Set d_theories; + TNodeToTheorySetMap d_theories; /** - * String representation of the visited map, for debugging purposes. + * Is true if the term we're traversing involves multiple theories. */ - std::string toString() const; + bool d_multipleTheories; /** - * Is there more than one theory involved. + * String representation of the visited map, for debugging purposes. */ - bool d_multipleTheories; + std::string toString() const; public: @@ -60,12 +61,16 @@ public: typedef bool return_type; PreRegisterVisitor(TheoryEngine* engine, context::Context* context) - : d_engine(engine), d_visited(context), d_theories(0) {} + : d_engine(engine) + , d_visited(context) + , d_theories(context) + , d_multipleTheories(false) + {} /** * Returns true is current has already been pre-registered with both current and parent theories. */ - bool alreadyVisited(TNode current, TNode parent) const; + bool alreadyVisited(TNode current, TNode parent); /** * Pre-registeres current with any of the current and parent theories that haven't seen the term yet. |