Support for SyGuS PBE + recursive functions (#3433)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 6 Nov 2019 16:00:08 +0000 (10:00 -0600)
committerGitHub <noreply@github.com>
Wed, 6 Nov 2019 16:00:08 +0000 (10:00 -0600)
commit52e71b709504ed06ced34962692a329f4c8282ce
treeda64b2bf12fd4f176833a53d36175131799e3c1d
parentdcccaec1155c66f2e52cfe823bc9654c46e3832b
Support for SyGuS PBE + recursive functions (#3433)
src/CMakeLists.txt
src/options/quantifiers_options.toml
src/theory/quantifiers/fun_def_evaluator.cpp [new file with mode: 0644]
src/theory/quantifiers/fun_def_evaluator.h [new file with mode: 0644]
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus/synth_engine.cpp
src/theory/quantifiers/sygus/synth_engine.h
src/theory/quantifiers/sygus/term_database_sygus.cpp
src/theory/quantifiers/sygus/term_database_sygus.h
test/regress/CMakeLists.txt
test/regress/regress1/sygus/rec-fun-sygus.sy [new file with mode: 0644]