projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 78bfaf2) | patch
Fix type rule for to_real (#6257)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 1 Apr 2021 20:44:34 +0000 (15:44 -0500)
committerGitHub <noreply@github.com>
Thu, 1 Apr 2021 20:44:34 +0000 (20:44 +0000)
commit71699a551d207ab373c733d8ea83a5b071ed99ee
tree639bf606f8374d2685e72919a48b4749088a3a43tree
parent78bfaf2c35fa3b4c7ff35b0b9a5fd0c8c7c5a922commit | 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.
src/api/cvc4cpp.cpp diff | blob | history
src/parser/tptp/tptp.cpp diff | blob | history
src/theory/arith/theory_arith_type_rules.h diff | blob | history
test/unit/api/sort_black.cpp diff | blob | history