From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 4 Feb 2010 23:59:41 +0000 (+0000)
Subject: minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim
X-Git-Tag: cvc5-1.0.0~9280
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b21aad9f82edd1f0241579bf2f1f8cd870eb582b;p=cvc5.git

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