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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 10 Oct 2017 02:56:40 +0000 (21:56 -0500)
committer	GitHub <noreply@github.com>
	Tue, 10 Oct 2017 02:56:40 +0000 (21:56 -0500)
commit	96a0bc3b022b67b5ab79bf2ab087573c65a8d248
tree	427223e34ce9bd100ef4443c80b95a9526169363	tree
parent	3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7	commit \| diff

Split term database (#1206)

* Move equality query to own file, move equality inference to quantifiers engine.

* Move quantifiers attributes out of TermDb and into QuantAttribute.

* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.

* Split term database into term util.

* Partial fix for #1205 that eliminates need for dependency in node.cpp.

* Add more references to github issues.

56 files changed:

src/Makefile.am		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/anti_skolem.cpp		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.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_instantiation.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_pbe.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/ceg_t_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/equality_query.h	[new file with mode: 0644]	blob
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_process.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.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/local_theory_ext.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_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_equality_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/term_util.h	[new file with mode: 0644]	blob
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/trigger.cpp		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/sep/theory_sep.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.h		diff \| blob \| history

RSS Atom