Merge from theory-break-dependences branch to break Theory and TheoryEngine dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine. If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).

2 files changed, 17 insertions, 17 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6084e3463..2100e0b38 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -22,7 +22,7 @@
 #include "expr/metakind.h"
 #include "expr/node_builder.h"
 
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 
 #include "util/rational.h"
 #include "util/integer.h"
@@ -567,7 +567,7 @@ void TheoryArith::propagate(Effort e) {
   // }
 }
 
-Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryArith::getValue(TNode n, Valuation* valuation) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
   switch(n.getKind()) {
@@ -578,7 +578,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
       Node eq = d_removedRows.find(var)->second;
       Assert(n == eq[0]);
       Node rhs = eq[1];
-      return getValue(rhs, engine);
+      return getValue(rhs, valuation);
     }
 
     DeltaRational drat = d_partialModel.getAssignment(var);
@@ -591,7 +591,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
 
   case kind::EQUAL: // 2 args
     return nodeManager->
-      mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+      mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
 
   case kind::PLUS: { // 2+ args
     Rational value = d_constants.d_ZERO;
@@ -599,7 +599,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
             iend = n.end();
           i != iend;
           ++i) {
-      value += engine->getValue(*i).getConst<Rational>();
+      value += valuation->getValue(*i).getConst<Rational>();
     }
     return nodeManager->mkConst(value);
   }
@@ -610,7 +610,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
             iend = n.end();
           i != iend;
           ++i) {
-      value *= engine->getValue(*i).getConst<Rational>();
+      value *= valuation->getValue(*i).getConst<Rational>();
     }
     return nodeManager->mkConst(value);
   }
@@ -624,24 +624,24 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
     Unreachable();
 
   case kind::DIVISION: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() /
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() /
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::LT: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::LEQ: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <=
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <=
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::GT: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   case kind::GEQ: // 2 args
-    return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >=
-                                 engine->getValue(n[1]).getConst<Rational>() );
+    return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >=
+                                 valuation->getValue(n[1]).getConst<Rational>() );
 
   default:
     Unhandled(n.getKind());
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 60d24708c..e29054c16 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -152,7 +152,7 @@ public:
 
   void notifyEq(TNode lhs, TNode rhs);
 
-  Node getValue(TNode n, TheoryEngine* engine);
+  Node getValue(TNode n, Valuation* valuation);
 
   void shutdown(){ }