Support for default grammar for datatypes in sygus. Support vts for infinity.
authorajreynol <andrew.j.reynolds@gmail.com>
Sat, 1 Aug 2015 10:25:11 +0000 (12:25 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Sat, 1 Aug 2015 10:25:11 +0000 (12:25 +0200)
commit8f4e966ae0c0f42e595e1c603cb7c3f779b713ef
treef3a46b20e752a2fb34e310ca477d4fb90bd7138e
parent91f40dee752910fca5d749656c0b6ee1bc1281aa
Support for default grammar for datatypes in sygus. Support vts for infinity.
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/theory/quantifiers/term_database.cpp
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/dt-no-syntax.sy [new file with mode: 0644]