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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 17 Mar 2021 18:43:39 +0000 (13:43 -0500)
committer	GitHub <noreply@github.com>
	Wed, 17 Mar 2021 18:43:39 +0000 (18:43 +0000)
commit	7e9a4a35084c4e9dcb047a4593dcdf256244bf9b
tree	a09ebd34408bd3c5ae0e6db2579833bcc452f508	tree
parent	c21a80e2f9d54596f2b1f993be4dbd271c3651aa	commit \| diff

Move utilities for inferred bounds on quantifers to own class (#6159)

This also moves some methods from TermEnumeration to QuantifiersBoundInference.

This is required for breaking several cyclic dependencies within quantifiers.

20 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/quant_bound_inference.h	[new file with mode: 0644]	blob
src/theory/quantifiers/quant_rep_bound_ext.cpp		diff \| blob \| history
src/theory/quantifiers/quant_rep_bound_ext.h		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_registry.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_registry.h		diff \| blob \| history
src/theory/quantifiers/term_enumeration.cpp		diff \| blob \| history
src/theory/quantifiers/term_enumeration.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history

RSS Atom