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, 28 insertions, 35 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index d0218236d..40f72dafc 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -130,19 +130,19 @@ private:
   TheoryId d_id;
 
   /**
-   * The context for the Theory.
+   * The SAT search context for the Theory.
    */
-  context::Context* d_context;
+  context::Context* d_satContext;
 
   /**
-   * The user context for the Theory.
+   * The user level assertion context for the Theory.
    */
   context::UserContext* d_userContext;
 
   /**
    * Information about the logic we're operating within.
    */
-  const LogicInfo* d_logicInfo;
+  const LogicInfo& d_logicInfo;
 
   /**
    * The assertFact() queue.
@@ -205,19 +205,20 @@ protected:
   /**
    * Construct a Theory.
    */
-  Theory(TheoryId id, context::Context* context, context::UserContext* userContext,
-         OutputChannel& out, Valuation valuation) throw() :
-    d_id(id),
-    d_context(context),
-    d_userContext(userContext),
-    d_facts(context),
-    d_factsHead(context, 0),
-    d_sharedTermsIndex(context, 0),
-    d_careGraph(0),
-    d_computeCareGraphTime(statName(id, "computeCareGraphTime")),
-    d_sharedTerms(context),
-    d_out(&out),
-    d_valuation(valuation)
+  Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
+         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw()
+  : d_id(id)
+  , d_satContext(satContext)
+  , d_userContext(userContext)
+  , d_logicInfo(logicInfo)
+  , d_facts(satContext)
+  , d_factsHead(satContext, 0)
+  , d_sharedTermsIndex(satContext, 0)
+  , d_careGraph(0)
+  , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
+  , d_sharedTerms(satContext)
+  , d_out(&out)
+  , d_valuation(valuation)
   {
     StatisticsRegistry::registerStat(&d_computeCareGraphTime);
   }
@@ -264,7 +265,7 @@ protected:
   }
 
   const LogicInfo& getLogicInfo() const {
-    return *d_logicInfo;
+    return d_logicInfo;
   }
 
   /**
@@ -393,10 +394,10 @@ public:
   }
 
   /**
-   * Get the context associated to this Theory.
+   * Get the SAT context associated to this Theory.
    */
-  context::Context* getContext() const {
-    return d_context;
+  context::Context* getSatContext() const {
+    return d_satContext;
   }
 
   /**
@@ -429,7 +430,7 @@ public:
    * Assert a fact in the current context.
    */
   void assertFact(TNode assertion, bool isPreregistered) {
-    Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_context->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl;
+    Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_satContext->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl;
     d_facts.push_back(Assertion(assertion, isPreregistered));
   }
 
@@ -457,19 +458,6 @@ public:
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
 
   /**
-   * This method is called by the shared term manager when a shared
-   * term lhs which this theory cares about (either because it
-   * received a previous addSharedTerm call with lhs or because it
-   * received a previous notifyEq call with lhs as the second
-   * argument) becomes equal to another shared term rhs.  This call
-   * also serves as notice to the theory that the shared term manager
-   * now considers rhs the representative for this equivalence class
-   * of shared terms, so future notifications for this class will be
-   * based on rhs not lhs.
-   */
-  virtual void notifyEq(TNode lhs, TNode rhs) { }
-
-  /**
    * Check the current assignment's consistency.
    *
    * An implementation of check() is required to either:
@@ -629,6 +617,11 @@ public:
     return set | (1 << theory);
   }
 
+  /** Add the theory to the set. If no set specified, just returns a singleton set */
+  static inline Set setRemove(TheoryId theory, Set set = 0) {
+    return set ^ (1 << theory);
+  }
+
   /** Check if the set contains the theory */
   static inline bool setContains(TheoryId theory, Set set) {
     return set & (1 << theory);