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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 12 Sep 2019 00:58:10 +0000 (19:58 -0500)
committer	GitHub <noreply@github.com>
	Thu, 12 Sep 2019 00:58:10 +0000 (19:58 -0500)
commit	d44ef0e9af9230e1949b0d3d4b03f1fcd497ad6d
tree	8de50a73a0730c9f9966b8605de4cd540a075001	tree
parent	dc3cee7cf3d49ad592139042a8e15e3905e55ee9	commit \| diff

Refactoring finite bounds in Quantifiers Engine (#3261)

14 files changed:

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