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

author	Tim King <taking@google.com>
	Thu, 13 Oct 2016 07:22:24 +0000 (00:22 -0700)
committer	Tim King <taking@google.com>
	Thu, 13 Oct 2016 07:22:24 +0000 (00:22 -0700)
commit	b468bb361f8b98bcb6b9d0febab4f285a6a872b3
tree	def542bce3971de0a6d646a620b79e871ae7a690	tree
parent	3395c5c13cd61d98aec0d9806e3b9bc3d707968a	commit \| diff

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

This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to 5f415d4585134612bc24e9a823289fee35541a01.

175 files changed:

.vscode/settings.json	[deleted file]	blob \| history
proofs/signatures/Makefile.am		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/expr/datatype.cpp		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/bitvector_proof.cpp		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/alpha_equivalence.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ambqi_builder.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ambqi_builder.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/anti_skolem.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/anti_skolem.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/bounded_integers.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/bounded_integers.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/candidate_generator.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/candidate_generator.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_instantiation.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_single_inv.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_single_inv_ei.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_single_inv_ei.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ceg_instantiator.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/ceg_instantiator.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/conjecture_generator.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/conjecture_generator.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/equality_infer.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/equality_infer.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/first_order_model.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/first_order_model.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/full_model_check.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/full_model_check.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/fun_def_engine.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/fun_def_engine.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/fun_def_process.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/fun_def_process.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_match.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_match.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_match_generator.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_match_generator.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_propagator.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_propagator.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/inst_strategy_e_matching.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/instantiation_engine.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/instantiation_engine.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/kinds	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/local_theory_ext.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/local_theory_ext.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/macros.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/macros.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/model_builder.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/model_builder.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/model_engine.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/model_engine.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_conflict_find.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_conflict_find.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_equality_engine.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_equality_engine.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_split.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_split.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_util.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quant_util.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quantifiers_attributes.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/quantifiers_rewriter.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/relevant_domain.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/relevant_domain.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/rewrite_engine.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/rewrite_engine.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/symmetry_breaking.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/symmetry_breaking.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/term_database.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/term_database.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/theory_quantifiers.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/theory_quantifiers.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/trigger.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/trigger.h	[changed mode: 0755->0644]	blob \| history
src/theory/sets/kinds		diff \| blob \| history
src/theory/sets/rels_utils.h	[deleted file]	blob \| history
src/theory/sets/theory_sets.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp	[deleted file]	blob \| history
src/theory/sets/theory_sets_rels.h	[deleted file]	blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
test/regress/regress0/sets/Makefile.am		diff \| blob \| history
test/regress/regress0/sets/rels/addr_book_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/addr_book_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/addr_book_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/garbage_collect.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_1tup_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_complex_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_complex_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_complex_3.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_complex_4.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_complex_5.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_conflict_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_2.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_3.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_3_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_4.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_5.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_6.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_join_7.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_mix_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_pressure_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_product_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_product_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_product_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_product_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_symbolic_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_10_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_11.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_3.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_3_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_4.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_4_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_5_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_6.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_7.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_8.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tc_9_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_2.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_2.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_3.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_int.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_tp_join_var.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_3.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_4.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_5.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_6.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/rel_transpose_7.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/rels/tobesolved/test.cvc	[deleted file]	blob \| history

RSS Atom