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

author	yoni206 <yoni206@users.noreply.github.com>
	Sat, 26 Mar 2022 17:10:06 +0000 (20:10 +0300)
committer	GitHub <noreply@github.com>
	Sat, 26 Mar 2022 17:10:06 +0000 (17:10 +0000)
commit	c7507cebfa909d6662b7a8635a9dc9e3f2bf801a
tree	b0ee2f4acaf372d056e267287244079a7559e603	tree
parent	8ee1078b5385cc03283fb2374f1f11261551b55a	commit \| diff

Separating produce-interpols from the mode of interpolant generation (#8326)

In current master, --produce-interpols takes a mode, where "none" is the default mode, in which interpolant generation is not enabled.
This PR makes --produce-interpols a Boolean, and adds a interpols-mode option to determine the mode, similarly to unsat cores.

21 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol1-push-pop.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol1.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol3-next.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol3.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol_arr1.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol_arr2.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol_cosa_1.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol_dt.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2		diff \| blob \| history
test/regress/cli/regress3/interpol2.smt2		diff \| blob \| history
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/python/test_solver.py		diff \| blob \| history

RSS Atom