projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c8015e6) | patch
Smt2 parsing support for nested recursive datatypes (#4575)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 6 Jun 2020 00:04:10 +0000 (19:04 -0500)
committerGitHub <noreply@github.com>
Sat, 6 Jun 2020 00:04:10 +0000 (19:04 -0500)
commit6a61c1a75b08867c7c06623b8c03084056b6bed7
tree9dbf9843b61a5b12a0884d1d78026c01a87fcb79tree
parentc8015e6dc858a3fd13234ec4acb22c80cb339ddccommit | diff
Smt2 parsing support for nested recursive datatypes (#4575)

Also includes some minor improvement to expand definitions in TheoryDatatypes leftover from the branch.

Adds 3 regressions using the option --dt-nested-rec.
src/parser/parser.cpp diff | blob | history
src/parser/parser.h diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress1/datatypes/non-simple-rec-param.smt2 [new file with mode: 0644] blob
test/regress/regress1/datatypes/non-simple-rec-set.smt2 [new file with mode: 0644] blob
test/regress/regress1/datatypes/non-simple-rec.smt2 [new file with mode: 0644] blob