projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ece1a22) | patch
Be permissive for subtyping in function definitions (#8568)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 5 Apr 2022 03:39:48 +0000 (22:39 -0500)
committerGitHub <noreply@github.com>
Tue, 5 Apr 2022 03:39:48 +0000 (03:39 +0000)
commit35ee938c99041a98338d48cf8f68730c04232958
tree97db24b15d82175f097cf6ddaa4066ec59f0352ctree
parentece1a2253eb0b35316ef3c88666099b91419225ccommit | diff
Be permissive for subtyping in function definitions (#8568)

This is to accommodate the Real theory in SMT-LIB, which says that numerals specify reals.

Instead of making our parser for numerals dependent on the logic, we are more permissive.

This fixes several spurious parsing issues in smtlib.
src/api/cpp/cvc5.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/parser/real-numerals.smt2 [new file with mode: 0644] blob