From 488ae3f42d9d3e06978e11a42d1d47e76072f797 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 15 May 2012 19:01:19 +0000 Subject: [PATCH] This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int. --- src/compat/cvc3_compat.cpp | 8 ++-- src/expr/pickler.cpp | 22 +++------- src/parser/antlr_input.h | 6 +-- src/parser/cvc/Cvc.g | 4 +- src/printer/cvc/cvc_printer.cpp | 7 +--- src/printer/smt2/smt2_printer.cpp | 13 +----- src/smt/smt_engine.cpp | 4 +- src/theory/arith/arith_rewriter.cpp | 32 +++++---------- src/theory/arith/arith_static_learner.cpp | 47 ++-------------------- src/theory/arith/arith_utilities.h | 38 ----------------- src/theory/arith/kinds | 9 +---- src/theory/arith/normal_form.h | 4 +- src/theory/arith/theory_arith.cpp | 13 +----- src/theory/arith/theory_arith_type_rules.h | 14 ++++--- test/unit/expr/expr_public.h | 22 +++++----- test/unit/expr/node_manager_black.h | 7 ---- test/unit/expr/node_manager_white.h | 4 +- test/unit/expr/node_white.h | 2 +- 18 files changed, 60 insertions(+), 196 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 16169c10a..15e0d8001 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1004,10 +1004,10 @@ Type ValidityChecker::intType() { Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { bool noLowerBound = l.getType().isString() && l.getConst() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst() == "_POSINF"; - CheckArgument(noLowerBound || l.getKind() == CVC4::kind::CONST_INTEGER, l); - CheckArgument(noUpperBound || r.getKind() == CVC4::kind::CONST_INTEGER, r); - CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst()); - CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst()); + CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst().isIntegral()), l); + CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst().isIntegral()), r); + CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst().getNumerator()); + CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst().getNumerator()); return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br)); } diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index f09c552d1..3d077502d 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -207,17 +207,11 @@ void PicklerPrivate::toCaseConstant(TNode n) { d_current << mkConstantHeader(k, 1); d_current << mkBlockBody(n.getConst()); break; - case kind::CONST_INTEGER: case kind::CONST_RATIONAL: { std::string asString; - if(k == kind::CONST_INTEGER) { - const Integer& i = n.getConst(); - asString = i.toString(16); - } else { - Assert(k == kind::CONST_RATIONAL); - const Rational& q = n.getConst(); - asString = q.toString(16); - } + Assert(k == kind::CONST_RATIONAL); + const Rational& q = n.getConst(); + asString = q.toString(16); toCaseString(k, asString); break; } @@ -357,16 +351,10 @@ Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) { bool b= val.d_body.d_data; return d_nm->mkConst(b); } - case kind::CONST_INTEGER: case kind::CONST_RATIONAL: { std::string s = fromCaseString(constblocks); - if(k == kind::CONST_INTEGER) { - Integer i(s, 16); - return d_nm->mkConst(i); - } else { - Rational q(s, 16); - return d_nm->mkConst(q); - } + Rational q(s, 16); + return d_nm->mkConst(q); } case kind::BITVECTOR_EXTRACT_OP: { Block high = d_current.dequeue(); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index a39defd14..bdf5fe59e 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -171,7 +171,7 @@ public: static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token ); /** Retrieve an Integer from the text of a token */ - static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token ); + static Rational tokenToInteger( pANTLR3_COMMON_TOKEN token ); /** Retrieve a Rational from the text of a token */ static Rational tokenToRational(pANTLR3_COMMON_TOKEN token); @@ -263,8 +263,8 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) { return result; } -inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { - return Integer( tokenText(token) ); +inline Rational AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { + return Rational( tokenText(token) ); } inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 52d32606b..2da9f0f63 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1165,7 +1165,7 @@ parameterization[CVC4::parser::DeclarationCheck check, bound returns [CVC4::parser::cvc::mySubrangeBound bound] : UNDERSCORE { $bound = SubrangeBound(); } - | k=integer { $bound = SubrangeBound(k); } + | k=integer { $bound = SubrangeBound(k.getNumerator()); } ; typeLetDecl[CVC4::parser::DeclarationCheck check] @@ -1991,7 +1991,7 @@ numeral returns [unsigned k = 0] /** * Similar to numeral but for arbitrary-precision, signed integer. */ -integer returns [CVC4::Integer k = 0] +integer returns [CVC4::Rational k = 0] : INTEGER_LITERAL { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); } | MINUS_TOK INTEGER_LITERAL diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 857513fa3..1f147479d 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -94,18 +94,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; case kind::CONST_RATIONAL: { const Rational& rat = n.getConst(); - if(rat.getDenominator() == 1) { + if(rat.isIntegral()) { out << rat.getNumerator(); } else { out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; } break; } - case kind::CONST_INTEGER: { - const Integer& num = n.getConst(); - out << num; - break; - } case kind::CONST_PSEUDOBOOLEAN: { const Pseudoboolean& num = n.getConst(); out << num; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 03422c162..2b686441a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -100,25 +100,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BUILTIN: out << smtKindString(n.getConst()); break; - case kind::CONST_INTEGER: { - Integer i = n.getConst(); - if(i < 0) { - out << "(- " << -i << ')'; - } else { - out << i; - } - break; - } case kind::CONST_RATIONAL: { Rational r = n.getConst(); if(r < 0) { - if(r.getDenominator() == 1) { + if(r.isIntegral()) { out << "(- " << -r << ')'; } else { out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))"; } } else { - if(r.getDenominator() == 1) { + if(r.isIntegral()) { out << r; } else { out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')'; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0acd81248..90d21c60d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -931,13 +931,13 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector& assertion SubrangeBounds bounds = t.getSubrangeBounds(); Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl; if(bounds.lower.hasBound()) { - Node c = NodeManager::currentNM()->mkConst(bounds.lower.getBound()); + Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound())); Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n); Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl; assertions.push_back(lb); } if(bounds.upper.hasBound()) { - Node c = NodeManager::currentNM()->mkConst(bounds.upper.getBound()); + Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound())); Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c); Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl; assertions.push_back(ub); 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() == intOne){ + Rational intOne(1); + if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst() == 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() == intOne){ - Integer intZero(0); - return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero)); + Rational intOne(1); + if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst() == 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() == qZero) { return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero)); } - } else if((*i).getKind() == kind::CONST_INTEGER) { - if((*i).getConst() == 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(); + d_maxMap[n] = n.getConst(); 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() == INTEGER_TYPE) { - k1 = c1.getConst(); - } else { - Rational r = c1.getConst(); - if(r.getDenominator() == 1) { - k1 = r.getNumerator(); - } else { - break; - } - } - if(c2.getType().getConst() == INTEGER_TYPE) { - k2 = c2.getConst(); - } else { - Rational r = c2.getConst(); - 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(); 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(q); } -inline Node mkIntegerNode(const Integer& z){ - return NodeManager::currentNM()->mkConst(z); -} - inline Node mkBoolNode(bool b){ return NodeManager::currentNM()->mkConst(b); } -inline Rational coerceToRational(TNode constant){ - switch(constant.getKind()){ - case kind::CONST_INTEGER: - { - Rational q(constant.getConst()); - return q; - } - case kind::CONST_RATIONAL: - return constant.getConst(); - default: - Unreachable(); - } - Rational unreachable(0,0); - return unreachable; -} - -inline Node coerceToRationalNode(TNode constant){ - switch(constant.getKind()){ - case kind::CONST_INTEGER: - { - Rational q(constant.getConst()); - 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()); - case kind::CONST_RATIONAL: return n.getConst(); @@ -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(); - } if (n[0].getKind() == kind::CONST_RATIONAL) { return getDeltaValue(n[1]) * n[0].getConst(); } @@ -1478,9 +1472,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { if (n[1].getKind() == kind::CONST_RATIONAL) { return getDeltaValue(n[0]) / n[0].getConst(); } - if (n[1].getKind() == kind::CONST_INTEGER) { - return getDeltaValue(n[0]) / n[0].getConst(); - } 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().isIntegral()){ + return nodeManager->integerType(); + }else{ + return nodeManager->realType(); + } } };/* class ArithConstantTypeRule */ @@ -101,12 +105,12 @@ public: const SubrangeBounds& bounds = type.getConst(); 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 */ diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 853d0086b..491f99584 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -66,8 +66,8 @@ public: d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool)); null = new Expr; - i1 = new Expr(d_em->mkConst(Integer("0"))); - i2 = new Expr(d_em->mkConst(Integer(23))); + i1 = new Expr(d_em->mkConst(Rational("0"))); + i2 = new Expr(d_em->mkConst(Rational(23))); r1 = new Expr(d_em->mkConst(Rational(1, 5))); r2 = new Expr(d_em->mkConst(Rational("0"))); } catch(Exception e) { @@ -218,8 +218,8 @@ public: TS_ASSERT(d_apply_fun_bool->getKind() == APPLY_UF); TS_ASSERT(null->getKind() == NULL_EXPR); - TS_ASSERT(i1->getKind() == CONST_INTEGER); - TS_ASSERT(i2->getKind() == CONST_INTEGER); + TS_ASSERT(i1->getKind() == CONST_RATIONAL); + TS_ASSERT(i2->getKind() == CONST_RATIONAL); TS_ASSERT(r1->getKind() == CONST_RATIONAL); TS_ASSERT(r2->getKind() == CONST_RATIONAL); } @@ -292,8 +292,8 @@ public: TS_ASSERT(d_apply_fun_bool->toString() == "(APPLY_UF f a)"); TS_ASSERT(null->toString() == "null"); - TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)"); - TS_ASSERT(i2->toString() == "(CONST_INTEGER 23)"); + TS_ASSERT(i1->toString() == "(CONST_RATIONAL 0)"); + TS_ASSERT(i2->toString() == "(CONST_RATIONAL 23)"); TS_ASSERT(r1->toString() == "(CONST_RATIONAL 1/5)"); TS_ASSERT(r2->toString() == "(CONST_RATIONAL 0)"); } @@ -324,8 +324,8 @@ public: TS_ASSERT(sd.str() == "(APPLY_UF f a)"); TS_ASSERT(snull.str() == "null"); - TS_ASSERT(si1.str() == "(CONST_INTEGER 0)"); - TS_ASSERT(si2.str() == "(CONST_INTEGER 23)"); + TS_ASSERT(si1.str() == "(CONST_RATIONAL 0)"); + TS_ASSERT(si2.str() == "(CONST_RATIONAL 23)"); TS_ASSERT(sr1.str() == "(CONST_RATIONAL 1/5)"); TS_ASSERT(sr2.str() == "(CONST_RATIONAL 0)"); } @@ -362,14 +362,14 @@ public: TS_ASSERT_THROWS(b_bool->getConst(), IllegalArgumentException); TS_ASSERT_THROWS(c_bool_and->getConst(), IllegalArgumentException); TS_ASSERT(and_op->getConst() == AND); - TS_ASSERT_THROWS(and_op->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(and_op->getConst(), IllegalArgumentException); TS_ASSERT(plus_op->getConst() == PLUS); TS_ASSERT_THROWS(plus_op->getConst(), IllegalArgumentException); TS_ASSERT_THROWS(d_apply_fun_bool->getConst(), IllegalArgumentException); TS_ASSERT_THROWS(null->getConst(), IllegalArgumentException); - TS_ASSERT(i1->getConst() == 0); - TS_ASSERT(i2->getConst() == 23); + TS_ASSERT(i1->getConst() == 0); + TS_ASSERT(i2->getConst() == 23); TS_ASSERT(r1->getConst() == Rational(1, 5)); TS_ASSERT(r2->getConst() == Rational("0")); diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index c30e4badb..cca2ff4fc 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -168,13 +168,6 @@ public: TS_ASSERT_EQUALS(ff.getConst(),false); } - - void testMkConstInt() { - Integer i("3"); - Node n = d_nodeManager->mkConst(i); - TS_ASSERT_EQUALS(n.getConst(),i); - } - void testMkConstRat() { Rational r("3/2"); Node n = d_nodeManager->mkConst(r); diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 735fe2ac8..15a178b5c 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -50,8 +50,8 @@ public: delete d_ctxt; } - void testMkConstInt() { - Integer i("3"); + void testMkConstRational() { + Rational i("3"); Node n = d_nm->mkConst(i); Node m = d_nm->mkConst(i); TS_ASSERT_EQUALS(n.getId(), m.getId()); diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index ce67004c6..a042b1752 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -73,7 +73,7 @@ public: Node x = d_nm->mkVar("x", d_nm->integerType()); Node y = d_nm->mkVar("y", d_nm->integerType()); Node x_plus_y = d_nm->mkNode(PLUS, x, y); - Node two = d_nm->mkConst(Integer(2)); + Node two = d_nm->mkConst(Rational(2)); Node x_times_2 = d_nm->mkNode(MULT, x, two); Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y); -- 2.30.2