From 39457da86ec7d5617804bb2b311cf59b497f1186 Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Mon, 29 Feb 2016 23:23:50 -0600 Subject: [PATCH] adapted the solver to accept sets of built-in types (int, string, real) use dummy lemmas to find tuple elements equality --- src/theory/sets/theory_sets_rels.cpp | 155 +++++++++++++---------- src/theory/sets/theory_sets_rels.h | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 12 ++ src/theory/sets/theory_sets_type_rules.h | 64 +++++++--- 4 files changed, 150 insertions(+), 83 deletions(-) diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 2b35fb077..ec2d28fa6 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -108,11 +108,11 @@ typedef std::map >::iterator mem_it; if(getRepresentative(r) == getRepresentative(d_trueNode) || getRepresentative(r) == getRepresentative(d_falseNode)) { // collect membership info - if(n.getKind() == kind::MEMBER && n[0].getType().isTuple()) { + if(n.getKind() == kind::MEMBER) { Node tup_rep = getRepresentative(n[0]); Node rel_rep = getRepresentative(n[1]); // No rel_rep is found - if(d_membership_cache.find(rel_rep) == d_membership_cache.end()) { + if( d_membership_cache.find(rel_rep) == d_membership_cache.end() ) { std::vector tups; tups.push_back(tup_rep); d_membership_cache[rel_rep] = tups; @@ -122,9 +122,9 @@ typedef std::map >::iterator mem_it; tups.clear(); tups.push_back(exp); d_membership_exp_cache[rel_rep] = tups; - } else if(std::find(d_membership_cache.at(rel_rep).begin(), - d_membership_cache.at(rel_rep).end(), tup_rep) - == d_membership_cache.at(rel_rep).end()) { + } else if( std::find(d_membership_cache[rel_rep].begin(), + d_membership_cache[rel_rep].end(), tup_rep) + == d_membership_cache[rel_rep].end() ) { d_membership_cache[rel_rep].push_back(tup_rep); Node exp = n; if(getRepresentative(r) == getRepresentative(d_falseNode)) @@ -133,22 +133,22 @@ typedef std::map >::iterator mem_it; } } // collect term info - } else if(r.getType().isSet() && r.getType().getSetElementType().isTuple()) { - if(n.getKind() == kind::TRANSPOSE || - n.getKind() == kind::JOIN || - n.getKind() == kind::PRODUCT || - n.getKind() == kind::TRANSCLOSURE) { + } else if( r.getType().isSet() ) { + if( n.getKind() == kind::TRANSPOSE || + n.getKind() == kind::JOIN || + n.getKind() == kind::PRODUCT || + n.getKind() == kind::TRANSCLOSURE ) { std::map > rel_terms; std::vector terms; // No r record is found - if(d_terms_cache.find(r) == d_terms_cache.end()) { + if( d_terms_cache.find(r) == d_terms_cache.end() ) { terms.push_back(n); rel_terms[n.getKind()] = terms; d_terms_cache[r] = rel_terms; } else { rel_terms = d_terms_cache[r]; // No n's kind record is found - if(rel_terms.find(n.getKind()) == rel_terms.end()) { + if( rel_terms.find(n.getKind()) == rel_terms.end() ) { terms.push_back(n); rel_terms[n.getKind()] = terms; } else { @@ -228,8 +228,8 @@ typedef std::map >::iterator mem_it; Node r1 = join_term[0]; Node r2 = join_term[1]; - // case: (a, b) IS_IN (X JOIN Y) - // => (a, z) IS_IN X && (z, b) IS_IN Y + // join-split rule: (a, b) IS_IN (X JOIN Y) + // => (a, z) IS_IN X && (z, b) IS_IN Y if(polarity) { Debug("rels-join") << "[sets-rels] Join rules (a, b) IS_IN (X JOIN Y) => " "((a, z) IS_IN X && (z, b) IS_IN Y)"<< std::endl; @@ -386,6 +386,7 @@ typedef std::map >::iterator mem_it; 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 << "\n r1_rep: " << r1_rep @@ -395,8 +396,6 @@ typedef std::map >::iterator mem_it; d_membership_cache.find(r2_rep) == d_membership_cache.end()) return; - TypeNode tn = n.getType().getSetElementType(); - Datatype dt = tn.getDatatype(); std::vector new_tups; std::vector new_exps; std::vector r1_elements = d_membership_cache[r1_rep]; @@ -405,28 +404,47 @@ typedef std::map >::iterator mem_it; std::vector r2_exps = d_membership_exp_cache[r2_rep]; Node new_rel = n.getKind() == kind::JOIN ? NodeManager::currentNM()->mkNode(kind::JOIN, r1_rep, r2_rep) : NodeManager::currentNM()->mkNode(kind::PRODUCT, r1_rep, r2_rep); - unsigned int t1_len = r1_elements.front().getType().getTupleLength(); - unsigned int t2_len = r2_elements.front().getType().getTupleLength(); - + unsigned int t1_len = 1; + unsigned int t2_len = 1; + if(r1_elements.front().getType().isTuple()) + t1_len = r1_elements.front().getType().getTupleLength(); + if(r2_elements.front().getType().isTuple()) + 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 joinedTuple; - joinedTuple.push_back(Node::fromExpr(dt[0].getConstructor())); - if((areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]) && n.getKind() == kind::JOIN) || - n.getKind() == kind::PRODUCT) { + + std::vector composedTuple; + TypeNode tn = n.getType().getSetElementType(); + if(tn.isTuple()) { + composedTuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + } + Node r1_e = r1_elements[i]; + Node r2_e = r2_elements[j]; + if(r1_e.getType().isTuple()) + r1_e = r1_elements[i][t1_len-1]; + if(r2_e.getType().isTuple()) + r2_e = r2_elements[j][0]; + + if((areEqual(r1_e, r2_e) && n.getKind() == kind::JOIN) || + n.getKind() == kind::PRODUCT) { unsigned int k = 0; unsigned int l = 1; for(; k < t1_len - 1; ++k) { - joinedTuple.push_back(r1_elements[i][k]); + composedTuple.push_back(r1_elements[i][k]); } if(kind::PRODUCT == n.getKind()) { - joinedTuple.push_back(r1_elements[i][k]); - joinedTuple.push_back(r1_elements[j][0]); + composedTuple.push_back(r1_elements[i][k]); + composedTuple.push_back(r1_elements[j][0]); } for(; l < t2_len; ++l) { - joinedTuple.push_back(r2_elements[j][l]); + composedTuple.push_back(r2_elements[j][l]); + } + Node fact; + if(tn.isTuple()) { + fact = nm->mkNode(kind::APPLY_CONSTRUCTOR, composedTuple); + } else { + fact = composedTuple[0]; } - Node fact = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, joinedTuple); new_tups.push_back(fact); fact = MEMBER(fact, new_rel); std::vector reasons; @@ -435,7 +453,7 @@ typedef std::map >::iterator mem_it; //Todo: think about how to deal with shared terms(?) if(n.getKind() == kind::JOIN) - reasons.push_back(EQUAL(r1_elements[i][t1_len-1], r2_elements[j][0])); + reasons.push_back(EQUAL(r1_e, r2_e)); if(r1 != r1_rep) { reasons.push_back(EQUAL(r1, r1_rep)); @@ -500,8 +518,9 @@ typedef std::map >::iterator mem_it; d_lemma_cache.push_back( lemma_or ); } - void TheorySetsRels::sendLemma(Node fact, Node reason, bool polarity) { - + void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { + Trace("rels-lemma") << "[sets-rels] Infer " << conc << " from " << ant << " by " << c << std::endl; + d_lemma_cache.push_back(conc); } void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) { @@ -549,47 +568,55 @@ typedef std::map >::iterator mem_it; bool TheorySetsRels::areEqual( Node a, Node b ){ if( hasTerm( a ) && hasTerm( b ) ){ - 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; - } - } +// 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; + Node x = NodeManager::currentNM()->mkSkolem( "sde", a.getType() ); + Node y = NodeManager::currentNM()->mkSkolem( "sde", b.getType() ); + Node set_a = NodeManager::currentNM()->mkNode( kind::SINGLETON, a ); + Node set_b = NodeManager::currentNM()->mkNode( kind::SINGLETON, b ); + Node dummy_lemma_1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, set_a ); + Node dummy_lemma_2 = NodeManager::currentNM()->mkNode( kind::MEMBER, y, set_b ); + sendLemma( dummy_lemma_1, d_trueNode, "dummy-lemma" ); + sendLemma( dummy_lemma_2, d_trueNode, "dummy-lemma" ); addSharedTerm(a); addSharedTerm(b); - sendSplit(a, b, "tuple-element-equality"); +// sendSplit(a, b, "tuple-element-equality"); return false; } } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index d0d926e69..16329fd43 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -82,7 +82,7 @@ private: Node reverseTuple( Node ); void sendInfer( Node fact, Node exp, const char * c ); - void sendLemma( Node fact, Node reason, bool polarity ); + void sendLemma( Node fact, Node reason, const char * c ); void sendSplit( Node a, Node b, const char * c ); void doPendingFacts(); void doPendingSplitFacts(); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index dac554d4f..8b639a2e5 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -64,6 +64,16 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } if(node[1].getKind() == kind::TRANSPOSE) { // only work for node[0] is an actual tuple like (a, b), won't work for tuple variables + if(node[0].getType().isSet() && !node[0].getType().getSetElementType().isTuple()) { + Node atom = node; + bool polarity = node.getKind() != kind::NOT; + if( !polarity ) + atom = atom[0]; + Node new_node = NodeManager::currentNM()->mkNode(kind::MEMBER, atom[0], atom[1][0]); + if(!polarity) + new_node = new_node.negate(); + return RewriteResponse(REWRITE_AGAIN, new_node); + } if(node[0].isVar()) return RewriteResponse(REWRITE_DONE, node); std::vector elements; @@ -198,6 +208,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { }//kind::UNION case kind::TRANSPOSE: { + if(node[0].getType().isSet() && !node[0].getType().getSetElementType().isTuple()) + return RewriteResponse(REWRITE_AGAIN, node[0]); if(node[0].getKind() != kind::TRANSPOSE) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 0909d8442..6a606ef5c 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -179,35 +179,60 @@ struct RelBinaryOperatorTypeRule { 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)"); - } +// if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) { +// throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)"); +// } std::vector newTupleTypes; - std::vector firstTupleTypes = firstRelType[0].getTupleTypes(); - std::vector secondTupleTypes = secondRelType[0].getTupleTypes(); + TypeNode set_element_type_1 = firstRelType.getSetElementType(); + TypeNode set_element_type_2 = secondRelType.getSetElementType(); + std::vector firstTupleTypes; + std::vector secondTupleTypes; + // JOIN is not allowed to apply on two unary sets - if(n.getKind() == kind::JOIN) { - if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) { + if( n.getKind() == kind::JOIN ) { + if( !set_element_type_1.isTuple() && !set_element_type_2.isTuple()) { throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations"); - } - if(firstTupleTypes.back() != secondTupleTypes.front()) { - throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations"); - } - - if(firstTupleTypes.size() == 1) { + } else if ( !set_element_type_1.isTuple() ) { + secondTupleTypes = set_element_type_2.getTupleTypes(); + if(set_element_type_1 != secondTupleTypes.front()) { + throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations"); + } newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end()); - } else if (secondTupleTypes.size() == 1) { + } else if ( !set_element_type_2.isTuple() ) { + firstTupleTypes = set_element_type_1.getTupleTypes(); + if(set_element_type_2 != firstTupleTypes.front()) { + throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations"); + } newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1); } else { + firstTupleTypes = set_element_type_1.getTupleTypes(); + secondTupleTypes = set_element_type_2.getTupleTypes(); + 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) { + }else if( n.getKind() == kind::PRODUCT ) { + if( !set_element_type_1.isTuple() ) { + firstTupleTypes.push_back(set_element_type_1); + } else { + firstTupleTypes = set_element_type_1.getTupleTypes(); + } + if( !set_element_type_2.isTuple() ) { + secondTupleTypes.push_back(set_element_type_2); + } else { + secondTupleTypes = set_element_type_2.getTupleTypes(); + } newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()); newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end()); } - resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); + Assert(newTupleTypes.size() >= 1); + if(newTupleTypes.size() > 1) + resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); + else + resultType = nodeManager->mkSetType(newTupleTypes[0]); } return resultType; } @@ -223,17 +248,20 @@ 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[0].isTuple()) { + if(check && !setType.isSet()) { throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-relation"); } + if(!setType.getSetElementType().isTuple()) + return setType; std::vector tupleTypes; std::vector originalTupleTypes = setType[0].getTupleTypes(); for(std::vector::reverse_iterator it = originalTupleTypes.rbegin(); it != originalTupleTypes.rend(); ++it) { tupleTypes.push_back(*it); } - return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); } -- 2.30.2