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

author	Gereon Kremer <gkremer@stanford.edu>
	Fri, 10 Dec 2021 20:31:01 +0000 (12:31 -0800)
committer	GitHub <noreply@github.com>
	Fri, 10 Dec 2021 20:31:01 +0000 (20:31 +0000)
commit	b14dddb404897200630c6ee1afeb98a0a24f99e0
tree	9eae862441a153b3a9002199c2f8de4ea6aa60f6	tree
parent	9ae093ec410f8dd224500113e3438bc748a19603	commit \| diff

Eliminate more static rewrites (#7786)

This PR eliminates almost all remaining static rewrites from the arithmetic theory.

12 files changed:

src/preprocessing/passes/learned_rewrite.cpp		diff \| blob \| history
src/theory/arith/bound_inference.cpp		diff \| blob \| history
src/theory/arith/bound_inference.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/infer_bounds.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.h		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history