Apply sygus repair constant techniques restricted to refinement lemmas (#3386)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 14 Oct 2019 19:23:38 +0000 (14:23 -0500)
committerGitHub <noreply@github.com>
Mon, 14 Oct 2019 19:23:38 +0000 (14:23 -0500)
commitae4be031cf818ccb69f79a588de0837d8e97897e
tree42a3124c1700e92e9e023ac8b5e813dd3ac879d5
parentd733e417bf9c96ae3da449e194e57d5b06a0607a
Apply sygus repair constant techniques restricted to refinement lemmas (#3386)
src/smt/smt_engine.cpp
src/theory/quantifiers/sygus/cegis.cpp
src/theory/quantifiers/sygus/cegis.h
src/theory/quantifiers/sygus/sygus_repair_const.cpp
src/theory/quantifiers/sygus/sygus_repair_const.h
test/regress/CMakeLists.txt
test/regress/regress1/sygus/coeff-solve-inv.sy [new file with mode: 0644]
test/regress/regress1/sygus/repair-const-rl.sy [new file with mode: 0644]