From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 19 Jan 2010 15:10:49 +0000 (+0000)
Subject: minor changes to Theory
X-Git-Tag: cvc5-1.0.0~9345
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5fcb5f9b5c9aa0f13b477c67d6d34f5b28ccb63d;p=cvc5.git

minor changes to Theory
---

diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 7fa828237..a4c8c41a9 100644
--- 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 b695ca03d..1372616ec 100644
--- 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;