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

author	Paul Meng <baolmeng@gmail.com>
	Tue, 11 Oct 2016 18:54:20 +0000 (13:54 -0500)
committer	Paul Meng <baolmeng@gmail.com>
	Tue, 11 Oct 2016 18:54:20 +0000 (13:54 -0500)
commit	3395c5c13cd61d98aec0d9806e3b9bc3d707968a
tree	0eadad9799862ec77d29f7abe03a46c300d80de8	tree
parent	773e7d27d606b71ff0f78e84efe1deef2653f016	commit \| diff
parent	5f415d4585134612bc24e9a823289fee35541a01	commit \| diff

Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
src/options/quantifiers_options

51 files changed:

src/Makefile.am	diff1 \|	diff2 \|	blob \| history
src/parser/smt2/smt2.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ambqi_builder.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ambqi_builder.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/anti_skolem.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/anti_skolem.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/candidate_generator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ce_guided_single_inv.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ceg_instantiator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ceg_instantiator.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/conjecture_generator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/full_model_check.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/full_model_check.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_match.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_match_generator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_match_generator.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_propagator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/instantiation_engine.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/instantiation_engine.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/local_theory_ext.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/macros.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/macros.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_builder.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_builder.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_engine.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_engine.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_conflict_find.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_conflict_find.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_split.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_split.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_util.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_util.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quantifiers_rewriter.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/relevant_domain.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/rewrite_engine.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/rewrite_engine.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/term_database.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/term_database.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/theory_quantifiers.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/theory_quantifiers.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/trigger.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/trigger.h	diff1 \|	diff2 \|	blob \| history
src/theory/sets/theory_sets_private.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/sets/theory_sets_private.h	diff1 \|	diff2 \|	blob \| history
test/regress/regress0/sets/Makefile.am	diff1 \|	diff2 \|	blob \| history

RSS Atom

src/Makefile.am	diff1 \|	diff2 \|	blob \| history
src/parser/smt2/smt2.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ambqi_builder.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ambqi_builder.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/anti_skolem.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/anti_skolem.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/candidate_generator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ce_guided_single_inv.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ceg_instantiator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/ceg_instantiator.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/conjecture_generator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/full_model_check.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/full_model_check.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_match.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_match_generator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_match_generator.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_propagator.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/instantiation_engine.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/instantiation_engine.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/local_theory_ext.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/macros.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/macros.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_builder.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_builder.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_engine.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/model_engine.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_conflict_find.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_conflict_find.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_split.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_split.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_util.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quant_util.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/quantifiers_rewriter.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/relevant_domain.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/rewrite_engine.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/rewrite_engine.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/term_database.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/term_database.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/theory_quantifiers.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/theory_quantifiers.h	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/trigger.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/quantifiers/trigger.h	diff1 \|	diff2 \|	blob \| history
src/theory/sets/theory_sets_private.cpp	diff1 \|	diff2 \|	blob \| history
src/theory/sets/theory_sets_private.h	diff1 \|	diff2 \|	blob \| history
test/regress/regress0/sets/Makefile.am	diff1 \|	diff2 \|	blob \| history