From 06f09df136eaf824a7cefe2e4a88f010ae6495d7 Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Mon, 29 Feb 2016 11:10:01 -0600 Subject: [PATCH] Added more benchmarks Fixed the problem that duplicates and split facts were sent as lemmas causing nontermination Fixed the computation of join and product relations without simplication --- src/theory/sets/theory_sets_rels.cpp | 111 ++++++++++++++---- src/theory/sets/theory_sets_rels.h | 3 + .../regress/regress0/sets/rels/rel_join_3.cvc | 29 +++++ .../regress0/sets/rels/rel_join_3_1.cvc | 29 +++++ .../regress/regress0/sets/rels/rel_join_4.cvc | 32 +++++ .../regress/regress0/sets/rels/rel_join_5.cvc | 19 +++ .../regress0/sets/rels/rel_product_0.cvc | 20 ++++ .../regress0/sets/rels/rel_product_0_1.cvc | 20 ++++ .../regress0/sets/rels/rel_product_1.cvc | 20 ++++ .../regress0/sets/rels/rel_product_1_1.cvc | 20 ++++ .../regress0/sets/rels/rel_tp_join_0.cvc | 32 +++++ .../regress0/sets/rels/rel_tp_join_1.cvc | 24 ++++ .../regress0/sets/rels/rel_tp_join_2.cvc | 19 +++ .../regress0/sets/rels/rel_tp_join_2_1.cvc | 19 +++ .../regress0/sets/rels/rel_tp_join_3.cvc | 28 +++++ .../regress0/sets/rels/rel_tp_join_pro_0.cvc | 21 ++++ .../regress0/sets/rels/rel_tp_join_var.cvc | 28 +++++ .../regress0/sets/rels/rel_transpose_2.cvc | 12 ++ .../regress0/sets/rels/rel_transpose_3.cvc | 14 +++ .../regress0/sets/rels/rel_transpose_4.cvc | 13 ++ 20 files changed, 492 insertions(+), 21 deletions(-) create mode 100644 test/regress/regress0/sets/rels/rel_join_3.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_3_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_4.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_5.cvc create mode 100644 test/regress/regress0/sets/rels/rel_product_0.cvc create mode 100644 test/regress/regress0/sets/rels/rel_product_0_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_product_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_product_1_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_tp_join_0.cvc create mode 100644 test/regress/regress0/sets/rels/rel_tp_join_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_tp_join_2.cvc create mode 100644 test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_tp_join_3.cvc create mode 100644 test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc create mode 100644 test/regress/regress0/sets/rels/rel_tp_join_var.cvc create mode 100644 test/regress/regress0/sets/rels/rel_transpose_2.cvc create mode 100644 test/regress/regress0/sets/rels/rel_transpose_3.cvc create mode 100644 test/regress/regress0/sets/rels/rel_transpose_4.cvc diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index de70e6a52..2b35fb077 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -43,7 +43,7 @@ typedef std::map >::iterator mem_it; Trace("rels-debug") << "[sets-rels] Start the relational solver..." << std::endl; collectRelationalInfo(); check(); -// doPendingFacts(); + doPendingSplitFacts(); doPendingLemmas(); Assert(d_lemma_cache.empty()); Assert(d_pending_facts.empty()); @@ -189,6 +189,28 @@ typedef std::map >::iterator mem_it; d_terms_cache.clear(); } + void TheorySetsRels::doPendingSplitFacts() { + std::map::iterator map_it = d_pending_split_facts.begin(); + while( !(*d_conflict) && map_it != d_pending_split_facts.end()) { + + Node fact = map_it->first; + Node exp = d_pending_split_facts[ fact ]; + if(fact.getKind() == kind::AND) { + for(size_t j=0; j >::iterator mem_it; if(!polarity) { if(d_terms_cache[getRepresentative(fact[1])].find(kind::JOIN) != d_terms_cache[getRepresentative(fact[1])].end()) { - computeJoinOrProductRelations(fact[1]); + std::vector join_terms = d_terms_cache[getRepresentative(fact[1])][kind::JOIN]; + for(unsigned int i = 0; i < join_terms.size(); i++) { + computeJoinOrProductRelations(join_terms[i]); + } } if(d_terms_cache[getRepresentative(fact[1])].find(kind::PRODUCT) != d_terms_cache[getRepresentative(fact[1])].end()) { - computeJoinOrProductRelations(fact[1]); + std::vector product_terms = d_terms_cache[getRepresentative(fact[1])][kind::PRODUCT]; + for(unsigned int i = 0; i < product_terms.size(); i++) { + computeJoinOrProductRelations(product_terms[i]); + } } fact = fact.negate(); } @@ -278,13 +306,12 @@ typedef std::map >::iterator mem_it; } void TheorySetsRels::computeJoinOrProductRelations(Node n) { + Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation " << n << std::endl; switch(n[0].getKind()) { - case kind::JOIN: - computeJoinOrProductRelations(n[0]); - break; case kind::TRANSPOSE: computeTransposeRelations(n[0]); break; + case kind::JOIN: case kind::PRODUCT: computeJoinOrProductRelations(n[0]); break; @@ -293,12 +320,10 @@ typedef std::map >::iterator mem_it; } switch(n[1].getKind()) { - case kind::JOIN: - computeJoinOrProductRelations(n[1]); - break; case kind::TRANSPOSE: computeTransposeRelations(n[1]); break; + case kind::JOIN: case kind::PRODUCT: computeJoinOrProductRelations(n[1]); break; @@ -349,9 +374,6 @@ typedef std::map >::iterator mem_it; rev_tuples.push_back(rev_tup); rev_exps.push_back(Rewriter::rewrite(reason)); sendInfer(MEMBER(rev_tup, n_rep), Rewriter::rewrite(reason), "transpose-rule"); -// if(std::find(rev_tuples.begin(), rev_tuples.end(), reverseTuple(tuples[i])) == rev_tuples.end()) { -// -// } } d_membership_cache[n_rep] = rev_tuples; d_membership_exp_cache[n_rep] = rev_exps; @@ -364,7 +386,7 @@ typedef std::map >::iterator mem_it; Node r2 = n[1]; Node r1_rep = getRepresentative(r1); Node r2_rep = getRepresentative(r2); - Trace("rels-debug") << "[sets-rels] start joining tuples in " + Trace("rels-debug") << "[sets-rels] start composing tuples in relations " << r1 << " and " << r2 << "\n r1_rep: " << r1_rep << "\n r2_rep: " << r2_rep << std::endl; @@ -390,10 +412,6 @@ typedef std::map >::iterator mem_it; for(unsigned int j = 0; j < r2_elements.size(); j++) { std::vector joinedTuple; joinedTuple.push_back(Node::fromExpr(dt[0].getConstructor())); - Debug("rels-debug") << "areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]):\n" - << " r1_elements[i][t1_len-1] = " << r1_elements[i][t1_len-1] - << " r2_elements[j][0]) = " << r2_elements[j][0] - << " are equal? " << areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]) << std::endl; if((areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]) && n.getKind() == kind::JOIN) || n.getKind() == kind::PRODUCT) { unsigned int k = 0; @@ -434,7 +452,7 @@ typedef std::map >::iterator mem_it; if(kind::JOIN == n.getKind()) sendInfer(fact, reason, "join-compose"); else if(kind::PRODUCT == n.getKind()) - sendInfer(fact, reason, "product-compose"); + sendInfer( fact, reason, "product-compose" ); } } } @@ -454,13 +472,18 @@ typedef std::map >::iterator mem_it; } void TheorySetsRels::doPendingLemmas() { - if( !(*d_conflict) && !d_lemma_cache.empty() ){ + if( !(*d_conflict) && (!d_lemma_cache.empty() || !d_pending_facts.empty())){ for( unsigned i=0; i < d_lemma_cache.size(); i++ ){ Trace("rels-debug") << "[sets-rels] Process pending lemma : " << d_lemma_cache[i] << std::endl; d_sets.d_out->lemma( d_lemma_cache[i] ); } for( std::map::iterator child_it = d_pending_facts.begin(); child_it != d_pending_facts.end(); child_it++ ) { + if(holds(child_it->first)) { + Trace("rels-debug") << "[sets-rels] Skip the already processed fact,: " << child_it->first << std::endl; + continue; + } + Trace("rels-debug") << "[sets-rels] Process pending fact as lemma : " << child_it->first << std::endl; d_sets.d_out->lemma(child_it->first); } @@ -483,6 +506,10 @@ typedef std::map >::iterator mem_it; void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) { Trace("rels-lemma") << "[sets-rels] Infer " << fact << " from " << exp << " by " << c << std::endl; + if( std::strcmp( c, "join-split" ) == 0 ) { + d_pending_split_facts[fact] = exp; + return; + } d_pending_facts[fact] = exp; d_infer.push_back( fact ); d_infer_exp.push_back( exp ); @@ -522,12 +549,44 @@ typedef std::map >::iterator mem_it; bool TheorySetsRels::areEqual( Node a, Node b ){ if( hasTerm( a ) && hasTerm( b ) ){ -// Trace("rels-debug") << "has a and b " << a << " " << b << " are equal? "<< d_eqEngine->areEqual( a, b ) << std::endl; + if( d_eqEngine->isTriggerTerm(a, THEORY_SETS) && + d_eqEngine->isTriggerTerm(b, THEORY_SETS) ) { + // Get representative trigger terms + TNode x_shared = d_eqEngine->getTriggerTermRepresentative(a, THEORY_SETS); + TNode y_shared = d_eqEngine->getTriggerTermRepresentative(b, THEORY_SETS); + EqualityStatus eqStatusDomain = d_sets.d_valuation.getEqualityStatus(x_shared, y_shared); + switch (eqStatusDomain) { + case EQUALITY_TRUE_AND_PROPAGATED: + // Should have been propagated to us + Trace("rels-debug") << "EQUALITY_TRUE_AND_PROPAGATED **** equality( a, b ) = true" << std::endl; + return true; + break; + case EQUALITY_TRUE: + // Missed propagation - need to add the pair so that theory engine can force propagation + Trace("rels-debug") << "EQUALITY_TRUE **** equality( a, b ) = true" << std::endl; + return true; + break; + case EQUALITY_FALSE_AND_PROPAGATED: + // Should have been propagated to us + Trace("rels-debug") << "EQUALITY_FALSE_AND_PROPAGATED ******** equality( a, b ) = false" << std::endl; + return false; + break; + case EQUALITY_FALSE: + Trace("rels-debug") << "EQUALITY_FALSE **** equality( a, b ) = false" << std::endl; + return false; + break; + + default: + // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN + break; + } + } + Trace("rels-debug") << "has a and b " << a << " " << b << " are equal? "<< d_eqEngine->areEqual( a, b ) << std::endl; return d_eqEngine->areEqual( a, b ); }else if( a.isConst() && b.isConst() ){ return a == b; }else { -// Trace("rels-debug") << "to split a and b " << a << " " << b << std::endl; + Trace("rels-debug") << "to split a and b " << a << " " << b << std::endl; addSharedTerm(a); addSharedTerm(b); sendSplit(a, b, "tuple-element-equality"); @@ -545,6 +604,16 @@ typedef std::map >::iterator mem_it; return std::find(v.begin(), v.end(), n) != v.end(); } + bool TheorySetsRels::holds(Node node) { + bool polarity = node.getKind() != kind::NOT; + Node atom = polarity ? node : node[0]; + Node polarity_atom = polarity ? d_trueNode : d_falseNode; + Node atom_mod = NodeManager::currentNM()->mkNode(atom.getKind(), getRepresentative(atom[0]), + getRepresentative(atom[1]) ); + d_eqEngine->addTerm(atom_mod); + return areEqual(atom_mod, polarity_atom); + } + TheorySetsRels::TheorySetsRels(context::Context* c, context::UserContext* u, eq::EqualityEngine* eq, diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 4eb30ab12..d0d926e69 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -54,6 +54,7 @@ private: // 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; /** inferences: maintained to ensure ref count for internally introduced nodes */ @@ -84,6 +85,7 @@ private: void sendLemma( Node fact, Node reason, bool polarity ); void sendSplit( Node a, Node b, const char * c ); void doPendingFacts(); + void doPendingSplitFacts(); void addSharedTerm( TNode n ); // Helper functions @@ -91,6 +93,7 @@ private: bool hasTerm( Node a ); bool areEqual( Node a, Node b ); bool exists( std::vector&, Node ); + bool holds(Node); }; diff --git a/test/regress/regress0/sets/rels/rel_join_3.cvc b/test/regress/regress0/sets/rels/rel_join_3.cvc new file mode 100644 index 000000000..6e190cecf --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_3.cvc @@ -0,0 +1,29 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN r); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_3_1.cvc b/test/regress/regress0/sets/rels/rel_join_3_1.cvc new file mode 100644 index 000000000..d4e666c6e --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_3_1.cvc @@ -0,0 +1,29 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT a IS_IN r; + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_4.cvc b/test/regress/regress0/sets/rels/rel_join_4.cvc new file mode 100644 index 000000000..030810f3d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_4.cvc @@ -0,0 +1,32 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +b : IntPair; +ASSERT b = (7, 5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT b IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN r); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_5.cvc b/test/regress/regress0/sets/rels/rel_join_5.cvc new file mode 100644 index 000000000..5209d8131 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_5.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; + +a : IntPair; +ASSERT a = (1,4); +ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); +ASSERT NOT (a IS_IN r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_0.cvc b/test/regress/regress0/sets/rels/rel_product_0.cvc new file mode 100644 index 000000000..09981be0b --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_0.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntTup; +ASSERT v = (1,2,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (v IS_IN (x PRODUCT y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_0_1.cvc b/test/regress/regress0/sets/rels/rel_product_0_1.cvc new file mode 100644 index 000000000..f141c7bd4 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_0_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntTup; +ASSERT v = (1,2,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT v IS_IN (x PRODUCT y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_1.cvc b/test/regress/regress0/sets/rels/rel_product_1.cvc new file mode 100644 index 000000000..1826e5a75 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2,3); +zt : IntPair; +ASSERT zt = (3,2,1); +v : IntTup; +ASSERT v = (1,2,3,3,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (v IS_IN (x PRODUCT y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_1_1.cvc b/test/regress/regress0/sets/rels/rel_product_1_1.cvc new file mode 100644 index 000000000..3e5280c19 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_product_1_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: SAT +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2,3); +zt : IntPair; +ASSERT zt = (3,2,1); +v : IntTup; +ASSERT v = (1,2,3,3,2,1); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT v IS_IN (x PRODUCT y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc new file mode 100644 index 000000000..a03f0e3fd --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc @@ -0,0 +1,32 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (5,1); + +b : IntPair; +ASSERT b = (7, 5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT b IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT r = (x JOIN y); +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc new file mode 100644 index 000000000..dca0a3bfa --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc @@ -0,0 +1,24 @@ +% 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 (1, 7) 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 = ((x JOIN y) JOIN z); + +ASSERT NOT (a IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_2.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc new file mode 100644 index 000000000..cc851f622 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; + +a : IntPair; +ASSERT a = (4,1); +ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); +ASSERT NOT (a IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc new file mode 100644 index 000000000..04856d825 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; + +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; +a : IntPair; +ASSERT a = (4,1); + +ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); +ASSERT a IS_IN (TRANSPOSE r); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_3.cvc b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc new file mode 100644 index 000000000..25277f43a --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +% crash on this +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +w : SET OF IntPair; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +ASSERT (7, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; +ASSERT (3, 3) IS_IN w; + +a : IntPair; +ASSERT a = (4,1); +%ASSERT r = (((TRANSPOSE x) JOIN y) JOIN (w JOIN z)); +ASSERT NOT (a IS_IN (TRANSPOSE r)); + +zz : SET OF IntPair; +ASSERT zz = ((TRANSPOSE x) JOIN y); +ASSERT NOT ((1,3) IS_IN w); +ASSERT NOT ((1,3) IS_IN (w | zz) ); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc new file mode 100644 index 000000000..b05026bc9 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc @@ -0,0 +1,21 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntTup; + +ASSERT (2, 1) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (2, 2) IS_IN y; +ASSERT (4, 7) IS_IN y; +ASSERT (3, 4) IS_IN z; + +v : IntTup; +ASSERT v = (4,3,2,1); + +ASSERT r = (((TRANSPOSE x) JOIN y) PRODUCT z); +ASSERT NOT (v IS_IN (TRANSPOSE r)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc new file mode 100644 index 000000000..c7757bd3e --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +w : SET OF IntPair; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; + +t : INT; +u : INT; + +ASSERT 4 < t AND t < 6; +ASSERT 4 < u AND u < 6; + +ASSERT (1, u) IS_IN x; +ASSERT (t, 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_2.cvc b/test/regress/regress0/sets/rels/rel_transpose_2.cvc new file mode 100644 index 000000000..15a035b58 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_2.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1); +zt : IntTup; +ASSERT zt = (1); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE x)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_3.cvc b/test/regress/regress0/sets/rels/rel_transpose_3.cvc new file mode 100644 index 000000000..225f3491c --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_3.cvc @@ -0,0 +1,14 @@ +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +ASSERT (x = y); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_4.cvc b/test/regress/regress0/sets/rels/rel_transpose_4.cvc new file mode 100644 index 000000000..b260147c8 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_4.cvc @@ -0,0 +1,13 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); + +ASSERT z IS_IN x; +ASSERT NOT ((2, 1) IS_IN (TRANSPOSE x)); + +CHECKSAT; -- 2.30.2