projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ddf1b9) | patch
Improvements to sygus, register equivalent terms based on rewrites of original conjec...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 28 Aug 2015 11:36:44 +0000 (13:36 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 28 Aug 2015 11:36:44 +0000 (13:36 +0200)
commit6842b50e9e59c89efc21b83faa541df069b5c333
tree8dad5fc6558728f5945620052caa07cdc77d30bbtree
parent0ddf1b9c74f2b2a78e0960b710c2edbdc5f8d02dcommit | diff
Improvements to sygus, register equivalent terms based on rewrites of original conjecture, set default invariant template mode to post-condition.
src/smt/smt_engine.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/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv_sol.h diff | blob | history
src/theory/quantifiers/options diff | blob | history