From: PaulMeng Date: Tue, 5 Jul 2016 17:56:53 +0000 (-0400) Subject: Merge branch 'master' of https://github.com/CVC4/CVC4.git X-Git-Tag: cvc5-1.0.0~6049 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=36a0d1d948f201471596e092136c5a00103f78af;p=cvc5.git Merge branch 'master' of https://github.com/CVC4/CVC4.git Conflicts: proofs/signatures/Makefile.am src/Makefile.am src/expr/datatype.cpp src/options/datatypes_options src/options/options_template.cpp src/options/quantifiers_options src/proof/arith_proof.cpp src/proof/arith_proof.h src/proof/array_proof.cpp src/proof/array_proof.h src/proof/bitvector_proof.cpp src/proof/bitvector_proof.h src/proof/cnf_proof.cpp src/proof/cnf_proof.h src/proof/proof_manager.cpp src/proof/proof_manager.h src/proof/sat_proof.h src/proof/sat_proof_implementation.h src/proof/skolemization_manager.h src/proof/theory_proof.cpp src/proof/theory_proof.h src/proof/uf_proof.cpp src/proof/uf_proof.h src/prop/cnf_stream.cpp src/prop/cnf_stream.h src/prop/minisat/core/Solver.cc src/prop/prop_engine.cpp src/prop/prop_engine.h src/prop/theory_proxy.cpp src/smt/smt_engine.cpp src/smt/smt_engine_check_proof.cpp src/theory/arrays/array_proof_reconstruction.cpp src/theory/arrays/theory_arrays.cpp src/theory/bv/eager_bitblaster.cpp src/theory/bv/lazy_bitblaster.cpp src/theory/datatypes/theory_datatypes.cpp src/theory/quantifiers/alpha_equivalence.cpp src/theory/quantifiers/candidate_generator.cpp src/theory/quantifiers/candidate_generator.h src/theory/quantifiers/ce_guided_single_inv.cpp src/theory/quantifiers/ceg_instantiator.cpp src/theory/quantifiers/conjecture_generator.cpp src/theory/quantifiers/equality_infer.cpp src/theory/quantifiers/equality_infer.h src/theory/quantifiers/inst_match_generator.cpp src/theory/quantifiers/inst_propagator.cpp src/theory/quantifiers/inst_propagator.h src/theory/quantifiers/inst_strategy_e_matching.cpp src/theory/quantifiers/inst_strategy_e_matching.h src/theory/quantifiers/instantiation_engine.cpp src/theory/quantifiers/model_builder.cpp src/theory/quantifiers/model_engine.cpp src/theory/quantifiers/quant_conflict_find.cpp src/theory/quantifiers/quant_conflict_find.h src/theory/quantifiers/quant_split.cpp src/theory/quantifiers/quant_util.cpp src/theory/quantifiers/quantifiers_rewriter.cpp src/theory/quantifiers/quantifiers_rewriter.h src/theory/quantifiers/term_database.cpp src/theory/quantifiers/term_database.h src/theory/quantifiers/trigger.cpp src/theory/quantifiers/trigger.h src/theory/quantifiers_engine.cpp src/theory/quantifiers_engine.h src/theory/sets/kinds src/theory/sets/theory_sets_private.cpp src/theory/sets/theory_sets_private.h src/theory/sets/theory_sets_rewriter.cpp src/theory/sets/theory_sets_type_rules.h src/theory/strings/theory_strings.cpp src/theory/strings/theory_strings.h src/theory/theory_engine.cpp src/theory/theory_engine.h src/theory/uf/equality_engine.cpp test/regress/regress0/fmf/Makefile.am test/regress/regress0/quantifiers/Makefile.am test/regress/regress0/strings/Makefile.am test/regress/regress0/sygus/Makefile.am test/regress/regress0/sygus/max2-univ.sy --- 36a0d1d948f201471596e092136c5a00103f78af diff --cc proofs/signatures/Makefile.am index 2b6d16cfd,75d9f3c5a..5947ad3f0 --- a/proofs/signatures/Makefile.am +++ b/proofs/signatures/Makefile.am @@@ -3,7 -3,7 +3,8 @@@ # add support for more theories, just list them here in the same order # you would to the LFSC proof-checker binary. # - CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf ++ + CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_bv_rewrites.plf th_real.plf th_int.plf noinst_LTLIBRARIES = libsignatures.la diff --cc src/expr/datatype.cpp index d14ac26d4,001f38a79..12cab48cc --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@@ -859,18 -859,9 +859,10 @@@ bool DatatypeConstructor::isInterpreted if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } + bool success = true; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - Type t = (*i).getRangeType(); - if( t.isDatatype() ){ - const Datatype& dt = ((DatatypeType)t).getDatatype(); - if( !dt.isUFinite() ){ - success = false; - } - }else if(!t.isSort() && !t.getCardinality().isFinite()) { - success = false; - } - if(!success ){ + TypeNode t = TypeNode::fromType( (*i).getRangeType() ); + if(!t.isInterpretedFinite()) { self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); return false; diff --cc src/expr/datatype.h index 1197b4a3b,dfd893fe8..a0c9cbe6b --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@@ -613,6 -613,6 +613,9 @@@ public /** get the record representation for this datatype */ inline Record * getRecord() const; ++ /** get the record representation for this datatype */ ++ inline Record * getRecord() const; ++ /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be diff --cc src/expr/expr_manager_template.h index 04f2f4289,31c911736..9c4e554e1 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@@ -124,6 -124,6 +124,9 @@@ public /** Get the type for regular expressions. */ RegExpType regExpType() const; ++ /** Get the type for regular expressions. */ ++ RegExpType regExpType() const; ++ /** Get the type for reals. */ RealType realType() const; diff --cc src/options/quantifiers_options index 74b3011a6,980179378..4d228bbad --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@@ -109,6 -111,9 +111,8 @@@ option instLevelInputOnly --inst-level- only input terms are assigned instantiation level zero option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode selection mode for representatives in quantifiers engine + option instRelevantCond --inst-rlv-cond bool :default false + add relevancy conditions for instantiations - option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly diff --cc src/proof/bitvector_proof.cpp index b63782226,f557d5063..f19e45920 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@@ -516,7 -797,7 +797,7 @@@ void LFSCBitVectorProof::printTermBitbl case kind::BITVECTOR_SHL : case kind::BITVECTOR_LSHR : case kind::BITVECTOR_ASHR : { -- // these are terms for which bit-blasting is not supported yet ++ // these are terms for which bit-blasting is not supported yet std::ostringstream paren; os <<"(trust_bblast_term _ "; paren <<")"; diff --cc src/prop/minisat/core/Solver.cc index 411b89514,d898b66a2..a682a893b --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@@ -379,7 -394,7 +394,7 @@@ bool Solver::addClause_(vec& ps, b cr = ca.alloc(clauseLevel, ps, false); clauses_persistent.push(cr); -- attachClause(cr); ++ attachClause(cr); if(PROOF_ON()) { PROOF( @@@ -1234,12 -1249,12 +1249,12 @@@ lbool Solver::search(int nof_conflicts } else { -- // If this was a final check, we are satisfiable ++ // If this was a final check, we are satisfiable if (check_type == CHECK_FINAL) { -- bool decisionEngineDone = proxy->isDecisionEngineDone(); ++ bool decisionEngineDone = proxy->isDecisionEngineDone(); // Unless a lemma has added more stuff to the queues if (!decisionEngineDone && -- (!order_heap.empty() || qhead < trail.size()) ) { ++ (!order_heap.empty() || qhead < trail.size()) ) { check_type = CHECK_WITH_THEORY; continue; } else if (recheck) { diff --cc src/theory/bv/bitblaster_template.h index cfbadbf32,929bccada..c6c0d6def --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@@ -268,6 -268,6 +268,8 @@@ class EagerBitblaster : public TBitblas MinisatEmptyNotify d_notify; ++ MinisatEmptyNotify d_notify; ++ Node getModelFromSatSolver(TNode a, bool fullModel); bool isSharedTerm(TNode node); diff --cc src/theory/quantifiers/alpha_equivalence.cpp index 80066d690,a00d6d8a1..a00d6d8a1 mode 100644,100644..100755 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp diff --cc src/theory/quantifiers/alpha_equivalence.h index 8e7556eb6,8e7556eb6..8e7556eb6 mode 100644,100644..100755 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h diff --cc src/theory/quantifiers/ambqi_builder.cpp index 5192da7de,97116dee4..97116dee4 mode 100644,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,3669d38b7..3669d38b7 mode 100644,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,c8d18aced..c8d18aced mode 100644,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,721371159..721371159 mode 100644,100644..100755 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h diff --cc src/theory/quantifiers/bounded_integers.cpp index d32ef59a1,7184624da..7184624da mode 100644,100644..100755 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp diff --cc src/theory/quantifiers/bounded_integers.h index 7d15097bd,ab4bcba96..ab4bcba96 mode 100644,100644..100755 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h diff --cc src/theory/quantifiers/candidate_generator.cpp index 43f5ee2fd,a0d9bda0f..a0d9bda0f mode 100644,100644..100755 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp diff --cc src/theory/quantifiers/candidate_generator.h index 18ef6a086,4fc6969fc..4fc6969fc mode 100644,100644..100755 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h diff --cc src/theory/quantifiers/ce_guided_instantiation.cpp index d9059a3e6,71bf7c426..71bf7c426 mode 100644,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_instantiation.h index 57dc31850,c8b41c035..c8b41c035 mode 100644,100644..100755 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h diff --cc src/theory/quantifiers/ce_guided_single_inv.cpp index 33856d226,3177739ac..3177739ac mode 100644,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 4d2f9a0e5,4d2f9a0e5..4d2f9a0e5 mode 100644,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/ce_guided_single_inv_ei.cpp index 6394fca3d,6394fca3d..6394fca3d mode 100644,100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp diff --cc src/theory/quantifiers/ce_guided_single_inv_ei.h index 42e0b0820,42e0b0820..42e0b0820 mode 100644,100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.h +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.h diff --cc src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 240c2ed12,240c2ed12..240c2ed12 mode 100644,100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff --cc src/theory/quantifiers/ce_guided_single_inv_sol.h index cb6f6bc41,cb6f6bc41..cb6f6bc41 mode 100644,100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h diff --cc src/theory/quantifiers/ceg_instantiator.cpp index da488ea98,cd263e90c..cd263e90c mode 100644,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,3d7bbcb55..3d7bbcb55 mode 100644,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 2cc49ef5a,f4eb67d74..f4eb67d74 mode 100644,100644..100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp diff --cc src/theory/quantifiers/conjecture_generator.h index c89d0f2ee,c89d0f2ee..c89d0f2ee mode 100644,100644..100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h diff --cc src/theory/quantifiers/equality_infer.cpp index c3064116f,5190025ee..5190025ee mode 100644,100644..100755 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp diff --cc src/theory/quantifiers/equality_infer.h index 93c7bd080,80d6ef98b..80d6ef98b mode 100644,100644..100755 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h diff --cc src/theory/quantifiers/first_order_model.cpp index a833f48d2,670f0eff3..670f0eff3 mode 100644,100644..100755 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp diff --cc src/theory/quantifiers/first_order_model.h index cbe83cfa5,cbe83cfa5..cbe83cfa5 mode 100644,100644..100755 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h diff --cc src/theory/quantifiers/full_model_check.cpp index 33c853328,a0665cb7f..a0665cb7f mode 100644,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,411b7a5eb..411b7a5eb mode 100644,100644..100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h diff --cc src/theory/quantifiers/fun_def_engine.cpp index cf1d14663,cf1d14663..cf1d14663 mode 100644,100644..100755 --- a/src/theory/quantifiers/fun_def_engine.cpp +++ b/src/theory/quantifiers/fun_def_engine.cpp diff --cc src/theory/quantifiers/fun_def_engine.h index 3b95281c0,3b95281c0..3b95281c0 mode 100644,100644..100755 --- a/src/theory/quantifiers/fun_def_engine.h +++ b/src/theory/quantifiers/fun_def_engine.h diff --cc src/theory/quantifiers/fun_def_process.cpp index 9109aab8a,9109aab8a..9109aab8a mode 100644,100644..100755 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp diff --cc src/theory/quantifiers/fun_def_process.h index 1f6ee6562,1f6ee6562..1f6ee6562 mode 100644,100644..100755 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h diff --cc src/theory/quantifiers/inst_match.cpp index 8818175db,8818175db..8818175db mode 100644,100644..100755 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp diff --cc src/theory/quantifiers/inst_match.h index ad287c1a3,ad287c1a3..ad287c1a3 mode 100644,100644..100755 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h diff --cc src/theory/quantifiers/inst_match_generator.cpp index bf05de3bb,2d3bf76f6..2d3bf76f6 mode 100644,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 a1d907001,096774c51..096774c51 mode 100644,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 d4be58636,41c9c40c8..41c9c40c8 mode 100644,100644..100755 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp diff --cc src/theory/quantifiers/inst_propagator.h index 0c02c7f95,6201cf152..6201cf152 mode 100644,100644..100755 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h diff --cc src/theory/quantifiers/inst_strategy_cbqi.cpp index 149330c61,523d868b5..523d868b5 mode 100644,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,8ed59778b..8ed59778b mode 100644,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 630880690,efd765c86..efd765c86 mode 100644,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/inst_strategy_e_matching.h index 028f24b27,e6d993294..e6d993294 mode 100644,100644..100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h diff --cc src/theory/quantifiers/instantiation_engine.cpp index 955dc5d86,db597d031..db597d031 mode 100644,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,d2b3740a1..d2b3740a1 mode 100644,100644..100755 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h diff --cc src/theory/quantifiers/kinds index b03c4ad3b,b03c4ad3b..b03c4ad3b mode 100644,100644..100755 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds diff --cc src/theory/quantifiers/local_theory_ext.cpp index ada28c084,ada28c084..ada28c084 mode 100644,100644..100755 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp diff --cc src/theory/quantifiers/local_theory_ext.h index 94abf3c90,94abf3c90..94abf3c90 mode 100644,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,582599680..582599680 mode 100644,100644..100755 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp diff --cc src/theory/quantifiers/macros.h index 39ec2f0a1,39ec2f0a1..39ec2f0a1 mode 100644,100644..100755 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h diff --cc src/theory/quantifiers/model_builder.cpp index 3ae36b1d4,10a5ae41b..10a5ae41b mode 100644,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 906673903,e4f9529a8..e4f9529a8 mode 100644,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 0bbca88eb,5d575969f..5d575969f mode 100644,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,12f18aa08..12f18aa08 mode 100644,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 ca87a607d,bac2aa35c..bac2aa35c mode 100644,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 8b42b0916,47a66b1b1..47a66b1b1 mode 100644,100644..100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h diff --cc src/theory/quantifiers/quant_equality_engine.cpp index 3f89a799c,3f89a799c..3f89a799c mode 100644,100644..100755 --- a/src/theory/quantifiers/quant_equality_engine.cpp +++ b/src/theory/quantifiers/quant_equality_engine.cpp diff --cc src/theory/quantifiers/quant_equality_engine.h index 26654de4d,26654de4d..26654de4d mode 100644,100644..100755 --- a/src/theory/quantifiers/quant_equality_engine.h +++ b/src/theory/quantifiers/quant_equality_engine.h diff --cc src/theory/quantifiers/quant_split.cpp index 9fb943e5e,5aff1a848..5aff1a848 mode 100644,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,d36824998..d36824998 mode 100644,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 3b7787a20,b9aab0236..b9aab0236 mode 100644,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,79cdae437..79cdae437 mode 100644,100644..100755 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h diff --cc src/theory/quantifiers/quantifiers_attributes.cpp index b797f4ce9,b797f4ce9..b797f4ce9 mode 100644,100644..100755 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp diff --cc src/theory/quantifiers/quantifiers_attributes.h index 53cef796a,53cef796a..53cef796a mode 100644,100644..100755 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h diff --cc src/theory/quantifiers/quantifiers_rewriter.cpp index 5aae4d640,68f824c57..68f824c57 mode 100644,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 2071d1793,776517109..776517109 mode 100644,100644..100755 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h diff --cc src/theory/quantifiers/relevant_domain.cpp index b353fce2f,b4b51fd84..b4b51fd84 mode 100644,100644..100755 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp diff --cc src/theory/quantifiers/relevant_domain.h index 2b90520fd,2b90520fd..2b90520fd mode 100644,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 5365dbcfa,2c58b8f77..2c58b8f77 mode 100644,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,424530696..424530696 mode 100644,100644..100755 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h diff --cc src/theory/quantifiers/symmetry_breaking.cpp index 2a2b13583,2a2b13583..2a2b13583 mode 100644,100644..100755 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp diff --cc src/theory/quantifiers/symmetry_breaking.h index 38fea4f45,e682955e7..e682955e7 mode 100644,100644..100755 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h diff --cc src/theory/quantifiers/term_database.cpp index 8b09d8e5d,d3a5e178f..d3a5e178f mode 100644,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 a62b343a2,7ab3668eb..7ab3668eb mode 100644,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 efe40aaa8,7ad13b3a8..7ad13b3a8 mode 100644,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,6775e0536..6775e0536 mode 100644,100644..100755 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h diff --cc src/theory/quantifiers/theory_quantifiers_type_rules.h index 6ba57afb4,6ba57afb4..6ba57afb4 mode 100644,100644..100755 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h diff --cc src/theory/quantifiers/trigger.cpp index 38635b37b,ee091919d..ee091919d mode 100644,100644..100755 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp diff --cc src/theory/quantifiers/trigger.h index 41f2a1c38,a3da4d398..a3da4d398 mode 100644,100644..100755 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h diff --cc src/theory/sets/kinds index 3fb73749d,14c87a947..c92eab4bd --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@@ -59,11 -54,6 +59,12 @@@ typerule EMPTYSET ::CVC4::theory: typerule INSERT ::CVC4::theory::sets::InsertTypeRule typerule CARD ::CVC4::theory::sets::CardTypeRule +typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule +typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule +typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule +typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule + ++ construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule diff --cc src/theory/sets/theory_sets_private.h index 217432670,e14efd7a4..37071eb2e --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@@ -139,6 -137,6 +139,20 @@@ private */ bool lemma(Node n, SetsLemmaTag t); ++ /** send out a lemma */ ++ enum SetsLemmaTag { ++ SETS_LEMMA_DISEQUAL, ++ SETS_LEMMA_MEMBER, ++ SETS_LEMMA_GRAPH, ++ SETS_LEMMA_OTHER ++ }; ++ ++ /** ++ * returns true if a lemmas was generated ++ * returns false otherwise (found in cache) ++ */ ++ bool lemma(Node n, SetsLemmaTag t); ++ class TermInfoManager { TheorySetsPrivate& d_theory; context::Context* d_context; diff --cc src/theory/sets/theory_sets_type_rules.h index 92d6c9b6d,7a8d7eed4..478dcbdb6 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@@ -183,98 -183,6 +183,99 @@@ struct InsertTypeRule } };/* struct InsertTypeRule */ +struct RelBinaryOperatorTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::PRODUCT || + n.getKind() == kind::JOIN); + + TypeNode firstRelType = n[0].getType(check); + TypeNode secondRelType = n[1].getType(check); + TypeNode resultType = firstRelType; + + if(check) { + + if(!firstRelType.isSet() || !secondRelType.isSet()) { + throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets"); + } + if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) { + throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)"); + } + + std::vector newTupleTypes; + std::vector firstTupleTypes = firstRelType[0].getTupleTypes(); + std::vector secondTupleTypes = secondRelType[0].getTupleTypes(); + + // JOIN is not allowed to apply on two unary sets + if( n.getKind() == kind::JOIN ) { + if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) { + throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations"); + } else if(firstTupleTypes.back() != secondTupleTypes.front()) { + throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations"); + } + newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1); + newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end()); + }else if( n.getKind() == kind::PRODUCT ) { + newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()); + newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end()); + } + resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); + } + return resultType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::JOIN || + n.getKind() == kind::PRODUCT); + return false; + } +};/* struct RelBinaryOperatorTypeRule */ + +struct RelTransposeTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::TRANSPOSE); + TypeNode setType = n[0].getType(check); + if(check && !setType.isSet() && !setType.getSetElementType().isTuple()) { + throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-relation"); + } + std::vector tupleTypes = setType[0].getTupleTypes(); + std::reverse(tupleTypes.begin(), tupleTypes.end()); + return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + return false; + } +};/* struct RelTransposeTypeRule */ + +struct RelTransClosureTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::TCLOSURE); + TypeNode setType = n[0].getType(check); + if(check) { + if(!setType.isSet() && !setType.getSetElementType().isTuple()) { + throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-relation"); + } + std::vector tupleTypes = setType[0].getTupleTypes(); + if(tupleTypes.size() != 2) { + throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-binary relations"); + } + if(tupleTypes[0] != tupleTypes[1]) { + throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-homogeneous binary relations"); + } + } + return setType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::TCLOSURE); + return false; + } +};/* struct RelTransClosureTypeRule */ + ++ struct SetsProperties { inline static Cardinality computeCardinality(TypeNode type) { Assert(type.getKind() == kind::SET_TYPE);