minor changes to Theory

diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 7fa828237c1eb371f55430fc4048336731a904fd..a4c8c41a9c02b7f491f016c55f7d257c6f26a223 100644 (file)
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -27,10 +27,10 @@ class Type;
 // this is essentially a traits structure
 class Type_attr {
 public:
-  
+
   // could use typeid but then different on different machines/compiles
   enum { hash_value = 11 };
-  
+
   typedef Type value_type;//Node?
   static const Type_attr marker;
 };

diff --git a/src/theory/theory.h b/src/theory/theory.h
index b695ca03d47ed3c8dd4d0541a0b8c1e8ecc2c1a4..1372616ecb4db6604a447a92f18c83a8a2470fc2 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -26,6 +26,11 @@ namespace theory {
  * Base class for T-solvers.  Abstract DPLL(T).
  */
 class Theory {
+  /**
+   * Return whether a node is shared or not.  Used by setup().
+   */
+  bool isShared(Node);
+
 public:
   /**
    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
@@ -50,7 +55,7 @@ public:
   static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
 
   /**
-   * Prepare for an Node.
+   * Prepare for a Node.
    */
   virtual void setup(Node) = 0;
 
@@ -77,7 +82,8 @@ public:
   virtual void propagate(Effort level = FULL_EFFORT) = 0;
 
   /**
-   * Return an explanation for the literal (which was previously propagated by this theory)..
+   * Return an explanation for the literal (which was previously
+   * propagated by this theory)..
    */
   virtual Node explain(Literal) = 0;