diff options
150 files changed, 4442 insertions, 46 deletions
diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 000000000..44d6fcbbf --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,4 @@ +// Place your settings in this file to overwrite default and user settings. +{ + "editor.fontSize": 18 +}
\ No newline at end of file diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am index 75d9f3c5a..5947ad3f0 100644 --- a/proofs/signatures/Makefile.am +++ b/proofs/signatures/Makefile.am @@ -3,6 +3,7 @@ # 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_bv_rewrites.plf th_real.plf th_int.plf noinst_LTLIBRARIES = libsignatures.la diff --git a/src/Makefile.am b/src/Makefile.am index 235d20deb..0e3f4823b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -267,6 +267,9 @@ libcvc4_la_SOURCES = \ theory/sets/theory_sets.h \ theory/sets/theory_sets_private.cpp \ theory/sets/theory_sets_private.h \ + theory/sets/theory_sets_rels.cpp \ + theory/sets/theory_sets_rels.h \ + theory/sets/rels_utils.h \ theory/sets/theory_sets_rewriter.cpp \ theory/sets/theory_sets_rewriter.h \ theory/sets/theory_sets_type_enumerator.h \ diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 001f38a79..12cab48cc 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -859,6 +859,7 @@ bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentExcep if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } + bool success = true; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { TypeNode t = TypeNode::fromType( (*i).getRangeType() ); if(!t.isInterpretedFinite()) { diff --git a/src/expr/datatype.h b/src/expr/datatype.h index dfd893fe8..a0c9cbe6b 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -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 --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 31c911736..9c4e554e1 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -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 --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 980179378..4d228bbad 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -113,7 +113,6 @@ option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMo 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 --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4c0516eb6..e6d7f9d86 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -109,6 +109,8 @@ tokens { SUBTYPE_TOK = 'SUBTYPE'; SET_TOK = 'SET'; + + TUPLE_TOK = 'TUPLE'; FORALL_TOK = 'FORALL'; EXISTS_TOK = 'EXISTS'; @@ -201,6 +203,12 @@ tokens { BVSGT_TOK = 'BVSGT'; BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; + + // Relations + JOIN_TOK = 'JOIN'; + TRANSPOSE_TOK = 'TRANSPOSE'; + PRODUCT_TOK = 'PRODUCT'; + TRANSCLOSURE_TOK = 'TCLOSURE'; // Strings @@ -307,9 +315,14 @@ int getOperatorPrecedence(int type) { case STAR_TOK: case INTDIV_TOK: case DIV_TOK: + case TUPLE_TOK: case MOD_TOK: return 23; case PLUS_TOK: - case MINUS_TOK: return 24; + case MINUS_TOK: + case JOIN_TOK: + case TRANSPOSE_TOK: + case PRODUCT_TOK: + case TRANSCLOSURE_TOK: return 24; case LEQ_TOK: case LT_TOK: case GEQ_TOK: @@ -346,6 +359,9 @@ Kind getOperatorKind(int type, bool& negate) { case OR_TOK: return kind::OR; case XOR_TOK: return kind::XOR; case AND_TOK: return kind::AND; + + case PRODUCT_TOK: return kind::PRODUCT; + case JOIN_TOK: return kind::JOIN; // comparisonBinop case EQUAL_TOK: return kind::EQUAL; @@ -1222,8 +1238,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check] { t = EXPR_MANAGER->mkArrayType(t, t2); } | SET_TOK OF_TOK restrictedType[t,check] - { t = EXPR_MANAGER->mkSetType(t); } - + { t = EXPR_MANAGER->mkSetType(t); } + /* subtypes */ | SUBTYPE_TOK LPAREN /* A bit tricky: this LAMBDA expression cannot refer to constants @@ -1472,6 +1488,8 @@ booleanBinop[unsigned& op] | OR_TOK | XOR_TOK | AND_TOK + | JOIN_TOK + | PRODUCT_TOK ; comparison[CVC4::Expr& f] @@ -1651,6 +1669,20 @@ bvNegTerm[CVC4::Expr& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } + | TRANSPOSE_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } + | TRANSCLOSURE_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::TCLOSURE, f); } + | TUPLE_TOK LPAREN bvNegTerm[f] RPAREN + { std::vector<Type> types; + std::vector<Expr> args; + args.push_back(f); + types.push_back(f.getType()); + DatatypeType t = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = t.getDatatype(); + args.insert( args.begin(), dt[0].getConstructor() ); + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); + } | postfixTerm[f] ; @@ -1969,8 +2001,8 @@ simpleTerm[CVC4::Expr& f] Type t, t2; } /* if-then-else */ - : iteTerm[f] - + : iteTerm[f] + /* parenthesized sub-formula / tuple literals */ | LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN @@ -1987,14 +2019,15 @@ simpleTerm[CVC4::Expr& f] args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } - } + } /* empty tuple literal */ | LPAREN RPAREN { std::vector<Type> types; DatatypeType t = EXPR_MANAGER->mkTupleType(types); const Datatype& dt = t.getDatatype(); - f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } + /* empty record literal */ | PARENHASH HASHPAREN { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a46eae475..9f3c43f09 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -234,6 +234,10 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::SETMINUS, "setminus"); addOperator(kind::SUBSET, "subset"); addOperator(kind::MEMBER, "member"); + addOperator(kind::TRANSPOSE, "transpose"); + addOperator(kind::TCLOSURE, "tclosure"); + addOperator(kind::JOIN, "join"); + addOperator(kind::PRODUCT, "product"); addOperator(kind::SINGLETON, "singleton"); addOperator(kind::INSERT, "insert"); addOperator(kind::CARD, "card"); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index bc59e37ba..8bd222ca7 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -768,6 +768,22 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << "IS_IN"; opType = INFIX; break; + case kind::PRODUCT: + op << "PRODUCT"; + opType = INFIX; + break; + case kind::JOIN: + op << "JOIN"; + opType = INFIX; + break; + case kind::TRANSPOSE: + op << "TRANSPOSE"; + opType = PREFIX; + break; + case kind::TCLOSURE: + op << "TCLOSURE"; + opType = PREFIX; + break; case kind::SINGLETON: out << "{"; toStream(out, n[0], depth, types, false); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 35e6f1a73..4006a9e08 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -512,6 +512,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SUBSET: case kind::MEMBER: case kind::SET_TYPE: + case kind::TCLOSURE: + case kind::TRANSPOSE: + case kind::JOIN: + case kind::PRODUCT: case kind::SINGLETON: out << smtKindString(k) << " "; break; // fp theory @@ -797,6 +801,10 @@ static string smtKindString(Kind k) throw() { case kind::SET_TYPE: return "Set"; case kind::SINGLETON: return "singleton"; case kind::INSERT: return "insert"; + case kind::TCLOSURE: return "tclosure"; + case kind::TRANSPOSE: return "transpose"; + case kind::PRODUCT: return "product"; + case kind::JOIN: return "join"; // fp theory case kind::FLOATINGPOINT_FP: return "fp"; diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index f557d5063..f19e45920 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -797,7 +797,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { 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 --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d898b66a2..a682a893b 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -394,7 +394,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) cr = ca.alloc(clauseLevel, ps, false); clauses_persistent.push(cr); - attachClause(cr); + attachClause(cr); if(PROOF_ON()) { PROOF( @@ -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 --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 929bccada..c6c0d6def 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -268,6 +268,8 @@ class EagerBitblaster : public TBitblaster<Node> { MinisatEmptyNotify d_notify; + MinisatEmptyNotify d_notify; + Node getModelFromSatSolver(TNode a, bool fullModel); bool isSharedTerm(TNode node); diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index a00d6d8a1..a00d6d8a1 100644..100755 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 8e7556eb6..8e7556eb6 100644..100755 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 97116dee4..97116dee4 100644..100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 3669d38b7..3669d38b7 100644..100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index c8d18aced..c8d18aced 100644..100755 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 721371159..721371159 100644..100755 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 7184624da..7184624da 100644..100755 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index ab4bcba96..ab4bcba96 100644..100755 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index a0d9bda0f..a0d9bda0f 100644..100755 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 4fc6969fc..4fc6969fc 100644..100755 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 71bf7c426..71bf7c426 100644..100755 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index c8b41c035..c8b41c035 100644..100755 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 3177739ac..3177739ac 100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 4d2f9a0e5..4d2f9a0e5 100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp index 6394fca3d..6394fca3d 100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.h b/src/theory/quantifiers/ce_guided_single_inv_ei.h index 42e0b0820..42e0b0820 100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.h +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.h diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 240c2ed12..240c2ed12 100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h index cb6f6bc41..cb6f6bc41 100644..100755 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index cd263e90c..cd263e90c 100644..100755 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 3d7bbcb55..3d7bbcb55 100644..100755 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f4eb67d74..f4eb67d74 100644..100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index c89d0f2ee..c89d0f2ee 100644..100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index 5190025ee..5190025ee 100644..100755 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 80d6ef98b..80d6ef98b 100644..100755 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 670f0eff3..670f0eff3 100644..100755 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index cbe83cfa5..cbe83cfa5 100644..100755 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index a0665cb7f..a0665cb7f 100644..100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 411b7a5eb..411b7a5eb 100644..100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp index cf1d14663..cf1d14663 100644..100755 --- a/src/theory/quantifiers/fun_def_engine.cpp +++ b/src/theory/quantifiers/fun_def_engine.cpp diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h index 3b95281c0..3b95281c0 100644..100755 --- a/src/theory/quantifiers/fun_def_engine.h +++ b/src/theory/quantifiers/fun_def_engine.h diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 9109aab8a..9109aab8a 100644..100755 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 1f6ee6562..1f6ee6562 100644..100755 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 8818175db..8818175db 100644..100755 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index ad287c1a3..ad287c1a3 100644..100755 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 2d3bf76f6..2d3bf76f6 100644..100755 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 096774c51..096774c51 100644..100755 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 41c9c40c8..41c9c40c8 100644..100755 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 6201cf152..6201cf152 100644..100755 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 523d868b5..523d868b5 100644..100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 8ed59778b..8ed59778b 100644..100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index efd765c86..efd765c86 100644..100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index e6d993294..e6d993294 100644..100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index db597d031..db597d031 100644..100755 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index d2b3740a1..d2b3740a1 100644..100755 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index b03c4ad3b..b03c4ad3b 100644..100755 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index ada28c084..ada28c084 100644..100755 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 94abf3c90..94abf3c90 100644..100755 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 582599680..582599680 100644..100755 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index 39ec2f0a1..39ec2f0a1 100644..100755 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 10a5ae41b..10a5ae41b 100644..100755 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index e4f9529a8..e4f9529a8 100644..100755 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 5d575969f..5d575969f 100644..100755 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 12f18aa08..12f18aa08 100644..100755 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index bac2aa35c..bac2aa35c 100644..100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 47a66b1b1..47a66b1b1 100644..100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp index 3f89a799c..3f89a799c 100644..100755 --- a/src/theory/quantifiers/quant_equality_engine.cpp +++ b/src/theory/quantifiers/quant_equality_engine.cpp diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h index 26654de4d..26654de4d 100644..100755 --- a/src/theory/quantifiers/quant_equality_engine.h +++ b/src/theory/quantifiers/quant_equality_engine.h diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 5aff1a848..5aff1a848 100644..100755 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index d36824998..d36824998 100644..100755 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b9aab0236..b9aab0236 100644..100755 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 79cdae437..79cdae437 100644..100755 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index b797f4ce9..b797f4ce9 100644..100755 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 53cef796a..53cef796a 100644..100755 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 68f824c57..68f824c57 100644..100755 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 776517109..776517109 100644..100755 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index b4b51fd84..b4b51fd84 100644..100755 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 2b90520fd..2b90520fd 100644..100755 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 2c58b8f77..2c58b8f77 100644..100755 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 424530696..424530696 100644..100755 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp index 2a2b13583..2a2b13583 100644..100755 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index e682955e7..e682955e7 100644..100755 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d3a5e178f..d3a5e178f 100644..100755 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7ab3668eb..7ab3668eb 100644..100755 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 7ad13b3a8..7ad13b3a8 100644..100755 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 6775e0536..6775e0536 100644..100755 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 6ba57afb4..6ba57afb4 100644..100755 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index ee091919d..ee091919d 100644..100755 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index a3da4d398..a3da4d398 100644..100755 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 14c87a947..c92eab4bd 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -44,6 +44,11 @@ operator SINGLETON 1 "the set of the single element given as a parameter" operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)" operator CARD 1 "set cardinality operator" +operator JOIN 2 "set join" +operator PRODUCT 2 "set cartesian product" +operator TRANSPOSE 1 "set transpose" +operator TCLOSURE 1 "set transitive closure" + typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -54,6 +59,12 @@ typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule 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 @@ -61,4 +72,9 @@ construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule construle INSERT ::CVC4::theory::sets::InsertTypeRule construle CARD ::CVC4::theory::sets::CardTypeRule +construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule +construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule +construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule +construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule + endtheory diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h new file mode 100644 index 000000000..3b9820360 --- /dev/null +++ b/src/theory/sets/rels_utils.h @@ -0,0 +1,95 @@ +/********************* */ +/*! \file rels_utils.h + ** \verbatim + ** Original author: Paul Meng + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sets theory implementation. + ** + ** Extension to Sets theory. + **/ + +#ifndef SRC_THEORY_SETS_RELS_UTILS_H_ +#define SRC_THEORY_SETS_RELS_UTILS_H_ + +namespace CVC4 { +namespace theory { +namespace sets { + +class RelsUtils { + +public: + + // Assumption: the input rel_mem contains all constant pairs + static std::set< Node > computeTC( std::set< Node > rel_mem, Node rel ) { + std::set< Node >::iterator mem_it = rel_mem.begin(); + std::map< Node, int > ele_num_map; + std::set< Node > tc_rel_mem; + + while( mem_it != rel_mem.end() ) { + Node fst = nthElementOfTuple( *mem_it, 0 ); + Node snd = nthElementOfTuple( *mem_it, 1 ); + std::set< Node > traversed; + traversed.insert(fst); + computeTC(rel, rel_mem, fst, snd, traversed, tc_rel_mem); + mem_it++; + } + return tc_rel_mem; + } + + static void computeTC( Node rel, std::set< Node >& rel_mem, Node fst, + Node snd, std::set< Node >& traversed, std::set< Node >& tc_rel_mem ) { + tc_rel_mem.insert(constructPair(rel, fst, snd)); + if( traversed.find(snd) == traversed.end() ) { + traversed.insert(snd); + } else { + return; + } + + std::set< Node >::iterator mem_it = rel_mem.begin(); + while( mem_it != rel_mem.end() ) { + Node new_fst = nthElementOfTuple( *mem_it, 0 ); + Node new_snd = nthElementOfTuple( *mem_it, 1 ); + if( snd == new_fst ) { + computeTC(rel, rel_mem, fst, new_snd, traversed, tc_rel_mem); + } + mem_it++; + } + } + + static Node nthElementOfTuple( Node tuple, int n_th ) { + if(tuple.isConst() || (!tuple.isVar() && !tuple.isConst())) + return tuple[n_th]; + Datatype dt = tuple.getType().getDatatype(); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][n_th].getSelector(), tuple); + } + + static Node reverseTuple( Node tuple ) { + Assert( tuple.getType().isTuple() ); + std::vector<Node> elements; + std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes(); + std::reverse( tuple_types.begin(), tuple_types.end() ); + TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types ); + Datatype dt = tn.getDatatype(); + elements.push_back( Node::fromExpr(dt[0].getConstructor() ) ); + for(int i = tuple_types.size() - 1; i >= 0; --i) { + elements.push_back( nthElementOfTuple(tuple, i) ); + } + return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements ); + } + static Node constructPair(Node rel, Node a, Node b) { + Datatype dt = rel.getType().getSetElementType().getDatatype(); + return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b); + } + +}; +}/* CVC4::theory::sets namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif
\ No newline at end of file diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index bbeaf4a4c..840135937 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -33,6 +33,7 @@ class TheorySets : public Theory { private: friend class TheorySetsPrivate; friend class TheorySetsScrutinize; + friend class TheorySetsRels; TheorySetsPrivate* d_internal; public: diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index a16e857dd..aec2c119c 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -97,8 +97,12 @@ void TheorySetsPrivate::check(Theory::Effort level) { // and that leads to conflict (externally). if(d_conflict) { return; } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; + } + // invoke the relational solver + d_rels->check(level); + if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { lemma(getLemma(), SETS_LEMMA_OTHER); return; @@ -123,19 +127,16 @@ void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt) bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; - // fact already holds if( holds(atom, polarity) ) { Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl; return; } - // assert fact & check for conflict if(learnt) { registerReason(reason, /*save=*/ true); } d_equalityEngine.assertEquality(atom, polarity, reason); - if(!d_equalityEngine.consistent()) { Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl; d_conflict = true; @@ -695,6 +696,11 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements std::inserter(cur, cur.begin()) ); break; } + case kind::JOIN: + case kind::TCLOSURE: + case kind::TRANSPOSE: + case kind::PRODUCT: + break; default: Assert(theory::kindToTheoryId(k) != theory::THEORY_SETS, (std::string("Kind belonging to set theory not explicitly handled: ") + kindToString(k)).c_str()); @@ -715,6 +721,7 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, << std::endl; Assert(S.getType().isSet()); + std::set<Node> temp_nodes; const Elements emptySetOfElements; const Elements& saved = @@ -758,6 +765,74 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, std::set_difference(left.begin(), left.end(), right.begin(), right.end(), std::inserter(cur, cur.begin()) ); break; + case kind::PRODUCT: { + std::set<Node> new_tuple_set; + Elements::const_iterator left_it = left.begin(); + int left_len = (*left_it).getType().getTupleLength(); + TypeNode tn = S.getType().getSetElementType(); + while(left_it != left.end()) { + Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *left_it << std::endl; + std::vector<Node> left_tuple; + left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + for(int i = 0; i < left_len; i++) { + left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); + } + Elements::const_iterator right_it = right.begin(); + int right_len = (*right_it).getType().getTupleLength(); + while(right_it != right.end()) { + std::vector<Node> right_tuple; + for(int j = 0; j < right_len; j++) { + right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j)); + } + std::vector<Node> new_tuple; + new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end()); + new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end()); + Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); + temp_nodes.insert(composed_tuple); + new_tuple_set.insert(composed_tuple); + right_it++; + } + left_it++; + } + cur.insert(new_tuple_set.begin(), new_tuple_set.end()); + Trace("rels-debug") << " ***** Done with check model for product operator" << std::endl; + break; + } + case kind::JOIN: { + std::set<Node> new_tuple_set; + Elements::const_iterator left_it = left.begin(); + int left_len = (*left_it).getType().getTupleLength(); + TypeNode tn = S.getType().getSetElementType(); + while(left_it != left.end()) { + std::vector<Node> left_tuple; + left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + for(int i = 0; i < left_len - 1; i++) { + left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); + } + Elements::const_iterator right_it = right.begin(); + int right_len = (*right_it).getType().getTupleLength(); + while(right_it != right.end()) { + if(RelsUtils::nthElementOfTuple(*left_it,left_len-1) == RelsUtils::nthElementOfTuple(*right_it,0)) { + std::vector<Node> right_tuple; + for(int j = 1; j < right_len; j++) { + right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j)); + } + std::vector<Node> new_tuple; + new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end()); + new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end()); + Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); + new_tuple_set.insert(composed_tuple); + } + right_it++; + } + left_it++; + } + cur.insert(new_tuple_set.begin(), new_tuple_set.end()); + Trace("rels-debug") << " ***** Done with check model for JOIN operator" << std::endl; + break; + } + case kind::TCLOSURE: + break; default: Unhandled(); } @@ -990,20 +1065,20 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) m->assertRepresentative(shape); } -#ifdef CVC4_ASSERTIONS - bool checkPassed = true; - BOOST_FOREACH(TNode term, terms) { - if( term.getType().isSet() ) { - checkPassed &= checkModel(settermElementsMap, term); - } - } - if(Trace.isOn("sets-checkmodel-ignore")) { - Trace("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl; - } else { - Assert( checkPassed, - "THEORY_SETS check-model failed. Run with -d sets-model for details." ); - } -#endif +// #ifdef CVC4_ASSERTIONS +// bool checkPassed = true; +// BOOST_FOREACH(TNode term, terms) { +// if( term.getType().isSet() ) { +// checkPassed &= checkModel(settermElementsMap, term); +// } +// } +// if(Trace.isOn("sets-checkmodel-ignore")) { +// Trace("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl; +// } else { +// Assert( checkPassed, +// "THEORY_SETS check-model failed. Run with -d sets-model for details." ); +// } +// #endif } Node TheorySetsPrivate::getModelValue(TNode n) @@ -1277,6 +1352,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_ccg_i(c), d_ccg_j(c), d_scrutinize(NULL), + d_rels(NULL), d_cardEnabled(false), d_cardTerms(c), d_typesAdded(), @@ -1296,6 +1372,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_relTerms(u) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); + d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external); d_equalityEngine.addFunctionKind(kind::UNION); d_equalityEngine.addFunctionKind(kind::INTERSECTION); @@ -1316,6 +1393,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, TheorySetsPrivate::~TheorySetsPrivate() { delete d_termInfoManager; + delete d_rels; if( Debug.isOn("sets-scrutinize") ) { Assert(d_scrutinize != NULL); delete d_scrutinize; @@ -1550,21 +1628,23 @@ void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl; d_theory.conflict(t1, t2); } - -// void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t) -// { -// Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl; -// } +// + void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t) + { + Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl; + d_theory.d_rels->eqNotifyNewClass(t); + } // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2) // { // Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; // } - -// void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2) -// { -// Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; -// } +// + void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2) + { + Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; + d_theory.d_rels->eqNotifyPostMerge(t1, t2); + } // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) // { diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index e14efd7a4..37071eb2e 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -25,6 +25,8 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/sets/term_info.h" +#include "theory/sets/theory_sets_rels.h" +#include "theory/sets/rels_utils.h" namespace CVC4 { namespace theory { @@ -96,14 +98,14 @@ private: TheorySetsPrivate& d_theory; public: - NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {} + NotifyClass(TheorySetsPrivate& theory): d_theory(theory){} bool eqNotifyTriggerEquality(TNode equality, bool value); bool eqNotifyTriggerPredicate(TNode predicate, bool value); bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); void eqNotifyConstantTermMerge(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t) {} + void eqNotifyNewClass(TNode t); void eqNotifyPreMerge(TNode t1, TNode t2) {} - void eqNotifyPostMerge(TNode t1, TNode t2) {} + void eqNotifyPostMerge(TNode t1, TNode t2); void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {} } d_notify; @@ -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; @@ -243,7 +259,8 @@ private: TheorySetsScrutinize* d_scrutinize; void dumpAssertionsHumanified() const; /** do some formatting to make them more readable */ - + // relational solver + TheorySetsRels* d_rels; /***** Cardinality handling *****/ bool d_cardEnabled; diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp new file mode 100644 index 000000000..3f7d079bd --- /dev/null +++ b/src/theory/sets/theory_sets_rels.cpp @@ -0,0 +1,1904 @@ +/********************* */ +/*! \file theory_sets_rels.cpp + ** \verbatim + ** Original author: Paul Meng + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sets theory implementation. + ** + ** Extension to Sets theory. + **/ + +#include "theory/sets/theory_sets_rels.h" + +#include "expr/datatype.h" +#include "theory/sets/expr_patterns.h" +#include "theory/sets/theory_sets_private.h" +#include "theory/sets/theory_sets.h" + + +using namespace std; +using namespace CVC4::expr::pattern; + +namespace CVC4 { +namespace theory { +namespace sets { + +typedef std::map<Node, std::vector<Node> >::iterator MEM_IT; +typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_PAIR_IT; +typedef std::map<Node, std::map<kind::Kind_t, std::vector<Node> > >::iterator TERM_IT; +typedef std::map<Node, std::map<Node, std::hash_set<Node, NodeHashFunction> > >::iterator TC_IT; + +int TheorySetsRels::EqcInfo::counter = 0; + + + // do a test + void TheorySetsRels::check(Theory::Effort level) { + Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver *******************************\n" << std::endl; + if(Theory::fullEffort(level)) { + collectRelsInfo(); + check(); + doPendingLemmas(); + Assert(d_lemma_cache.empty()); + Assert(d_pending_facts.empty()); + } else { + doPendingMerge(); + doPendingLemmas(); + } + Trace("rels") << "\n[sets-rels] ******************************* Done with the relational solver *******************************\n" << std::endl; + } + + void TheorySetsRels::check() { + MEM_IT m_it = d_membership_constraints_cache.begin(); + while(m_it != d_membership_constraints_cache.end()) { + Node rel_rep = m_it->first; + + // No relational terms found with rel_rep as its representative + // But TRANSPOSE(rel_rep) may occur in the context + if(d_terms_cache.find(rel_rep) == d_terms_cache.end()) { + Node tp_rel = NodeManager::currentNM()->mkNode(kind::TRANSPOSE, rel_rep); + Node tp_rel_rep = getRepresentative(tp_rel); + + if(d_terms_cache.find(tp_rel_rep) != d_terms_cache.end()) { + for(unsigned int i = 0; i < m_it->second.size(); i++) { + // Lazily apply transpose-occur rule. + // Need to eagerly apply if we don't send facts as lemmas + applyTransposeRule(d_membership_exp_cache[rel_rep][i], tp_rel_rep, true); + } + } + } else { + for(unsigned int i = 0; i < m_it->second.size(); i++) { + Node exp = d_membership_exp_cache[rel_rep][i]; + std::map<kind::Kind_t, std::vector<Node> > kind_terms = d_terms_cache[rel_rep]; + if(kind_terms.find(kind::TRANSPOSE) != kind_terms.end()) { + std::vector<Node> tp_terms = kind_terms[kind::TRANSPOSE]; + // exp is a membership term and tp_terms contains all + // transposed terms that are equal to the right hand side of exp + for(unsigned int j = 0; j < tp_terms.size(); j++) { + applyTransposeRule(exp, tp_terms[j]); + } + } + if(kind_terms.find(kind::JOIN) != kind_terms.end()) { + std::vector<Node> join_terms = kind_terms[kind::JOIN]; + // exp is a membership term and join_terms contains all + // terms involving "join" operator that are in the same equivalence class with the right hand side of exp + for(unsigned int j = 0; j < join_terms.size(); j++) { + applyJoinRule(exp, join_terms[j]); + } + } + if(kind_terms.find(kind::PRODUCT) != kind_terms.end()) { + std::vector<Node> product_terms = kind_terms[kind::PRODUCT]; + for(unsigned int j = 0; j < product_terms.size(); j++) { + applyProductRule(exp, product_terms[j]); + } + } + if(kind_terms.find(kind::TCLOSURE) != kind_terms.end()) { + std::vector<Node> tc_terms = kind_terms[kind::TCLOSURE]; + for(unsigned int j = 0; j < tc_terms.size(); j++) { + applyTCRule(exp, tc_terms[j]); + } + } + } + } + m_it++; + } + finalizeTCInfer(); + } + + /* + * Polulate the relational terms data structure + */ + + void TheorySetsRels::collectRelsInfo() { + Trace("rels-debug") << "[sets-rels] Start collecting relational terms..." << std::endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); + while( !eqcs_i.isFinished() ){ + Node r = (*eqcs_i); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine ); + Trace("rels-ee") << "[sets-rels-ee] term representative: " << r << std::endl; + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + Trace("rels-ee") << " term : " << n << std::endl; + + if(getRepresentative(r) == getRepresentative(d_trueNode) || + getRepresentative(r) == getRepresentative(d_falseNode)) { + // collect membership info + if(n.getKind() == kind::MEMBER && n[1].getType().getSetElementType().isTuple()) { + Node tup_rep = getRepresentative(n[0]); + Node rel_rep = getRepresentative(n[1]); + // Todo: check n[0] or n[0]'s rep is a var?? + if(n[0].isVar()){ + reduceTupleVar(n); + } else { + if(safeAddToMap(d_membership_constraints_cache, rel_rep, tup_rep)) { + bool true_eq = areEqual(r, d_trueNode); + Node reason = true_eq ? n : n.negate(); + + addToMap(d_membership_exp_cache, rel_rep, reason); + Trace("rels-mem") << "[******] exp: " << reason << " for " << rel_rep << std::endl; + if(true_eq) { + addToMembershipDB(rel_rep, tup_rep, reason); + } + } + } + } + // collect relational terms info + } else if( r.getType().isSet() && r.getType().getSetElementType().isTuple() ) { + if( n.getKind() == kind::TRANSPOSE || + n.getKind() == kind::JOIN || + n.getKind() == kind::PRODUCT || + n.getKind() == kind::TCLOSURE ) { + std::map<kind::Kind_t, std::vector<Node> > rel_terms; + std::vector<Node> terms; + // No r record is found + if( d_terms_cache.find(r) == d_terms_cache.end() ) { + terms.push_back(n); + rel_terms[n.getKind()] = terms; + d_terms_cache[r] = rel_terms; + } else { + // No n's kind record is found + if( d_terms_cache[r].find(n.getKind()) == d_terms_cache[r].end() ) { + terms.push_back(n); + d_terms_cache[r][n.getKind()] = terms; + } else { + d_terms_cache[r][n.getKind()].push_back(n); + } + } + } + // need to add all tuple elements as shared terms + } else if(n.getType().isTuple() && !n.isConst() && !n.isVar()) { + for(unsigned int i = 0; i < n.getType().getTupleLength(); i++) { + Node element = RelsUtils::nthElementOfTuple(n, i); + + if(!element.isConst()) { + makeSharedTerm(element); + } + } + } + ++eqc_i; + } + ++eqcs_i; + } + Trace("rels-debug") << "[sets-rels] Done with collecting relational terms!" << std::endl; + } + + /* + * + * + * transitive closure rule 1: y = (TCLOSURE x) + * --------------------------------------------- + * y = x | x.x | x.x.x | ... (| is union) + * + * + * + * transitive closure rule 2: TCLOSURE(x) + * ----------------------------------------------------------- + * x <= TCLOSURE(x) && (x JOIN x) <= TCLOSURE(x) .... + * + * TC(x) = TC(y) => x = y ? + * + */ + + void TheorySetsRels::buildTCGraph(Node tc_r_rep, Node tc_rep, Node tc_term) { + std::map< Node, std::hash_set< Node, NodeHashFunction > > tc_graph; + MEM_IT mem_it = d_membership_db.find(tc_r_rep); + + if(mem_it != d_membership_db.end()) { + for(std::vector<Node>::iterator pair_it = mem_it->second.begin(); + pair_it != mem_it->second.end(); pair_it++) { + Node fst_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 0)); + Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 1)); + TC_PAIR_IT pair_set_it = tc_graph.find(fst_rep); + + if( pair_set_it != tc_graph.end() ) { + pair_set_it->second.insert(snd_rep); + } else { + std::hash_set< Node, NodeHashFunction > snd_set; + snd_set.insert(snd_rep); + tc_graph[fst_rep] = snd_set; + } + } + } + Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]); + if(!reason.isNull()) { + d_membership_tc_exp_cache[tc_rep] = reason; + } + d_membership_tc_cache[tc_rep] = tc_graph; + } + + void TheorySetsRels::applyTCRule(Node exp, Node tc_term) { + Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSITIVE CLOSURE rule on " + << tc_term << " with explanation " << exp << std::endl; + bool polarity = exp.getKind() != kind::NOT; + Node atom = polarity ? exp : exp[0]; + Node tup_rep = getRepresentative(atom[0]); + Node tc_rep = getRepresentative(tc_term); + Node tc_r_rep = getRepresentative(tc_term[0]); + + // build the TC graph for tc_rep if it was not created before + if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) { + Trace("rels-debug") << "[sets-rels] Start building the TC graph!" << std::endl; + buildTCGraph(tc_r_rep, tc_rep, tc_term); + d_rel_nodes.insert(tc_rep); + } + + // insert tup_rep in the tc_graph if it is not in the graph already + TC_IT tc_graph_it = d_membership_tc_cache.find(tc_rep); + + if(polarity) { + Node fst_rep = getRepresentative(RelsUtils::nthElementOfTuple(tup_rep, 0)); + Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(tup_rep, 1)); + + if(tc_graph_it != d_membership_tc_cache.end()) { + TC_PAIR_IT pair_set_it = tc_graph_it->second.find(fst_rep); + + if(pair_set_it != tc_graph_it->second.end()) { + pair_set_it->second.insert(snd_rep); + } else { + std::hash_set< Node, NodeHashFunction > pair_set; + pair_set.insert(snd_rep); + tc_graph_it->second[fst_rep] = pair_set; + } + + Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]); + std::map< Node, Node >::iterator exp_it = d_membership_tc_exp_cache.find(tc_rep); + + if(!reason.isNull() && exp_it->second != reason) { + d_membership_tc_exp_cache[tc_rep] = Rewriter::rewrite(AND(exp_it->second, reason)); + } + } else { + std::map< Node, std::hash_set< Node, NodeHashFunction > > pair_set; + std::hash_set< Node, NodeHashFunction > snd_set; + + snd_set.insert(snd_rep); + pair_set[fst_rep] = snd_set; + d_membership_tc_cache[tc_rep] = pair_set; + Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]); + + if(!reason.isNull()) { + d_membership_tc_exp_cache[tc_rep] = reason; + } + } + // check if tup_rep already exists in TC graph for conflict + } else { + if(tc_graph_it != d_membership_tc_cache.end()) { + checkTCGraphForConflict(atom, tc_rep, d_trueNode, RelsUtils::nthElementOfTuple(tup_rep, 0), + RelsUtils::nthElementOfTuple(tup_rep, 1), tc_graph_it->second); + } + } + } + + void TheorySetsRels::checkTCGraphForConflict (Node atom, Node tc_rep, Node exp, Node a, Node b, + std::map< Node, std::hash_set< Node, NodeHashFunction > >& pair_set) { + TC_PAIR_IT pair_set_it = pair_set.find(a); + + if(pair_set_it != pair_set.end()) { + if(pair_set_it->second.find(b) != pair_set_it->second.end()) { + Node reason = AND(exp, findMemExp(tc_rep, constructPair(tc_rep, a, b))); + + if(atom[1] != tc_rep) { + reason = AND(exp, explain(EQUAL(atom[1], tc_rep))); + } + Trace("rels-debug") << "[sets-rels] found a conflict and send out lemma : " + << NodeManager::currentNM()->mkNode(kind::IMPLIES, Rewriter::rewrite(reason), atom) << std::endl; + d_sets_theory.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, Rewriter::rewrite(reason), atom)); +// Trace("rels-debug") << "[sets-rels] found a conflict and send out lemma : " +// << AND(reason.negate(), atom) << std::endl; +// d_sets_theory.d_out->conflict(AND(reason.negate(), atom)); + } else { + std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); + + while(set_it != pair_set_it->second.end()) { + // need to check if *set_it has been looked already + if(!areEqual(*set_it, a)) { + checkTCGraphForConflict(atom, tc_rep, AND(exp, findMemExp(tc_rep, constructPair(tc_rep, a, *set_it))), + *set_it, b, pair_set); + } + set_it++; + } + } + } + } + + + /* product-split rule: (a, b) IS_IN (X PRODUCT Y) + * ---------------------------------- + * a IS_IN X && b IS_IN Y + * + * product-compose rule: (a, b) IS_IN X (c, d) IS_IN Y NOT (r, s, t, u) IS_IN (X PRODUCT Y) + * ---------------------------------------------------------------------- + * (a, b, c, d) IS_IN (X PRODUCT Y) + */ + + void TheorySetsRels::applyProductRule(Node exp, Node product_term) { + Trace("rels-debug") << "\n[sets-rels] *********** Applying PRODUCT rule " << std::endl; + + if(d_rel_nodes.find(product_term) == d_rel_nodes.end()) { + computeRels(product_term); + d_rel_nodes.insert(product_term); + } + bool polarity = exp.getKind() != kind::NOT; + Node atom = polarity ? exp : exp[0]; + Node r1_rep = getRepresentative(product_term[0]); + Node r2_rep = getRepresentative(product_term[1]); + + Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-SPLIT rule on term: " << product_term + << " with explanation: " << exp << std::endl; + std::vector<Node> r1_element; + std::vector<Node> r2_element; + NodeManager *nm = NodeManager::currentNM(); + Datatype dt = r1_rep.getType().getSetElementType().getDatatype(); + unsigned int i = 0; + unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength(); + unsigned int tup_len = product_term.getType().getSetElementType().getTupleLength(); + + r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); + for(; i < s1_len; ++i) { + r1_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); + } + + dt = r2_rep.getType().getSetElementType().getDatatype(); + r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); + for(; i < tup_len; ++i) { + r2_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); + } + + Node fact_1; + Node fact_2; + Node reason_1 = exp; + Node reason_2 = exp; + Node t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element); + Node t1_rep = getRepresentative(t1); + Node t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element); + Node t2_rep = getRepresentative(t2); + + fact_1 = MEMBER( t1, r1_rep ); + fact_2 = MEMBER( t2, r2_rep ); + if(r1_rep != product_term[0]) { + reason_1 = AND(reason_1, explain(EQUAL(r1_rep, product_term[0]))); + } + if(t1 != t1_rep) { + reason_1 = Rewriter::rewrite(AND(reason_1, explain(EQUAL(t1, t1_rep)))); + } + if(r2_rep != product_term[1]) { + reason_2 = AND(reason_2, explain(EQUAL(r2_rep, product_term[1]))); + } + if(t2 != t2_rep) { + reason_2 = Rewriter::rewrite(AND(reason_2, explain(EQUAL(t2, t2_rep)))); + } + if(polarity) { + sendInfer(fact_1, reason_1, "product-split"); + sendInfer(fact_2, reason_2, "product-split"); + } else { + sendInfer(fact_1.negate(), reason_1, "product-split"); + sendInfer(fact_2.negate(), reason_2, "product-split"); + + // ONLY need to explicitly compute joins if there are negative literals involving PRODUCT + Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-COMPOSE rule on term: " << product_term + << " with explanation: " << exp << std::endl; + } + } + + /* join-split rule: (a, b) IS_IN (X JOIN Y) + * -------------------------------------------- + * exists z | (a, z) IS_IN X && (z, b) IS_IN Y + * + * + * join-compose rule: (a, b) IS_IN X (b, c) IS_IN Y NOT (t, u) IS_IN (X JOIN Y) + * ------------------------------------------------------------- + * (a, c) IS_IN (X JOIN Y) + */ + void TheorySetsRels::applyJoinRule(Node exp, Node join_term) { + Trace("rels-debug") << "\n[sets-rels] *********** Applying JOIN rule " << std::endl; + if(d_rel_nodes.find(join_term) == d_rel_nodes.end()) { + computeRels(join_term); + d_rel_nodes.insert(join_term); + } + + bool polarity = exp.getKind() != kind::NOT; + Node atom = polarity ? exp : exp[0]; + Node r1_rep = getRepresentative(join_term[0]); + Node r2_rep = getRepresentative(join_term[1]); + + if(polarity) { + + Trace("rels-debug") << "\n[sets-rels] Apply JOIN-SPLIT rule on term: " << join_term + << " with explanation: " << exp << std::endl; + + std::vector<Node> r1_element; + std::vector<Node> r2_element; + NodeManager *nm = NodeManager::currentNM(); + TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0]; + Node shared_x = nm->mkSkolem("sde_", shared_type); + Datatype dt = r1_rep.getType().getSetElementType().getDatatype(); + unsigned int i = 0; + unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength(); + unsigned int tup_len = join_term.getType().getSetElementType().getTupleLength(); + + r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); + for(; i < s1_len-1; ++i) { + r1_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); + } + + r1_element.push_back(shared_x); + dt = r2_rep.getType().getSetElementType().getDatatype(); + r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); + r2_element.push_back(shared_x); + + for(; i < tup_len; ++i) { + r2_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); + } + + Node t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element); + Node t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element); + computeTupleReps(t1); + computeTupleReps(t2); + + std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[t1]); + + for(unsigned int j = 0; j < elements.size(); j++) { + std::vector<Node> new_tup; + new_tup.push_back(elements[j]); + new_tup.insert(new_tup.end(), d_tuple_reps[t2].begin()+1, d_tuple_reps[t2].end()); + if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) { + return; + } + } + + Node fact; + Node reason = atom[1] == join_term ? exp : AND(exp, explain(EQUAL(atom[1], join_term))); + Node reasons = reason; + + fact = MEMBER(t1, r1_rep); + if(r1_rep != join_term[0]) { + reasons = Rewriter::rewrite(AND(reason, explain(EQUAL(r1_rep, join_term[0])))); + } + sendInfer(fact, reasons, "join-split"); + + reasons = reason; + fact = MEMBER(t2, r2_rep); + + if(r2_rep != join_term[1]) { + reasons = Rewriter::rewrite(AND(reason, explain(EQUAL(r2_rep, join_term[1])))); + } + sendInfer(fact, reasons, "join-split"); + + // Need to make the skolem "shared_x" as shared term + makeSharedTerm(shared_x); + } else { + // ONLY need to explicitly compute joins if there are negative literals involving JOIN + Trace("rels-debug") << "\n[sets-rels] Apply JOIN-COMPOSE rule on term: " << join_term + << " with explanation: " << exp << std::endl; + } + } + + /* + * transpose-occur rule: [NOT] (a, b) IS_IN X (TRANSPOSE X) occurs + * ------------------------------------------------------- + * [NOT] (b, a) IS_IN (TRANSPOSE X) + * + * transpose-reverse rule: [NOT] (a, b) IS_IN (TRANSPOSE X) + * ------------------------------------------------ + * [NOT] (b, a) IS_IN X + * + * + * transpose-equal rule: [NOT] (TRANSPOSE X) = (TRANSPOSE Y) + * ----------------------------------------------- + * [NOT] (X = Y) + */ + void TheorySetsRels::applyTransposeRule(Node exp, Node tp_term, bool tp_occur) { + Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSPOSE rule " << std::endl; + bool polarity = exp.getKind() != kind::NOT; + Node atom = polarity ? exp : exp[0]; + Node reversedTuple = getRepresentative(RelsUtils::reverseTuple(atom[0])); + + if(tp_occur) { + Trace("rels-debug") << "\n[sets-rels] Apply TRANSPOSE-OCCUR rule on term: " << tp_term + << " with explanation: " << exp << std::endl; + Node fact = polarity ? MEMBER(reversedTuple, tp_term) : MEMBER(reversedTuple, tp_term).negate(); + sendInfer(fact, exp, "transpose-occur"); + return; + } + + Node tp_t0_rep = getRepresentative(tp_term[0]); + Node reason = atom[1] == tp_term ? exp : Rewriter::rewrite(AND(exp, EQUAL(atom[1], tp_term))); + Node fact = MEMBER(reversedTuple, tp_t0_rep); + + if(!polarity) { + // tp_term is a nested term and we eagerly compute its subterms' members + if(d_terms_cache[tp_t0_rep].find(kind::JOIN) + != d_terms_cache[tp_t0_rep].end()) { + std::vector<Node> join_terms = d_terms_cache[tp_t0_rep][kind::JOIN]; + for(unsigned int i = 0; i < join_terms.size(); i++) { + if(d_rel_nodes.find(join_terms[i]) == d_rel_nodes.end()) { + computeRels(join_terms[i]); + } + } + } + if(d_terms_cache[tp_t0_rep].find(kind::PRODUCT) + != d_terms_cache[tp_t0_rep].end()) { + std::vector<Node> product_terms = d_terms_cache[tp_t0_rep][kind::PRODUCT]; + for(unsigned int i = 0; i < product_terms.size(); i++) { + if(d_rel_nodes.find(product_terms[i]) == d_rel_nodes.end()) { + computeRels(product_terms[i]); + } + } + } + fact = fact.negate(); + } + sendInfer(fact, reason, "transpose-rule"); + } + + + void TheorySetsRels::inferTC( Node exp, Node tc_rep, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, + Node start_node, Node cur_node, std::hash_set< Node, NodeHashFunction >& traversed ) { + Node pair = constructPair(tc_rep, start_node, cur_node); + std::map<Node, std::vector<Node> >::iterator mem_it = d_membership_db.find(tc_rep); + + if(mem_it != d_membership_db.end()) { + if(std::find(mem_it->second.begin(), mem_it->second.end(), pair) == mem_it->second.end()) { + sendLemma( MEMBER(pair, tc_rep), Rewriter::rewrite(exp), "Transitivity" ); + } + } + // check if cur_node has been traversed or not + if(traversed.find(cur_node) != traversed.end()) { + return; + } + + traversed.insert(cur_node); + Node reason = exp; + std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator cur_set = tc_graph.find(cur_node); + + if(cur_set != tc_graph.end()) { + for(std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); + set_it != cur_set->second.end(); set_it++) { + Node new_pair = constructPair( tc_rep, cur_node, *set_it ); + Assert(!reason.isNull()); + inferTC( AND( findMemExp(tc_rep, new_pair), reason ), tc_rep, tc_graph, start_node, *set_it, traversed ); + } + } + } + + void TheorySetsRels::finalizeTCInfer() { + Trace("rels-debug") << "[sets-rels] Finalizing transitive closure inferences!" << std::endl; + for(TC_IT tc_it = d_membership_tc_cache.begin(); tc_it != d_membership_tc_cache.end(); tc_it++) { + inferTC(tc_it->first, tc_it->second); + } + } + + void TheorySetsRels::inferTC(Node tc_rep, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph) { + Trace("rels-debug") << "[sets-rels] Build TC graph for tc_rep = " << tc_rep << std::endl; + for(std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator pair_set_it = tc_graph.begin(); + pair_set_it != tc_graph.end(); pair_set_it++) { + for(std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); + set_it != pair_set_it->second.end(); set_it++) { + std::hash_set<Node, NodeHashFunction> elements; + Node pair = constructPair(tc_rep, pair_set_it->first, *set_it); + Node exp = findMemExp(tc_rep, pair); + + if(d_membership_tc_exp_cache.find(tc_rep) != d_membership_tc_exp_cache.end()) { + exp = AND(d_membership_tc_exp_cache[tc_rep], exp); + } + Assert(!exp.isNull()); + elements.insert(pair_set_it->first); + inferTC( exp, tc_rep, tc_graph, pair_set_it->first, *set_it, elements ); + } + } + } + + // Bottom-up fashion to compute relations + void TheorySetsRels::computeRels(Node n) { + Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation " << n << std::endl; + switch(n[0].getKind()) { + case kind::TRANSPOSE: + computeTransposeRelations(n[0]); + break; + case kind::JOIN: + case kind::PRODUCT: + computeRels(n[0]); + break; + default: + break; + } + + switch(n[1].getKind()) { + case kind::TRANSPOSE: + computeTransposeRelations(n[1]); + break; + case kind::JOIN: + case kind::PRODUCT: + computeRels(n[1]); + break; + default: + break; + } + + if(d_membership_db.find(getRepresentative(n[0])) == d_membership_db.end() || + d_membership_db.find(getRepresentative(n[1])) == d_membership_db.end()) + return; + composeTupleMemForRels(n); + } + + void TheorySetsRels::computeTransposeRelations(Node n) { + switch(n[0].getKind()) { + case kind::TRANSPOSE: + computeTransposeRelations(n[0]); + break; + case kind::JOIN: + case kind::PRODUCT: + computeRels(n[0]); + break; + default: + break; + } + + if(d_membership_db.find(getRepresentative(n[0])) == d_membership_db.end()) + return; + + Node n_rep = getRepresentative(n); + Node n0_rep = getRepresentative(n[0]); + std::vector<Node> tuples = d_membership_db[n0_rep]; + std::vector<Node> exps = d_membership_exp_db[n0_rep]; + Assert(tuples.size() == exps.size()); + for(unsigned int i = 0; i < tuples.size(); i++) { + Node reason = exps[i][1] == n0_rep ? exps[i] : AND(exps[i], EQUAL(exps[i][1], n0_rep)); + Node rev_tup = getRepresentative(RelsUtils::reverseTuple(tuples[i])); + Node fact = MEMBER(rev_tup, n_rep); + + if(holds(fact)) { + Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl; + } else { + sendInfer(fact, Rewriter::rewrite(reason), "transpose-rule"); + } + } + } + + /* + * Explicitly compose the join or product relations of r1 and r2 + * e.g. If (a, b) in X and (b, c) in Y, (a, c) in (X JOIN Y) + * + */ + void TheorySetsRels::composeTupleMemForRels( Node n ) { + Node r1 = n[0]; + Node r2 = n[1]; + Node r1_rep = getRepresentative(r1); + Node r2_rep = getRepresentative(r2); + NodeManager* nm = NodeManager::currentNM(); + + Trace("rels-debug") << "[sets-rels] start composing tuples in relations " + << r1 << " and " << r2 << std::endl; + + if(d_membership_db.find(r1_rep) == d_membership_db.end() || + d_membership_db.find(r2_rep) == d_membership_db.end()) + return; + + std::vector<Node> new_tups; + std::vector<Node> new_exps; + std::vector<Node> r1_elements = d_membership_db[r1_rep]; + std::vector<Node> r2_elements = d_membership_db[r2_rep]; + std::vector<Node> r1_exps = d_membership_exp_db[r1_rep]; + std::vector<Node> r2_exps = d_membership_exp_db[r2_rep]; + + Node new_rel = n.getKind() == kind::JOIN ? nm->mkNode(kind::JOIN, r1_rep, r2_rep) + : nm->mkNode(kind::PRODUCT, r1_rep, r2_rep); + + Node new_rel_rep = getRepresentative(new_rel); + unsigned int t1_len = r1_elements.front().getType().getTupleLength(); + unsigned int t2_len = r2_elements.front().getType().getTupleLength(); + + for(unsigned int i = 0; i < r1_elements.size(); i++) { + for(unsigned int j = 0; j < r2_elements.size(); j++) { + std::vector<Node> composed_tuple; + TypeNode tn = n.getType().getSetElementType(); + Node r1_rmost = RelsUtils::nthElementOfTuple(r1_elements[i], t1_len-1); + Node r2_lmost = RelsUtils::nthElementOfTuple(r2_elements[j], 0); + composed_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + + if((areEqual(r1_rmost, r2_lmost) && n.getKind() == kind::JOIN) || + n.getKind() == kind::PRODUCT) { + bool isProduct = n.getKind() == kind::PRODUCT; + unsigned int k = 0; + unsigned int l = 1; + + for(; k < t1_len - 1; ++k) { + composed_tuple.push_back(RelsUtils::nthElementOfTuple(r1_elements[i], k)); + } + if(isProduct) { + composed_tuple.push_back(RelsUtils::nthElementOfTuple(r1_elements[i], k)); + composed_tuple.push_back(RelsUtils::nthElementOfTuple(r2_elements[j], 0)); + } + for(; l < t2_len; ++l) { + composed_tuple.push_back(RelsUtils::nthElementOfTuple(r2_elements[j], l)); + } + Node composed_tuple_rep = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, composed_tuple)); + Node fact = MEMBER(composed_tuple_rep, new_rel_rep); + + if(holds(fact)) { + Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl; + } else { + std::vector<Node> reasons; + //Todo: need more explanation + reasons.push_back(explain(r1_exps[i])); + reasons.push_back(explain(r2_exps[j])); + if(r1_exps[i].getKind() == kind::MEMBER && r1_exps[i][0] != r1_elements[i]) { + reasons.push_back(explain(EQUAL(r1_elements[i], r1_exps[i][0]))); + } + if(r2_exps[j].getKind() == kind::MEMBER && r2_exps[j][0] != r2_elements[j]) { + reasons.push_back(explain(EQUAL(r2_elements[j], r2_exps[j][0]))); + } + if(!isProduct) { + if(r1_rmost != r2_lmost) { + reasons.push_back(explain(EQUAL(r1_rmost, r2_lmost))); + } + } + if(r1 != r1_rep) { + reasons.push_back(explain(EQUAL(r1, r1_rep))); + } + if(r2 != r2_rep) { + reasons.push_back(explain(EQUAL(r2, r2_rep))); + } + + Node reason = Rewriter::rewrite(nm->mkNode(kind::AND, reasons)); + if(isProduct) { + sendInfer( fact, reason, "product-compose" ); + } else { + sendInfer( fact, reason, "join-compose" ); + } + + Trace("rels-debug") << "[sets-rels] Compose tuples: " << r1_elements[i] + << " and " << r2_elements[j] + << "\n Produce a new fact: " << fact + << "\n Reason: " << reason<< std::endl; + } + } + } + } + Trace("rels-debug") << "[sets-rels] Done with composing tuples !" << std::endl; + } + + void TheorySetsRels::doPendingLemmas() { + if( !(*d_conflict) && (!d_lemma_cache.empty() || !d_pending_facts.empty())){ + for( unsigned i=0; i < d_lemma_cache.size(); i++ ){ + Assert(d_lemma_cache[i].getKind() == kind::IMPLIES); + if(holds( d_lemma_cache[i][1] )) { + Trace("rels-lemma") << "[sets-rels-lemma-skip] Skip the already held lemma: " + << d_lemma_cache[i]<< std::endl; + continue; + } + Trace("rels-lemma") << "[sets-rels-lemma] Process pending lemma : " + << d_lemma_cache[i] << std::endl; + d_sets_theory.d_out->lemma( d_lemma_cache[i] ); +// d_sets_theory.d_out->conflict() + } + for( std::map<Node, Node>::iterator child_it = d_pending_facts.begin(); + child_it != d_pending_facts.end(); child_it++ ) { + if(holds(child_it->first)) { + Trace("rels-lemma") << "[sets-rels-fact-lemma-skip] Skip the already held fact,: " + << child_it->first << std::endl; + continue; + } + Trace("rels-lemma") << "[sets-rels-fact-lemma] Process pending fact as lemma : " + << child_it->first << " with reason " << child_it->second << std::endl; + d_sets_theory.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, child_it->second, child_it->first)); + } + } + d_rel_nodes.clear(); + d_pending_facts.clear(); + d_membership_constraints_cache.clear(); + d_membership_tc_cache.clear(); + d_membership_tc_exp_cache.clear(); + d_membership_exp_cache.clear(); + d_membership_db.clear(); + d_membership_exp_db.clear(); + d_terms_cache.clear(); + d_lemma_cache.clear(); + d_membership_trie.clear(); + d_tuple_reps.clear(); + d_id_node.clear(); + d_node_id.clear(); + } + + void TheorySetsRels::sendSplit(Node a, Node b, const char * c) { + Node eq = a.eqNode( b ); + Node neq = NOT( eq ); + Node lemma_or = OR( eq, neq ); + + Trace("rels-lemma") << "[sets-lemma] Lemma " << c << " SPLIT : " << lemma_or << std::endl; + d_lemma_cache.push_back( lemma_or ); + } + + void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { + Trace("rels-lemma") << "[sets-lemma] Infer " << conc << " from " << ant << " by " << c << std::endl; + Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); + d_lemma_cache.push_back(lemma); + d_lemma.insert(lemma); + } + + void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) { + Trace("rels-lemma") << "[sets-fact] Infer " << fact << " from " << exp << " by " << c << std::endl; + d_pending_facts[fact] = exp; + d_infer.push_back( fact ); + d_infer_exp.push_back( exp ); + } + + void TheorySetsRels::doPendingFacts() { + std::map<Node, Node>::iterator map_it = d_pending_facts.begin(); + while( !(*d_conflict) && map_it != d_pending_facts.end()) { + Node fact = map_it->first; + Node exp = d_pending_facts[ fact ]; + + if(fact.getKind() == kind::AND) { + for(size_t j=0; j<fact.getNumChildren(); j++) { + bool polarity = fact[j].getKind() != kind::NOT; + Node atom = polarity ? fact[j] : fact[j][0]; + assertMembership(atom, exp, polarity); + } + } else { + bool polarity = fact.getKind() != kind::NOT; + Node atom = polarity ? fact : fact[0]; + assertMembership(atom, exp, polarity); + } + map_it++; + } + d_pending_facts.clear(); + d_membership_constraints_cache.clear(); + d_membership_db.clear(); + d_membership_exp_cache.clear(); + d_terms_cache.clear(); + } + + void TheorySetsRels::doPendingSplitFacts() { + std::map<Node, Node>::iterator map_it = d_pending_split_facts.begin(); + while( !(*d_conflict) && map_it != d_pending_split_facts.end()) { + Node fact = map_it->first; + Node exp = d_pending_split_facts[ fact ]; + + if(fact.getKind() == kind::AND) { + for(size_t j=0; j<fact.getNumChildren(); j++) { + bool polarity = fact[j].getKind() != kind::NOT; + Node atom = polarity ? fact[j] : fact[j][0]; + assertMembership(atom, exp, polarity); + } + } else { + Trace("rels-lemma") << "[sets-split-fact] Send " << fact << " from " << exp << std::endl; + bool polarity = fact.getKind() != kind::NOT; + Node atom = polarity ? fact : fact[0]; + assertMembership(atom, exp, polarity); + } + map_it++; + } + d_pending_split_facts.clear(); + } + + void TheorySetsRels::assertMembership( Node fact, Node reason, bool polarity ) { + d_eqEngine->assertPredicate( fact, polarity, reason ); + } + + Node TheorySetsRels::getRepresentative( Node t ) { + if( d_eqEngine->hasTerm( t ) ){ + return d_eqEngine->getRepresentative( t ); + }else{ + return t; + } + } + + bool TheorySetsRels::hasTerm( Node a ){ + return d_eqEngine->hasTerm( a ); + } + + bool TheorySetsRels::areEqual( Node a, Node b ){ + Assert(a.getType() == b.getType()); + Trace("rels-eq") << "[sets-rels]**** checking equality between " << a << " and " << b << std::endl; + if(a == b) { + return true; + } else if( hasTerm( a ) && hasTerm( b ) ){ + return d_eqEngine->areEqual( a, b ); + } else if(a.getType().isTuple()) { + bool equal = true; + for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) { + equal = equal && areEqual(RelsUtils::nthElementOfTuple(a, i), RelsUtils::nthElementOfTuple(b, i)); + } + return equal; + } else if(!a.getType().isBoolean()){ + makeSharedTerm(a); + makeSharedTerm(b); + } + return false; + } + + bool TheorySetsRels::checkCycles(Node join_term) { + return false; + } + + bool TheorySetsRels::safeAddToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) { + std::map< Node, std::vector< Node > >::iterator mem_it = map.find(rel_rep); + if(mem_it == map.end()) { + std::vector<Node> members; + members.push_back(member); + map[rel_rep] = members; + return true; + } else { + std::vector<Node>::iterator mems = mem_it->second.begin(); + while(mems != mem_it->second.end()) { + if(areEqual(*mems, member)) { + return false; + } + mems++; + } + map[rel_rep].push_back(member); + return true; + } + return false; + } + + void TheorySetsRels::addToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) { + if(map.find(rel_rep) == map.end()) { + std::vector<Node> members; + members.push_back(member); + map[rel_rep] = members; + } else { + map[rel_rep].push_back(member); + } + } + + inline Node TheorySetsRels::getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r) { + Trace("rels-reason") << "[sets-rels] getReason(" << tc_rep << ", " << tc_term << ", " << tc_r_rep << ", " << tc_r << std::endl; + if(tc_term != tc_rep) { + Node reason = explain(EQUAL(tc_term, tc_rep)); + + if(tc_term[0] != tc_r_rep) { + return AND(reason, explain(EQUAL(tc_term[0], tc_r_rep))); + } + } + Trace("rels-reason") << "[sets-rels] done getReason(" << tc_rep << ", " << tc_term << ", " << tc_r_rep << ", " << tc_r << std::endl; + return Node::null(); + } + + // tuple might be a member of tc_rep; or it might be a member of rels or tc_terms such that + // tc_terms are transitive closure of rels and are modulo equal to tc_rep + Node TheorySetsRels::findMemExp(Node tc_rep, Node pair) { + Trace("rels-exp") << "TheorySetsRels::findMemExp ( tc_rep = " << tc_rep << ", pair = " << pair << ")" << std::endl; + Node fst = RelsUtils::nthElementOfTuple(pair, 0); + Node snd = RelsUtils::nthElementOfTuple(pair, 1); + std::vector<Node> tc_terms = d_terms_cache.find(tc_rep)->second[kind::TCLOSURE]; + + Assert(tc_terms.size() > 0); + for(unsigned int i = 0; i < tc_terms.size(); i++) { + Node tc_term = tc_terms[i]; + Node tc_r_rep = getRepresentative(tc_term[0]); + + Trace("rels-exp") << "TheorySetsRels::findMemExp ( r_rep = " << tc_r_rep << ", pair = " << pair << ")" << std::endl; + std::map< Node, std::vector< Node > >::iterator tc_r_mems = d_membership_db.find(tc_r_rep); + if(tc_r_mems != d_membership_db.end()) { + for(unsigned int i = 0; i < tc_r_mems->second.size(); i++) { + Node fst_mem = RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 0); + Node snd_mem = RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 1); + + if(areEqual(fst_mem, fst) && areEqual(snd_mem, snd)) { + Node exp = MEMBER(tc_r_mems->second[i], tc_r_mems->first); + + if(tc_r_rep != tc_term[0]) { + exp = explain(EQUAL(tc_r_rep, tc_term[0])); + } + if(tc_rep != tc_term) { + exp = AND(exp, explain(EQUAL(tc_rep, tc_term))); + } + if(tc_r_mems->second[i] != pair) { + if(fst_mem != fst) { + exp = AND(exp, explain(EQUAL(fst_mem, fst))); + } + if(snd_mem != snd) { + exp = AND(exp, explain(EQUAL(snd_mem, snd))); + } + exp = AND(exp, EQUAL(tc_r_mems->second[i], pair)); + } + return Rewriter::rewrite(AND(exp, explain(d_membership_exp_db[tc_r_rep][i]))); + } + } + } + + Node tc_term_rep = getRepresentative(tc_terms[i]); + std::map< Node, std::vector< Node > >::iterator tc_t_mems = d_membership_db.find(tc_term_rep); + + if(tc_t_mems != d_membership_db.end()) { + for(unsigned int j = 0; j < tc_t_mems->second.size(); j++) { + Node fst_mem = RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 0); + Node snd_mem = RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 1); + + if(areEqual(fst_mem, fst) && areEqual(snd_mem, snd)) { + Node exp = MEMBER(tc_t_mems->second[j], tc_t_mems->first); + if(tc_rep != tc_terms[i]) { + exp = AND(exp, explain(EQUAL(tc_rep, tc_terms[i]))); + } + if(tc_term_rep != tc_terms[i]) { + exp = AND(exp, explain(EQUAL(tc_term_rep, tc_terms[i]))); + } + if(tc_t_mems->second[j] != pair) { + if(fst_mem != fst) { + exp = AND(exp, explain(EQUAL(fst_mem, fst))); + } + if(snd_mem != snd) { + exp = AND(exp, explain(EQUAL(snd_mem, snd))); + } + exp = AND(exp, EQUAL(tc_t_mems->second[j], pair)); + } + return Rewriter::rewrite(AND(exp, explain(d_membership_exp_db[tc_term_rep][j]))); + } + } + } + } + return Node::null(); + } + + void TheorySetsRels::addSharedTerm( TNode n ) { + Trace("rels-debug") << "[sets-rels] Add a shared term: " << n << std::endl; + d_sets_theory.addSharedTerm(n); + d_eqEngine->addTriggerTerm(n, THEORY_SETS); + } + + bool TheorySetsRels::hasMember( Node rel_rep, Node tuple ){ + if(d_membership_db.find(rel_rep) == d_membership_db.end()) + return false; + return std::find(d_membership_db[rel_rep].begin(), + d_membership_db[rel_rep].end(), tuple) != d_membership_db[rel_rep].end(); + } + + void TheorySetsRels::makeSharedTerm( Node n ) { + Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl; + if(d_shared_terms.find(n) == d_shared_terms.end()) { + Node skolem = NodeManager::currentNM()->mkSkolem( "sde", n.getType() ); + sendLemma(MEMBER(skolem, SINGLETON(n)), d_trueNode, "share-term"); + d_shared_terms.insert(n); + } + } + + bool TheorySetsRels::holds(Node node) { + Trace("rels-check") << " [sets-rels] Check if node = " << node << " already holds " << std::endl; + bool polarity = node.getKind() != kind::NOT; + Node atom = polarity ? node : node[0]; + Node polarity_atom = polarity ? d_trueNode : d_falseNode; + + if(d_eqEngine->hasTerm(atom)) { + Trace("rels-check") << " [sets-rels] node = " << node << " is in the EE " << std::endl; + return areEqual(atom, polarity_atom); + } else { + Node atom_mod = NodeManager::currentNM()->mkNode(atom.getKind(), + getRepresentative(atom[0]), + getRepresentative(atom[1])); + if(d_eqEngine->hasTerm(atom_mod)) { + return areEqual(atom_mod, polarity_atom); + } + } + return false; + } + + void TheorySetsRels::computeTupleReps( Node n ) { + if( d_tuple_reps.find( n ) == d_tuple_reps.end() ){ + for( unsigned i = 0; i < n.getType().getTupleLength(); i++ ){ + d_tuple_reps[n].push_back( getRepresentative( RelsUtils::nthElementOfTuple(n, i) ) ); + } + } + } + + inline void TheorySetsRels::addToMembershipDB(Node rel, Node member, Node reasons) { + addToMap(d_membership_db, rel, member); + addToMap(d_membership_exp_db, rel, reasons); + computeTupleReps(member); + d_membership_trie[rel].addTerm(member, d_tuple_reps[member]); + } + + inline Node TheorySetsRels::constructPair(Node tc_rep, Node a, Node b) { + Datatype dt = tc_rep.getType().getSetElementType().getDatatype(); + return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b); + } + + void TheorySetsRels::reduceTupleVar(Node n) { + if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) { + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one " << std::endl; + std::vector<Node> tuple_elements; + tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); + + for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { + Node element = RelsUtils::nthElementOfTuple(n[0], i); + makeSharedTerm(element); + tuple_elements.push_back(element); + } + Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); + tuple_reduct = MEMBER(tuple_reduct, n[1]); + Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct); + sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); + d_symbolic_tuples.insert(n); + } + } + + TheorySetsRels::TheorySetsRels(context::Context* c, + context::UserContext* u, + eq::EqualityEngine* eq, + context::CDO<bool>* conflict, + TheorySets& d_set): + d_eqEngine(eq), + d_sets_theory(d_set), + d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)), + d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)), + d_pending_merge(c), + d_infer(c), + d_infer_exp(c), + d_lemma(u), + d_shared_terms(u), + d_tc_saver(u), + d_conflict(conflict) + { + d_eqEngine->addFunctionKind(kind::PRODUCT); + d_eqEngine->addFunctionKind(kind::JOIN); + d_eqEngine->addFunctionKind(kind::TRANSPOSE); + d_eqEngine->addFunctionKind(kind::TCLOSURE); + } + + TheorySetsRels::~TheorySetsRels() {} + + std::vector<Node> TupleTrie::findTerms( std::vector< Node >& reps, int argIndex ) { + std::vector<Node> nodes; + std::map< Node, TupleTrie >::iterator it; + + if( argIndex==(int)reps.size()-1 ){ + if(reps[argIndex].getKind() == kind::SKOLEM) { + it = d_data.begin(); + while(it != d_data.end()) { + nodes.push_back(it->first); + it++; + } + } + return nodes; + }else{ + it = d_data.find( reps[argIndex] ); + if( it==d_data.end() ){ + return nodes; + }else{ + return it->second.findTerms( reps, argIndex+1 ); + } + } + } + + Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) { + if( argIndex==(int)reps.size() ){ + if( d_data.empty() ){ + return Node::null(); + }else{ + return d_data.begin()->first; + } + }else{ + std::map< Node, TupleTrie >::iterator it = d_data.find( reps[argIndex] ); + if( it==d_data.end() ){ + return Node::null(); + }else{ + return it->second.existsTerm( reps, argIndex+1 ); + } + } + } + + bool TupleTrie::addTerm( Node n, std::vector< Node >& reps, int argIndex ){ + if( argIndex==(int)reps.size() ){ + if( d_data.empty() ){ + //store n in d_data (this should be interpretted as the "data" and not as a reference to a child) + d_data[n].clear(); + return true; + }else{ + return false; + } + }else{ + return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 ); + } + } + + void TupleTrie::debugPrint( const char * c, Node n, unsigned depth ) { + for( std::map< Node, TupleTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ + for( unsigned i=0; i<depth; i++ ){ Debug(c) << " "; } + Debug(c) << it->first << std::endl; + it->second.debugPrint( c, n, depth+1 ); + } + } + + Node TheorySetsRels::explain(Node literal) + { + Trace("rels-exp") << "[sets-rels] TheorySetsRels::explain(" << literal << ")"<< std::endl; + std::vector<TNode> assumptions; + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + + if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + d_eqEngine->explainEquality(atom[0], atom[1], polarity, assumptions); + } else if(atom.getKind() == kind::MEMBER) { + if( !d_eqEngine->hasTerm(atom)) { + d_eqEngine->addTerm(atom); + } + d_eqEngine->explainPredicate(atom, polarity, assumptions); + } else { + Trace("rels-exp") << "unhandled: " << literal << "; (" << atom << ", " + << polarity << "); kind" << atom.getKind() << std::endl; + Unhandled(); + } + Trace("rels-exp") << "[sets-rels] ****** done with TheorySetsRels::explain(" << literal << ")"<< std::endl; + return mkAnd(assumptions); + } + + TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) : + d_mem(c), d_not_mem(c), d_in(c), d_out(c), d_mem_exp(c), + d_tp(c), d_pt(c), d_join(c), d_tc(c), d_id_in(c), d_id_out(c) {} + + void TheorySetsRels::eqNotifyNewClass( Node n ) { + Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl; + if(isRel(n) && (n.getKind() == kind::TRANSPOSE || + n.getKind() == kind::PRODUCT || + n.getKind() == kind::JOIN || + n.getKind() == kind::TCLOSURE)) { + getOrMakeEqcInfo( n, true ); + } + } + + // Create a integer id for tuple element + int TheorySetsRels::getOrMakeElementRepId(EqcInfo* ei, Node e_rep) { + Trace("rels-std") << "[sets-rels] getOrMakeElementRepId:" << " e_rep = " << e_rep << std::endl; + std::map<Node, int>::iterator nid_it = d_node_id.find(e_rep); + + if( nid_it == d_node_id.end() ) { + Trace("rels-std") << "[sets-rels] getOrMakeElementRepId:" << " *** 0"<< std::endl; + if(d_eqEngine->hasTerm(e_rep)) { + // it is possible that e's rep changes at this moment, thus we need to know the eqc of e's previous rep + eq::EqClassIterator rep_eqc_i = eq::EqClassIterator( e_rep, d_eqEngine ); + Trace("rels-std") << "[sets-rels] getOrMakeElementRepId:" << " *** 1"<< std::endl; + while(!rep_eqc_i.isFinished()) { + std::map<Node, int>::iterator id_it = d_node_id.find(*rep_eqc_i); + + if( id_it != d_node_id.end() ) { + d_id_node[id_it->second] = e_rep; + d_node_id[e_rep] = id_it->second; + return id_it->second; + } + rep_eqc_i++; + } + } + d_id_node[ei->counter] = e_rep; + d_node_id[e_rep] = ei->counter; + ei->counter++; + return ei->counter-1; + } + Trace("rels-std") << "[sets-rels] finish getOrMakeElementRepId:" << " e_rep = " << e_rep << std::endl; + return nid_it->second; + } + + bool TheorySetsRels::insertIntoIdList(IdList& idList, int mem) { + IdList::const_iterator idListIt = idList.begin(); + while(idListIt != idList.end()) { + if(*idListIt == mem) { + return false; + } + idListIt++; + } + idList.push_back(mem); + return true; + } + + void TheorySetsRels::addTCMemAndSendInfer(EqcInfo* tc_ei, Node membership, Node exp, bool fromRel) { + Trace("rels-std") << "[sets-rels] addTCMemAndSendInfer:" << " membership = " << membership << " from a relation? " << fromRel<< std::endl; + IdList* in_lst; + IdList* out_lst; + Node fst = RelsUtils::nthElementOfTuple(membership[0], 0); + Node snd = RelsUtils::nthElementOfTuple(membership[0], 1); + Node fst_rep = getRepresentative(fst); + Node snd_rep = getRepresentative(snd); + Node mem_rep = RelsUtils::constructPair(tc_ei->d_tc, fst_rep, snd_rep); + + if(tc_ei->d_mem.find(mem_rep) != tc_ei->d_mem.end()) { + return; + } + + int fst_rep_id = getOrMakeElementRepId(tc_ei, fst_rep); + int snd_rep_id = getOrMakeElementRepId(tc_ei, snd_rep); + + IdListMap::iterator tc_in_mem_it = tc_ei->d_id_in.find(snd_rep_id); + + if(tc_in_mem_it == tc_ei->d_id_in.end()) { + in_lst = new(d_sets_theory.getSatContext()->getCMM()) IdList( true, d_sets_theory.getSatContext(), false, + context::ContextMemoryAllocator<TNode>(d_sets_theory.getSatContext()->getCMM()) ); + tc_ei->d_id_in.insertDataFromContextMemory(snd_rep_id, in_lst); + Trace("rels-std") << "Create in cache for " << snd_rep << std::endl; + } else { + in_lst = (*tc_in_mem_it).second; + } + + std::hash_set<int> in_reachable; + std::hash_set<int> out_reachable; + collectInReachableNodes(tc_ei, fst_rep_id, in_reachable); + collectOutReachableNodes(tc_ei, snd_rep_id, out_reachable); + + // If fst_rep is inserted into in_lst successfully, + // save rep pair's exp and send out TC inference lemmas. + // Otherwise, mem's rep is already in the TC and return. + if(insertIntoIdList(*in_lst, fst_rep_id)) { + Node reason = exp == Node::null() ? explain(membership) : exp; + if(!fromRel && tc_ei->d_tc.get() != membership[1]) { + reason = AND(reason, explain(EQUAL(tc_ei->d_tc.get(), membership[1]))); + } + if(fst != fst_rep) { + reason = AND(reason, explain(EQUAL(fst, fst_rep))); + } + if(snd != snd_rep) { + reason = AND(reason, explain(EQUAL(snd, snd_rep))); + } + tc_ei->d_mem_exp[mem_rep] = reason; + Trace("rels-std") << "Added member " << mem_rep << " for " << tc_ei->d_tc.get()<< " with reason = " << reason << std::endl; + tc_ei->d_mem.insert(mem_rep); + Trace("rels-std") << "Added in membership arrow for " << snd_rep << " from: " << fst_rep << std::endl; + } else { + // Nothing inserted into the eqc + return; + } + + IdListMap::iterator tc_out_mem_it = tc_ei->d_id_out.find(fst_rep_id); + if(tc_out_mem_it == tc_ei->d_id_out.end()) { + out_lst = new(d_sets_theory.getSatContext()->getCMM()) IdList( true, d_sets_theory.getSatContext(), false, + context::ContextMemoryAllocator<TNode>(d_sets_theory.getSatContext()->getCMM()) ); + tc_ei->d_id_out.insertDataFromContextMemory(fst_rep_id, out_lst); + Trace("rels-std") << "Create out arrow cache for " << snd_rep << std::endl; + } else { + out_lst = (*tc_out_mem_it).second; + } + insertIntoIdList(*out_lst, snd_rep_id); + Trace("rels-std") << "Add out membership arrow for " << fst_rep << " to : " << snd_rep << std::endl; + sendTCInference(tc_ei, in_reachable, out_reachable, mem_rep, fst_rep, snd_rep, fst_rep_id, snd_rep_id); + } + + Node TheorySetsRels::explainTCMem(EqcInfo* ei, Node pair, Node fst, Node snd) { + if(ei->d_mem_exp.find(pair) != ei->d_mem_exp.end()) { + return (*ei->d_mem_exp.find(pair)).second; + } + NodeMap::iterator mem_exp_it = ei->d_mem_exp.begin(); + while(mem_exp_it != ei->d_mem_exp.end()) { + Node tuple = (*mem_exp_it).first; + Node fst_e = RelsUtils::nthElementOfTuple(tuple, 0); + Node snd_e = RelsUtils::nthElementOfTuple(tuple, 1); + if(areEqual(fst, fst_e) && areEqual(snd, snd_e)) { + return AND(explain(EQUAL(snd, snd_e)), AND(explain(EQUAL(fst, fst_e)), (*mem_exp_it).second)); + } + ++mem_exp_it; + } + return Node::null(); + } + + void TheorySetsRels::sendTCInference(EqcInfo* tc_ei, std::hash_set<int> in_reachable, std::hash_set<int> out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2) { + Trace("rels-std") << "Start making TC inference after adding a member " << mem_rep << " to " << tc_ei->d_tc.get() << std::endl; + + NodeMap::iterator map_it = tc_ei->d_mem_exp.begin(); + while(map_it != tc_ei->d_mem_exp.end()) { + Trace("rels-debug") << " mem = "<< (*map_it).first << " exp = " << (*map_it).second<< std::endl; + map_it++; + } + Node exp = explainTCMem(tc_ei, mem_rep, fst_rep, snd_rep); + Assert(!exp.isNull()); + Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, MEMBER(mem_rep, tc_ei->d_tc.get())); + d_pending_merge.push_back(tc_lemma); + d_lemma.insert(tc_lemma); + + Trace("rels-std") << "Start making TC inference after adding a member " << mem_rep << " to " << tc_ei->d_tc.get() + << " in_reachable size = " << in_reachable.size() + << " out_reachable size = " << out_reachable.size() + << " ***** 2" << std::endl; + + std::hash_set<int>::iterator in_reachable_it = in_reachable.begin(); + while(in_reachable_it != in_reachable.end()) { + Node in_node = d_id_node[*in_reachable_it]; + Node in_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, fst_rep); + Node new_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, snd_rep); + + Trace("rels-std") << "Reason for " << in_pair << " " << explainTCMem(tc_ei, in_pair, in_node, fst_rep) << std::endl; + + Node reason = AND(explainTCMem(tc_ei, in_pair, in_node, fst_rep), exp); + tc_ei->d_mem_exp[new_pair] = reason; + tc_ei->d_mem.insert(new_pair); + Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, MEMBER(new_pair, tc_ei->d_tc.get())); + d_pending_merge.push_back(tc_lemma); + d_lemma.insert(tc_lemma); + in_reachable_it++; + } + Trace("rels-std") << "Start making TC inference after adding a member " << mem_rep << " to " << tc_ei->d_tc.get() << " ***** 3" << std::endl; + std::hash_set<int>::iterator out_reachable_it = out_reachable.begin(); + while(out_reachable_it != out_reachable.end()) { + Node out_node = d_id_node[*out_reachable_it]; + Node out_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), snd_rep, out_node); + Node reason = explainTCMem(tc_ei, out_pair, snd_rep, out_node); + Assert(reason != Node::null()); + + std::hash_set<int>::iterator in_reachable_it = in_reachable.begin(); + while(in_reachable_it != in_reachable.end()) { + Node in_node = d_id_node[*in_reachable_it]; + Node in_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, snd_rep); + Node new_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, out_node); + Node in_pair_exp = explainTCMem(tc_ei, in_pair, in_node, snd_rep); + + Assert(in_pair_exp != Node::null()); + reason = AND(reason, in_pair_exp); + + Trace("rels-std") << "Start making TC inference after adding a member " << mem_rep << " to " << tc_ei->d_tc.get() << " ***** 3 9" << std::endl; + tc_ei->d_mem_exp[new_pair] = reason; + tc_ei->d_mem.insert(new_pair); + Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, MEMBER(new_pair, tc_ei->d_tc.get())); + d_pending_merge.push_back(tc_lemma); + d_lemma.insert(tc_lemma); + in_reachable_it++; + } + out_reachable_it++; + } + Trace("rels-std") << "Start making TC inference after adding a member " << mem_rep << " to " << tc_ei->d_tc.get() << " ***** 4" << std::endl; + } + + void TheorySetsRels::collectInReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& in_reachable, bool firstRound) { + Trace("rels-std") << "**** Start collecting in-reachable nodes for node with id " << start_id << std::endl; + if(in_reachable.find(start_id) != in_reachable.end()) { + return; + } + if(!firstRound) { + in_reachable.insert(start_id); + } + IdListMap::const_iterator id_list_map_it = tc_ei->d_id_in.find(start_id); + + if(id_list_map_it != tc_ei->d_id_in.end()) { + IdList::const_iterator id_list_it = (*id_list_map_it).second->begin(); + while(id_list_it != (*id_list_map_it).second->end()) { + collectInReachableNodes(tc_ei, *id_list_it, in_reachable, false); + id_list_it++; + } + } + } + + void TheorySetsRels::collectOutReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& out_reachable, bool firstRound) { + Trace("rels-std") << "**** Start collecting out-reachable nodes for node with id " << start_id << std::endl; + if(out_reachable.find(start_id) != out_reachable.end()) { + return; + } + if(!firstRound) { + out_reachable.insert(start_id); + } + IdListMap::const_iterator id_list_map_it = tc_ei->d_id_out.find(start_id); + + if(id_list_map_it != tc_ei->d_id_out.end()) { + IdList::const_iterator id_list_it = (*id_list_map_it).second->begin(); + while(id_list_it != (*id_list_map_it).second->end()) { + collectOutReachableNodes(tc_ei, *id_list_it, out_reachable, false); + id_list_it++; + } + } + } + + // Merge t2 into t1, t1 will be the rep of the new eqc + void TheorySetsRels::eqNotifyPostMerge( Node t1, Node t2 ) { + Trace("rels-std") << "[sets-rels] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; + + // Merge membership constraint with "true" or "false" eqc + // Todo: t1 might not be "true" or "false" rep + if((t1 == d_trueNode || t1 == d_falseNode) && + t2.getKind() == kind::MEMBER && + t2[0].getType().isTuple()) { + + Assert(t1 == d_trueNode || t1 == d_falseNode); + bool polarity = t1 == d_trueNode; + Node t2_1rep = getRepresentative(t2[1]); + EqcInfo* ei = getOrMakeEqcInfo( t2_1rep ); + + if(ei == NULL) { + ei = getOrMakeEqcInfo( t2_1rep, true ); + } + if(polarity) { + ei->d_mem.insert(t2[0]); + ei->d_mem_exp[t2[0]] = explain(t2); + } else { + ei->d_not_mem.insert(t2[0]); + } + // Process a membership constraint that a tuple is a member of transpose of rel + if(!ei->d_tp.get().isNull()) { + Node exp = polarity ? explain(t2) : explain(t2.negate()); + if(ei->d_tp.get() != t2[1]) { + exp = AND( explain(EQUAL( ei->d_tp.get(), t2[1]) ), exp ); + } + sendInferTranspose( polarity, t2[0], ei->d_tp.get(), exp, true ); + } + // Process a membership constraint that a tuple is a member of product of rel + if(!ei->d_pt.get().isNull()) { + Node exp = polarity ? explain(t2) : explain(t2.negate()); + if(ei->d_pt.get() != t2[1]) { + exp = AND( explain(EQUAL( ei->d_pt.get(), t2[1]) ), exp ); + } + sendInferProduct(polarity, t2[0], ei->d_pt.get(), exp); + } + // Process a membership constraint that a tuple is a member of transitive closure of rel + if(polarity) { + if(!ei->d_tc.get().isNull()) { + addTCMemAndSendInfer(ei, t2, Node::null()); + // when we see (a, b) in R and TC(R) has not been seen, we create a EQC for TC(R) to save (a, b) + } else { + std::vector<TypeNode> tup_types = t2[1].getType().getSetElementType().getTupleTypes(); + + if( tup_types.size() == 2 && tup_types[0] == tup_types[1] ) { + Node tc_n = NodeManager::currentNM()->mkNode(kind::TCLOSURE, t2[1]); + EqcInfo* tc_ei = getOrMakeEqcInfo( tc_n ); + if( tc_ei != NULL ) { + addTCMemAndSendInfer(tc_ei, t2, Node::null(), true); + } + } + } + } + + // Merge two relation eqcs + } else if(t1.getType().isSet() && + t2.getType().isSet() && + t1.getType().getSetElementType().isTuple()) { + mergeTransposeEqcs(t1, t2); + mergeProductEqcs(t1, t2); + mergeTCEqcs(t1, t2); + } + + Trace("rels-std") << "[sets-rels] done with eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; + } + + void TheorySetsRels::mergeTCEqcs(Node t1, Node t2) { + Trace("rels-std") << "[sets-rels] Merge TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; + EqcInfo* t1_ei = getOrMakeEqcInfo(t1); + EqcInfo* t2_ei = getOrMakeEqcInfo(t2); + if(t1_ei != NULL && t2_ei != NULL) { + NodeSet::const_iterator non_mem_it = t2_ei->d_not_mem.begin(); + while(non_mem_it != t2_ei->d_not_mem.end()) { + t1_ei->d_not_mem.insert(*non_mem_it); + non_mem_it++; + } + if(!t1_ei->d_tc.get().isNull()) { + NodeSet::const_iterator mem_it = t2_ei->d_mem.begin(); + while(mem_it != t2_ei->d_mem.end()) { + addTCMemAndSendInfer(t1_ei, MEMBER(*mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*mem_it)).second); + mem_it++; + } + } else if(!t2_ei->d_tc.get().isNull()) { + t1_ei->d_tc.set(t2_ei->d_tc); + NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); + while(t1_mem_it != t1_ei->d_mem.end()) { + addTCMemAndSendInfer(t1_ei, MEMBER(*t1_mem_it, t1_ei->d_tc.get()), (*t1_ei->d_mem_exp.find(*t1_mem_it)).second); + t1_mem_it++; + } + NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin(); + while(t2_mem_it != t2_ei->d_mem.end()) { + addTCMemAndSendInfer(t1_ei, MEMBER(*t2_mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*t2_mem_it)).second); + t2_mem_it++; + } + } + } + Trace("rels-std") << "[sets-rels] Done with merging TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; + } + + + + + void TheorySetsRels::mergeProductEqcs(Node t1, Node t2) { + Trace("rels-std") << "[sets-rels] Merge PRODUCT eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; + EqcInfo* t1_ei = getOrMakeEqcInfo(t1); + EqcInfo* t2_ei = getOrMakeEqcInfo(t2); + if(t1_ei != NULL && t2_ei != NULL) { + // PT(t1) = PT(t2) -> t1 = t2; + if(!t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull()) { + sendInferProduct( true, t1_ei->d_pt.get(), t2_ei->d_pt.get(), explain(EQUAL(t1, t2)) ); + } + // Apply Product rule on (non)members of t2 and t1->pt + if(!t1_ei->d_pt.get().isNull()) { + for(NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++) { + if(!t1_ei->d_mem.contains(*itr)) { + sendInferProduct( true, *itr, t1_ei->d_pt.get(), AND(explain(EQUAL(t1_ei->d_pt.get(), t2)), explain(MEMBER(*itr, t2))) ); + } + } + for(NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++) { + if(!t1_ei->d_not_mem.contains(*itr)) { + sendInferProduct( false, *itr, t1_ei->d_pt.get(), AND(explain(EQUAL(t1_ei->d_pt.get(), t2)), explain(MEMBER(*itr, t2).negate())) ); + } + } + } else if(!t2_ei->d_pt.get().isNull()) { + t1_ei->d_pt.set(t2_ei->d_pt); + for(NodeSet::key_iterator itr = t1_ei->d_mem.key_begin(); itr != t1_ei->d_mem.key_end(); itr++) { + if(!t2_ei->d_mem.contains(*itr)) { + sendInferProduct( true, *itr, t2_ei->d_pt.get(), AND(explain(EQUAL(t1, t2_ei->d_pt.get())), explain(MEMBER(*itr, t1))) ); + } + } + for(NodeSet::key_iterator itr = t1_ei->d_not_mem.key_begin(); itr != t1_ei->d_not_mem.key_end(); itr++) { + if(!t2_ei->d_not_mem.contains(*itr)) { + sendInferProduct( false, *itr, t2_ei->d_pt.get(), AND(explain(EQUAL(t1, t2_ei->d_pt.get())), explain(MEMBER(*itr, t1).negate())) ); + } + } + } + // t1 was created already and t2 was not + } else if(t1_ei != NULL) { + if(t1_ei->d_pt.get().isNull() && t2.getKind() == kind::PRODUCT) { + t1_ei->d_pt.set( t2 ); + } + } else if(t2_ei != NULL){ + t1_ei = getOrMakeEqcInfo(t1, true); + for(NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++) { + t1_ei->d_mem.insert(*itr); + } + for(NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++) { + t1_ei->d_not_mem.insert(*itr); + } + if(t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull()) { + t1_ei->d_pt.set(t2_ei->d_pt); + } + } + } + + void TheorySetsRels::mergeTransposeEqcs(Node t1, Node t2) { + Trace("rels-std") << "[sets-rels] Merge TRANSPOSE eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; + EqcInfo* t1_ei = getOrMakeEqcInfo(t1); + EqcInfo* t2_ei = getOrMakeEqcInfo(t2); + + if(t1_ei != NULL && t2_ei != NULL) { + // TP(t1) = TP(t2) -> t1 = t2; + if(!t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull()) { + sendInferTranspose( true, t1_ei->d_tp.get(), t2_ei->d_tp.get(), explain(EQUAL(t1, t2)) ); + } + // Apply transpose rule on (non)members of t2 and t1->tp + if(!t1_ei->d_tp.get().isNull()) { + for(NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++) { + if(!t1_ei->d_mem.contains(*itr)) { + sendInferTranspose( true, *itr, t1_ei->d_tp.get(), AND(explain(EQUAL(t1_ei->d_tp.get(), t2)), explain(MEMBER(*itr, t2))) ); + } + } + for(NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++) { + if(!t1_ei->d_not_mem.contains(*itr)) { + sendInferTranspose( false, *itr, t1_ei->d_tp.get(), AND(explain(EQUAL(t1_ei->d_tp.get(), t2)), explain(MEMBER(*itr, t2).negate())) ); + } + } + // Apply transpose rule on (non)members of t1 and t2->tp + } else if(!t2_ei->d_tp.get().isNull()) { + t1_ei->d_tp.set(t2_ei->d_tp); + for(NodeSet::key_iterator itr = t1_ei->d_mem.key_begin(); itr != t1_ei->d_mem.key_end(); itr++) { + if(!t2_ei->d_mem.contains(*itr)) { + sendInferTranspose( true, *itr, t2_ei->d_tp.get(), AND(explain(EQUAL(t1, t2_ei->d_tp.get())), explain(MEMBER(*itr, t1))) ); + } + } + for(NodeSet::key_iterator itr = t1_ei->d_not_mem.key_begin(); itr != t1_ei->d_not_mem.key_end(); itr++) { + if(!t2_ei->d_not_mem.contains(*itr)) { + sendInferTranspose( false, *itr, t2_ei->d_tp.get(), AND(explain(EQUAL(t1, t2_ei->d_tp.get())), explain(MEMBER(*itr, t1).negate())) ); + } + } + } + // t1 was created already and t2 was not + } else if(t1_ei != NULL) { + if(t1_ei->d_tp.get().isNull() && t2.getKind() == kind::TRANSPOSE) { + t1_ei->d_tp.set( t2 ); + } + } else if(t2_ei != NULL){ + t1_ei = getOrMakeEqcInfo(t1, true); + for(NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++) { + t1_ei->d_mem.insert(*itr); + } + for(NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++) { + t1_ei->d_not_mem.insert(*itr); + } + if(t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull()) { + t1_ei->d_tp.set(t2_ei->d_tp); + } + } + } + + void TheorySetsRels::doPendingMerge() { + for(NodeList::const_iterator itr = d_pending_merge.begin(); itr != d_pending_merge.end(); itr++) { + Trace("rels-std") << "[sets-rels-lemma] Process pending merge fact : " + << *itr << std::endl; + d_sets_theory.d_out->lemma(*itr); + } + } + + void TheorySetsRels::sendInferTranspose( bool polarity, Node t1, Node t2, Node exp, bool reverseOnly ) { + Assert(t2.getKind() == kind::TRANSPOSE); + if(polarity && isRel(t1) && isRel(t2)) { + Assert(t1.getKind() == kind::TRANSPOSE); + Node n = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, EQUAL(t1[0], t2[0]) ); + Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying transpose rule: " + << n << std::endl; + d_pending_merge.push_back(n); + d_lemma.insert(n); + return; + } + + Node n1; + if(reverseOnly) { + if(polarity) { + n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]) ); + } else { + n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]).negate() ); + } + } else { + Node n2; + if(polarity) { + n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(t1, t2) ); + n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]) ); + } else { + n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(t1, t2).negate() ); + n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]).negate() ); + } + Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying transpose rule: " + << n2 << std::endl; + d_pending_merge.push_back(n2); + d_lemma.insert(n2); + } + Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying transpose rule: " + << n1 << std::endl; + d_pending_merge.push_back(n1); + d_lemma.insert(n1); + + } + + void TheorySetsRels::sendInferProduct( bool polarity, Node t1, Node t2, Node exp ) { + Assert(t2.getKind() == kind::PRODUCT); + if(polarity && isRel(t1) && isRel(t2)) { + //PRODUCT(x) = PRODUCT(y) => x = y; + Assert(t1.getKind() == kind::PRODUCT); + Node n = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, EQUAL(t1[0], t2[0]) ); + Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying product rule: " + << n << std::endl; + d_pending_merge.push_back(n); + d_lemma.insert(n); + return; + } + + std::vector<Node> r1_element; + std::vector<Node> r2_element; + Node r1 = t2[0]; + Node r2 = t2[1]; + NodeManager *nm = NodeManager::currentNM(); + Datatype dt = r1.getType().getSetElementType().getDatatype(); + unsigned int i = 0; + unsigned int s1_len = r1.getType().getSetElementType().getTupleLength(); + unsigned int tup_len = t2.getType().getSetElementType().getTupleLength(); + + r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); + for(; i < s1_len; ++i) { + r1_element.push_back(RelsUtils::nthElementOfTuple(t1, i)); + } + + dt = r2.getType().getSetElementType().getDatatype(); + r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); + for(; i < tup_len; ++i) { + r2_element.push_back(RelsUtils::nthElementOfTuple(t1, i)); + } + + Node n1; + Node n2; + Node tuple_1 = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element)); + Node tuple_2 = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element)); + + if(polarity) { + n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(tuple_1, r1) ); + n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(tuple_2, r2) ); + } else { + n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(tuple_1, r1).negate() ); + n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(tuple_2, r2).negate() ); + } + Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying product-split rule: " + << n1 << std::endl; + d_pending_merge.push_back(n1); + d_lemma.insert(n1); + Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying product-split rule: " + << n2 << std::endl; + d_pending_merge.push_back(n2); + d_lemma.insert(n2); + + } + + TheorySetsRels::EqcInfo* TheorySetsRels::getOrMakeEqcInfo( Node n, bool doMake ){ + std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); + if(eqc_i == d_eqc_info.end()){ + if( doMake ){ + EqcInfo* ei; + if(eqc_i!=d_eqc_info.end()){ + ei = eqc_i->second; + }else{ + ei = new EqcInfo(d_sets_theory.getSatContext()); + d_eqc_info[n] = ei; + } + if(n.getKind() == kind::TRANSPOSE){ + ei->d_tp = n; + } else if(n.getKind() == kind::PRODUCT) { + ei->d_pt = n; + } else if(n.getKind() == kind::TCLOSURE) { + ei->d_tc = n; + } else if(n.getKind() == kind::JOIN) { + ei->d_join = n; + } + return ei; + }else{ + return NULL; + } + }else{ + return (*eqc_i).second; + } + } + + + Node TheorySetsRels::mkAnd( std::vector<TNode>& conjunctions ) { + Assert(conjunctions.size() > 0); + std::set<TNode> all; + + for (unsigned i = 0; i < conjunctions.size(); ++i) { + TNode t = conjunctions[i]; + if (t.getKind() == kind::AND) { + for(TNode::iterator child_it = t.begin(); + child_it != t.end(); ++child_it) { + Assert((*child_it).getKind() != kind::AND); + all.insert(*child_it); + } + } + else { + all.insert(t); + } + } + Assert(all.size() > 0); + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; + }/* mkAnd() */ + + void TheorySetsRels::printNodeMap(char* fst, char* snd, NodeMap map) { + NodeMap::iterator map_it = map.begin(); + while(map_it != map.end()) { + Trace("rels-debug") << fst << " "<< (*map_it).first << " " << snd << " " << (*map_it).second<< std::endl; + map_it++; + } + } + +} +} +} + + + + + + + + + + + + + + diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h new file mode 100644 index 000000000..381ccddd9 --- /dev/null +++ b/src/theory/sets/theory_sets_rels.h @@ -0,0 +1,218 @@ +/********************* */ +/*! \file theory_sets_rels.h + ** \verbatim + ** Original author: Paul Meng + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sets theory implementation. + ** + ** Extension to Sets theory. + **/ + +#ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_ +#define SRC_THEORY_SETS_THEORY_SETS_RELS_H_ + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" +#include "context/cdhashset.h" +#include "context/cdchunk_list.h" +#include "theory/sets/rels_utils.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +class TheorySets; + + +class TupleTrie { +public: + /** the data */ + std::map< Node, TupleTrie > d_data; +public: + std::vector<Node> findTerms( std::vector< Node >& reps, int argIndex = 0 ); + Node existsTerm( std::vector< Node >& reps, int argIndex = 0 ); + bool addTerm( Node n, std::vector< Node >& reps, int argIndex = 0 ); + void debugPrint( const char * c, Node n, unsigned depth = 0 ); + void clear() { d_data.clear(); } +};/* class TupleTrie */ + +class TheorySetsRels { + + typedef context::CDChunkList<Node> NodeList; + typedef context::CDChunkList<int> IdList; + typedef context::CDHashMap<int, IdList*> IdListMap; + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; + typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; + typedef context::CDHashMap<Node, NodeSet*, NodeHashFunction> NodeSetMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; + +public: + TheorySetsRels(context::Context* c, + context::UserContext* u, + eq::EqualityEngine*, + context::CDO<bool>*, + TheorySets&); + + ~TheorySetsRels(); + void check(Theory::Effort); + void doPendingLemmas(); + +private: + /** equivalence class info + * d_mem tuples that are members of this equivalence class + * d_not_mem tuples that are not members of this equivalence class + * d_tp is a node of kind TRANSPOSE (if any) in this equivalence class, + * d_pt is a node of kind PRODUCT (if any) in this equivalence class, + * d_join is a node of kind JOIN (if any) in this equivalence class, + * d_tc is a node of kind TCLOSURE (if any) in this equivalence class, + */ + class EqcInfo + { + public: + EqcInfo( context::Context* c ); + ~EqcInfo(){} + static int counter; + NodeSet d_mem; + NodeSet d_not_mem; + NodeListMap d_in; + NodeListMap d_out; + NodeMap d_mem_exp; + IdListMap d_id_in; // mapping from a element rep id to a list of rep ids that pointed by + IdListMap d_id_out; // mapping from a element rep id to a list of rep ids that point to + context::CDO< Node > d_tp; + context::CDO< Node > d_pt; + context::CDO< Node > d_join; + context::CDO< Node > d_tc; + }; + +private: + std::map<int, Node> d_id_node; // mapping between integer id and tuple element rep + std::map<Node, int> d_node_id; // mapping between tuple element rep and integer id + + /** has eqc info */ + bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); } + + +private: + eq::EqualityEngine *d_eqEngine; + context::CDO<bool> *d_conflict; + TheorySets& d_sets_theory; + /** True and false constant nodes */ + Node d_trueNode; + Node d_falseNode; + // Facts and lemmas to be sent to EE + std::map< Node, Node > d_pending_facts; + std::map< Node, Node > d_pending_split_facts; + std::vector< Node > d_lemma_cache; + NodeList d_pending_merge; + /** inferences: maintained to ensure ref count for internally introduced nodes */ + NodeList d_infer; + NodeList d_infer_exp; + NodeSet d_lemma; + NodeSet d_shared_terms; + // tc terms that have been decomposed + NodeSet d_tc_saver; + + std::hash_set< Node, NodeHashFunction > d_rel_nodes; + std::map< Node, std::vector<Node> > d_tuple_reps; + std::map< Node, TupleTrie > d_membership_trie; + std::hash_set< Node, NodeHashFunction > d_symbolic_tuples; + std::map< Node, std::vector<Node> > d_membership_constraints_cache; + std::map< Node, std::vector<Node> > d_membership_exp_cache; + std::map< Node, std::vector<Node> > d_membership_db; + std::map< Node, std::vector<Node> > d_membership_exp_db; + std::map< Node, Node > d_membership_tc_exp_cache; + std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache; + std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_membership_tc_cache; + + /** information necessary for equivalence classes */ +public: + void eqNotifyNewClass(Node t); + void eqNotifyPostMerge(Node t1, Node t2); + +private: + + void doPendingMerge(); + std::map< Node, EqcInfo* > d_eqc_info; + EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); + void mergeTransposeEqcs(Node t1, Node t2); + void mergeProductEqcs(Node t1, Node t2); + void mergeTCEqcs(Node t1, Node t2); + void sendInferTranspose(bool, Node, Node, Node, bool reverseOnly = false); + void sendInferProduct(bool, Node, Node, Node); + void sendTCInference(EqcInfo* tc_ei, std::hash_set<int> in_reachable, std::hash_set<int> out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2); + void addTCMemAndSendInfer(EqcInfo* tc_ei, Node mem, Node exp, bool fromRel = false); + Node findTCMemExp(EqcInfo*, Node); + void mergeTCEqcExp(EqcInfo*, EqcInfo*); + void buildTCAndExp(Node, EqcInfo*); + int getOrMakeElementRepId(EqcInfo*, Node); + void collectInReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& in_reachable, bool firstRound = true); + void collectOutReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& out_reachable, bool firstRound = true); + Node explainTCMem(EqcInfo*, Node, Node, Node); + + + void check(); + void collectRelsInfo(); + void assertMembership( Node fact, Node reason, bool polarity ); + void composeTupleMemForRels( Node ); + void applyTransposeRule( Node, Node, bool tp_occur_rule = false ); + void applyJoinRule( Node, Node ); + void applyProductRule( Node, Node ); + void applyTCRule( Node, Node ); + void buildTCGraph( Node, Node, Node ); + void computeRels( Node ); + void computeTransposeRelations( Node ); + void finalizeTCInfer(); + void inferTC( Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >& ); + void inferTC( Node, Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >&, + Node, Node, std::hash_set< Node, NodeHashFunction >&); + + Node explain(Node); + + void sendInfer( Node fact, Node exp, const char * c ); + void sendLemma( Node fact, Node reason, const char * c ); + void sendSplit( Node a, Node b, const char * c ); + void doPendingFacts(); + void doPendingSplitFacts(); + void addSharedTerm( TNode n ); + void checkTCGraphForConflict( Node, Node, Node, Node, Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >& ); + bool checkCycles( Node ); + + // Helper functions + bool insertIntoIdList(IdList&, int); + inline Node getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r); + inline Node constructPair(Node tc_rep, Node a, Node b); + Node findMemExp(Node r, Node pair); + bool safeAddToMap( std::map< Node, std::vector<Node> >&, Node, Node ); + void addToMap( std::map< Node, std::vector<Node> >&, Node, Node ); + bool hasMember( Node, Node ); + Node getRepresentative( Node t ); + bool hasTerm( Node a ); + bool areEqual( Node a, Node b ); + bool exists( std::vector<Node>&, Node ); + bool holds( Node ); + void computeTupleReps( Node ); + void makeSharedTerm( Node ); + void reduceTupleVar( Node ); + inline void addToMembershipDB( Node, Node, Node ); + bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();} + Node mkAnd( std::vector< TNode >& assumptions ); + void printNodeMap(char* fst, char* snd, NodeMap map); + +}; + + +}/* CVC4::theory::sets namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + + + +#endif /* SRC_THEORY_SETS_THEORY_SETS_RELS_H_ */ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 8dbca1e73..5204dcaed 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -16,6 +16,8 @@ #include "theory/sets/theory_sets_rewriter.h" #include "theory/sets/normal_form.h" +#include "theory/sets/theory_sets_rels.h" +#include "theory/sets/rels_utils.h" #include "expr/attribute.h" #include "options/sets_options.h" @@ -315,6 +317,145 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } } + case kind::TRANSPOSE: { + if(node[0].getKind() == kind::TRANSPOSE) { + return RewriteResponse(REWRITE_AGAIN, node[0][0]); + } + + if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + } else if(node[0].isConst()) { + std::set<Node> new_tuple_set; + std::set<Node> tuple_set = NormalForm::getElementsFromNormalConstant(node[0]); + std::set<Node>::iterator tuple_it = tuple_set.begin(); + + while(tuple_it != tuple_set.end()) { + new_tuple_set.insert(RelsUtils::reverseTuple(*tuple_it)); + tuple_it++; + } + Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); + Assert(new_node.isConst()); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; + return RewriteResponse(REWRITE_DONE, new_node); + + } + if(node[0].getKind() != kind::TRANSPOSE) { + Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl; + return RewriteResponse(REWRITE_DONE, node); + } + break; + } + + case kind::PRODUCT: { + Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " << node << std::endl; + if( node[0].getKind() == kind::EMPTYSET || + node[1].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + } else if( node[0].isConst() && node[1].isConst() ) { + Trace("sets-rels-postrewrite") << "Sets::postRewrite processing **** " << node << std::endl; + std::set<Node> new_tuple_set; + std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); + std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); + std::set<Node>::iterator left_it = left.begin(); + int left_len = (*left_it).getType().getTupleLength(); + TypeNode tn = node.getType().getSetElementType(); + while(left_it != left.end()) { + Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *left_it << std::endl; + std::vector<Node> left_tuple; + left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + for(int i = 0; i < left_len; i++) { + left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); + } + std::set<Node>::iterator right_it = right.begin(); + int right_len = (*right_it).getType().getTupleLength(); + while(right_it != right.end()) { + Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *right_it << std::endl; + std::vector<Node> right_tuple; + for(int j = 0; j < right_len; j++) { + right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j)); + } + std::vector<Node> new_tuple; + new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end()); + new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end()); + Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); + new_tuple_set.insert(composed_tuple); + right_it++; + } + left_it++; + } + Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); + Assert(new_node.isConst()); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; + return RewriteResponse(REWRITE_DONE, new_node); + } + break; + } + + case kind::JOIN: { + if( node[0].getKind() == kind::EMPTYSET || + node[1].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + } else if( node[0].isConst() && node[1].isConst() ) { + Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " << node << std::endl; + std::set<Node> new_tuple_set; + std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); + std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); + std::set<Node>::iterator left_it = left.begin(); + int left_len = (*left_it).getType().getTupleLength(); + TypeNode tn = node.getType().getSetElementType(); + while(left_it != left.end()) { + std::vector<Node> left_tuple; + left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + for(int i = 0; i < left_len - 1; i++) { + left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); + } + std::set<Node>::iterator right_it = right.begin(); + int right_len = (*right_it).getType().getTupleLength(); + while(right_it != right.end()) { + if(RelsUtils::nthElementOfTuple(*left_it,left_len-1) == RelsUtils::nthElementOfTuple(*right_it,0)) { + std::vector<Node> right_tuple; + for(int j = 1; j < right_len; j++) { + right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j)); + } + std::vector<Node> new_tuple; + new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end()); + new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end()); + Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); + new_tuple_set.insert(composed_tuple); + } + right_it++; + } + left_it++; + } + Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); + Assert(new_node.isConst()); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; + return RewriteResponse(REWRITE_DONE, new_node); + } + + break; + } + + case kind::TCLOSURE: { + if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + } else if (node[0].isConst()) { + std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); + std::set<Node> tc_rel_mems = RelsUtils::computeTC(rel_mems, node); + Node new_node = NormalForm::elementsToSet(tc_rel_mems, node.getType()); + Assert(new_node.isConst()); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; + return RewriteResponse(REWRITE_DONE, new_node); + + } else if(node[0].getKind() == kind::TCLOSURE) { + return RewriteResponse(REWRITE_AGAIN, node[0]); + } else if(node[0].getKind() != kind::TCLOSURE) { + Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl; + return RewriteResponse(REWRITE_DONE, node); + } + break; + } + default: break; }//switch(node.getKind()) diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 7a8d7eed4..478dcbdb6 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -105,7 +105,7 @@ struct MemberTypeRule { throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set"); } TypeNode elementType = n[0].getType(check); - if(elementType != setType.getSetElementType()) { + if(!setType.getSetElementType().isSubtypeOf(elementType)) { throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types"); } } @@ -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<TypeNode> newTupleTypes; + std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes(); + std::vector<TypeNode> 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<TypeNode> 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<TypeNode> 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); diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 19f6313fb..5069d061e 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -83,4 +83,4 @@ regress regress0 test: check # do nothing in this subdir .PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +regress1 regress2 regress3:
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel_1tup_0.cvc b/test/regress/regress0/sets/rels/rel_1tup_0.cvc new file mode 100644 index 000000000..50d4defd5 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_1tup_0.cvc @@ -0,0 +1,24 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT]; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; +z: SET OF IntTup; + +b : IntPair; +ASSERT b = (2, 1); +ASSERT b IS_IN x; + +a : IntTup; +ASSERT a = TUPLE(1); +ASSERT a IS_IN y; + +c : IntTup; +ASSERT c = TUPLE(2); + +ASSERT z = (x JOIN y); + +ASSERT NOT (c IS_IN z); + +CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel_complex_0.cvc b/test/regress/regress0/sets/rels/rel_complex_0.cvc new file mode 100644 index 000000000..dcb753973 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_0.cvc @@ -0,0 +1,31 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +z : SET OF INT; +f : INT; +g : INT; + +e : IntPair; +ASSERT e = (4, f); +ASSERT e IS_IN x; + +d : IntPair; +ASSERT d = (g,3); +ASSERT d IS_IN y; + + +ASSERT z = {f, g}; +ASSERT 0 = f - g; + + + +a : IntPair; +ASSERT a = (4,3); + +ASSERT r = (x JOIN y); + +ASSERT NOT (a IS_IN r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_complex_1.cvc b/test/regress/regress0/sets/rels/rel_complex_1.cvc new file mode 100644 index 000000000..969d0d71c --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_1.cvc @@ -0,0 +1,34 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +w : SET OF IntTup; +z : SET OF IntTup; +r2 : SET OF IntPair; + +a : IntPair; +ASSERT a = (3,1); +ASSERT a IS_IN x; + +d : IntPair; +ASSERT d = (1,3); +ASSERT d IS_IN y; + +e : IntPair; +ASSERT e = (4,3); +ASSERT r = (x JOIN y); + +ASSERT TUPLE(1) IS_IN w; +ASSERT TUPLE(2) IS_IN z; +ASSERT r2 = (w PRODUCT z); + +ASSERT NOT (e IS_IN r); +%ASSERT e IS_IN r2; +ASSERT (r <= r2); +ASSERT NOT ((3,3) IS_IN r2); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_complex_3.cvc b/test/regress/regress0/sets/rels/rel_complex_3.cvc new file mode 100644 index 000000000..492c94432 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_3.cvc @@ -0,0 +1,49 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + + +f : IntPair; +ASSERT f = (3,1); +ASSERT f IS_IN x; + +g : IntPair; +ASSERT g = (1,3); +ASSERT g IS_IN y; + +h : IntPair; +ASSERT h = (3,5); +ASSERT h IS_IN x; +ASSERT h IS_IN y; + +ASSERT r = (x JOIN y); + +e : IntPair; + +ASSERT NOT (e IS_IN r); +ASSERT NOT(z = (x & y)); +ASSERT z = (x - y); +ASSERT x <= y; +ASSERT e IS_IN (r JOIN z); +ASSERT e IS_IN x; +ASSERT e IS_IN (x & y); +CHECKSAT TRUE; + + + + + + + + + + + + + + diff --git a/test/regress/regress0/sets/rels/rel_complex_4.cvc b/test/regress/regress0/sets/rels/rel_complex_4.cvc new file mode 100644 index 000000000..f473b00aa --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_4.cvc @@ -0,0 +1,52 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + + +f : IntPair; +ASSERT f = (3,1); +ASSERT f IS_IN x; + +g : IntPair; +ASSERT g = (1,3); +ASSERT g IS_IN y; + +h : IntPair; +ASSERT h = (3,5); +ASSERT h IS_IN x; +ASSERT h IS_IN y; + +ASSERT r = (x JOIN y); +a:INT; +e : IntPair; +ASSERT e = (a,a); +ASSERT w = {e}; +ASSERT TRANSPOSE(w) <= y; + +ASSERT NOT (e IS_IN r); +ASSERT NOT(z = (x & y)); +ASSERT z = (x - y); +ASSERT x <= y; +ASSERT e IS_IN (r JOIN z); +ASSERT e IS_IN x; +ASSERT e IS_IN (x & y); +CHECKSAT TRUE; + + + + + + + + + + + + + + diff --git a/test/regress/regress0/sets/rels/rel_complex_5.cvc b/test/regress/regress0/sets/rels/rel_complex_5.cvc new file mode 100644 index 000000000..d64817187 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_5.cvc @@ -0,0 +1,55 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + + +f : IntPair; +ASSERT f = (3,1); +ASSERT f IS_IN x; + +g : IntPair; +ASSERT g = (1,3); +ASSERT g IS_IN y; + +h : IntPair; +ASSERT h = (3,5); +ASSERT h IS_IN x; +ASSERT h IS_IN y; + +ASSERT r = (x JOIN y); +a:IntTup; +ASSERT a = TUPLE(1); +e : IntPair; +ASSERT e = (1,1); + +ASSERT w = ({a} PRODUCT {a}); +ASSERT TRANSPOSE(w) <= y; + +ASSERT NOT (e IS_IN r); +ASSERT NOT(z = (x & y)); +ASSERT z = (x - y); +ASSERT x <= y; +ASSERT e IS_IN (r JOIN z); +ASSERT e IS_IN x; +ASSERT e IS_IN (x & y); +CHECKSAT TRUE; + + + + + + + + + + + + + + diff --git a/test/regress/regress0/sets/rels/rel_conflict_0.cvc b/test/regress/regress0/sets/rels/rel_conflict_0.cvc new file mode 100644 index 000000000..c1b82339f --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_conflict_0.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +e : IntPair; +ASSERT e = (4, 4); +ASSERT e IS_IN x; + +ASSERT NOT ((4, 4) IS_IN x); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_0.cvc b/test/regress/regress0/sets/rels/rel_join_0.cvc new file mode 100644 index 000000000..406b8d312 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_0.cvc @@ -0,0 +1,24 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (7, 5) IS_IN y; + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_0_1.cvc b/test/regress/regress0/sets/rels/rel_join_0_1.cvc new file mode 100644 index 000000000..a7fa7efb9 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_0_1.cvc @@ -0,0 +1,27 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (4, 3) IS_IN x; +ASSERT (7, 5) IS_IN y; + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +%ASSERT a IS_IN (x JOIN y); +%ASSERT NOT (v IS_IN (x JOIN y)); +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_1.cvc b/test/regress/regress0/sets/rels/rel_join_1.cvc new file mode 100644 index 000000000..c8921afb9 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_1.cvc @@ -0,0 +1,31 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_1_1.cvc b/test/regress/regress0/sets/rels/rel_join_1_1.cvc new file mode 100644 index 000000000..3436bd707 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_1_1.cvc @@ -0,0 +1,31 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_2.cvc b/test/regress/regress0/sets/rels/rel_join_2.cvc new file mode 100644 index 000000000..cac7ce84d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_2.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_join_2_1.cvc new file mode 100644 index 000000000..3e27b9cc5 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_2_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_3.cvc b/test/regress/regress0/sets/rels/rel_join_3.cvc new file mode 100644 index 000000000..6e190cecf --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_3.cvc @@ -0,0 +1,29 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN r); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_3_1.cvc b/test/regress/regress0/sets/rels/rel_join_3_1.cvc new file mode 100644 index 000000000..d4e666c6e --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_3_1.cvc @@ -0,0 +1,29 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT a IS_IN r; + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_4.cvc b/test/regress/regress0/sets/rels/rel_join_4.cvc new file mode 100644 index 000000000..030810f3d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_4.cvc @@ -0,0 +1,32 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +b : IntPair; +ASSERT b = (7, 5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT b IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN r); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_5.cvc b/test/regress/regress0/sets/rels/rel_join_5.cvc new file mode 100644 index 000000000..5209d8131 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_5.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; + +a : IntPair; +ASSERT a = (1,4); +ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); +ASSERT NOT (a IS_IN r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_6.cvc b/test/regress/regress0/sets/rels/rel_join_6.cvc new file mode 100644 index 000000000..17318872f --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_6.cvc @@ -0,0 +1,13 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +ASSERT x = {(1,2), (3, 4)}; + +ASSERT y = (x JOIN {(2,1), (4,3)}); + +ASSERT NOT ((1,1) IS_IN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_7.cvc b/test/regress/regress0/sets/rels/rel_join_7.cvc new file mode 100644 index 000000000..fff5b6efe --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_7.cvc @@ -0,0 +1,26 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (7, 5) IS_IN y; + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT w = (r | (x JOIN y)); +ASSERT NOT (a IS_IN w); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_mix_0.cvc b/test/regress/regress0/sets/rels/rel_mix_0.cvc new file mode 100644 index 000000000..723a9b2e2 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_mix_0.cvc @@ -0,0 +1,30 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +w : SET OF IntTup; +z : SET OF IntTup; +r2 : SET OF IntPair; + +d : IntPair; +ASSERT d = (1,3); +ASSERT (1,3) IS_IN y; + +a : IntPair; +ASSERT a IS_IN x; + +e : IntPair; +ASSERT e = (4,3); + +ASSERT r = (x JOIN y); +ASSERT r2 = (w PRODUCT z); + +ASSERT NOT (e IS_IN r); +%ASSERT e IS_IN r2; +ASSERT NOT (r = r2); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_pressure_0.cvc b/test/regress/regress0/sets/rels/rel_pressure_0.cvc new file mode 100644 index 000000000..6cdf03600 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_pressure_0.cvc @@ -0,0 +1,617 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +a11 : IntPair; +ASSERT a11 = (1, 1); +ASSERT a11 IS_IN x; +a12 : IntPair; +ASSERT a12 = (1, 2); +ASSERT a12 IS_IN x; +a13 : IntPair; +ASSERT a13 = (1, 3); +ASSERT a13 IS_IN x; +a14 : IntPair; +ASSERT a14 = (1, 4); +ASSERT a14 IS_IN x; +a15 : IntPair; +ASSERT a15 = (1, 5); +ASSERT a15 IS_IN x; +a16 : IntPair; +ASSERT a16 = (1, 6); +ASSERT a16 IS_IN x; +a17 : IntPair; +ASSERT a17 = (1, 7); +ASSERT a17 IS_IN x; +a18 : IntPair; +ASSERT a18 = (1, 8); +ASSERT a18 IS_IN x; +a19 : IntPair; +ASSERT a19 = (1, 9); +ASSERT a19 IS_IN x; +a110 : IntPair; +ASSERT a110 = (1, 10); +ASSERT a110 IS_IN x; +a21 : IntPair; +ASSERT a21 = (2, 1); +ASSERT a21 IS_IN x; +a22 : IntPair; +ASSERT a22 = (2, 2); +ASSERT a22 IS_IN x; +a23 : IntPair; +ASSERT a23 = (2, 3); +ASSERT a23 IS_IN x; +a24 : IntPair; +ASSERT a24 = (2, 4); +ASSERT a24 IS_IN x; +a25 : IntPair; +ASSERT a25 = (2, 5); +ASSERT a25 IS_IN x; +a26 : IntPair; +ASSERT a26 = (2, 6); +ASSERT a26 IS_IN x; +a27 : IntPair; +ASSERT a27 = (2, 7); +ASSERT a27 IS_IN x; +a28 : IntPair; +ASSERT a28 = (2, 8); +ASSERT a28 IS_IN x; +a29 : IntPair; +ASSERT a29 = (2, 9); +ASSERT a29 IS_IN x; +a210 : IntPair; +ASSERT a210 = (2, 10); +ASSERT a210 IS_IN x; +a31 : IntPair; +ASSERT a31 = (3, 1); +ASSERT a31 IS_IN x; +a32 : IntPair; +ASSERT a32 = (3, 2); +ASSERT a32 IS_IN x; +a33 : IntPair; +ASSERT a33 = (3, 3); +ASSERT a33 IS_IN x; +a34 : IntPair; +ASSERT a34 = (3, 4); +ASSERT a34 IS_IN x; +a35 : IntPair; +ASSERT a35 = (3, 5); +ASSERT a35 IS_IN x; +a36 : IntPair; +ASSERT a36 = (3, 6); +ASSERT a36 IS_IN x; +a37 : IntPair; +ASSERT a37 = (3, 7); +ASSERT a37 IS_IN x; +a38 : IntPair; +ASSERT a38 = (3, 8); +ASSERT a38 IS_IN x; +a39 : IntPair; +ASSERT a39 = (3, 9); +ASSERT a39 IS_IN x; +a310 : IntPair; +ASSERT a310 = (3, 10); +ASSERT a310 IS_IN x; +a41 : IntPair; +ASSERT a41 = (4, 1); +ASSERT a41 IS_IN x; +a42 : IntPair; +ASSERT a42 = (4, 2); +ASSERT a42 IS_IN x; +a43 : IntPair; +ASSERT a43 = (4, 3); +ASSERT a43 IS_IN x; +a44 : IntPair; +ASSERT a44 = (4, 4); +ASSERT a44 IS_IN x; +a45 : IntPair; +ASSERT a45 = (4, 5); +ASSERT a45 IS_IN x; +a46 : IntPair; +ASSERT a46 = (4, 6); +ASSERT a46 IS_IN x; +a47 : IntPair; +ASSERT a47 = (4, 7); +ASSERT a47 IS_IN x; +a48 : IntPair; +ASSERT a48 = (4, 8); +ASSERT a48 IS_IN x; +a49 : IntPair; +ASSERT a49 = (4, 9); +ASSERT a49 IS_IN x; +a410 : IntPair; +ASSERT a410 = (4, 10); +ASSERT a410 IS_IN x; +a51 : IntPair; +ASSERT a51 = (5, 1); +ASSERT a51 IS_IN x; +a52 : IntPair; +ASSERT a52 = (5, 2); +ASSERT a52 IS_IN x; +a53 : IntPair; +ASSERT a53 = (5, 3); +ASSERT a53 IS_IN x; +a54 : IntPair; +ASSERT a54 = (5, 4); +ASSERT a54 IS_IN x; +a55 : IntPair; +ASSERT a55 = (5, 5); +ASSERT a55 IS_IN x; +a56 : IntPair; +ASSERT a56 = (5, 6); +ASSERT a56 IS_IN x; +a57 : IntPair; +ASSERT a57 = (5, 7); +ASSERT a57 IS_IN x; +a58 : IntPair; +ASSERT a58 = (5, 8); +ASSERT a58 IS_IN x; +a59 : IntPair; +ASSERT a59 = (5, 9); +ASSERT a59 IS_IN x; +a510 : IntPair; +ASSERT a510 = (5, 10); +ASSERT a510 IS_IN x; +a61 : IntPair; +ASSERT a61 = (6, 1); +ASSERT a61 IS_IN x; +a62 : IntPair; +ASSERT a62 = (6, 2); +ASSERT a62 IS_IN x; +a63 : IntPair; +ASSERT a63 = (6, 3); +ASSERT a63 IS_IN x; +a64 : IntPair; +ASSERT a64 = (6, 4); +ASSERT a64 IS_IN x; +a65 : IntPair; +ASSERT a65 = (6, 5); +ASSERT a65 IS_IN x; +a66 : IntPair; +ASSERT a66 = (6, 6); +ASSERT a66 IS_IN x; +a67 : IntPair; +ASSERT a67 = (6, 7); +ASSERT a67 IS_IN x; +a68 : IntPair; +ASSERT a68 = (6, 8); +ASSERT a68 IS_IN x; +a69 : IntPair; +ASSERT a69 = (6, 9); +ASSERT a69 IS_IN x; +a610 : IntPair; +ASSERT a610 = (6, 10); +ASSERT a610 IS_IN x; +a71 : IntPair; +ASSERT a71 = (7, 1); +ASSERT a71 IS_IN x; +a72 : IntPair; +ASSERT a72 = (7, 2); +ASSERT a72 IS_IN x; +a73 : IntPair; +ASSERT a73 = (7, 3); +ASSERT a73 IS_IN x; +a74 : IntPair; +ASSERT a74 = (7, 4); +ASSERT a74 IS_IN x; +a75 : IntPair; +ASSERT a75 = (7, 5); +ASSERT a75 IS_IN x; +a76 : IntPair; +ASSERT a76 = (7, 6); +ASSERT a76 IS_IN x; +a77 : IntPair; +ASSERT a77 = (7, 7); +ASSERT a77 IS_IN x; +a78 : IntPair; +ASSERT a78 = (7, 8); +ASSERT a78 IS_IN x; +a79 : IntPair; +ASSERT a79 = (7, 9); +ASSERT a79 IS_IN x; +a710 : IntPair; +ASSERT a710 = (7, 10); +ASSERT a710 IS_IN x; +a81 : IntPair; +ASSERT a81 = (8, 1); +ASSERT a81 IS_IN x; +a82 : IntPair; +ASSERT a82 = (8, 2); +ASSERT a82 IS_IN x; +a83 : IntPair; +ASSERT a83 = (8, 3); +ASSERT a83 IS_IN x; +a84 : IntPair; +ASSERT a84 = (8, 4); +ASSERT a84 IS_IN x; +a85 : IntPair; +ASSERT a85 = (8, 5); +ASSERT a85 IS_IN x; +a86 : IntPair; +ASSERT a86 = (8, 6); +ASSERT a86 IS_IN x; +a87 : IntPair; +ASSERT a87 = (8, 7); +ASSERT a87 IS_IN x; +a88 : IntPair; +ASSERT a88 = (8, 8); +ASSERT a88 IS_IN x; +a89 : IntPair; +ASSERT a89 = (8, 9); +ASSERT a89 IS_IN x; +a810 : IntPair; +ASSERT a810 = (8, 10); +ASSERT a810 IS_IN x; +a91 : IntPair; +ASSERT a91 = (9, 1); +ASSERT a91 IS_IN x; +a92 : IntPair; +ASSERT a92 = (9, 2); +ASSERT a92 IS_IN x; +a93 : IntPair; +ASSERT a93 = (9, 3); +ASSERT a93 IS_IN x; +a94 : IntPair; +ASSERT a94 = (9, 4); +ASSERT a94 IS_IN x; +a95 : IntPair; +ASSERT a95 = (9, 5); +ASSERT a95 IS_IN x; +a96 : IntPair; +ASSERT a96 = (9, 6); +ASSERT a96 IS_IN x; +a97 : IntPair; +ASSERT a97 = (9, 7); +ASSERT a97 IS_IN x; +a98 : IntPair; +ASSERT a98 = (9, 8); +ASSERT a98 IS_IN x; +a99 : IntPair; +ASSERT a99 = (9, 9); +ASSERT a99 IS_IN x; +a910 : IntPair; +ASSERT a910 = (9, 10); +ASSERT a910 IS_IN x; +a101 : IntPair; +ASSERT a101 = (10, 1); +ASSERT a101 IS_IN x; +a102 : IntPair; +ASSERT a102 = (10, 2); +ASSERT a102 IS_IN x; +a103 : IntPair; +ASSERT a103 = (10, 3); +ASSERT a103 IS_IN x; +a104 : IntPair; +ASSERT a104 = (10, 4); +ASSERT a104 IS_IN x; +a105 : IntPair; +ASSERT a105 = (10, 5); +ASSERT a105 IS_IN x; +a106 : IntPair; +ASSERT a106 = (10, 6); +ASSERT a106 IS_IN x; +a107 : IntPair; +ASSERT a107 = (10, 7); +ASSERT a107 IS_IN x; +a108 : IntPair; +ASSERT a108 = (10, 8); +ASSERT a108 IS_IN x; +a109 : IntPair; +ASSERT a109 = (10, 9); +ASSERT a109 IS_IN x; +a1010 : IntPair; +ASSERT a1010 = (10, 10); +ASSERT a1010 IS_IN x; +b11 : IntPair; +ASSERT b11 = (1, 1); +ASSERT b11 IS_IN y; +b12 : IntPair; +ASSERT b12 = (1, 2); +ASSERT b12 IS_IN y; +b13 : IntPair; +ASSERT b13 = (1, 3); +ASSERT b13 IS_IN y; +b14 : IntPair; +ASSERT b14 = (1, 4); +ASSERT b14 IS_IN y; +b15 : IntPair; +ASSERT b15 = (1, 5); +ASSERT b15 IS_IN y; +b16 : IntPair; +ASSERT b16 = (1, 6); +ASSERT b16 IS_IN y; +b17 : IntPair; +ASSERT b17 = (1, 7); +ASSERT b17 IS_IN y; +b18 : IntPair; +ASSERT b18 = (1, 8); +ASSERT b18 IS_IN y; +b19 : IntPair; +ASSERT b19 = (1, 9); +ASSERT b19 IS_IN y; +b110 : IntPair; +ASSERT b110 = (1, 10); +ASSERT b110 IS_IN y; +b21 : IntPair; +ASSERT b21 = (2, 1); +ASSERT b21 IS_IN y; +b22 : IntPair; +ASSERT b22 = (2, 2); +ASSERT b22 IS_IN y; +b23 : IntPair; +ASSERT b23 = (2, 3); +ASSERT b23 IS_IN y; +b24 : IntPair; +ASSERT b24 = (2, 4); +ASSERT b24 IS_IN y; +b25 : IntPair; +ASSERT b25 = (2, 5); +ASSERT b25 IS_IN y; +b26 : IntPair; +ASSERT b26 = (2, 6); +ASSERT b26 IS_IN y; +b27 : IntPair; +ASSERT b27 = (2, 7); +ASSERT b27 IS_IN y; +b28 : IntPair; +ASSERT b28 = (2, 8); +ASSERT b28 IS_IN y; +b29 : IntPair; +ASSERT b29 = (2, 9); +ASSERT b29 IS_IN y; +b210 : IntPair; +ASSERT b210 = (2, 10); +ASSERT b210 IS_IN y; +b31 : IntPair; +ASSERT b31 = (3, 1); +ASSERT b31 IS_IN y; +b32 : IntPair; +ASSERT b32 = (3, 2); +ASSERT b32 IS_IN y; +b33 : IntPair; +ASSERT b33 = (3, 3); +ASSERT b33 IS_IN y; +b34 : IntPair; +ASSERT b34 = (3, 4); +ASSERT b34 IS_IN y; +b35 : IntPair; +ASSERT b35 = (3, 5); +ASSERT b35 IS_IN y; +b36 : IntPair; +ASSERT b36 = (3, 6); +ASSERT b36 IS_IN y; +b37 : IntPair; +ASSERT b37 = (3, 7); +ASSERT b37 IS_IN y; +b38 : IntPair; +ASSERT b38 = (3, 8); +ASSERT b38 IS_IN y; +b39 : IntPair; +ASSERT b39 = (3, 9); +ASSERT b39 IS_IN y; +b310 : IntPair; +ASSERT b310 = (3, 10); +ASSERT b310 IS_IN y; +b41 : IntPair; +ASSERT b41 = (4, 1); +ASSERT b41 IS_IN y; +b42 : IntPair; +ASSERT b42 = (4, 2); +ASSERT b42 IS_IN y; +b43 : IntPair; +ASSERT b43 = (4, 3); +ASSERT b43 IS_IN y; +b44 : IntPair; +ASSERT b44 = (4, 4); +ASSERT b44 IS_IN y; +b45 : IntPair; +ASSERT b45 = (4, 5); +ASSERT b45 IS_IN y; +b46 : IntPair; +ASSERT b46 = (4, 6); +ASSERT b46 IS_IN y; +b47 : IntPair; +ASSERT b47 = (4, 7); +ASSERT b47 IS_IN y; +b48 : IntPair; +ASSERT b48 = (4, 8); +ASSERT b48 IS_IN y; +b49 : IntPair; +ASSERT b49 = (4, 9); +ASSERT b49 IS_IN y; +b410 : IntPair; +ASSERT b410 = (4, 10); +ASSERT b410 IS_IN y; +b51 : IntPair; +ASSERT b51 = (5, 1); +ASSERT b51 IS_IN y; +b52 : IntPair; +ASSERT b52 = (5, 2); +ASSERT b52 IS_IN y; +b53 : IntPair; +ASSERT b53 = (5, 3); +ASSERT b53 IS_IN y; +b54 : IntPair; +ASSERT b54 = (5, 4); +ASSERT b54 IS_IN y; +b55 : IntPair; +ASSERT b55 = (5, 5); +ASSERT b55 IS_IN y; +b56 : IntPair; +ASSERT b56 = (5, 6); +ASSERT b56 IS_IN y; +b57 : IntPair; +ASSERT b57 = (5, 7); +ASSERT b57 IS_IN y; +b58 : IntPair; +ASSERT b58 = (5, 8); +ASSERT b58 IS_IN y; +b59 : IntPair; +ASSERT b59 = (5, 9); +ASSERT b59 IS_IN y; +b510 : IntPair; +ASSERT b510 = (5, 10); +ASSERT b510 IS_IN y; +b61 : IntPair; +ASSERT b61 = (6, 1); +ASSERT b61 IS_IN y; +b62 : IntPair; +ASSERT b62 = (6, 2); +ASSERT b62 IS_IN y; +b63 : IntPair; +ASSERT b63 = (6, 3); +ASSERT b63 IS_IN y; +b64 : IntPair; +ASSERT b64 = (6, 4); +ASSERT b64 IS_IN y; +b65 : IntPair; +ASSERT b65 = (6, 5); +ASSERT b65 IS_IN y; +b66 : IntPair; +ASSERT b66 = (6, 6); +ASSERT b66 IS_IN y; +b67 : IntPair; +ASSERT b67 = (6, 7); +ASSERT b67 IS_IN y; +b68 : IntPair; +ASSERT b68 = (6, 8); +ASSERT b68 IS_IN y; +b69 : IntPair; +ASSERT b69 = (6, 9); +ASSERT b69 IS_IN y; +b610 : IntPair; +ASSERT b610 = (6, 10); +ASSERT b610 IS_IN y; +b71 : IntPair; +ASSERT b71 = (7, 1); +ASSERT b71 IS_IN y; +b72 : IntPair; +ASSERT b72 = (7, 2); +ASSERT b72 IS_IN y; +b73 : IntPair; +ASSERT b73 = (7, 3); +ASSERT b73 IS_IN y; +b74 : IntPair; +ASSERT b74 = (7, 4); +ASSERT b74 IS_IN y; +b75 : IntPair; +ASSERT b75 = (7, 5); +ASSERT b75 IS_IN y; +b76 : IntPair; +ASSERT b76 = (7, 6); +ASSERT b76 IS_IN y; +b77 : IntPair; +ASSERT b77 = (7, 7); +ASSERT b77 IS_IN y; +b78 : IntPair; +ASSERT b78 = (7, 8); +ASSERT b78 IS_IN y; +b79 : IntPair; +ASSERT b79 = (7, 9); +ASSERT b79 IS_IN y; +b710 : IntPair; +ASSERT b710 = (7, 10); +ASSERT b710 IS_IN y; +b81 : IntPair; +ASSERT b81 = (8, 1); +ASSERT b81 IS_IN y; +b82 : IntPair; +ASSERT b82 = (8, 2); +ASSERT b82 IS_IN y; +b83 : IntPair; +ASSERT b83 = (8, 3); +ASSERT b83 IS_IN y; +b84 : IntPair; +ASSERT b84 = (8, 4); +ASSERT b84 IS_IN y; +b85 : IntPair; +ASSERT b85 = (8, 5); +ASSERT b85 IS_IN y; +b86 : IntPair; +ASSERT b86 = (8, 6); +ASSERT b86 IS_IN y; +b87 : IntPair; +ASSERT b87 = (8, 7); +ASSERT b87 IS_IN y; +b88 : IntPair; +ASSERT b88 = (8, 8); +ASSERT b88 IS_IN y; +b89 : IntPair; +ASSERT b89 = (8, 9); +ASSERT b89 IS_IN y; +b810 : IntPair; +ASSERT b810 = (8, 10); +ASSERT b810 IS_IN y; +b91 : IntPair; +ASSERT b91 = (9, 1); +ASSERT b91 IS_IN y; +b92 : IntPair; +ASSERT b92 = (9, 2); +ASSERT b92 IS_IN y; +b93 : IntPair; +ASSERT b93 = (9, 3); +ASSERT b93 IS_IN y; +b94 : IntPair; +ASSERT b94 = (9, 4); +ASSERT b94 IS_IN y; +b95 : IntPair; +ASSERT b95 = (9, 5); +ASSERT b95 IS_IN y; +b96 : IntPair; +ASSERT b96 = (9, 6); +ASSERT b96 IS_IN y; +b97 : IntPair; +ASSERT b97 = (9, 7); +ASSERT b97 IS_IN y; +b98 : IntPair; +ASSERT b98 = (9, 8); +ASSERT b98 IS_IN y; +b99 : IntPair; +ASSERT b99 = (9, 9); +ASSERT b99 IS_IN y; +b910 : IntPair; +ASSERT b910 = (9, 10); +ASSERT b910 IS_IN y; +b101 : IntPair; +ASSERT b101 = (10, 1); +ASSERT b101 IS_IN y; +b102 : IntPair; +ASSERT b102 = (10, 2); +ASSERT b102 IS_IN y; +b103 : IntPair; +ASSERT b103 = (10, 3); +ASSERT b103 IS_IN y; +b104 : IntPair; +ASSERT b104 = (10, 4); +ASSERT b104 IS_IN y; +b105 : IntPair; +ASSERT b105 = (10, 5); +ASSERT b105 IS_IN y; +b106 : IntPair; +ASSERT b106 = (10, 6); +ASSERT b106 IS_IN y; +b107 : IntPair; +ASSERT b107 = (10, 7); +ASSERT b107 IS_IN y; +b108 : IntPair; +ASSERT b108 = (10, 8); +ASSERT b108 IS_IN y; +b109 : IntPair; +ASSERT b109 = (10, 9); +ASSERT b109 IS_IN y; +b1010 : IntPair; +ASSERT b1010 = (10, 10); +ASSERT b1010 IS_IN y; + +ASSERT (1, 9) IS_IN z; + +a : IntPair; +ASSERT a = (9,1); +ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); +ASSERT NOT (a IS_IN (TRANSPOSE r)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_0.cvc b/test/regress/regress0/sets/rels/rel_product_0.cvc new file mode 100644 index 000000000..09981be0b --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_0.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntTup; +ASSERT v = (1,2,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (v IS_IN (x PRODUCT y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_0_1.cvc b/test/regress/regress0/sets/rels/rel_product_0_1.cvc new file mode 100644 index 000000000..f141c7bd4 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_0_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntTup; +ASSERT v = (1,2,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT v IS_IN (x PRODUCT y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_1.cvc b/test/regress/regress0/sets/rels/rel_product_1.cvc new file mode 100644 index 000000000..1826e5a75 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2,3); +zt : IntPair; +ASSERT zt = (3,2,1); +v : IntTup; +ASSERT v = (1,2,3,3,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (v IS_IN (x PRODUCT y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_1_1.cvc b/test/regress/regress0/sets/rels/rel_product_1_1.cvc new file mode 100644 index 000000000..3e5280c19 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_1_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: SAT +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2,3); +zt : IntPair; +ASSERT zt = (3,2,1); +v : IntTup; +ASSERT v = (1,2,3,3,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT v IS_IN (x PRODUCT y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc new file mode 100644 index 000000000..08ed32411 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +f : INT; +d : IntPair; +ASSERT d = (f,3); +ASSERT d IS_IN y; +e : IntPair; +ASSERT e = (4, f); +ASSERT e IS_IN x; + +a : IntPair; +ASSERT a = (4,3); + +ASSERT r = (x JOIN y); + +ASSERT NOT (a IS_IN r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc new file mode 100644 index 000000000..df2d7f412 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +d : IntPair; +ASSERT d IS_IN y; + +a : IntPair; +ASSERT a IS_IN x; + +e : IntPair; +ASSERT e = (4,3); + +ASSERT r = (x JOIN y); + +ASSERT NOT (e IS_IN r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc new file mode 100644 index 000000000..082604dc2 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +d : IntPair; +ASSERT d = (1,3); +ASSERT (1,3) IS_IN y; + +a : IntPair; +ASSERT a IS_IN x; + +e : IntPair; +ASSERT e = (4,3); + +ASSERT r = (x JOIN y); + +ASSERT NOT (e IS_IN r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc new file mode 100644 index 000000000..b1720b50e --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +f : INT; +d : IntPair; +ASSERT d IS_IN y; + +e : IntPair; +ASSERT e = (4, f); +ASSERT e IS_IN x; + +a : IntPair; +ASSERT a = (4,3); + +ASSERT r = (x JOIN y); + +ASSERT NOT (a IS_IN r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_3.cvc b/test/regress/regress0/sets/rels/rel_tc_3.cvc new file mode 100644 index 000000000..79ba32448 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_3.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +a: INT; +b:INT; +c:INT; +d:INT; +ASSERT (1, a) IS_IN x; +ASSERT (1, c) IS_IN x; +ASSERT (1, d) IS_IN x; +ASSERT (b, 1) IS_IN x; +ASSERT (b = d); +ASSERT (2,3) IS_IN ((x JOIN x) JOIN x); +ASSERT NOT (2, 3) IS_IN (TRANSCLOSURE x); +ASSERT y = (TRANSCLOSURE x); +ASSERT NOT ((1, 1) IS_IN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_2.cvc b/test/regress/regress0/sets/rels/rel_tp_2.cvc new file mode 100644 index 000000000..441e79c45 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_2.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +ASSERT (z = TRANSPOSE(y) OR z = TRANSPOSE(x)); +ASSERT NOT (TRANSPOSE(z) = y); +ASSERT NOT (TRANSPOSE(z) = x); +CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel_tp_join_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc new file mode 100644 index 000000000..a03f0e3fd --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc @@ -0,0 +1,32 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (5,1); + +b : IntPair; +ASSERT b = (7, 5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT b IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc new file mode 100644 index 000000000..60b6edf58 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc @@ -0,0 +1,32 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +b : IntPair; +ASSERT b = (1,7); +c : IntPair; +ASSERT c = (2,3); +ASSERT b IS_IN x; +ASSERT c IS_IN x; + +d : IntPair; +ASSERT d = (7,3); +e : IntPair; +ASSERT e = (4,7); + +ASSERT d IS_IN y; +ASSERT e IS_IN y; + +ASSERT (3, 4) IS_IN z; + +a : IntPair; +ASSERT a = (4,1); + +ASSERT r = ((x JOIN y) JOIN z); + +ASSERT NOT (a IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_2.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc new file mode 100644 index 000000000..cc851f622 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; + +a : IntPair; +ASSERT a = (4,1); +ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); +ASSERT NOT (a IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc new file mode 100644 index 000000000..04856d825 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; + +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; +a : IntPair; +ASSERT a = (4,1); + +ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); +ASSERT a IS_IN (TRANSPOSE r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_3.cvc b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc new file mode 100644 index 000000000..25277f43a --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +% crash on this +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +w : SET OF IntPair; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; +ASSERT (3, 3) IS_IN w; + +a : IntPair; +ASSERT a = (4,1); +%ASSERT r = (((TRANSPOSE x) JOIN y) JOIN (w JOIN z)); +ASSERT NOT (a IS_IN (TRANSPOSE r)); + +zz : SET OF IntPair; +ASSERT zz = ((TRANSPOSE x) JOIN y); +ASSERT NOT ((1,3) IS_IN w); +ASSERT NOT ((1,3) IS_IN (w | zz) ); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc new file mode 100644 index 000000000..54e16dd51 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + + +ASSERT x = {(1,7), (2,3)}; + +d : IntPair; +ASSERT d = (7,3); +e : IntPair; +ASSERT e = (4,7); + +ASSERT d IS_IN y; +ASSERT e IS_IN y; + +ASSERT (3, 4) IS_IN z; + +a : IntPair; +ASSERT a = (4,1); + +ASSERT r = ((x JOIN y) JOIN z); + +ASSERT NOT (a IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_int.cvc b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc new file mode 100644 index 000000000..8d149a48d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc @@ -0,0 +1,26 @@ +% EXPECT: unsat +% crash on this +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +w : SET OF IntPair; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +t : INT; +u : INT; + +ASSERT 4 < t AND t < 6; +ASSERT 4 < u AND u < 6; + +ASSERT (1, u) IS_IN x; +ASSERT (t, 3) IS_IN y; + +a : IntPair; +ASSERT a = (1,3); + +ASSERT NOT (a IS_IN (x JOIN y)); + + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc new file mode 100644 index 000000000..b05026bc9 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc @@ -0,0 +1,21 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntTup; + +ASSERT (2, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (2, 2) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; + +v : IntTup; +ASSERT v = (4,3,2,1); + +ASSERT r = (((TRANSPOSE x) JOIN y) PRODUCT z); +ASSERT NOT (v IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc new file mode 100644 index 000000000..aacf6c054 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +w : SET OF IntPair; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +t : INT; +u : INT; + +ASSERT 4 < t AND t < 6; +ASSERT 4 < u AND u < 6; + +ASSERT (1, t) IS_IN x; +ASSERT (u, 3) IS_IN y; + +a : IntPair; +ASSERT a = (1,3); + +ASSERT NOT (a IS_IN (x JOIN y)); + +st : SET OF INT; +su : SET OF INT; +ASSERT t IS_IN st; +ASSERT u IS_IN su; +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_0.cvc b/test/regress/regress0/sets/rels/rel_transpose_0.cvc new file mode 100644 index 000000000..6da02ea2d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_0.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); + +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE x)); + +ASSERT z IS_IN y; +ASSERT NOT (zt IS_IN (TRANSPOSE y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1.cvc new file mode 100644 index 000000000..bdcf31bb8 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_1.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1,2,3); +zt : IntTup; +ASSERT zt = (3,2,1); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE x)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc new file mode 100644 index 000000000..11653de04 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1,2,3); +zt : IntTup; +ASSERT zt = (3,2,1); +ASSERT z IS_IN x; +ASSERT zt IS_IN (TRANSPOSE x); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_3.cvc b/test/regress/regress0/sets/rels/rel_transpose_3.cvc new file mode 100644 index 000000000..225f3491c --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_3.cvc @@ -0,0 +1,14 @@ +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +ASSERT (x = y); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_4.cvc b/test/regress/regress0/sets/rels/rel_transpose_4.cvc new file mode 100644 index 000000000..b260147c8 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_4.cvc @@ -0,0 +1,13 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); + +ASSERT z IS_IN x; +ASSERT NOT ((2, 1) IS_IN (TRANSPOSE x)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_5.cvc b/test/regress/regress0/sets/rels/rel_transpose_5.cvc new file mode 100644 index 000000000..203e8b3d2 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_5.cvc @@ -0,0 +1,22 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +ASSERT zt IS_IN y; + +w : IntPair; +ASSERT w = (2, 2); +ASSERT w IS_IN y; +ASSERT z IS_IN x; + +ASSERT NOT (zt IS_IN (TRANSPOSE (x JOIN y))); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_6.cvc b/test/regress/regress0/sets/rels/rel_transpose_6.cvc new file mode 100644 index 000000000..a2e8bcf10 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_6.cvc @@ -0,0 +1,24 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); + +ASSERT z IS_IN x; +ASSERT (3, 4) IS_IN x; +ASSERT (3, 5) IS_IN x; +ASSERT (3, 3) IS_IN x; + +ASSERT x = TRANSPOSE(y); + +ASSERT NOT (zt IS_IN y); + +ASSERT z IS_IN y; +ASSERT NOT (zt IS_IN (TRANSPOSE y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_7.cvc b/test/regress/regress0/sets/rels/rel_transpose_7.cvc new file mode 100644 index 000000000..bcc3babc8 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_7.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +ASSERT x = y; +ASSERT NOT (TRANSPOSE(x) = TRANSPOSE(y)); + +CHECKSAT; |