projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: de3d3ca) | patch
Do not allow unresolved sorts in smt2 (#8587)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 8 Apr 2022 21:17:29 +0000 (16:17 -0500)
committerGitHub <noreply@github.com>
Fri, 8 Apr 2022 21:17:29 +0000 (21:17 +0000)
commit5e8e2d12c80bfe13ddd41ad355b348cf97eb8191
tree27bfb9c410a7271f7b98fe48b996769118d7eefctree
parentde3d3cabc372a50c953404e3e193b15ef7609ba4commit | diff
Do not allow unresolved sorts in smt2 (#8587)

This simplifies the smt2 parser so that we never parse "inlined" unresolved sorts. This infrastructure was used for accomodating the ad-hoc datatype syntax from SMT-LIB <=2.5, and SyGuS 1.0.

We now assume that sorts are fully declared wherever we parse them.
src/parser/smt2/Smt2.g diff | blob | history