4 files changed, 51 insertions, 11 deletions
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 4e4088bb0..f270dacb4 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -148,7 +148,7 @@ public:
         }
       }else{
         d_nonbasic.insert(x_j);
-        d_coeffs.insert(make_pair(x_j,a_sj));
+        d_coeffs.insert(std::make_pair(x_j,a_sj));
       }
     }
   }
@@ -289,7 +289,7 @@ public:
     d_activeRows.erase(basic);
     d_activeBasicVars.erase(basic);
 
-    d_inactiveRows.insert(make_pair(basic, row));
+    d_inactiveRows.insert(std::make_pair(basic, row));
   }
 
   void reinjectBasic(TNode basic){
@@ -299,7 +299,7 @@ public:
 
     d_inactiveRows.erase(basic);
     d_activeBasicVars.insert(basic);
-    d_activeRows.insert(make_pair(basic, row));
+    d_activeRows.insert(std::make_pair(basic, row));
 
     updateRow(row);
   }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 26d554356..cb9dc85f7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -315,6 +315,34 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
   return sum;
 }
 
+RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
+  // Look for multiplications with a 0 argument and rewrite the whole
+  // thing as 0
+  if(n.getKind() == MULT) {
+    Rational ratZero;
+    Integer intZero;
+    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+      if((*i).getKind() == CONST_RATIONAL) {
+        if((*i).getConst<Rational>() == ratZero) {
+          n = NodeManager::currentNM()->mkConst(ratZero);
+          break;
+        }
+      } else if((*i).getKind() == CONST_INTEGER) {
+        if((*i).getConst<Integer>() == intZero) {
+          if(n.getType().isInteger()) {
+            n = NodeManager::currentNM()->mkConst(intZero);
+            break;
+          } else {
+            n = NodeManager::currentNM()->mkConst(ratZero);
+            break;
+          }
+        }
+      }
+    }
+  }
+  return RewritingComplete(Node(n));
+}
+
 Node TheoryArith::rewrite(TNode n){
   Debug("arith") << "rewrite(" << n << ")" << endl;
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ba9b5329d..465adacbc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -41,7 +41,6 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-
 /**
  * Implementation of QF_LRA.
  * Based upon:
@@ -109,6 +108,18 @@ public:
   Node rewrite(TNode n);
 
   /**
+   * Rewriting optimizations.
+   */
+  RewriteResponse preRewrite(TNode n, bool topLevel);
+
+  /**
+   * Plug in old rewrite to the new (pre,post)rewrite interface.
+   */
+  RewriteResponse postRewrite(TNode n, bool topLevel) {
+    return RewritingComplete(topLevel ? rewrite(n) : Node(n));
+  }
+
+  /**
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n);
@@ -122,6 +133,7 @@ public:
 
   void shutdown(){ }
 
+  std::string identify() const { return std::string("TheoryArith"); }
 
 private:
   /**
@@ -254,7 +266,7 @@ private:
   Statistics d_statistics;
 
 
-};
+};/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index a995f90af..9b22b14bb 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY_ARITH_TYPE_RULES_H_
-#define __CVC4__THEORY_ARITH_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -72,8 +72,8 @@ public:
   }
 };
 
-}
-}
-}
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif /* THEORY_ARITH_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */