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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 1 Nov 2017 20:20:37 +0000 (15:20 -0500)
committer	GitHub <noreply@github.com>
	Wed, 1 Nov 2017 20:20:37 +0000 (15:20 -0500)
commit	4b580ea3876055f701b13e67e0e4e78abbe47674
tree	35d1cd8f48077dfed5a5bae682f2efc90d80703f	tree
parent	13e452be03bef09e2f54f42e2bc42383505ffcea	commit \| diff

(Refactor) Split term util (#1303)

* Fix some documentation.

* Move model basis out of term db.

* Moving

* Finished moving.

* Document Skolemize and term enumeration.

* Minor

* Model basis to first order model.

* Change function name.

* Minor

* Clang format.

* Minor

* Format

* Minor

* Format

* Address review.

34 files changed:

src/Makefile.am		diff \| blob \| history
src/theory/quantifiers/ambqi_builder.cpp		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		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/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/macros.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/skolemize.h	[new file with mode: 0644]	blob
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/term_enumeration.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/term_enumeration.h	[new file with mode: 0644]	blob
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers/term_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.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.h		diff \| blob \| history

RSS Atom