projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6417016) | patch
Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 10 Jun 2015 13:35:07 +0000 (15:35 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 10 Jun 2015 13:35:07 +0000 (15:35 +0200)
commit2f2b368448c3a5e50db46b3ec2cc364ae8959ac1
tree91576c0fd2ed7fee5da14598f15138a18c2cc27atree
parent6417016a38e24b09bc062a4bd4b0a5945fbcc0eccommit | diff
Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus.  Bug fix sygus argument generalization.  Add regressions.
14 files changed:
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h 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/let-ringer.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/let-simp.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/twolets2-orig.sy [new file with mode: 0644] blob