diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-01-19 15:10:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-01-19 15:10:49 +0000 |
commit | 5fcb5f9b5c9aa0f13b477c67d6d34f5b28ccb63d (patch) | |
tree | b8d39300912b138e559366f0d3dc2db9481fefb8 /src/theory/theory.h | |
parent | 1b16b221af56d12dfa88497f8a72eda5ad977f7d (diff) |
minor changes to Theory
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 10 |
1 files changed, 8 insertions, 2 deletions
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; |