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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a04d16d066abf1b4af8182e54862e2df97167b12..ed8f61ee6b71c056d7b228643b2d666770ae56f3 100644 (file)
--- 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 8daa0149f2911f2cf704d4894b16c67a3be455ac..ad89a2aaaba7db62222b797a1f89e6689fe4ff3b 100644 (file)
--- 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 3fb11b510127eb4fca8602d9d229f789aa3dcf86..348d7e6dfa7d863b9ae6f567ba23c3b53e32c7e7 100644 (file)
--- 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 9c3431499450f7ddd012623d780dfef2a2e3f2f1..9bbf89fffb4b6c3321f92f2bc1ea248d3b4e182c 100644 (file)
--- 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 92e4c4f8c5c689cb6794aca0a2d39d9b13328ba3..9b6101a2a6ac3f0fb753bf0ee19aa9b019c994e6 100644 (file)
--- 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 801daa8633ec64e6b8f13836d960ba6917caa1c5..72943ee9907059629a220abeedc985011a7d6d34 100644 (file)
--- 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 (file)
index 582c8a6..0000000
--- 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 */