* New normal form for arithmetic is in place.

* src/theory/arith/normal_form.{h,cpp} contains the description for the new
  normal form as well as utilities for dealing with the normal form.
* src/theory/arith/next_arith_rewriter.{h,cpp} contains the new rewriter.
  The new rewriter implements preRewrite() and postRewrite() for arithmetic.
* src/theory/arith/arith_rewriter.{h,cpp} have been removed.
* TheoryArith::rewrite() has been removed.
* Arithmetic with the new normal form outperforms the trunk where the branch
  occurred (-r797) on 46% of the examples in QF_LRA. (33% have no noticeable
  difference.) Some important optimizations are stilling pending to the code
  for handling the new normal form. (Bug 196.)

1 files changed, 16 insertions, 1 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index fa3356c60..6706ad76a 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -27,7 +27,7 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-inline Node mkRationalNode(Rational& q){
+inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }
 
@@ -87,6 +87,21 @@ inline bool isRelationOperator(Kind k){
   }
 }
 
+/** is k \in {LT, LEQ, EQ, GEQ, GT} */
+inline Kind negateRelationKind(Kind k){
+  using namespace kind;
+
+  switch(k){
+  case LT: return GT;
+  case LEQ: return GEQ;
+  case EQUAL: return EQUAL;
+  case GEQ: return LEQ;
+  case GT: return LT;
+
+  default:
+    Unreachable();
+  }
+}
 inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
   using namespace kind;