projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e6d75ab) | patch
Add option to minimize sygus solutions based on using weakest implicants of instantia...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 26 Jul 2016 22:55:09 +0000 (17:55 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 26 Jul 2016 22:55:16 +0000 (17:55 -0500)
commit4cff52d94318646415fe89dfe3b97750451eb7c1
tree2bc60458c4ac8075ffc3ffe74175b5e76136dd1atree
parente6d75ab22dfb56df202b916ecd9b4327f931c782commit | diff
Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores.
src/options/quantifiers_options diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history