projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d41d2a8) | patch
Move fix for vacuous sygus types out of the parser (#3820)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 Feb 2020 02:08:01 +0000 (20:08 -0600)
committerGitHub <noreply@github.com>
Thu, 27 Feb 2020 02:08:01 +0000 (20:08 -0600)
commit80f7cf5cd02ff5bb277657fd0adb616020bb9f65
treed0ddbbb05d3bf65bf819c4b4094bf3dfbda3cd8ftree
parentd41d2a817f884e0f6c8d5cb3b87b4298bc1b56f5commit | diff
Move fix for vacuous sygus types out of the parser (#3820)

This moves a fix for vacuous sygus types out of the parser and into the Expr-level datatype.

This is a temporary fix so that further progress can be made on parser migration (and to declutter the parser).

This will be refactored when an API for SyGuS is established (CVC4/cvc4-projects#38).
src/expr/datatype.cpp diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history