diff options
| author | Tim King <taking@google.com> | 2016-10-13 00:22:24 -0700 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-10-13 00:22:24 -0700 |
| commit | b468bb361f8b98bcb6b9d0febab4f285a6a872b3 (patch) | |
| tree | def542bce3971de0a6d646a620b79e871ae7a690 | |
| parent | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (diff) | |
Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to 5f415d4585134612bc24e9a823289fee35541a01.
175 files changed, 45 insertions, 5851 deletions
diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 44d6fcbbf..000000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,4 +0,0 @@ -// 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 5947ad3f0..75d9f3c5a 100644 --- a/proofs/signatures/Makefile.am +++ b/proofs/signatures/Makefile.am @@ -3,7 +3,6 @@ # 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 e89cd3974..f5e3776e5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -267,9 +267,6 @@ 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 12cab48cc..001f38a79 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -859,7 +859,6 @@ 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/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index e6d7f9d86..4c0516eb6 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -109,8 +109,6 @@ tokens { SUBTYPE_TOK = 'SUBTYPE'; SET_TOK = 'SET'; - - TUPLE_TOK = 'TUPLE'; FORALL_TOK = 'FORALL'; EXISTS_TOK = 'EXISTS'; @@ -203,12 +201,6 @@ tokens { BVSGT_TOK = 'BVSGT'; BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; - - // Relations - JOIN_TOK = 'JOIN'; - TRANSPOSE_TOK = 'TRANSPOSE'; - PRODUCT_TOK = 'PRODUCT'; - TRANSCLOSURE_TOK = 'TCLOSURE'; // Strings @@ -315,14 +307,9 @@ 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: - case JOIN_TOK: - case TRANSPOSE_TOK: - case PRODUCT_TOK: - case TRANSCLOSURE_TOK: return 24; + case MINUS_TOK: return 24; case LEQ_TOK: case LT_TOK: case GEQ_TOK: @@ -359,9 +346,6 @@ 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; @@ -1238,8 +1222,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 @@ -1488,8 +1472,6 @@ booleanBinop[unsigned& op] | OR_TOK | XOR_TOK | AND_TOK - | JOIN_TOK - | PRODUCT_TOK ; comparison[CVC4::Expr& f] @@ -1669,20 +1651,6 @@ 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] ; @@ -2001,8 +1969,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 @@ -2019,15 +1987,14 @@ 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 30573cdff..8db344f92 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -234,10 +234,6 @@ 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 84c8eecf5..d09290db5 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -768,22 +768,6 @@ 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 c9dc814f2..7b7d569b7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -512,10 +512,6 @@ 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 @@ -801,10 +797,6 @@ 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 8c6af5c34..cbe54ff4b 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -835,7 +835,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 a682a893b..d898b66a2 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/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index a00d6d8a1..a00d6d8a1 100755..100644 --- 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 100755..100644 --- 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 2ccc17e55..2ccc17e55 100755..100644 --- 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 0adaef638..0adaef638 100755..100644 --- 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 9ccba38cd..9ccba38cd 100755..100644 --- 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 48205db9d..48205db9d 100755..100644 --- 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 54853ceaf..54853ceaf 100755..100644 --- 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 c3fb05641..c3fb05641 100755..100644 --- 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 8e8f34cac..8e8f34cac 100755..100644 --- 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 100755..100644 --- 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 54415d974..54415d974 100755..100644 --- 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 100755..100644 --- 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 e0bbbf8ac..e0bbbf8ac 100755..100644 --- 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 449ab7189..449ab7189 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 61a20ad42..61a20ad42 100755..100644 --- 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 94d02de9b..94d02de9b 100755..100644 --- 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 11adc61fd..11adc61fd 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 72057e734..72057e734 100755..100644 --- 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 7d21b4185..7d21b4185 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 12e15d353..12e15d353 100755..100644 --- 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 68446922f..68446922f 100755..100644 --- 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 2a940f1fd..2a940f1fd 100755..100644 --- 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 c238e3c4e..c238e3c4e 100755..100644 --- 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 1f68fb787..1f68fb787 100755..100644 --- 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 100755..100644 --- 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 ac6e1edbe..ac6e1edbe 100755..100644 --- 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 c9f62243f..c9f62243f 100755..100644 --- 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 c4bf61b28..c4bf61b28 100755..100644 --- 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 100755..100644 --- 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 afeed1e5d..afeed1e5d 100755..100644 --- 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 79963cb45..79963cb45 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 04a6bc9c8..04a6bc9c8 100755..100644 --- 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 976b81e60..976b81e60 100755..100644 --- 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 60af7ad0a..60af7ad0a 100755..100644 --- 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 b30c2addb..b30c2addb 100755..100644 --- 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 9b89e5ef6..9b89e5ef6 100755..100644 --- 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 9c09371c4..9c09371c4 100755..100644 --- 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 e89be8d2b..e89be8d2b 100755..100644 --- 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 1e484311c..1e484311c 100755..100644 --- 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 dc8a9acb2..dc8a9acb2 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 df8533135..df8533135 100755..100644 --- 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 3e3b08814..3e3b08814 100755..100644 --- 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 f4284a8ab..f4284a8ab 100755..100644 --- 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 3ff21aa6e..3ff21aa6e 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 de8875ae3..de8875ae3 100755..100644 --- 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 90a22f4b7..90a22f4b7 100755..100644 --- 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 100755..100644 --- 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 aae8f6c5b..aae8f6c5b 100755..100644 --- 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 ec1b41a98..ec1b41a98 100755..100644 --- 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 ef3337e53..ef3337e53 100755..100644 --- 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 100755..100644 --- 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 100755..100644 --- 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 2c6bfb7d3..2c6bfb7d3 100755..100644 --- 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 d4fdaa5e5..d4fdaa5e5 100755..100644 --- 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 e97a76ce6..e97a76ce6 100755..100644 --- 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 ba5a75d86..ba5a75d86 100755..100644 --- 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 100755..100644 --- 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 3017238ca..3017238ca 100755..100644 --- 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 631627331..631627331 100755..100644 --- 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 c92eab4bd..14c87a947 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -44,11 +44,6 @@ 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 @@ -59,12 +54,6 @@ 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 @@ -72,9 +61,4 @@ 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 deleted file mode 100644 index df14bf53b..000000000 --- a/src/theory/sets/rels_utils.h +++ /dev/null @@ -1,96 +0,0 @@ -/********************* */ -/*! \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.getKind() == kind::APPLY_CONSTRUCTOR ) { - 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 diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 840135937..bbeaf4a4c 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -33,7 +33,6 @@ 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 e996cb215..6fb90fea3 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -97,12 +97,8 @@ 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; @@ -127,16 +123,19 @@ 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; @@ -708,11 +707,6 @@ 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()); @@ -733,7 +727,6 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, << std::endl; Assert(S.getType().isSet()); - std::set<Node> temp_nodes; const Elements emptySetOfElements; const Elements& saved = @@ -777,74 +770,6 @@ 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(); } @@ -1079,20 +1004,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) @@ -1371,7 +1296,6 @@ 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(), @@ -1391,7 +1315,6 @@ 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); @@ -1412,7 +1335,6 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, TheorySetsPrivate::~TheorySetsPrivate() { delete d_termInfoManager; - delete d_rels; if( Debug.isOn("sets-scrutinize") ) { Assert(d_scrutinize != NULL); delete d_scrutinize; @@ -1651,23 +1573,21 @@ 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; - d_theory.d_rels->eqNotifyNewClass(t); - } + +// void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t) +// { +// Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl; +// } // 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; - d_theory.d_rels->eqNotifyPostMerge(t1, t2); - } + +// void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2) +// { +// Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; +// } // 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 3ed608b90..049e95786 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -25,8 +25,6 @@ #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 { @@ -98,14 +96,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; @@ -246,8 +244,7 @@ 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 deleted file mode 100644 index d8230d31b..000000000 --- a/src/theory/sets/theory_sets_rels.cpp +++ /dev/null @@ -1,1950 +0,0 @@ -/********************* */ -/*! \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< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_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; - - 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; - - 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] ); - } - } - - MEM_IT tp_it = d_arg_rep_tp_terms.find( rel_rep ); - - if( tp_it != d_arg_rep_tp_terms.end() ) { - std::vector< Node >::iterator tp_ts_it = tp_it->second.begin(); - - while( tp_ts_it != tp_it->second.end() ) { - applyTransposeRule( exp, *tp_ts_it, (*tp_ts_it)[0] == rel_rep?Node::null():explain(EQUAL((*tp_ts_it)[0], rel_rep)), true ); - ++tp_ts_it; - } - ++tp_it; - } - } - m_it++; - } - - TERM_IT t_it = d_terms_cache.begin(); - while( t_it != d_terms_cache.end() ) { - if(d_membership_constraints_cache.find(t_it->first) == d_membership_constraints_cache.end()) { - Trace("rels-debug") << "[sets-rels-ee] A term that does not have membership constraints: " << t_it->first << std::endl; - KIND_TERM_IT k_t_it = t_it->second.begin(); - - while(k_t_it != t_it->second.end()) { - if(k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT) { - std::vector<Node>::iterator term_it = k_t_it->second.begin(); - while(term_it != k_t_it->second.end()) { - computeMembersForRel(*term_it); - term_it++; - } - } else if ( k_t_it->first == kind::TRANSPOSE ) { - std::vector<Node>::iterator term_it = k_t_it->second.begin(); - while(term_it != k_t_it->second.end()) { - computeMembersForTpRel(*term_it); - term_it++; - } - } - k_t_it++; - } - } - t_it++; - } - - finalizeTCInference(); - } - - /* - * Populate relational terms data structure - */ - - void TheorySetsRels::collectRelsInfo() { - Trace("rels") << "[sets-rels] Start collecting relational terms..." << std::endl; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc_rep = (*eqcs_i); - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine ); - - Trace("rels-ee") << "[sets-rels-ee] term representative: " << eqc_rep << std::endl; - - while( !eqc_i.isFinished() ){ - Node eqc_node = (*eqc_i); - - Trace("rels-ee") << " term : " << eqc_node << std::endl; - - if(getRepresentative(eqc_rep) == getRepresentative(d_trueNode) || - getRepresentative(eqc_rep) == getRepresentative(d_falseNode)) { - // collect membership info - if(eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple()) { - Node tup_rep = getRepresentative(eqc_node[0]); - Node rel_rep = getRepresentative(eqc_node[1]); - - if(eqc_node[0].isVar()){ - reduceTupleVar(eqc_node); - } - if( safelyAddToMap(d_membership_constraints_cache, rel_rep, tup_rep) ) { - bool is_true_eq = areEqual(eqc_rep, d_trueNode); - Node reason = is_true_eq ? eqc_node : eqc_node.negate(); - addToMap(d_membership_exp_cache, rel_rep, reason); - if( is_true_eq ) { - // add tup_rep to membership database - // and store mapping between tuple and tuple's elements representatives - addToMembershipDB(rel_rep, tup_rep, reason); - } - } - } - // collect relational terms info - } else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) { - if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN || - eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ) { - std::vector<Node> terms; - std::map<kind::Kind_t, std::vector<Node> > rel_terms; - TERM_IT terms_it = d_terms_cache.find(eqc_rep); - - if( eqc_node.getKind() == kind::TRANSPOSE ) { - Node eqc_node0_rep = getRepresentative( eqc_node[0] ); - MEM_IT mem_it = d_arg_rep_tp_terms.find( eqc_node0_rep ); - - if( mem_it != d_arg_rep_tp_terms.end() ) { - mem_it->second.push_back( eqc_node ); - } else { - std::vector< Node > tp_terms; - tp_terms.push_back( eqc_node ); - d_arg_rep_tp_terms[eqc_node0_rep] = tp_terms; - } - } - - if( terms_it == d_terms_cache.end() ) { - terms.push_back(eqc_node); - rel_terms[eqc_node.getKind()] = terms; - d_terms_cache[eqc_rep] = rel_terms; - } else { - KIND_TERM_IT kind_term_it = terms_it->second.find(eqc_node.getKind()); - - if( kind_term_it == terms_it->second.end() ) { - terms.push_back(eqc_node); - d_terms_cache[eqc_rep][eqc_node.getKind()] = terms; - } else { - kind_term_it->second.push_back(eqc_node); - } - } - } - // need to add all tuple elements as shared terms - } else if(eqc_node.getType().isTuple() && !eqc_node.isConst() && !eqc_node.isVar()) { - for(unsigned int i = 0; i < eqc_node.getType().getTupleLength(); i++) { - Node element = RelsUtils::nthElementOfTuple(eqc_node, i); - if(!element.isConst()) { - makeSharedTerm(element); - } - } - } - ++eqc_i; - } - ++eqcs_i; - } - Trace("rels-debug") << "[sets-rels] Done with collecting relational terms!" << std::endl; - } - - /* - * Construct transitive closure graph for tc_rep based on the members of tc_r_rep - */ - - std::map< Node, std::hash_set< Node, NodeHashFunction > > TheorySetsRels::constructTCGraph(Node tc_r_rep, Node tc_rep, Node tc_term) { - Trace("rels-tc") << "[sets-rels] Construct TC graph for transitive closure relation " << tc_rep << std::endl; - - std::map< Node, std::hash_set< Node, NodeHashFunction > > tc_graph; - std::map< Node, std::hash_set< Node, NodeHashFunction > > tc_r_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); - TC_PAIR_IT r_pair_set_it = tc_r_graph.find(fst_rep); - - Trace("rels-tc") << "[sets-rels] **** Member of r = (" << fst_rep << ", " << snd_rep << ")" << std::endl; - - if( pair_set_it != tc_graph.end() ) { - pair_set_it->second.insert(snd_rep); - r_pair_set_it->second.insert(snd_rep); - } else { - std::hash_set< Node, NodeHashFunction > snd_set; - snd_set.insert(snd_rep); - tc_r_graph[fst_rep] = snd_set; - 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_tc_r_graph[tc_rep] = tc_r_graph; - - TC_PAIR_IT tc_mem_it = d_tc_membership_db.find(tc_term); - - if( tc_mem_it != d_tc_membership_db.end() ) { - for(std::hash_set<Node, NodeHashFunction>::iterator pair_it = tc_mem_it->second.begin(); - pair_it != tc_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); - Trace("rels-tc") << "[sets-rels] **** Member of TC(r) = (" << fst_rep << ", " << snd_rep << ")" << std::endl; - - 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; - } - } - } - - return tc_graph; - } - - /* - * - * - * 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::applyTCRule(Node exp, Node tc_term) { - Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSITIVE CLOSURE rule on " - << tc_term << " with explanation " << exp << std::endl; - - Node tc_rep = getRepresentative(tc_term); - bool polarity = exp.getKind() != kind::NOT; - - if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) { - d_tc_rep_term[tc_rep] = tc_term; - d_rel_nodes.insert(tc_rep); - } - if(polarity) { - TC_PAIR_IT mem_it = d_tc_membership_db.find(tc_term); - - if( mem_it == d_tc_membership_db.end() ) { - std::hash_set<Node, NodeHashFunction> members; - members.insert(exp[0]); - d_tc_membership_db[tc_term] = members; - } else { - mem_it->second.insert(exp[0]); - } - } else { - Trace("rels-tc") << "TC non-member = " << exp << std::endl; - } - //todo: need to construct a tc_graph if transitive closure is used in the context -// // 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()) { - computeMembersForRel(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()) { - Trace("rels-debug") << "\n[sets-rels] Apply JOIN-COMPOSE rule on term: " << join_term - << " with explanation: " << exp << std::endl; - - computeMembersForRel(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])))); - } - Trace("rels-debug") << "\n[sets-rels] After applying JOIN-split rule, generate a fact : " << fact - << " with explanation: " << reasons << std::endl; - 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])))); - } - Trace("rels-debug") << "[sets-rels] After applying JOIN-split rule, generate a fact : " << fact - << " with explanation: " << reasons << std::endl; - sendInfer(fact, reasons, "join-split"); - makeSharedTerm(shared_x); - } - } - - /* - * 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 - * - * Not implemented yet! - * transpose-equal rule: [NOT] (TRANSPOSE X) = (TRANSPOSE Y) - * ----------------------------------------------- - * [NOT] (X = Y) - */ - void TheorySetsRels::applyTransposeRule(Node exp, Node tp_term, Node more_reason, bool tp_occur) { - Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSPOSE rule on term " << tp_term << 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, more_reason == Node::null()?exp:AND(exp, more_reason), "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) { - fact = fact.negate(); - } - sendInfer(fact, reason, "transpose-rule"); - } - - - void TheorySetsRels::finalizeTCInference() { - Trace("rels-tc") << "[sets-rels] ****** Finalizing transitive closure inferences!" << std::endl; - std::map<Node, Node>::iterator map_it = d_tc_rep_term.begin(); - - while( map_it != d_tc_rep_term.end() ) { - Trace("rels-tc") << "[sets-rels] Start building the TC graph for " << map_it->first << std::endl; - - std::map< Node, std::hash_set<Node, NodeHashFunction> > d_tc_graph = constructTCGraph(getRepresentative(map_it->second[0]), map_it->first, map_it->second); - inferTC(map_it->first, d_tc_graph); - map_it++; - } - } - - void TheorySetsRels::inferTC(Node tc_rep, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph) { - Trace("rels-tc") << "[sets-rels] Infer TC lemma from tc_graph of " << tc_rep << std::endl; - - for(TC_PAIR_IT 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 ); - } - } - } - - 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); - MEM_IT 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()) { - Trace("rels-tc") << "[sets-rels] Infered a TC lemma = " << MEMBER(pair, tc_rep) << " by Transitivity" - << " with explanation = " << Rewriter::rewrite(exp) << std::endl; - sendLemma( MEMBER(pair, tc_rep), Rewriter::rewrite(exp), "Transitivity" ); - } - } else { - Trace("rels-tc") << "[sets-rels] Infered a TC lemma = " << MEMBER(pair, tc_rep) << " by Transitivity" - << " with explanation = " << Rewriter::rewrite(exp) << std::endl; - 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; - TC_PAIR_IT 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 ); - } - } - } - - // Bottom-up fashion to compute relations - void TheorySetsRels::computeMembersForRel(Node n) { - Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation " << n << std::endl; - switch(n[0].getKind()) { - case kind::TRANSPOSE: - computeMembersForTpRel(n[0]); - break; - case kind::JOIN: - case kind::PRODUCT: - computeMembersForRel(n[0]); - break; - default: - break; - } - - switch(n[1].getKind()) { - case kind::TRANSPOSE: - computeMembersForTpRel(n[1]); - break; - case kind::JOIN: - case kind::PRODUCT: - computeMembersForRel(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; - composeTupleMemForRel(n); - } - - void TheorySetsRels::computeMembersForTpRel(Node n) { - switch(n[0].getKind()) { - case kind::TRANSPOSE: - computeMembersForTpRel(n[0]); - break; - case kind::JOIN: - case kind::PRODUCT: - computeMembersForRel(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::composeTupleMemForRel( 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; - 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) ){ - if ( (!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 an already held lemma: " - << d_lemma_cache[i]<< std::endl; - continue; - } - Trace("rels-lemma") << "[sets-rels-lemma] Send out a lemma : " - << d_lemma_cache[i] << std::endl; - d_sets_theory.d_out->lemma( d_lemma_cache[i] ); - } - 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 an already held fact,: " - << child_it->first << std::endl; - continue; - } - Trace("rels-lemma") << "[sets-rels-fact-lemma] Send out a 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)); - } - } - doTCLemmas(); - } - - d_arg_rep_tp_terms.clear(); - d_tc_membership_db.clear(); - d_rel_nodes.clear(); - d_pending_facts.clear(); - d_membership_constraints_cache.clear(); - d_tc_r_graph.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(); - d_tc_rep_term.clear(); - } - - void TheorySetsRels::doTCLemmas() { - Trace("rels-debug") << "[sets-rels] Start processing TC lemmas .......... " << std::endl; - std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator mem_it = d_tc_membership_db.begin(); - - while(mem_it != d_tc_membership_db.end()) { - Node tc_rep = getRepresentative(mem_it->first); - Node tc_r_rep = getRepresentative(mem_it->first[0]); - std::hash_set< Node, NodeHashFunction >::iterator set_it = mem_it->second.begin(); - - while(set_it != mem_it->second.end()) { - std::hash_set<Node, NodeHashFunction> hasSeen; - bool isReachable = false; - Node fst = RelsUtils::nthElementOfTuple(*set_it, 0); - Node snd = RelsUtils::nthElementOfTuple(*set_it, 1); - Node fst_rep = getRepresentative(fst); - Node snd_rep = getRepresentative(snd); - TC_IT tc_graph_it = d_tc_r_graph.find(tc_rep); - - // the tc_graph of TC(r) is built based on the members of r and TC(r)???????? - isTCReachable(fst_rep, snd_rep, hasSeen, tc_graph_it->second, isReachable); - Trace("rels-tc") << "tuple = " << *set_it << " with rep = (" << fst_rep << ", " << snd_rep << ") " - << " isReachable? = " << isReachable << std::endl; - if((tc_graph_it != d_tc_r_graph.end() && !isReachable) || - (tc_graph_it == d_tc_r_graph.end())) { - Node reason = explain(MEMBER(*set_it, mem_it->first)); - Node sk_1 = NodeManager::currentNM()->mkSkolem("sde", fst_rep.getType()); - Node sk_2 = NodeManager::currentNM()->mkSkolem("sde", snd_rep.getType()); - Node mem_of_r = MEMBER(RelsUtils::constructPair(tc_r_rep, fst_rep, snd_rep), tc_r_rep); - Node sk_eq = EQUAL(sk_1, sk_2); - - if(fst_rep != fst) { - reason = AND(reason, explain(EQUAL(fst_rep, fst))); - } - if(snd_rep != snd) { - reason = AND(reason, explain(EQUAL(snd_rep, snd))); - } - if(tc_r_rep != mem_it->first[0]) { - reason = AND(reason, explain(EQUAL(tc_r_rep, mem_it->first[0]))); - } - if(tc_rep != mem_it->first) { - reason = AND(reason, explain(EQUAL(tc_rep, mem_it->first))); - } - - Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, - OR(mem_of_r, - (AND(MEMBER(RelsUtils::constructPair(tc_r_rep, fst_rep, sk_1), tc_r_rep), - (AND(MEMBER(RelsUtils::constructPair(tc_r_rep, sk_2, snd_rep), tc_r_rep), - (OR(sk_eq, MEMBER(RelsUtils::constructPair(tc_rep, sk_1, sk_2), tc_rep))))))))); - Trace("rels-lemma") << "[sets-rels-lemma] Send out a TC lemma : " - << tc_lemma << std::endl; - d_sets_theory.d_out->lemma(tc_lemma); - d_sets_theory.d_out->requirePhase(Rewriter::rewrite(mem_of_r), true); - d_sets_theory.d_out->requirePhase(Rewriter::rewrite(sk_eq), true); - } - set_it++; - } - mem_it++; - } - } - - void TheorySetsRels::isTCReachable(Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable) { - if(hasSeen.find(start) == hasSeen.end()) { - hasSeen.insert(start); - } - - TC_PAIR_IT pair_set_it = tc_graph.find(start); - - if(pair_set_it != tc_graph.end()) { - if(pair_set_it->second.find(dest) != pair_set_it->second.end()) { - isReachable = true; - return; - } 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(hasSeen.find(*set_it) == hasSeen.end()) { - isTCReachable(*set_it, dest, hasSeen, tc_graph, isReachable); - } - set_it++; - } - } - } - } - - void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { - 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 ) { - d_pending_facts[fact] = exp; - d_infer.push_back( fact ); - d_infer_exp.push_back( exp ); - } - - 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; - } - - /* - * Make sure duplicate members are not added in map - */ - bool TheorySetsRels::safelyAddToMap(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) { - 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))); - } - } - 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); - } - - 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; - } - - /* - * For each tuple n, we store a mapping between n and a list of its elements representatives - * in d_tuple_reps. This would later be used for applying JOIN operator. - */ - 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); - } - - /* - * Node n[0] is a tuple variable, reduce n[0] to a concrete representation, - * which is (e1, ..., en) where e1, ... ,en are concrete elements of tuple n[0]. - */ - 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 " << " node = " << n << 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_vec_size(c), - d_eqEngine(eq), - d_conflict(conflict), - 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_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_mem_exp(c), d_in(c), d_out(c), - d_tp(c), d_pt(c), d_join(c), d_tc(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 an 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() ) { - if( d_eqEngine->hasTerm(e_rep) ) { - // it is possible that e's rep changes at this moment, thus we need to know the previous rep id of eqc of e - eq::EqClassIterator rep_eqc_i = eq::EqClassIterator( e_rep, d_eqEngine ); - 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; - - 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(membership[1], 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 ); - - std::hash_set<int> in_reachable; - std::hash_set<int> out_reachable; - collectReachableNodes(tc_ei->d_id_inIds, fst_rep_id, in_reachable); - collectReachableNodes(tc_ei->d_id_outIds, 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( addId(tc_ei->d_id_inIds, snd_rep_id, 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; - } - Trace("rels-std") << "Add out membership arrow for " << fst_rep << " to : " << snd_rep << std::endl; - addId(tc_ei->d_id_inIds, fst_rep_id, snd_rep_id); - 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) { - Trace("rels-tc") << "explainTCMem ############ pair = " << pair << std::endl; - 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; - } - if(!ei->d_tc.get().isNull()) { - Node rel_rep = getRepresentative(ei->d_tc.get()[0]); - EqcInfo* rel_ei = getOrMakeEqcInfo(rel_rep); - if(rel_ei != NULL) { - NodeMap::iterator rel_mem_exp_it = rel_ei->d_mem_exp.begin(); - while(rel_mem_exp_it != rel_ei->d_mem_exp.end()) { - Node exp = rel_rep == ei->d_tc.get()[0] ? d_trueNode : explain(EQUAL(rel_rep, ei->d_tc.get()[0])); - Node tuple = (*rel_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(exp, AND(explain(EQUAL(snd, snd_e)), AND(explain(EQUAL(fst, fst_e)), (*rel_mem_exp_it).second))); - } - ++rel_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; - - 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); - 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); - Node tc_exp = explainTCMem(tc_ei, in_pair, in_node, fst_rep); - Node reason = tc_exp.isNull() ? exp : AND(tc_exp, 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++; - } - - 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); - 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++; - } - } - - void TheorySetsRels::collectReachableNodes(std::map< int, std::vector< int > >& id_map, int start_id, std::hash_set< int >& reachable_set, bool firstRound) { - Trace("rels-std") << "**** Collecting reachable nodes for node with id " << start_id << std::endl; - if(reachable_set.find(start_id) != reachable_set.end()) { - return; - } - if(!firstRound) { - reachable_set.insert(start_id); - } - - std::vector< int > id_list = getIdList(id_map, start_id); - std::vector< int >::iterator id_list_it = id_list.begin(); - - while( id_list_it != id_list.end() ) { - collectReachableNodes( id_map, *id_list_it, reachable_set, 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 - 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, 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 && !ei->d_tc.get().isNull() ) { - addTCMemAndSendInfer( ei, t2, Node::null() ); - } - - // 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()) { - NodeMap::const_iterator reason_it = t1_ei->d_mem_exp.find(*t1_mem_it); - Assert(reason_it != t1_ei->d_mem_exp.end()); - addTCMemAndSendInfer(t1_ei, MEMBER(*t1_mem_it, t1_ei->d_tc.get()), (*reason_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); - if(t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull()) { - t1_ei->d_pt.set(t2_ei->d_pt); - 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); - t1_ei->d_mem_exp.insert(*itr, t2_ei->d_mem_exp[*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); - } - } - } - } - - 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 ) { - Trace("rels-std") << "[sets-rels] 0 Merge TRANSPOSE eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; - // 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 ); - if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { - t1_ei->d_tp.set( t2_ei->d_tp ); - 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 ); - t1_ei->d_mem_exp.insert( *itr, t2_ei->d_mem_exp[*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 ); - } - } - } - } - - 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++; - } - } - - bool TheorySetsRels::addId( std::map< int, std::vector< int > >& id_map, int key, int id ) { - int n_data = d_vec_size[key]; - int len = n_data < id_map[key].size() ? n_data : id_map[key].size(); - - for( int i = 0; i < len; i++ ) { - if( id_map[key][i] == id) { - return false; - } - } - if( n_data < id_map[key].size() ) { - id_map[key][n_data] = id; - } else { - id_map[key].push_back( id ); - } - d_vec_size[key] = n_data+1; - return true; - } - - std::vector< int > TheorySetsRels::getIdList( std::map< int, std::vector< int > >& id_map, int key ) { - std::vector< int > id_list; - int n_data = d_vec_size[key]; - int len = n_data < id_map[key].size() ? n_data : id_map[key].size(); - - for( int i = 0; i < len; i++ ) { - id_list.push_back(id_map[key][i]); - } - return id_list; - } - -} -} -} - - - - - - - - - - - - - diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h deleted file mode 100644 index 83f9bf5d4..000000000 --- a/src/theory/sets/theory_sets_rels.h +++ /dev/null @@ -1,261 +0,0 @@ -/********************* */ -/*! \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; - NodeMap d_mem_exp; - NodeListMap d_in; - NodeListMap d_out; - context::CDO< Node > d_tp; - context::CDO< Node > d_pt; - context::CDO< Node > d_join; - context::CDO< Node > d_tc; - /** mapping from an element rep id to a list of rep ids that pointed by */ - /** Context dependent map Int -> IntList */ - std::map< int, std::vector< int > > d_id_inIds; - /** mapping from an element rep id to a list of rep ids that point to */ - /** Context dependent map Int -> IntList */ - std::map< int, std::vector< int > > d_id_outIds; - }; - -private: - /** Context */ - context::CDHashMap< int, int > d_vec_size; - - /** Mapping between integer id and tuple element rep */ - std::map< int, Node > d_id_node; - - /** Mapping between tuple element rep and integer id*/ - std::map< Node, int > d_node_id; - - /** has eqc info */ - bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); } - - bool addId( std::map< int, std::vector< int > >& id_map, int key, int id ); - std::vector< int > getIdList( std::map< int, std::vector< int > >& id_map, int key ); - - void collectReachableNodes(std::map< int, std::vector< int > >& id_map, int start_id, std::hash_set<int>& reachable_set, bool firstRound=true); - - -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; - - /** Relations that have been applied JOIN, PRODUCT, TC composition rules */ - std::hash_set< Node, NodeHashFunction > d_rel_nodes; - std::map< Node, std::vector<Node> > d_tuple_reps; - std::map< Node, TupleTrie > d_membership_trie; - - /** Symbolic tuple variables that has been reduced to concrete ones */ - std::hash_set< Node, NodeHashFunction > d_symbolic_tuples; - - /** Mapping between relation and its (non)members representatives */ - std::map< Node, std::vector<Node> > d_membership_constraints_cache; - - /** Mapping between relation and its (non)members' explanation */ - std::map< Node, std::vector<Node> > d_membership_exp_cache; - - /** Mapping between relation and its member representatives */ - std::map< Node, std::vector<Node> > d_membership_db; - - /** Mapping between relation and its members' explanation */ - std::map< Node, std::vector<Node> > d_membership_exp_db; - - /** Mapping between a relation representative and its equivalent relations involving relational operators */ - std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache; - - /** Mapping between relation and its member representatives */ - std::map< Node, std::vector<Node> > d_arg_rep_tp_terms; - - /** Mapping between TC(r) and one explanation when building TC graph*/ - std::map< Node, Node > d_membership_tc_exp_cache; - - /** Mapping between transitive closure relation TC(r) (is not necessary a representative) and members directly asserted members */ - std::map< Node, std::hash_set<Node, NodeHashFunction> > d_tc_membership_db; - - /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tc_r_graph; - - /** Mapping between transitive closure TC(r)'s representative and TC(r) */ - std::map< Node, Node > d_tc_rep_term; - std::map< Node, EqcInfo* > d_eqc_info; - -public: - void eqNotifyNewClass(Node t); - void eqNotifyPostMerge(Node t1, Node t2); - -private: - - void doPendingMerge(); - Node findTCMemExp(EqcInfo*, Node); - void buildTCAndExp(Node, EqcInfo*); - void mergeTCEqcs(Node t1, Node t2); - void mergeTCEqcExp(EqcInfo*, EqcInfo*); - void mergeProductEqcs(Node t1, Node t2); - int getOrMakeElementRepId(EqcInfo*, Node); - void mergeTransposeEqcs(Node t1, Node t2); - Node explainTCMem(EqcInfo*, Node, Node, Node); - void sendInferProduct(bool, Node, Node, Node); - EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); - void sendInferTranspose(bool, Node, Node, Node, bool reverseOnly = false); - void addTCMemAndSendInfer(EqcInfo* tc_ei, Node mem, Node exp, bool fromRel = false); - 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 check(); - Node explain(Node); - void collectRelsInfo(); - void applyTCRule( Node, Node ); - void applyJoinRule( Node, Node ); - void applyProductRule( Node, Node ); - void composeTupleMemForRel( Node ); - void assertMembership( Node fact, Node reason, bool polarity ); - void applyTransposeRule( Node, Node, Node more_reason = Node::null(), bool tp_occur_rule = false ); - - - - void computeMembersForRel( Node ); - void computeMembersForTpRel( Node ); - void finalizeTCInference(); - 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 >&); - void isTCReachable(Node fst, Node snd, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool&); - std::map< Node, std::hash_set< Node, NodeHashFunction > > constructTCGraph( Node, Node, Node ); - - - void doTCLemmas(); - void addSharedTerm( TNode n ); - void sendInfer( Node fact, Node exp, const char * c ); - void sendLemma( Node fact, Node reason, const char * c ); - void checkTCGraphForConflict( Node, Node, Node, Node, Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >& ); - - // Helper functions - bool holds( Node ); - bool hasTerm( Node a ); - void makeSharedTerm( Node ); - void reduceTupleVar( Node ); - bool hasMember( Node, Node ); - void computeTupleReps( Node ); - bool areEqual( Node a, Node b ); - Node getRepresentative( Node t ); - Node findMemExp(Node r, Node pair); - bool insertIntoIdList(IdList&, int); - bool exists( std::vector<Node>&, Node ); - Node mkAnd( std::vector< TNode >& assumptions ); - inline void addToMembershipDB( Node, Node, Node ); - void printNodeMap(char* fst, char* snd, NodeMap map); - inline Node constructPair(Node tc_rep, Node a, Node b); - void addToMap( std::map< Node, std::vector<Node> >&, Node, Node ); - bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node ); - inline Node getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r); - bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();} - - -}; - - -}/* 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 5204dcaed..8dbca1e73 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -16,8 +16,6 @@ #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" @@ -317,145 +315,6 @@ 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 89d481746..7a8d7eed4 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(!setType.getSetElementType().isSubtypeOf(elementType)) { + if(elementType != setType.getSetElementType()) { throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types"); } } @@ -183,97 +183,6 @@ 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(!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 abb6c02b2..2f36cc188 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -86,4 +86,4 @@ regress regress0 test: check # do nothing in this subdir .PHONY: regress1 regress2 regress3 -regress1 regress2 regress3:
\ No newline at end of file +regress1 regress2 regress3: diff --git a/test/regress/regress0/sets/rels/addr_book_0.cvc b/test/regress/regress0/sets/rels/addr_book_0.cvc deleted file mode 100644 index fbe782ab2..000000000 --- a/test/regress/regress0/sets/rels/addr_book_0.cvc +++ /dev/null @@ -1,49 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -Atom : TYPE; -AtomTup : TYPE = [Atom]; -AtomBinTup : TYPE = [Atom, Atom]; -AtomTerTup : TYPE = [Atom, Atom, Atom]; -Target: SET OF AtomTup; - -Name: SET OF AtomTup; -Addr: SET OF AtomTup; -Book: SET OF AtomTup; -names: SET OF AtomBinTup; -addr: SET OF AtomTerTup; - -b1: Atom; -b1_tup : AtomTup; -ASSERT b1_tup = TUPLE(b1); -ASSERT b1_tup IS_IN Book; - -b2: Atom; -b2_tup : AtomTup; -ASSERT b2_tup = TUPLE(b2); -ASSERT b2_tup IS_IN Book; - -b3: Atom; -b3_tup : AtomTup; -ASSERT b3_tup = TUPLE(b3); -ASSERT b3_tup IS_IN Book; - -n: Atom; -n_tup : AtomTup; -ASSERT n_tup = TUPLE(n); -ASSERT n_tup IS_IN Name; - -t: Atom; -t_tup : AtomTup; -ASSERT t_tup = TUPLE(t); -ASSERT t_tup IS_IN Target; - -ASSERT ((Book JOIN addr) JOIN Target) = Name; -ASSERT (Book JOIN names) = Name; -ASSERT (Name & Addr) = {}::SET OF AtomTup; - -ASSERT ({n_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; -ASSERT ({n_tup} JOIN ({b2_tup} JOIN addr)) = ({n_tup} JOIN ({b1_tup} JOIN addr)) | {t_tup}; -ASSERT ({n_tup} JOIN ({b3_tup} JOIN addr)) = ({n_tup} JOIN ({b2_tup} JOIN addr)) - {t_tup}; -ASSERT NOT (({n_tup} JOIN ({b1_tup} JOIN addr)) = ({n_tup} JOIN ({b3_tup} JOIN addr))); - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/addr_book_1.cvc b/test/regress/regress0/sets/rels/addr_book_1.cvc deleted file mode 100644 index 34176f274..000000000 --- a/test/regress/regress0/sets/rels/addr_book_1.cvc +++ /dev/null @@ -1,45 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -Atom : TYPE; -AtomTup : TYPE = [Atom]; -AtomBinTup : TYPE = [Atom, Atom]; -AtomTerTup : TYPE = [Atom, Atom, Atom]; -Target: SET OF AtomTup; - -Name: SET OF AtomTup; -Addr: SET OF AtomTup; -Book: SET OF AtomTup; -names: SET OF AtomBinTup; -addr: SET OF AtomTerTup; - -b1: Atom; -b1_tup : AtomTup; -ASSERT b1_tup = TUPLE(b1); -ASSERT b1_tup IS_IN Book; - -b2: Atom; -b2_tup : AtomTup; -ASSERT b2_tup = TUPLE(b2); -ASSERT b2_tup IS_IN Book; - -b3: Atom; -b3_tup : AtomTup; -ASSERT b3_tup = TUPLE(b3); -ASSERT b3_tup IS_IN Book; - -m: Atom; -m_tup : AtomTup; -ASSERT m_tup = TUPLE(m); -ASSERT m_tup IS_IN Name; - -t: Atom; -t_tup : AtomTup; -ASSERT t_tup = TUPLE(t); -ASSERT t_tup IS_IN Target; - -ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; -ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)}; -ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)}; -ASSERT NOT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr)); - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/addr_book_1_1.cvc b/test/regress/regress0/sets/rels/addr_book_1_1.cvc deleted file mode 100644 index 74e29eaee..000000000 --- a/test/regress/regress0/sets/rels/addr_book_1_1.cvc +++ /dev/null @@ -1,45 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -Atom : TYPE; -AtomTup : TYPE = [Atom]; -AtomBinTup : TYPE = [Atom, Atom]; -AtomTerTup : TYPE = [Atom, Atom, Atom]; -Target: SET OF AtomTup; - -Name: SET OF AtomTup; -Addr: SET OF AtomTup; -Book: SET OF AtomTup; -names: SET OF AtomBinTup; -addr: SET OF AtomTerTup; - -b1: Atom; -b1_tup : AtomTup; -ASSERT b1_tup = TUPLE(b1); -ASSERT b1_tup IS_IN Book; - -b2: Atom; -b2_tup : AtomTup; -ASSERT b2_tup = TUPLE(b2); -ASSERT b2_tup IS_IN Book; - -b3: Atom; -b3_tup : AtomTup; -ASSERT b3_tup = TUPLE(b3); -ASSERT b3_tup IS_IN Book; - -m: Atom; -m_tup : AtomTup; -ASSERT m_tup = TUPLE(m); -ASSERT m_tup IS_IN Name; - -t: Atom; -t_tup : AtomTup; -ASSERT t_tup = TUPLE(t); -ASSERT t_tup IS_IN Target; - -ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; -ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)}; -ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)}; -ASSERT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr)); - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/garbage_collect.cvc b/test/regress/regress0/sets/rels/garbage_collect.cvc deleted file mode 100644 index dd5995c42..000000000 --- a/test/regress/regress0/sets/rels/garbage_collect.cvc +++ /dev/null @@ -1,59 +0,0 @@ -H_TYPE: TYPE; -H: TYPE = [H_TYPE]; -Obj: TYPE; -Obj_Tup: TYPE = [Obj]; -MARK_TYPE: TYPE = [H_TYPE, Obj]; -RELATE: TYPE = [Obj, Obj]; -REF_TYPE: TYPE = [H_TYPE, Obj, Obj]; - -% Symbols h0 to h3 are constants of type H that represents the system state; -h0: SET OF H; -h1: SET OF H; -h2: SET OF H; -h3: SET OF H; -s0: H_TYPE; -s1: H_TYPE; -s2: H_TYPE; -s3: H_TYPE; -ASSERT h0 = {TUPLE(s0)}; -ASSERT h1 = {TUPLE(s1)}; -ASSERT h2 = {TUPLE(s2)}; -ASSERT h3 = {TUPLE(s3)}; - -% ref ⊆ H × Obj × Obj represents references between objects in each state; -ref : SET OF REF_TYPE; - -% mark ⊆ H × Obj represents the marked objects in each state -mark: SET OF MARK_TYPE; - -empty_obj_set: SET OF Obj_Tup; -ASSERT empty_obj_set = {}:: SET OF Obj_Tup; - -% root and live are two constants of type Obj that represents objects; -root: Obj; -live: Obj; - -% The state transition (h0–h1) resets all the marks -ASSERT (h1 JOIN mark) = empty_obj_set; -ASSERT (h0 JOIN ref) <= (h1 JOIN ref); - -% (h1–h2) marks objects reachable from root -ASSERT FORALL (n : Obj) : ((root, n) IS_IN TCLOSURE(h1 JOIN ref)) - => (TUPLE(n) IS_IN (h2 JOIN mark)); -ASSERT (h1 JOIN ref) <= (h2 JOIN ref); - -% (h2–h3) sweeps references of non-marked objects - -ASSERT FORALL (n: Obj) : (NOT (TUPLE(n) IS_IN (h2 JOIN mark))) - => ({TUPLE(n)} JOIN (h3 JOIN ref)) = empty_obj_set; - -ASSERT FORALL (n: Obj) : (TUPLE(n) IS_IN (h2 JOIN mark)) - => ({TUPLE(n)} JOIN (h3 JOIN ref)) = ({TUPLE(n)} JOIN (h2 JOIN ref)); - -%The safety property is negated, thus it checks if -%in the final state, there is a live object that was originally reachable from root -%in the beginning state, but some of its references have been swept -ASSERT (root, live) IS_IN TCLOSURE(h0 JOIN ref); -ASSERT NOT (({TUPLE(live)} JOIN (h0 JOIN ref)) <= ({TUPLE(live)} JOIN (h3 JOIN ref))); - -CHECKSAT;
\ 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 deleted file mode 100644 index 50d4defd5..000000000 --- a/test/regress/regress0/sets/rels/rel_1tup_0.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% 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 deleted file mode 100644 index dcb753973..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_0.cvc +++ /dev/null @@ -1,31 +0,0 @@ -% 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 deleted file mode 100644 index 969d0d71c..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_1.cvc +++ /dev/null @@ -1,34 +0,0 @@ -% 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 deleted file mode 100644 index 492c94432..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_3.cvc +++ /dev/null @@ -1,49 +0,0 @@ -% 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 deleted file mode 100644 index f473b00aa..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_4.cvc +++ /dev/null @@ -1,52 +0,0 @@ -% 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 deleted file mode 100644 index d64817187..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_5.cvc +++ /dev/null @@ -1,55 +0,0 @@ -% 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 deleted file mode 100644 index c1b82339f..000000000 --- a/test/regress/regress0/sets/rels/rel_conflict_0.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 deleted file mode 100644 index 406b8d312..000000000 --- a/test/regress/regress0/sets/rels/rel_join_0.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% 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 deleted file mode 100644 index a7fa7efb9..000000000 --- a/test/regress/regress0/sets/rels/rel_join_0_1.cvc +++ /dev/null @@ -1,27 +0,0 @@ -% 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 deleted file mode 100644 index c8921afb9..000000000 --- a/test/regress/regress0/sets/rels/rel_join_1.cvc +++ /dev/null @@ -1,31 +0,0 @@ -% 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 deleted file mode 100644 index 75fc08387..000000000 --- a/test/regress/regress0/sets/rels/rel_join_1_1.cvc +++ /dev/null @@ -1,31 +0,0 @@ -% 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 r = (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 deleted file mode 100644 index cac7ce84d..000000000 --- a/test/regress/regress0/sets/rels/rel_join_2.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 deleted file mode 100644 index 3e27b9cc5..000000000 --- a/test/regress/regress0/sets/rels/rel_join_2_1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 deleted file mode 100644 index 6e190cecf..000000000 --- a/test/regress/regress0/sets/rels/rel_join_3.cvc +++ /dev/null @@ -1,29 +0,0 @@ -% 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 deleted file mode 100644 index d4e666c6e..000000000 --- a/test/regress/regress0/sets/rels/rel_join_3_1.cvc +++ /dev/null @@ -1,29 +0,0 @@ -% 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 deleted file mode 100644 index 030810f3d..000000000 --- a/test/regress/regress0/sets/rels/rel_join_4.cvc +++ /dev/null @@ -1,32 +0,0 @@ -% 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 deleted file mode 100644 index 5209d8131..000000000 --- a/test/regress/regress0/sets/rels/rel_join_5.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 deleted file mode 100644 index 17318872f..000000000 --- a/test/regress/regress0/sets/rels/rel_join_6.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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 deleted file mode 100644 index fff5b6efe..000000000 --- a/test/regress/regress0/sets/rels/rel_join_7.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% 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 deleted file mode 100644 index 723a9b2e2..000000000 --- a/test/regress/regress0/sets/rels/rel_mix_0.cvc +++ /dev/null @@ -1,30 +0,0 @@ -% 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 deleted file mode 100644 index 6cdf03600..000000000 --- a/test/regress/regress0/sets/rels/rel_pressure_0.cvc +++ /dev/null @@ -1,617 +0,0 @@ -% 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 deleted file mode 100644 index 09981be0b..000000000 --- a/test/regress/regress0/sets/rels/rel_product_0.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 deleted file mode 100644 index f141c7bd4..000000000 --- a/test/regress/regress0/sets/rels/rel_product_0_1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 deleted file mode 100644 index 1826e5a75..000000000 --- a/test/regress/regress0/sets/rels/rel_product_1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 deleted file mode 100644 index 9559b74e1..000000000 --- a/test/regress/regress0/sets/rels/rel_product_1_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 IntTup; - -z : IntPair; -ASSERT z = (1,2,3); -zt : IntPair; -ASSERT zt = (3,2,1); - - -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -ASSERT (1,1,1,1,1,1) IS_IN r; -ASSERT r = (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 deleted file mode 100644 index 08ed32411..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 deleted file mode 100644 index df2d7f412..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 deleted file mode 100644 index 082604dc2..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 deleted file mode 100644 index b1720b50e..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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_10_1.cvc b/test/regress/regress0/sets/rels/rel_tc_10_1.cvc deleted file mode 100644 index 67c444070..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_10_1.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: sat -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 a = c; -ASSERT a = d; -ASSERT (1, c) IS_IN x; -ASSERT (2, d) IS_IN x; -ASSERT (a, 5) IS_IN y; -ASSERT y = (TCLOSURE x); -ASSERT ((2, 5) IS_IN y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_11.cvc b/test/regress/regress0/sets/rels/rel_tc_11.cvc deleted file mode 100644 index 7edeb0efb..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_11.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 IntTup; -ASSERT (2, 3) IS_IN x; -ASSERT (5, 3) IS_IN x; -ASSERT (3, 9) IS_IN x; -ASSERT z = (x PRODUCT y); -ASSERT (1, 2, 3, 4) IS_IN z; -ASSERT NOT ((5, 9) IS_IN x); -ASSERT (3, 8) IS_IN y; -ASSERT y = (TCLOSURE x); -ASSERT NOT ((1, 2) IS_IN y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_2_1.cvc b/test/regress/regress0/sets/rels/rel_tc_2_1.cvc deleted file mode 100644 index d5d42eaad..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_2_1.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - e: INT; - -a : IntPair; -ASSERT a = (1, e); - -d : IntPair; -ASSERT d = (e,5); - -ASSERT a IS_IN x; -ASSERT d IS_IN x; -ASSERT NOT ((1,1) IS_IN x); -ASSERT NOT ((1,2) IS_IN x); -ASSERT NOT ((1,3) IS_IN x); -ASSERT NOT ((1,4) IS_IN x); -ASSERT NOT ((1,5) IS_IN x); -ASSERT NOT ((1,6) IS_IN x); -ASSERT NOT ((1,7) IS_IN x); - -ASSERT y = TCLOSURE(x); - -ASSERT (1, 5) IS_IN y; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_3.cvc b/test/regress/regress0/sets/rels/rel_tc_3.cvc deleted file mode 100644 index 39564c4cf..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_3.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 (b > (d -1)); -ASSERT (b < (d+1)); -%ASSERT (2,3) IS_IN ((x JOIN x) JOIN x); -%ASSERT NOT (2, 3) IS_IN (TCLOSURE x); -ASSERT y = (TCLOSURE x); -ASSERT NOT ((1, 1) IS_IN y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_3_1.cvc b/test/regress/regress0/sets/rels/rel_tc_3_1.cvc deleted file mode 100644 index e48ba4eb6..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_3_1.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 y = (TCLOSURE x); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_4.cvc b/test/regress/regress0/sets/rels/rel_tc_4.cvc deleted file mode 100644 index decd38fe1..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_4.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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,b) IS_IN ((x JOIN x) JOIN x); -ASSERT NOT (2, 1) IS_IN (TCLOSURE x); - - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_4_1.cvc b/test/regress/regress0/sets/rels/rel_tc_4_1.cvc deleted file mode 100644 index 8ee75f7e9..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_4_1.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -ASSERT y = ((TCLOSURE x) JOIN x); -ASSERT NOT (y = TCLOSURE x); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_5_1.cvc b/test/regress/regress0/sets/rels/rel_tc_5_1.cvc deleted file mode 100644 index fd9caeade..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_5_1.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -ASSERT y = (TCLOSURE x); -ASSERT NOT ( y = ((x JOIN x) JOIN x)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_6.cvc b/test/regress/regress0/sets/rels/rel_tc_6.cvc deleted file mode 100644 index 4570c5a8d..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_6.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -ASSERT y = (TCLOSURE x); -ASSERT NOT (((x JOIN x) JOIN x) <= y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_7.cvc b/test/regress/regress0/sets/rels/rel_tc_7.cvc deleted file mode 100644 index 15c0510a6..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_7.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -ASSERT y = ((TCLOSURE x) JOIN x); -ASSERT (1,2) IS_IN ((x JOIN x) JOIN x); -ASSERT NOT (y <= TCLOSURE x); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_8.cvc b/test/regress/regress0/sets/rels/rel_tc_8.cvc deleted file mode 100644 index 9f5879c6d..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_8.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -ASSERT (2, 2) IS_IN (TCLOSURE x); -ASSERT x = {}::SET OF IntPair; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_9_1.cvc b/test/regress/regress0/sets/rels/rel_tc_9_1.cvc deleted file mode 100644 index f884349b1..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_9_1.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -w : SET OF IntPair; - -ASSERT z = (TCLOSURE x); -ASSERT w = (x JOIN y); -ASSERT (2, 2) IS_IN z; -ASSERT (0,3) IS_IN y; -ASSERT (-1,3) IS_IN y; -ASSERT (1,3) IS_IN y; -ASSERT (-2,3) IS_IN y; -ASSERT (2,3) IS_IN y; -ASSERT (3,3) IS_IN y; -ASSERT (4,3) IS_IN y; -ASSERT (5,3) IS_IN y; -ASSERT NOT (2, 3) IS_IN (x JOIN y); -ASSERT NOT (2,1) IS_IN x; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_2.cvc b/test/regress/regress0/sets/rels/rel_tp_2.cvc deleted file mode 100644 index 441e79c45..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_2.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 deleted file mode 100644 index a03f0e3fd..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_0.cvc +++ /dev/null @@ -1,32 +0,0 @@ -% 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 deleted file mode 100644 index 60b6edf58..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc +++ /dev/null @@ -1,32 +0,0 @@ -% 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 deleted file mode 100644 index cc851f622..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_2.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 deleted file mode 100644 index 04856d825..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 deleted file mode 100644 index 25277f43a..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_3.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% 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 deleted file mode 100644 index 54e16dd51..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% 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 deleted file mode 100644 index 8d149a48d..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_int.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% 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 deleted file mode 100644 index b05026bc9..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 deleted file mode 100644 index aacf6c054..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% 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 deleted file mode 100644 index 49fb87569..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_0.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -a: INT; -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 y = (TRANSPOSE x); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1.cvc deleted file mode 100644 index bdcf31bb8..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_1.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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 deleted file mode 100644 index fa6ee5069..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntTup: TYPE = [INT, INT, INT]; -x : SET OF IntTup; -y : SET OF IntTup; -z : IntTup; -a: INT; -ASSERT z = (1,2,a); -zt : IntTup; -ASSERT zt = (3,2,2); -ASSERT z IS_IN x; -ASSERT zt IS_IN (TRANSPOSE x); -ASSERT y = (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 deleted file mode 100644 index 225f3491c..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_3.cvc +++ /dev/null @@ -1,14 +0,0 @@ -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 deleted file mode 100644 index b260147c8..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_4.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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 deleted file mode 100644 index 203e8b3d2..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_5.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 deleted file mode 100644 index a2e8bcf10..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_6.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% 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 deleted file mode 100644 index bcc3babc8..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_7.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; diff --git a/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc b/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc deleted file mode 100644 index dd5995c42..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc +++ /dev/null @@ -1,59 +0,0 @@ -H_TYPE: TYPE; -H: TYPE = [H_TYPE]; -Obj: TYPE; -Obj_Tup: TYPE = [Obj]; -MARK_TYPE: TYPE = [H_TYPE, Obj]; -RELATE: TYPE = [Obj, Obj]; -REF_TYPE: TYPE = [H_TYPE, Obj, Obj]; - -% Symbols h0 to h3 are constants of type H that represents the system state; -h0: SET OF H; -h1: SET OF H; -h2: SET OF H; -h3: SET OF H; -s0: H_TYPE; -s1: H_TYPE; -s2: H_TYPE; -s3: H_TYPE; -ASSERT h0 = {TUPLE(s0)}; -ASSERT h1 = {TUPLE(s1)}; -ASSERT h2 = {TUPLE(s2)}; -ASSERT h3 = {TUPLE(s3)}; - -% ref ⊆ H × Obj × Obj represents references between objects in each state; -ref : SET OF REF_TYPE; - -% mark ⊆ H × Obj represents the marked objects in each state -mark: SET OF MARK_TYPE; - -empty_obj_set: SET OF Obj_Tup; -ASSERT empty_obj_set = {}:: SET OF Obj_Tup; - -% root and live are two constants of type Obj that represents objects; -root: Obj; -live: Obj; - -% The state transition (h0–h1) resets all the marks -ASSERT (h1 JOIN mark) = empty_obj_set; -ASSERT (h0 JOIN ref) <= (h1 JOIN ref); - -% (h1–h2) marks objects reachable from root -ASSERT FORALL (n : Obj) : ((root, n) IS_IN TCLOSURE(h1 JOIN ref)) - => (TUPLE(n) IS_IN (h2 JOIN mark)); -ASSERT (h1 JOIN ref) <= (h2 JOIN ref); - -% (h2–h3) sweeps references of non-marked objects - -ASSERT FORALL (n: Obj) : (NOT (TUPLE(n) IS_IN (h2 JOIN mark))) - => ({TUPLE(n)} JOIN (h3 JOIN ref)) = empty_obj_set; - -ASSERT FORALL (n: Obj) : (TUPLE(n) IS_IN (h2 JOIN mark)) - => ({TUPLE(n)} JOIN (h3 JOIN ref)) = ({TUPLE(n)} JOIN (h2 JOIN ref)); - -%The safety property is negated, thus it checks if -%in the final state, there is a live object that was originally reachable from root -%in the beginning state, but some of its references have been swept -ASSERT (root, live) IS_IN TCLOSURE(h0 JOIN ref); -ASSERT NOT (({TUPLE(live)} JOIN (h0 JOIN ref)) <= ({TUPLE(live)} JOIN (h3 JOIN ref))); - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc deleted file mode 100644 index 0b4a13d09..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntTup: TYPE = [INT]; -IntPair: TYPE = [INT, INT]; -x : SET OF IntTup; -y : SET OF IntTup; -z: SET OF IntTup; - -b : IntTup; -ASSERT b = TUPLE(2); -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/tobesolved/rel_complex_2.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc deleted file mode 100644 index 5dfe957ca..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc +++ /dev/null @@ -1,34 +0,0 @@ -% 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; - - -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 = (4,3); -ASSERT h IS_IN x; -ASSERT h IS_IN y; - -ASSERT r = (x JOIN y); - -e : IntPair; - -ASSERT r = (x | y); -ASSERT NOT(z = (x & y)); -ASSERT z = (x - y); -ASSERT x <= y; -ASSERT e IS_IN (z JOIN x); -ASSERT e IS_IN x; -ASSERT e IS_IN (x & y); -CHECKSAT TRUE;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc deleted file mode 100644 index 60e39a5b2..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc +++ /dev/null @@ -1,652 +0,0 @@ -% 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; - -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; - -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/tobesolved/rel_join_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc deleted file mode 100644 index 034eebd22..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; - -ASSERT (1, 2) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (3, 4) IS_IN z; - -ASSERT ((1, 1) IS_IN (x JOIN x)); - -%ASSERT y = (x JOIN x); - -ASSERT (NOT (1,4) IS_IN ((x JOIN x) JOIN z)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc deleted file mode 100644 index 5fce37ef4..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -a: INT; -b: INT; - -ASSERT (1, b) IS_IN x; -ASSERT (a, 3) IS_IN y; - -ASSERT NOT ((1,3) IS_IN (x JOIN y)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc deleted file mode 100644 index ca6369087..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc +++ /dev/null @@ -1,35 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT]; -w : SET OF IntPair; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; - -r : SET OF IntPair; -r2 : SET OF IntPair; - -d : IntPair; -ASSERT d = (3,1); -ASSERT (1,3) IS_IN y; -ASSERT d IS_IN y; - -ASSERT (3,1) IS_IN y; -ASSERT (4,1) IS_IN y; -ASSERT (1,3) IS_IN z; - -a : IntPair; -ASSERT a IS_IN x; - -e : IntPair; -ASSERT e = (4,3); -ASSERT e IS_IN x; - -ASSERT r = (x JOIN y); -ASSERT r2 = (y JOIN z); -ASSERT (1,3) IS_IN r; -ASSERT r = r2; -ASSERT NOT (e IS_IN r); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc deleted file mode 100644 index 32d529df3..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc +++ /dev/null @@ -1,31 +0,0 @@ -% EXPECT: sat -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; -r2 : SET OF IntPair; - -d : IntPair; -ASSERT d = (3,1); -ASSERT (1,3) IS_IN y; -ASSERT d IS_IN y; - -ASSERT (3,1) IS_IN y; -ASSERT (4,1) IS_IN y; -ASSERT (1,3) IS_IN z; - -a : IntPair; -ASSERT a IS_IN x; - -e : IntPair; -ASSERT e = (4,3); -ASSERT e IS_IN x; - -ASSERT y = ((x JOIN y) JOIN z); - - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc deleted file mode 100644 index 7257d5a0d..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc +++ /dev/null @@ -1,25 +0,0 @@ -% 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; -w : SET OF IntTup; - -z : IntPair; -ASSERT z = (1,3); -zt : IntPair; -ASSERT zt = (2,1); -v : IntTup; -ASSERT v = (1,2,2,1); - -ASSERT zt IS_IN y; -ASSERT v IS_IN (x PRODUCT y); -ASSERT (4, 4, 5, 5) IS_IN w; -ASSERT z IS_IN x; - -ASSERT w = (x PRODUCT y); -ASSERT NOT (4,4) IS_IN x; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc deleted file mode 100644 index 0a2ec79be..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -a : IntPair; -ASSERT a = (1,2); -b : IntPair; -ASSERT b = (2,1); -c: IntPair; -ASSERT c = (1,1); -d : IntPair; -ASSERT d = (1,5); - -ASSERT a IS_IN x; -ASSERT b IS_IN x; -ASSERT c IS_IN x; -ASSERT d IS_IN x; -ASSERT y = (TCLOSURE x); -ASSERT NOT ((1, 1) IS_IN y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc deleted file mode 100644 index b8ab773b1..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -e: INT; -a : IntPair; -ASSERT a = (1,e); -b : IntPair; -ASSERT b = (e,1); - - -ASSERT a IS_IN x; -ASSERT b IS_IN x; - -ASSERT y = (TCLOSURE x); -ASSERT NOT ((1, 1) IS_IN y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc deleted file mode 100644 index f074011ce..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z: SET OF IntPair; - -ASSERT (1, 3) IS_IN x; -ASSERT ((2,3) IS_IN z OR (2,1) IS_IN z); -ASSERT y = (TRANSPOSE x); -ASSERT NOT (1,2) IS_IN y; -ASSERT NOT (3,2) IS_IN y; -ASSERT x = z; -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc deleted file mode 100644 index 183be8d9b..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -ASSERT (2, 2) IS_IN (TCLOSURE x); -ASSERT NOT (2,1) IS_IN x; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/test.cvc b/test/regress/regress0/sets/rels/tobesolved/test.cvc deleted file mode 100644 index aa4e17eab..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/test.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; -ASSERT (y JOIN x) = x; - -ASSERT (1,2) IS_IN x; - -CHECKSAT; |