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/compat | |
| 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/compat')
| -rw-r--r-- | src/compat/cvc3_compat.cpp | 8 |
1 files changed, 4 insertions, 4 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<string>() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_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<Integer>()); - CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Integer>()); + CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); + CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r); + CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator()); + CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator()); return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br)); } |