projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c871e20) | patch
Make fun-def quantifiers carry the function app they define, make fun-def utilities...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 8 Apr 2015 10:15:27 +0000 (12:15 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 8 Apr 2015 10:15:33 +0000 (12:15 +0200)
commit4448f36d5c60c05aa2fca3bc760f534cf9926caa
tree6c10032e7f2de811b0361fa50f5f4b5355a43d64tree
parentc871e203705d3e191b8c8028a3f22bca6adb0d16commit | diff
Make fun-def quantifiers carry the function app they define, make fun-def utilities more robust.  Fix bug in conjecture generation for non-parameterized operators.
src/parser/smt2/Smt2.g diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.h diff | blob | history
src/theory/quantifiers/fun_def_process.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history