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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Mon, 28 Mar 2022 22:30:19 +0000 (15:30 -0700)
committer	GitHub <noreply@github.com>
	Mon, 28 Mar 2022 22:30:19 +0000 (15:30 -0700)
commit	8ae907ba487d68f6d07324d144a810eb78dd0250
tree	78fc2309b5f18ec2ffe3a9e0ed8671fae82202c0	tree
parent	a8b58d71052ac692438f0303121adc06f08585ee	commit \| diff

Rename get-interpol to get-interpolant. (#8424)

35 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/java/io/github/cvc5/api/Solver.java		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/interpolation_solver.h		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/smt_mode.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_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/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