projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3072a39) | patch
Quickly recognize when PBE conjectures are infeasible (#2718)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 21 Nov 2018 22:24:16 +0000 (16:24 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 21 Nov 2018 22:24:16 +0000 (14:24 -0800)
commit1e7ce9dcc5268c8e13466f63ac2c4159d71a583a
treee705a65b9957960a278382d9de70681aabae5594tree
parent3072a39f6bda5a5ce0dd538e0f1a1bd1b744d122commit | diff
Quickly recognize when PBE conjectures are infeasible (#2718)

Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.

This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.

After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.h diff | blob | history
src/theory/quantifiers/sygus/sygus_unif_io.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/array_search_2.sy diff | blob | history