diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:35:03 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:50:58 -0500 |
commit | 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch) | |
tree | 9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /src/compat | |
parent | d6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff) |
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index be24dacdd..2757e3dbe 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -27,7 +27,6 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/kind.h" -#include "expr/predicate.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -1257,6 +1256,7 @@ Type ValidityChecker::intType() { } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { +/* bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF"; CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); @@ -1264,10 +1264,12 @@ Type ValidityChecker::subrangeType(const Expr& l, const Expr& 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)); + */ + Unimplemented("Subrange types not supported by CVC4 (sorry!)"); } Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) { - Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)"); + Unimplemented("Predicate subtyping not supported by CVC4 (sorry!)"); /* if(witness.isNull()) { return d_em->mkPredicateSubtype(pred); |