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/util | |
parent | 7b3ae98cc2cd9b70e0e00ab07418e796a87e3f97 (diff) |
minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim
Diffstat (limited to 'src/util')
-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 |
4 files changed, 4 insertions, 31 deletions
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 */ |