From eea4ce60a90e6807b008b430e39f16dcb263c8a6 Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Wed, 17 Feb 2016 15:01:40 -0600 Subject: [PATCH] added rules for join and transpose operators added more benchmarks --- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/sets/theory_sets_rels.cpp | 197 +++++++++++++++--- src/theory/sets/theory_sets_rels.h | 22 +- src/theory/sets/theory_sets_type_rules.h | 4 +- test/regress/regress0/sets/Makefile.am | 3 +- test/regress/regress0/sets/rels/rel.cvc | 20 -- test/regress/regress0/sets/rels/rel_join.cvc | 26 +++ .../regress/regress0/sets/rels/rel_join_0.cvc | 25 +++ .../regress0/sets/rels/rel_join_0_1.cvc | 26 +++ .../regress/regress0/sets/rels/rel_join_1.cvc | 31 +++ .../regress0/sets/rels/rel_join_1_1.cvc | 31 +++ .../regress/regress0/sets/rels/rel_join_2.cvc | 20 ++ .../regress0/sets/rels/rel_join_2_1.cvc | 20 ++ .../regress0/sets/rels/rel_transpose.cvc | 12 ++ .../regress0/sets/rels/rel_transpose_0.cvc | 14 ++ .../regress0/sets/rels/rel_transpose_1.cvc | 12 ++ .../regress0/sets/rels/rel_transpose_1_1.cvc | 12 ++ 17 files changed, 416 insertions(+), 61 deletions(-) delete mode 100644 test/regress/regress0/sets/rels/rel.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_0.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_0_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_1_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_2.cvc create mode 100644 test/regress/regress0/sets/rels/rel_join_2_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_transpose.cvc create mode 100644 test/regress/regress0/sets/rels/rel_transpose_0.cvc create mode 100644 test/regress/regress0/sets/rels/rel_transpose_1.cvc create mode 100644 test/regress/regress0/sets/rels/rel_transpose_1_1.cvc diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 9d3f7e08e..5e328b4fd 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1111,7 +1111,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_rels(NULL) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); - d_rels = new TheorySetsRels(c, u, &d_equalityEngine); + d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict); d_equalityEngine.addFunctionKind(kind::UNION); d_equalityEngine.addFunctionKind(kind::INTERSECTION); diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 24a69bfdb..fcab5b5ca 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -35,10 +35,12 @@ namespace sets { TheorySetsRels::TheorySetsRels(context::Context* c, context::UserContext* u, - eq::EqualityEngine* eq): + eq::EqualityEngine* eq, + context::CDO* conflict): d_trueNode(NodeManager::currentNM()->mkConst(true)), d_falseNode(NodeManager::currentNM()->mkConst(false)), d_eqEngine(eq), + d_conflict(conflict), d_relsSaver(c) { d_eqEngine->addFunctionKind(kind::PRODUCT); @@ -59,10 +61,8 @@ namespace sets { while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); - bool firstTime = true; - Debug("rels-eqc") << " " << r; - Debug("rels-eqc") << " : { "; eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine ); + while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); @@ -70,53 +70,186 @@ namespace sets { if((d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_trueNode) || d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_falseNode)) && !d_relsSaver.contains(n)) { - d_relsSaver.insert(n); - // case: (b, a) IS_IN (TRANSPOSE X) - // => (a, b) IS_IN X + // case: [NOT] (b, a) IS_IN (TRANSPOSE X) + // => [NOT] (a, b) IS_IN X if(n.getKind() == kind::MEMBER) { + d_relsSaver.insert(n); if(kind::TRANSPOSE == n[1].getKind()) { Node reversedTuple = reverseTuple(n[0]); Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, reversedTuple, n[1][0]); -// assertMembership(fact, n, r == d_trueNode); + Node exp = n; + if(d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_falseNode)) { + fact = fact.negate(); + exp = n.negate(); + } + d_pending_facts[fact] = exp; } else if(kind::JOIN == n[1].getKind()) { - + TNode r1 = n[1][0]; + TNode r2 = n[1][1]; + // Need to do this efficiently... Join relations after collecting all of them + // So that we would just need to iterate over EE once + joinRelations(r1, r2, n[1].getType().getSetElementType()); + + // case: (a, b) IS_IN (X JOIN Y) + // => (a, z) IS_IN X && (z, b) IS_IN Y + if(d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_trueNode)) { + Debug("rels-join") << "Join rules (a, b) IS_IN (X JOIN Y) => ((a, z) IS_IN X && (z, b) IS_IN Y)"<< std::endl; + Assert((r1.getType().getSetElementType()).isDatatype()); + Assert((r2.getType().getSetElementType()).isDatatype()); + + unsigned int i = 0; + std::vector r1_tuple; + std::vector r2_tuple; + Node::iterator child_it = n[0].begin(); + unsigned int s1_len = r1.getType().getSetElementType().getTupleLength(); + Node shared_x = NodeManager::currentNM()->mkSkolem("sde_", r2.getType().getSetElementType().getTupleTypes()[0]); + Datatype dt = r1.getType().getSetElementType().getDatatype(); + + r1_tuple.push_back(Node::fromExpr(dt[0].getConstructor())); + for(; i < s1_len-1; ++child_it) { + r1_tuple.push_back(*child_it); + ++i; + } + r1_tuple.push_back(shared_x); + dt = r2.getType().getSetElementType().getDatatype(); + r2_tuple.push_back(Node::fromExpr(dt[0].getConstructor())); + r2_tuple.push_back(shared_x); + for(; child_it != n[0].end(); ++child_it) { + r2_tuple.push_back(*child_it); + } + Node t1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_tuple); + Node t2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_tuple); + Node f1 = NodeManager::currentNM()->mkNode(kind::MEMBER, t1, r1); + Node f2 = NodeManager::currentNM()->mkNode(kind::MEMBER, t2, r2); + d_pending_facts[f1] = n; + d_pending_facts[f2] = n; + } }else if(kind::PRODUCT == n[1].getKind()) { } } } + ++eqc_i; + } + ++eqcs_i; + } + doPendingFacts(); + } - if( r!=n ){ - if( firstTime ){ - Debug("rels-eqc") << std::endl; - firstTime = false; - } - if (n.getKind() == kind::PRODUCT || - n.getKind() == kind::JOIN || - n.getKind() == kind::TRANSCLOSURE || - n.getKind() == kind::TRANSPOSE) { - Debug("rels-eqc") << " *** " << n << std::endl; - }else{ - Debug("rels-eqc") << " " << n <consistent()) + return; + Debug("rels-join") << "start joining tuples in " + << r1 << " and " << r2 << std::endl; + + std::vector r1_elements; + std::vector r2_elements; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); + + // collect all tuples that are in r1, r2 + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if(d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_trueNode) + && n.getKind() == kind::MEMBER && n[0].getType().isTuple()) { + if(n[1] == r1) { + Debug("rels-join") << "r1 tuple: " << n[0] << std::endl; + r1_elements.push_back(n[0]); + } else if (n[1] == r2) { + Debug("rels-join") << "r2 tuple: " << n[0] << std::endl; + r2_elements.push_back(n[0]); } } ++eqc_i; } - if( !firstTime ){ Debug("rels-eqc") << " "; } - Debug("rels-eqc") << "}" << std::endl; ++eqcs_i; } + if(r1_elements.size() == 0 || r2_elements.size() == 0) + return; + + // Join r1 and r2 + joinTuples(r1, r2, r1_elements, r2_elements, tn); + } + void TheorySetsRels::joinTuples(TNode r1, TNode r2, std::vector& r1_elements, std::vector& r2_elements, TypeNode tn) { + Datatype dt = tn.getDatatype(); + 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++) { + if(r1_elements[i][t1_len-1] == r2_elements[j][0]) { + std::vector joinedTuple; + joinedTuple.push_back(Node::fromExpr(dt[0].getConstructor())); + for(unsigned int k = 0; k < t1_len - 1; ++k) { + joinedTuple.push_back(r1_elements[i][k]); + } + for(unsigned int l = 1; l < t2_len; ++l) { + joinedTuple.push_back(r2_elements[j][l]); + } + Node fact = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, joinedTuple); + fact = NodeManager::currentNM()->mkNode(kind::MEMBER, fact, NodeManager::currentNM()->mkNode(kind::JOIN, r1, r2)); + Node reason = NodeManager::currentNM()->mkNode(kind::AND, + NodeManager::currentNM()->mkNode(kind::MEMBER, r1_elements[i], r1), + NodeManager::currentNM()->mkNode(kind::MEMBER, r2_elements[j], r2)); + Debug("rels-join") << "join tuples: " << r1_elements[i] + << " and " << r2_elements[j] + << "\nnew fact: " << fact + << "\nreason: " << reason<< std::endl; + d_pending_facts[fact] = reason; + } + } + } + } + + + void TheorySetsRels::sendLemma(TNode fact, TNode reason, bool polarity) { + + } + + void TheorySetsRels::doPendingFacts() { + std::map::iterator map_it = d_pending_facts.begin(); + while( !(*d_conflict) && map_it != d_pending_facts.end()) { + + Node fact = map_it->first; + Node exp = d_pending_facts[ fact ]; + Debug("rels") << "sending out pending fact: " << fact + << " reason: " << exp + << std::endl; + if(fact.getKind() == kind::AND) { + for(size_t j=0; j elements; - Datatype dt = (Datatype)((tuple.getType()).getDatatype()); + std::vector 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(tuple.getOperator()); + elements.push_back(Node::fromExpr(dt[0].getConstructor())); for(Node::iterator child_it = tuple.end()-1; child_it != tuple.begin()-1; --child_it) { elements.push_back(*child_it); @@ -125,12 +258,10 @@ namespace sets { } void TheorySetsRels::assertMembership(TNode fact, TNode reason, bool polarity) { - TNode explain = reason; - if(!polarity) { - explain = reason.negate(); - } - Debug("rels") << " polarity : " << polarity << " reason: " << explain << std::endl; - d_eqEngine->assertPredicate(fact, polarity, explain); + Debug("rels") << "fact: " << fact + << "\npolarity : " << polarity + << "\nreason: " << reason << std::endl; + d_eqEngine->assertPredicate(fact, polarity, reason); } } } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index c48217275..537fc2d43 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -30,7 +30,8 @@ class TheorySetsRels { public: TheorySetsRels(context::Context* c, context::UserContext* u, - eq::EqualityEngine*); + eq::EqualityEngine*, + context::CDO* ); ~TheorySetsRels(); @@ -42,14 +43,31 @@ private: Node d_trueNode; Node d_falseNode; + // Facts and lemmas to be sent to EE + std::map< Node, Node> d_pending_facts; + std::vector< Node > d_lemma_cache; + + // Relation pairs to be joined +// std::map d_rel_pairs; +// std::hash_set d_rels; + eq::EqualityEngine *d_eqEngine; + context::CDO *d_conflict; // save all the relational terms seen so far context::CDHashSet d_relsSaver; void assertMembership(TNode fact, TNode reason, bool polarity); - Node reverseTuple(TNode tuple); + void joinRelations(TNode, TNode, TypeNode); + void joinTuples(TNode, TNode, std::vector&, std::vector&, TypeNode tn); + + Node reverseTuple(TNode); + + void sendLemma(TNode fact, TNode reason, bool polarity); + void doPendingLemmas(); + void doPendingFacts(); + }; }/* CVC4::theory::sets namespace */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 8d294ceeb..0909d8442 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -209,8 +209,6 @@ struct RelBinaryOperatorTypeRule { } resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); } - - Debug("rels") << "The resulting Type is " << resultType << std::endl; return resultType; } @@ -263,7 +261,7 @@ struct RelTransClosureTypeRule { inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { Assert(n.getKind() == kind::TRANSCLOSURE); - return true; + return false; } };/* struct RelTransClosureTypeRule */ diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index d694d553b..5069d061e 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -39,7 +39,6 @@ TESTS = \ mar2014/smaller.smt2 \ mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \ mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \ - rels/rel.cvc \ copy_check_heap_access_33_4.smt2 \ cvc-sample.cvc \ emptyset.smt2 \ @@ -84,4 +83,4 @@ regress regress0 test: check # do nothing in this subdir .PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +regress1 regress2 regress3: \ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel.cvc b/test/regress/regress0/sets/rels/rel.cvc deleted file mode 100644 index 27eb43b9f..000000000 --- a/test/regress/regress0/sets/rels/rel.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; -z : SET OF IntPair; -m: SET OF INT; -a: IntPair; -b: INT; - -ASSERT a IS_IN (y JOIN z); -ASSERT (y PRODUCT x) = (y PRODUCT z); -ASSERT x = ((y JOIN z) JOIN x); - -ASSERT x = y | z; -ASSERT x = y & z; -ASSERT y = y - z; -ASSERT z = (TRANSPOSE z); -ASSERT z = x | y; -CHECKSAT TRUE; diff --git a/test/regress/regress0/sets/rels/rel_join.cvc b/test/regress/regress0/sets/rels/rel_join.cvc new file mode 100644 index 000000000..7cce736f5 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join.cvc @@ -0,0 +1,26 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +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 a IS_IN (x JOIN y); +%ASSERT NOT (v IS_IN (x JOIN y)); +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_0.cvc b/test/regress/regress0/sets/rels/rel_join_0.cvc new file mode 100644 index 000000000..a251218c6 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_0.cvc @@ -0,0 +1,25 @@ +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 a IS_IN (x JOIN y); +%ASSERT NOT (v IS_IN (x JOIN y)); +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_0_1.cvc b/test/regress/regress0/sets/rels/rel_join_0_1.cvc new file mode 100644 index 000000000..70e35164a --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_0_1.cvc @@ -0,0 +1,26 @@ +% 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 (7, 5) IS_IN y; + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +%ASSERT a IS_IN (x JOIN y); +%ASSERT NOT (v IS_IN (x JOIN y)); +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_1.cvc b/test/regress/regress0/sets/rels/rel_join_1.cvc new file mode 100644 index 000000000..c8921afb9 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_1.cvc @@ -0,0 +1,31 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_1_1.cvc b/test/regress/regress0/sets/rels/rel_join_1_1.cvc new file mode 100644 index 000000000..3436bd707 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_1_1.cvc @@ -0,0 +1,31 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_2.cvc b/test/regress/regress0/sets/rels/rel_join_2.cvc new file mode 100644 index 000000000..cac7ce84d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_2.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_join_2_1.cvc new file mode 100644 index 000000000..3e27b9cc5 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_2_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose.cvc b/test/regress/regress0/sets/rels/rel_transpose.cvc new file mode 100644 index 000000000..10644d794 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE x)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_0.cvc b/test/regress/regress0/sets/rels/rel_transpose_0.cvc new file mode 100644 index 000000000..d06528fd2 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_0.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 z IS_IN x; +ASSERT NOT (zt IS_IN (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 new file mode 100644 index 000000000..bdcf31bb8 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_1.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1,2,3); +zt : IntTup; +ASSERT zt = (3,2,1); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE x)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc new file mode 100644 index 000000000..11653de04 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1,2,3); +zt : IntTup; +ASSERT zt = (3,2,1); +ASSERT z IS_IN x; +ASSERT zt IS_IN (TRANSPOSE x); +CHECKSAT; -- 2.30.2