diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
commit | 488ae3f42d9d3e06978e11a42d1d47e76072f797 (patch) | |
tree | f466859889ceee9947e20d695fd35f99065277f8 /src/theory/arith | |
parent | fe2088f892af594765fc50d8cc9f2b4f87286b7c (diff) |
This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 32 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 47 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.h | 38 | ||||
-rw-r--r-- | src/theory/arith/kinds | 9 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 13 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 14 |
7 files changed, 27 insertions, 130 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 863eb5c31..d7a6c0443 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -40,9 +40,9 @@ bool ArithRewriter::isAtom(TNode n) { RewriteResponse ArithRewriter::rewriteConstant(TNode t){ Assert(t.getMetaKind() == kind::metakind::CONSTANT); - Node val = coerceToRationalNode(t); + Assert(t.getKind() == kind::CONST_RATIONAL); - return RewriteResponse(REWRITE_DONE, val); + return RewriteResponse(REWRITE_DONE, t); } RewriteResponse ArithRewriter::rewriteVariable(TNode t){ @@ -91,27 +91,23 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ }else if(t.getKind() == kind::UMINUS){ return rewriteUMinus(t, true); }else if(t.getKind() == kind::DIVISION){ - if(t[0].getKind()== kind::CONST_RATIONAL){ - return rewriteDivByConstant(t, true); - }else{ - return RewriteResponse(REWRITE_DONE, t); - } + return RewriteResponse(REWRITE_DONE, t); // wait until t[1] is rewritten }else if(t.getKind() == kind::PLUS){ return preRewritePlus(t); }else if(t.getKind() == kind::MULT){ return preRewriteMult(t); }else if(t.getKind() == kind::INTS_DIVISION){ - Integer intOne(1); - if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){ + Rational intOne(1); + if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){ return RewriteResponse(REWRITE_AGAIN, t[0]); }else{ return RewriteResponse(REWRITE_DONE, t); } }else if(t.getKind() == kind::INTS_MODULUS){ - Integer intOne(1); - if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){ - Integer intZero(0); - return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero)); + Rational intOne(1); + if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){ + Rational intZero(0); + return RewriteResponse(REWRITE_AGAIN, mkRationalNode(intZero)); }else{ return RewriteResponse(REWRITE_DONE, t); } @@ -147,8 +143,6 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){ Assert(t.getKind()== kind::MULT); // Rewrite multiplications with a 0 argument and to 0 - Integer intZero; - Rational qZero(0); for(TNode::iterator i = t.begin(); i != t.end(); ++i) { @@ -156,14 +150,6 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){ if((*i).getConst<Rational>() == qZero) { return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero)); } - } else if((*i).getKind() == kind::CONST_INTEGER) { - if((*i).getConst<Integer>() == intZero) { - if(t.getType().isInteger()) { - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(intZero)); - } else { - return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero)); - } - } } } return RewriteResponse(REWRITE_DONE, t); diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 8ecc3abdc..e88ec073d 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -152,10 +152,9 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet } break; case CONST_RATIONAL: - case CONST_INTEGER: // Mark constants as minmax - d_minMap[n] = coerceToRational(n); - d_maxMap[n] = coerceToRational(n); + d_minMap[n] = n.getConst<Rational>(); + d_maxMap[n] = n.getConst<Rational>(); break; case OR: { // Look for things like "x = 0 OR x = 1" (that are defTrue) and @@ -193,46 +192,6 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet break; } - Integer k1, k2; - if(c1.getType().getConst<TypeConstant>() == INTEGER_TYPE) { - k1 = c1.getConst<Integer>(); - } else { - Rational r = c1.getConst<Rational>(); - if(r.getDenominator() == 1) { - k1 = r.getNumerator(); - } else { - break; - } - } - if(c2.getType().getConst<TypeConstant>() == INTEGER_TYPE) { - k2 = c2.getConst<Integer>(); - } else { - Rational r = c2.getConst<Rational>(); - if(r.getDenominator() == 1) { - k2 = r.getNumerator(); - } else { - break; - } - } - if(k1 > k2) { - swap(k1, k2); - } - if(k1 + 1 == k2) { - Debug("arith::static") << "==> found " << n << endl - << " which indicates " << var << " \\in { " - << k1 << " , " << k2 << " }" << endl; - c1 = NodeManager::currentNM()->mkConst(k1); - c2 = NodeManager::currentNM()->mkConst(k2); - Node lhs = NodeBuilder<2>(kind::GEQ) << var << c1; - Node rhs = NodeBuilder<2>(kind::LEQ) << var << c2; - Node l = lhs && rhs; - Debug("arith::static") << " learned: " << l << endl; - learned << l; - if(k1 == 0) { - Assert(k2 == 1); - replaceWithPseudoboolean(var); - } - } break; } default: // Do nothing @@ -466,7 +425,7 @@ void ArithStaticLearner::addBound(TNode n) { NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]); NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n[0]); - Rational constant = coerceToRational(n[1]); + Rational constant = n[1].getConst<Rational>(); DeltaRational bound = constant; switch(Kind k = n.getKind()) { diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index af32c3f87..fb669cce4 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -41,50 +41,12 @@ inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst<Rational>(q); } -inline Node mkIntegerNode(const Integer& z){ - return NodeManager::currentNM()->mkConst<Integer>(z); -} - inline Node mkBoolNode(bool b){ return NodeManager::currentNM()->mkConst<bool>(b); } -inline Rational coerceToRational(TNode constant){ - switch(constant.getKind()){ - case kind::CONST_INTEGER: - { - Rational q(constant.getConst<Integer>()); - return q; - } - case kind::CONST_RATIONAL: - return constant.getConst<Rational>(); - default: - Unreachable(); - } - Rational unreachable(0,0); - return unreachable; -} - -inline Node coerceToRationalNode(TNode constant){ - switch(constant.getKind()){ - case kind::CONST_INTEGER: - { - Rational q(constant.getConst<Integer>()); - Node n = mkRationalNode(q); - return n; - } - case kind::CONST_RATIONAL: - return constant; - default: - Unreachable(); - } - return Node::null(); -} - - - /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */ inline bool isRelationOperator(Kind k){ using namespace kind; diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 95d7d6ed1..e00d8dc5e 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -31,7 +31,7 @@ sort REAL_TYPE \ sort INTEGER_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(Integer(0))" \ + "NodeManager::currentNM()->mkConst(Rational(0))" \ "expr/node_manager.h" \ "Integer type" sort PSEUDOBOOLEAN_TYPE \ @@ -59,11 +59,7 @@ constant CONST_RATIONAL \ ::CVC4::RationalHashStrategy \ "util/rational.h" \ "a multiple-precision rational constant" -constant CONST_INTEGER \ - ::CVC4::Integer \ - ::CVC4::IntegerHashStrategy \ - "util/integer.h" \ - "a multiple-precision integer constant" + constant CONST_PSEUDOBOOLEAN \ ::CVC4::Pseudoboolean \ ::CVC4::PseudobooleanHashStrategy \ @@ -83,7 +79,6 @@ typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule -typerule CONST_INTEGER ::CVC4::theory::arith::ArithConstantTypeRule typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 434be42a2..d67cd46a9 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -232,7 +232,6 @@ public: // TODO: check if it's a theory leaf also static bool isMember(Node n) { - if (n.getKind() == kind::CONST_INTEGER) return false; if (n.getKind() == kind::CONST_RATIONAL) return false; if (isRelationOperator(n.getKind())) return false; return Theory::isLeafOf(n, theory::THEORY_ARITH); @@ -283,7 +282,8 @@ public: bool isNormalForm() { return isMember(getNode()); } static Constant mkConstant(Node n) { - return Constant(coerceToRationalNode(n)); + Assert(n.getKind() == kind::CONST_RATIONAL); + return Constant(n); } static Constant mkConstant(const Rational& rat) { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d660cb4cd..1bd3277cd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1239,8 +1239,8 @@ Node TheoryArith::roundRobinBranch(){ Integer floor_d = d.floor(); Integer ceil_d = d.ceiling(); - Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkIntegerNode(floor_d))); - Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkIntegerNode(ceil_d))); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d))); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d))); Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); @@ -1436,9 +1436,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { switch(n.getKind()) { - case kind::CONST_INTEGER: - return Rational(n.getConst<Integer>()); - case kind::CONST_RATIONAL: return n.getConst<Rational>(); @@ -1456,9 +1453,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { case kind::MULT: { // 2+ args Assert(n.getNumChildren() == 2 && n[0].isConst()); DeltaRational value(1); - if (n[0].getKind() == kind::CONST_INTEGER) { - return getDeltaValue(n[1]) * n[0].getConst<Integer>(); - } if (n[0].getKind() == kind::CONST_RATIONAL) { return getDeltaValue(n[1]) * n[0].getConst<Rational>(); } @@ -1478,9 +1472,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { if (n[1].getKind() == kind::CONST_RATIONAL) { return getDeltaValue(n[0]) / n[0].getConst<Rational>(); } - if (n[1].getKind() == kind::CONST_INTEGER) { - return getDeltaValue(n[0]) / n[0].getConst<Integer>(); - } Unreachable(); diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 8d0d79f0a..69c98a255 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -32,8 +32,12 @@ class ArithConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType(); - return nodeManager->integerType(); + Assert(n.getKind() == kind::CONST_RATIONAL); + if(n.getConst<Rational>().isIntegral()){ + return nodeManager->integerType(); + }else{ + return nodeManager->realType(); + } } };/* class ArithConstantTypeRule */ @@ -101,12 +105,12 @@ public: const SubrangeBounds& bounds = type.getConst<SubrangeBounds>(); if(bounds.lower.hasBound()) { - return NodeManager::currentNM()->mkConst(bounds.lower.getBound()); + return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound())); } if(bounds.upper.hasBound()) { - return NodeManager::currentNM()->mkConst(bounds.upper.getBound()); + return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound())); } - return NodeManager::currentNM()->mkConst(Integer(0)); + return NodeManager::currentNM()->mkConst(Rational(0)); } };/* class SubrangeProperties */ |