projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8182ab9) | patch
Trivial solve method for single invocation sygus (#3328)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 1 Oct 2019 06:56:57 +0000 (01:56 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 1 Oct 2019 06:56:57 +0000 (23:56 -0700)
commit2e1b546811778f2c95f07b70f42e458b0552fab0
treee819e393153d339128914477b9bbf0e458bcf4edtree
parent8182ab9f7d8d6c732202371c24bafd721ef6cfcccommit | diff
Trivial solve method for single invocation sygus (#3328)

This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/cegqi-si-string-triv.sy [new file with mode: 0644] blob