minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim

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 */