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/parser/tptp/tptp.cpp | |
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/parser/tptp/tptp.cpp')
-rw-r--r-- | src/parser/tptp/tptp.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
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); } |