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/arith_utilities.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/arith_utilities.h')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 17 |
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; |