summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-01-19 15:10:49 +0000
committerMorgan Deters <mdeters@gmail.com>2010-01-19 15:10:49 +0000
commit5fcb5f9b5c9aa0f13b477c67d6d34f5b28ccb63d (patch)
treeb8d39300912b138e559366f0d3dc2db9481fefb8 /src
parent1b16b221af56d12dfa88497f8a72eda5ad977f7d (diff)
minor changes to Theory
Diffstat (limited to 'src')
-rw-r--r--src/expr/attr_type.h4
-rw-r--r--src/theory/theory.h10
2 files changed, 10 insertions, 4 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback