diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-04 19:40:33 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-04 19:40:33 +0000 |
commit | a311ba5ad6b922903fb706c1576d3e5c8eb5c599 (patch) | |
tree | 41747e4916b004b0a8c6f94f821d8557d29820fd /src/theory/arith/arith_rewriter.cpp | |
parent | 419c9bff0daabe30b012bd9a4de0757b0eac7609 (diff) |
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.
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 10 |
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; |