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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 7 May 2022 02:22:12 +0000 (21:22 -0500)
committer	GitHub <noreply@github.com>
	Sat, 7 May 2022 02:22:12 +0000 (02:22 +0000)
commit	42e503ba7d13c054f0b755a7fbda76abd3506f4b
tree	2b93a50dbc217d178c179ed94d8a9159dd154bfb	tree
parent	4e44b19469f46def8b3b6db6f9bb8bcc2423c22f	commit \| diff

More preparation for strict type rules (#8733)

This is work towards making equalities and substitutions between terms of equal types.

20 files changed:

src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/theory/arith/arith_msum.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/linear/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/proof_checker.cpp		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/substitutions.cpp		diff \| blob \| history
test/api/cpp/reset_assertions.cpp		diff \| blob \| history
test/api/python/reset_assertions.py		diff \| blob \| history
test/regress/cli/CMakeLists.txt		diff \| blob \| history
test/regress/cli/regress0/datatypes/dd.pair-real-bool-const-conf.smt2	[new file with mode: 0644]	blob
test/regress/cli/regress1/abduction/abd-real-const.smt2		diff \| blob \| history
test/regress/cli/regress1/ho/issue4758.smt2		diff \| blob \| history