From: Paul Meng Date: Tue, 11 Oct 2016 18:54:20 +0000 (-0500) Subject: Merge branch 'origin' of https://github.com/CVC4/CVC4.git X-Git-Tag: cvc5-1.0.0~6028 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3395c5c13cd61d98aec0d9806e3b9bc3d707968a;p=cvc5.git Merge branch 'origin' of https://github.com/CVC4/CVC4.git Conflicts: src/options/quantifiers_options --- 3395c5c13cd61d98aec0d9806e3b9bc3d707968a diff --cc src/theory/quantifiers/ambqi_builder.cpp index 97116dee4,2ccc17e55..2ccc17e55 mode 100755,100644..100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp diff --cc src/theory/quantifiers/ambqi_builder.h index 3669d38b7,0adaef638..0adaef638 mode 100755,100644..100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h diff --cc src/theory/quantifiers/anti_skolem.cpp index c8d18aced,9ccba38cd..9ccba38cd mode 100755,100644..100755 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp diff --cc src/theory/quantifiers/anti_skolem.h index 721371159,48205db9d..48205db9d mode 100755,100644..100755 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h diff --cc src/theory/quantifiers/candidate_generator.cpp index a0d9bda0f,8e8f34cac..8e8f34cac mode 100755,100644..100755 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp diff --cc src/theory/quantifiers/ce_guided_instantiation.cpp index 71bf7c426,54415d974..54415d974 mode 100755,100644..100755 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp diff --cc src/theory/quantifiers/ce_guided_single_inv.cpp index 981abea94,e0bbbf8ac..e0bbbf8ac mode 100755,100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp diff --cc src/theory/quantifiers/ce_guided_single_inv.h index feadeca39,449ab7189..449ab7189 mode 100755,100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h diff --cc src/theory/quantifiers/ceg_instantiator.cpp index 0fe4b98c7,61a20ad42..61a20ad42 mode 100755,100644..100755 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp diff --cc src/theory/quantifiers/ceg_instantiator.h index 3d7bbcb55,94d02de9b..94d02de9b mode 100755,100644..100755 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h diff --cc src/theory/quantifiers/conjecture_generator.cpp index f4eb67d74,11adc61fd..11adc61fd mode 100755,100644..100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp diff --cc src/theory/quantifiers/full_model_check.cpp index be608aeaa,72057e734..72057e734 mode 100755,100644..100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp diff --cc src/theory/quantifiers/full_model_check.h index 411b7a5eb,7d21b4185..7d21b4185 mode 100755,100644..100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h diff --cc src/theory/quantifiers/inst_match.cpp index 7e5424d9c,12e15d353..12e15d353 mode 100755,100644..100755 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp diff --cc src/theory/quantifiers/inst_match_generator.cpp index b3df9ca5d,2a940f1fd..2a940f1fd mode 100755,100644..100755 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp diff --cc src/theory/quantifiers/inst_match_generator.h index 65c5a1427,c238e3c4e..c238e3c4e mode 100755,100644..100755 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h diff --cc src/theory/quantifiers/inst_propagator.cpp index 41c9c40c8,1f68fb787..1f68fb787 mode 100755,100644..100755 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp diff --cc src/theory/quantifiers/inst_strategy_cbqi.cpp index 523d868b5,ac6e1edbe..ac6e1edbe mode 100755,100644..100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp diff --cc src/theory/quantifiers/inst_strategy_cbqi.h index 8ed59778b,c9f62243f..c9f62243f mode 100755,100644..100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h diff --cc src/theory/quantifiers/inst_strategy_e_matching.cpp index 49e0a698f,c4bf61b28..c4bf61b28 mode 100755,100644..100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp diff --cc src/theory/quantifiers/instantiation_engine.cpp index db597d031,afeed1e5d..afeed1e5d mode 100755,100644..100755 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp diff --cc src/theory/quantifiers/instantiation_engine.h index d2b3740a1,79963cb45..79963cb45 mode 100755,100644..100755 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h diff --cc src/theory/quantifiers/local_theory_ext.h index 94abf3c90,04a6bc9c8..04a6bc9c8 mode 100755,100644..100755 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h diff --cc src/theory/quantifiers/macros.cpp index 582599680,976b81e60..976b81e60 mode 100755,100644..100755 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp diff --cc src/theory/quantifiers/macros.h index 39ec2f0a1,60af7ad0a..60af7ad0a mode 100755,100644..100755 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h diff --cc src/theory/quantifiers/model_builder.cpp index 7bbe06108,b30c2addb..b30c2addb mode 100755,100644..100755 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp diff --cc src/theory/quantifiers/model_builder.h index e4f9529a8,9b89e5ef6..9b89e5ef6 mode 100755,100644..100755 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h diff --cc src/theory/quantifiers/model_engine.cpp index 7658f2b6b,9c09371c4..9c09371c4 mode 100755,100644..100755 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp diff --cc src/theory/quantifiers/model_engine.h index 12f18aa08,e89be8d2b..e89be8d2b mode 100755,100644..100755 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h diff --cc src/theory/quantifiers/quant_conflict_find.cpp index bac2aa35c,1e484311c..1e484311c mode 100755,100644..100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp diff --cc src/theory/quantifiers/quant_conflict_find.h index 47a66b1b1,dc8a9acb2..dc8a9acb2 mode 100755,100644..100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h diff --cc src/theory/quantifiers/quant_split.cpp index 5aff1a848,df8533135..df8533135 mode 100755,100644..100755 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp diff --cc src/theory/quantifiers/quant_split.h index d36824998,3e3b08814..3e3b08814 mode 100755,100644..100755 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h diff --cc src/theory/quantifiers/quant_util.cpp index b9aab0236,f4284a8ab..f4284a8ab mode 100755,100644..100755 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp diff --cc src/theory/quantifiers/quant_util.h index 79cdae437,3ff21aa6e..3ff21aa6e mode 100755,100644..100755 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h diff --cc src/theory/quantifiers/quantifiers_rewriter.cpp index 963889a85,de8875ae3..de8875ae3 mode 100755,100644..100755 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp diff --cc src/theory/quantifiers/quantifiers_rewriter.h index 60dc8ab10,90a22f4b7..90a22f4b7 mode 100755,100644..100755 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h diff --cc src/theory/quantifiers/relevant_domain.h index 2b90520fd,aae8f6c5b..aae8f6c5b mode 100755,100644..100755 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h diff --cc src/theory/quantifiers/rewrite_engine.cpp index 2c58b8f77,ec1b41a98..ec1b41a98 mode 100755,100644..100755 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp diff --cc src/theory/quantifiers/rewrite_engine.h index 424530696,ef3337e53..ef3337e53 mode 100755,100644..100755 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h diff --cc src/theory/quantifiers/term_database.cpp index d3a5e178f,2c6bfb7d3..2c6bfb7d3 mode 100755,100644..100755 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp diff --cc src/theory/quantifiers/term_database.h index 7ab3668eb,d4fdaa5e5..d4fdaa5e5 mode 100755,100644..100755 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h diff --cc src/theory/quantifiers/theory_quantifiers.cpp index 7ad13b3a8,e97a76ce6..e97a76ce6 mode 100755,100644..100755 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp diff --cc src/theory/quantifiers/theory_quantifiers.h index 6775e0536,ba5a75d86..ba5a75d86 mode 100755,100644..100755 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h diff --cc src/theory/quantifiers/trigger.cpp index 2faed3af0,3017238ca..3017238ca mode 100755,100644..100755 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp diff --cc src/theory/quantifiers/trigger.h index 6d7bf1f4d,631627331..631627331 mode 100755,100644..100755 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h