diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
| -rw-r--r-- | src/theory/theory.h | 19 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 20 | ||||
| -rw-r--r-- | src/util/Makefile.am | 1 | ||||
| -rw-r--r-- | src/util/decision_engine.cpp | 4 | ||||
| -rw-r--r-- | src/util/decision_engine.h | 4 | ||||
| -rw-r--r-- | src/util/literal.h | 26 |
7 files changed, 36 insertions, 40 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a04d16d06..ed8f61ee6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -31,7 +31,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : d_opts(opts) { d_de = new DecisionEngine(); - d_te = new TheoryEngine(); + d_te = new TheoryEngine(this); d_prop = new PropEngine(opts, d_de, d_te); } 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 */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 9c3431499..9bbf89fff 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -14,7 +14,6 @@ libutil_la_SOURCES = \ decision_engine.cpp \ decision_engine.h \ exception.h \ - literal.h \ model.h \ options.h \ output.cpp \ diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index 92e4c4f8c..9b6101a2a 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -14,7 +14,7 @@ #include "util/decision_engine.h" #include "util/Assert.h" -#include "util/literal.h" +#include "expr/node.h" namespace CVC4 { @@ -25,7 +25,7 @@ DecisionEngine::~DecisionEngine() { * Only here to permit compilation and linkage. This may be pure * virtual in the final design (?) */ -Literal DecisionEngine::nextDecision() { +Node DecisionEngine::nextDecision() { Unreachable(); } diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 801daa863..72943ee99 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -17,7 +17,7 @@ #define __CVC4__DECISION_ENGINE_H #include "cvc4_config.h" -#include "util/literal.h" +#include "expr/node.h" namespace CVC4 { @@ -37,7 +37,7 @@ public: /** * Get the next decision. */ - virtual Literal nextDecision();// = 0 + virtual Node nextDecision();// = 0 // TODO: design decision: decision engine should be notified of // propagated lits, and also why(?) (so that it can make decisions diff --git a/src/util/literal.h b/src/util/literal.h deleted file mode 100644 index 582c8a646..000000000 --- a/src/util/literal.h +++ /dev/null @@ -1,26 +0,0 @@ -/********************* */ -/** literal.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** A literal. - **/ - -#ifndef __CVC4__LITERAL_H -#define __CVC4__LITERAL_H - -namespace CVC4 { - -class Literal { -}; - -}/* CVC4 namespace */ - -#endif /* __CVC4__LITERAL_H */ |