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/api | |
| 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/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 5 |
1 files changed, 3 insertions, 2 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()) { |