projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4262723) | patch
Infrastructure for partially single invocation properties. Bug fix for unconstrained...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 25 Nov 2015 17:19:57 +0000 (18:19 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 25 Nov 2015 17:20:15 +0000 (18:20 +0100)
commit7f43bd304b3d6bede36a777ee85ab68fab35d742
tree7b3f35a95f7af95ad2a67f502317ef177096f95atree
parent4262723336d82944ffed768604fcd175cdc749a9commit | diff
Infrastructure for partially single invocation properties. Bug fix for unconstrained functions in sygus solver.
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/options diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/no-mention.sy [new file with mode: 0644] blob