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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 14 Feb 2018 23:55:23 +0000 (17:55 -0600)
committer	GitHub <noreply@github.com>
	Wed, 14 Feb 2018 23:55:23 +0000 (17:55 -0600)
commit	bf385ca69a958e0939524d8fbcf988c1fb45d131
tree	469f60484b68df6ccd00cbc68320b1b18f2e0865	tree
parent	3c730da7c39dc5cba11bdea99191e361e505bbc8	commit \| diff

Quantifiers subdirectories (#1608)

120 files changed:

src/Makefile.am		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.h		diff \| blob \| history
src/theory/quantifiers/ambqi_builder.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ambqi_builder.h	[deleted file]	blob \| history
src/theory/quantifiers/bounded_integers.cpp	[deleted file]	blob \| history
src/theory/quantifiers/bounded_integers.h	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_conjecture.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_conjecture.h	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_instantiation.h	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_pbe.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_pbe.h	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_single_inv.h	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.h	[deleted file]	blob \| history
src/theory/quantifiers/ceg_instantiator.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ceg_instantiator.h	[deleted file]	blob \| history
src/theory/quantifiers/ceg_t_instantiator.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ceg_t_instantiator.h	[deleted file]	blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/cegqi/ceg_instantiator.h	[new file with mode: 0644]	blob
src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/cegqi/ceg_t_instantiator.h	[new file with mode: 0644]	blob
src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/cegqi/inst_strategy_cbqi.h	[new file with mode: 0644]	blob
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/ho_trigger.h	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/inst_match_generator.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/inst_match_generator.h	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/inst_strategy_e_matching.h	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/instantiation_engine.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/instantiation_engine.h	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/trigger.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/trigger.h	[new file with mode: 0644]	blob
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/ambqi_builder.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/ambqi_builder.h	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/bounded_integers.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/bounded_integers.h	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/full_model_check.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/full_model_check.h	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/model_builder.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/model_builder.h	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/model_engine.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/fmf/model_engine.h	[new file with mode: 0644]	blob
src/theory/quantifiers/full_model_check.cpp	[deleted file]	blob \| history
src/theory/quantifiers/full_model_check.h	[deleted file]	blob \| history
src/theory/quantifiers/ho_trigger.cpp	[deleted file]	blob \| history
src/theory/quantifiers/ho_trigger.h	[deleted file]	blob \| history
src/theory/quantifiers/inst_match_generator.cpp	[deleted file]	blob \| history
src/theory/quantifiers/inst_match_generator.h	[deleted file]	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp	[deleted file]	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h	[deleted file]	blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp	[deleted file]	blob \| history
src/theory/quantifiers/inst_strategy_e_matching.h	[deleted file]	blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.cpp	[deleted file]	blob \| history
src/theory/quantifiers/instantiation_engine.h	[deleted file]	blob \| history
src/theory/quantifiers/macros.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp	[deleted file]	blob \| history
src/theory/quantifiers/model_builder.h	[deleted file]	blob \| history
src/theory/quantifiers/model_engine.cpp	[deleted file]	blob \| history
src/theory/quantifiers/model_engine.h	[deleted file]	blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.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/rewrite_engine.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_conjecture.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/ce_guided_conjecture.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/ce_guided_instantiation.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/ce_guided_instantiation.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/ce_guided_single_inv.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_explain.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_explain.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_grammar_cons.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_grammar_norm.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_grammar_red.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_grammar_red.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_invariance.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_invariance.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_pbe.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_pbe.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_process_conj.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_process_conj.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/term_database_sygus.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/term_database_sygus.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus_explain.cpp	[deleted file]	blob \| history
src/theory/quantifiers/sygus_explain.h	[deleted file]	blob \| history
src/theory/quantifiers/sygus_grammar_cons.cpp	[deleted file]	blob \| history
src/theory/quantifiers/sygus_grammar_cons.h	[deleted file]	blob \| history
src/theory/quantifiers/sygus_grammar_norm.cpp	[deleted file]	blob \| history
src/theory/quantifiers/sygus_grammar_norm.h	[deleted file]	blob \| history
src/theory/quantifiers/sygus_grammar_red.cpp	[deleted file]	blob \| history
src/theory/quantifiers/sygus_grammar_red.h	[deleted file]	blob \| history
src/theory/quantifiers/sygus_invariance.cpp	[deleted file]	blob \| history
src/theory/quantifiers/sygus_invariance.h	[deleted file]	blob \| history
src/theory/quantifiers/sygus_process_conj.cpp	[deleted file]	blob \| history
src/theory/quantifiers/sygus_process_conj.h	[deleted file]	blob \| history
src/theory/quantifiers/sygus_sampler.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database_sygus.cpp	[deleted file]	blob \| history
src/theory/quantifiers/term_database_sygus.h	[deleted file]	blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/trigger.cpp	[deleted file]	blob \| history
src/theory/quantifiers/trigger.h	[deleted file]	blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_instantiator_white.h		diff \| blob \| history

RSS Atom