projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5ad9f1e) | patch
Update experimental scripts. Support top-level non-terminals in sygus grammars....
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 11 Jun 2015 13:03:52 +0000 (15:03 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 11 Jun 2015 13:03:52 +0000 (15:03 +0200)
commitf1f79835adeac5c22fb744c38a83fef01d0002ad
treed6f69c1426ee36f8aeba5fbd0a92a008c4f68d7ftree
parent5ad9f1e8a19d9658a86203fe2db8ad9fb329cd8ecommit | diff
Update experimental scripts.  Support top-level non-terminals in sygus grammars.  Allow -N in sygus terms.  Minor bug fix in datatypes_sygus. Add regression.
contrib/run-script-smtcomp2015-application-experimental diff | blob | history
contrib/run-script-smtcomp2015-experimental diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/tl-type.sy [new file with mode: 0644] blob