diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-04 23:59:41 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-04 23:59:41 +0000 |
commit | b21aad9f82edd1f0241579bf2f1f8cd870eb582b (patch) | |
tree | 68622fe26ba2609deb302118102e06921dba43d0 /src/theory | |
parent | 7b3ae98cc2cd9b70e0e00ab07418e796a87e3f97 (diff) |
minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory.h | 19 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 20 |
2 files changed, 31 insertions, 8 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 8daa0149f..ad89a2aaa 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -17,7 +17,6 @@ #define __CVC4__THEORY__THEORY_H #include "expr/node.h" -#include "util/literal.h" #include "theory/output_channel.h" namespace CVC4 { @@ -31,7 +30,7 @@ class Theory { /** * Return whether a node is shared or not. Used by setup(). */ - bool isShared(Node); + bool isShared(const Node& n); public: @@ -66,29 +65,33 @@ public: /** * Prepare for a Node. */ - virtual void setup(Node) = 0; + virtual void setup(const Node& n) = 0; /** - * Assert a literal in the current context. + * Assert a fact in the current context. */ - void assertLiteral(Literal); + void assertFact(const Node& n); /** * Check the current assignment's consistency. */ - virtual void check(OutputChannel& out, Effort level = FULL_EFFORT) = 0; + virtual void check(OutputChannel& out, + Effort level = FULL_EFFORT) = 0; /** * T-propagate new literal assignments in the current context. */ - virtual void propagate(OutputChannel& out, Effort level = FULL_EFFORT) = 0; + virtual void propagate(OutputChannel& out, + Effort level = FULL_EFFORT) = 0; /** * Return an explanation for the literal represented by parameter n * (which was previously propagated by this theory). Report * explanations to an output channel. */ - virtual void explain(OutputChannel& out, Node n, Effort level = FULL_EFFORT) = 0; + virtual void explain(OutputChannel& out, + const Node& n, + Effort level = FULL_EFFORT) = 0; };/* class Theory */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3fb11b510..348d7e6df 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -16,8 +16,13 @@ #ifndef __CVC4__THEORY_ENGINE_H #define __CVC4__THEORY_ENGINE_H +#include "expr/node.h" +#include "theory/theory.h" + namespace CVC4 { +class SmtEngine; + // In terms of abstraction, this is below (and provides services to) // PropEngine. @@ -28,7 +33,22 @@ namespace CVC4 { * CVC4. */ class TheoryEngine { + + SmtEngine* d_smt; + public: + + /** + * Construct a theory engine. + */ + TheoryEngine(SmtEngine* smt) : d_smt(smt) { + } + + /** + * Get the theory associated to a given Node. + */ + CVC4::theory::Theory* theoryOf(const Node& n); + };/* class TheoryEngine */ }/* CVC4 namespace */ |