projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9e5b1fd) | patch
Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 20 Jan 2015 13:23:04 +0000 (14:23 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 20 Jan 2015 13:23:04 +0000 (14:23 +0100)
commita50f977b02c5653e03d4f3d9d8c7df1f9e2be48e
tree9e8c569a9250c6c8c7eb7826539e63ae414133d9tree
parent9e5b1fd1083c1c82d5bbc61a4a316211db629c43commit | diff
Mark datatypes as sygus.  Add option to normalize sygus terms in search.  Add sygus regressions.
15 files changed:
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/util/datatype.cpp diff | blob | history
src/util/datatype.h diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/commutative.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/constant.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/hd-01-d1-prog.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/icfp_28_10.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/max.sl diff | blob | history
test/regress/regress0/sygus/multi-fun-polynomial2.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy [new file with mode: 0644] blob