Changed how assignments are saved during check. These are now backed by an attribute. There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed. A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling.

1 files changed, 0 insertions, 10 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 19980cd20..5c2a1e996 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -20,7 +20,6 @@
 
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/normal.h"
 
 #include <vector>
 #include <set>
@@ -542,10 +541,6 @@ Kind multKind(Kind k, int sgn){
 Node ArithRewriter::rewrite(TNode n){
   Debug("arithrewriter") << "Trace rewrite:" << n << std::endl;
 
-  if(n.getAttribute(IsNormal())){
-    return n;
-  }
-
   Node res;
 
   if(isRelationOperator(n.getKind())){
@@ -554,11 +549,6 @@ Node ArithRewriter::rewrite(TNode n){
     res = rewriteTerm(n);
   }
 
-  if(n == res){
-    n.setAttribute(NormalForm(), Node::null());
-  }else{
-    n.setAttribute(NormalForm(), res);
-  }
   Debug("arithrewriter") << "Trace rewrite:" << n << "|->"<< res << std::endl;
 
   return res;