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

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.