This commit merges into trunk the branch branches/arithmetic/integers2 from r2650 to r2779.

- This excludes revision 2777.  This revision had some strange performance implications and was delaying the merge.
- This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts.
- The DioSolver can be disabled at command line using --disable-dio-solver.
- This includes a number of changes to the arithmetic normal form.
- The Integer class features a number of new number theoretic function.
- This commit includes a few rather loud warning. I will do my best to take care of them today.

1 files changed, 28 insertions, 22 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 66223b479..a309b9403 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -182,37 +182,43 @@ RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){
   TNode left  = t[0];
   TNode right = t[1];
 
-  Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
+  Comparison cmp = Comparison::mkNormalComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
 
-  if(cmp.isBoolean()){
-    return RewriteResponse(REWRITE_DONE, cmp.getNode());
-  }
+  Assert(cmp.isNormalForm());
+  return RewriteResponse(REWRITE_DONE, cmp.getNode());
 
-  if(cmp.getLeft().containsConstant()){
-    Monomial constantHead = cmp.getLeft().getHead();
-    Assert(constantHead.isConstant());
 
-    Constant constant = constantHead.getConstant();
+  // Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
 
-    Constant negativeConstantHead = -constant;
+  // if(cmp.isBoolean()){
+  //   return RewriteResponse(REWRITE_DONE, cmp.getNode());
+  // }
 
-    cmp = cmp.addConstant(negativeConstantHead);
-  }
-  Assert(!cmp.getLeft().containsConstant());
+  // if(cmp.getLeft().containsConstant()){
+  //   Monomial constantHead = cmp.getLeft().getHead();
+  //   Assert(constantHead.isConstant());
 
-  if(!cmp.getLeft().getHead().coefficientIsOne()){
-    Monomial constantHead = cmp.getLeft().getHead();
-    Assert(!constantHead.isConstant());
-    Constant constant = constantHead.getConstant();
+  //   Constant constant = constantHead.getConstant();
 
-    Constant inverse = Constant::mkConstant(constant.getValue().inverse());
+  //   Constant negativeConstantHead = -constant;
 
-    cmp = cmp.multiplyConstant(inverse);
-  }
-  Assert(cmp.getLeft().getHead().coefficientIsOne());
+  //   cmp = cmp.addConstant(negativeConstantHead);
+  // }
+  // Assert(!cmp.getLeft().containsConstant());
 
-  Assert(cmp.isBoolean() || cmp.isNormalForm());
-  return RewriteResponse(REWRITE_DONE, cmp.getNode());
+  // if(!cmp.getLeft().getHead().coefficientIsOne()){
+  //   Monomial constantHead = cmp.getLeft().getHead();
+  //   Assert(!constantHead.isConstant());
+  //   Constant constant = constantHead.getConstant();
+
+  //   Constant inverse = Constant::mkConstant(constant.getValue().inverse());
+
+  //   cmp = cmp.multiplyConstant(inverse);
+  // }
+  // Assert(cmp.getLeft().getHead().coefficientIsOne());
+
+  // Assert(cmp.isBoolean() || cmp.isNormalForm());
+  // return RewriteResponse(REWRITE_DONE, cmp.getNode());
 }
 
 RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){