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/theory | |
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/theory')
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 7 |
1 files changed, 6 insertions, 1 deletions
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; |