diff options
author | Tim King <taking@cs.nyu.edu> | 2010-09-13 16:08:21 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-09-13 16:08:21 +0000 |
commit | 0e18d60841c2a7cd5c079b6c0dacf5d61afb4835 (patch) | |
tree | 470e4868ca9576dc20d491afa7462d6e9f1f8c56 /src/theory/arith/tableau.h | |
parent | 8d74ddb6380f39034e5cae5d4b094a283e14ffb3 (diff) |
* 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.)
Diffstat (limited to 'src/theory/arith/tableau.h')
-rw-r--r-- | src/theory/arith/tableau.h | 41 |
1 files changed, 19 insertions, 22 deletions
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 12d93d9fe..603eb5278 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -23,7 +23,7 @@ #include "theory/arith/basic.h" #include "theory/arith/arith_activity.h" - +#include "theory/arith/normal_form.h" #include <ext/hash_map> #include <map> @@ -52,21 +52,21 @@ public: * Construct a row equal to: * basic = \sum_{x_i} c_i * x_i */ - Row(TNode basic, TNode sum): + Row(TNode basic, const Polynomial& sum): d_x_i(basic), d_coeffs(){ Assert(d_x_i.getMetaKind() == kind::metakind::VARIABLE); - Assert(sum.getKind() == kind::PLUS); - - for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){ - TNode pair = *iter; - Assert(pair.getKind() == kind::MULT); - Assert(pair.getNumChildren() == 2); - TNode coeff = pair[0]; - TNode var_i = pair[1]; + + for(Polynomial::iterator iter=sum.begin(), end = sum.end(); iter != end; ++iter){ + const Monomial& mono = *iter; + + Assert(!mono.isConstant()); + + TNode coeff = mono.getConstant().getNode(); + TNode var_i = mono.getVarList().getNode(); + Assert(coeff.getKind() == kind::CONST_RATIONAL); - Assert(var_i.getKind() == kind::VARIABLE); Assert(!has(var_i)); d_coeffs[var_i] = coeff.getConst<Rational>(); @@ -192,14 +192,13 @@ private: public: void addRow(TNode eq){ - Assert(eq.getKind() == kind::EQUAL); - Assert(eq.getNumChildren() == 2); - TNode var = eq[0]; - TNode sum = eq[1]; + TNode sumNode = eq[1]; Assert(var.getAttribute(IsBasic())); + Polynomial sum = Polynomial::parsePolynomial(sumNode); + //The new basic variable cannot already be a basic variable Assert(!isActiveBasicVariable(var)); d_activeBasicVars.insert(var); @@ -208,13 +207,11 @@ public: //A variable in the row may have been made non-basic already. //If this is the case we fake pivoting this variable - for(TNode::iterator sumIter = sum.begin(); sumIter!=sum.end(); ++sumIter){ - TNode child = *sumIter; - Assert(child.getKind() == kind::MULT); - Assert(child.getNumChildren() == 2); - Assert(child[0].getKind() == kind::CONST_RATIONAL); - TNode c = child[1]; - Assert(var.getMetaKind() == kind::metakind::VARIABLE); + for(Polynomial::iterator sumIter = sum.begin(); sumIter!= sum.end(); ++sumIter){ + const Monomial& child = *sumIter; + + Assert(!child.isConstant()); + TNode c = child.getVarList().getNode(); if(isActiveBasicVariable(c)){ Row* row_c = lookup(c); row_var->subsitute(*row_c); |