New algorithm for interpolation and abduction based on unsat cores (#3255)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 6 Dec 2019 18:03:40 +0000 (12:03 -0600)
committerGitHub <noreply@github.com>
Fri, 6 Dec 2019 18:03:40 +0000 (12:03 -0600)
commit30e5875e066e917b69d01189233aec26ce226cd6
tree9ff9dd4a609a0989f416880c10183e228276c048
parentc7c2d593674e3776ab0c720be1c0c759db8f9453
New algorithm for interpolation and abduction based on unsat cores (#3255)
12 files changed:
src/CMakeLists.txt
src/options/quantifiers_options.toml
src/options/smt_options.toml
src/smt/smt_engine.cpp
src/theory/quantifiers/sygus/cegis_core_connective.cpp [new file with mode: 0644]
src/theory/quantifiers/sygus/cegis_core_connective.h [new file with mode: 0644]
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus/synth_conjecture.h
test/regress/CMakeLists.txt
test/regress/regress1/sygus-abduct-test-ccore.smt2 [new file with mode: 0644]
test/regress/regress1/sygus-abduct-test-user.smt2
test/regress/regress1/sygus/abd-simple-conj-4.smt2 [new file with mode: 0644]