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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 2 Sep 2021 18:06:46 +0000 (13:06 -0500)
committer	GitHub <noreply@github.com>
	Thu, 2 Sep 2021 18:06:46 +0000 (18:06 +0000)
commit	522fd010b5a64574040c6e4d2a479fa0d8b569d2
tree	3bce307ba2e979aa156b09cfae733a90cefe74b9	tree
parent	b6e6029655bff19058161ea51af6c456a8151835	commit \| diff

Remove more instances of ufHo (#7087)

Towards replacing that option with a logic check throughout.

12 files changed:

src/theory/model_manager.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/sort_inference.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_model_builder.h		diff \| blob \| history
src/theory/uf/ho_extension.cpp		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.cpp		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.h		diff \| blob \| history