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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 18 Feb 2021 02:41:19 +0000 (20:41 -0600)
committer	GitHub <noreply@github.com>
	Thu, 18 Feb 2021 02:41:19 +0000 (18:41 -0800)
commit	7ca17deba3b0f0308bda304ac739caf43e9536c0
tree	6cc31f6f0692e49731e0afdcfedbed6d4f6a1fcb	tree
parent	0f03dbb1378354adcfef635a93f8b13987c2d983	commit \| diff

Move first order model for full model check to own file (#5918)

This moves the derived model class used in finite model finding to its own file, in the src/theory/quantifiers/fmf directory.

Updates the code to meet guidelines, no behavior changes.

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/first_order_model_fmc.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/first_order_model_fmc.h	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/full_model_check.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history

RSS Atom