diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-01 15:44:34 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-01 20:44:34 +0000 |
commit | 71699a551d207ab373c733d8ea83a5b071ed99ee (patch) | |
tree | 639bf606f8374d2685e72919a48b4749088a3a43 /src | |
parent | 78bfaf2c35fa3b4c7ff35b0b9a5fd0c8c7c5a922 (diff) |
Fix type rule for to_real (#6257)
This fixes the type rule for to_real to match SMT-LIB: its argument must be an integer.
This required fixing the TPTP parser which has a more relaxed semantics for to_real / to_rat.
This also fixes Solver::isReal, which should return false if we are the integer type.
Fixes #6208.
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 5 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 7 |
3 files changed, 21 insertions, 3 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 9e55cdaf0..f304ae5a0 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1087,7 +1087,8 @@ bool Sort::isReal() const { CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_type->isReal(); + // notice that we do not expose internal subtyping to the user + return d_type->isReal() && !d_type->isInteger(); //////// CVC4_API_TRY_CATCH_END; } @@ -4432,7 +4433,7 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const } // Integers are reals, too - Assert(t.isReal()); + Assert(t.d_type->isReal()); Term res = term; if (t.isInteger()) { diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 136319225..7a3a47ec9 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -340,6 +340,18 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) { return d_solver->mkTerm(api::UMINUS, args[0]); } + if (kind == api::TO_REAL) + { + // If the type is real, this is a no-op. We require this special + // case in the TPTP parser since TO_REAL is designed to match the + // SMT-LIB operator, meaning it can only be applied to integers, whereas + // the TPTP to_real / to_rat do not have the same semantics. + api::Sort s = args[0].getSort(); + if (s.isReal()) + { + return args[0]; + } + } return d_solver->mkTerm(kind, args); } diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index e192270ff..e8769064a 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -46,6 +46,7 @@ public: TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); bool isInteger = true; + Kind k = n.getKind(); for(; child_it != child_it_end; ++child_it) { TypeNode childType = (*child_it).getType(check); if (!childType.isInteger()) { @@ -58,9 +59,13 @@ public: if(!childType.isReal()) { throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm"); } + if (k == kind::TO_REAL && !childType.isInteger()) + { + throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm"); + } } } - switch (Kind k = n.getKind()) + switch (k) { case kind::TO_REAL: case kind::CAST_TO_REAL: return realType; |