git.libre-soc.org Git - cvc5.git/commit

author	Ying Sheng <sqy1415@gmail.com>
	Tue, 15 Sep 2020 01:47:15 +0000 (09:47 +0800)
committer	GitHub <noreply@github.com>
	Tue, 15 Sep 2020 01:47:15 +0000 (20:47 -0500)
commit	51be2e14c632d45e63a40659dea2177133251dfa
tree	d47380a72d05dc3ede4d61f4c04f9e4034b791fc	tree
parent	9e2a36f53007b932412a98c8e7ff1556a53f37c5	commit \| diff

Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)

Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

20 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/smt/interpolation_solver.cpp	[new file with mode: 0644]	blob
src/smt/interpolation_solver.h	[new file with mode: 0644]	blob
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_engine_state.cpp		diff \| blob \| history
src/smt/smt_engine_state.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/sygus/interpol1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol_arr1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol_arr2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol_cosa_1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol_dt.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol_from_pono_1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol_from_pono_2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol_from_pono_3.smt2	[new file with mode: 0644]	blob

RSS Atom