diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:03 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:20 -0600 |
commit | d73fdfe7e1fe071670a7e5f843c7609db290b63e (patch) | |
tree | ff8ad52565f6a149689668f74957292486b2eeab /src/theory/sets | |
parent | 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 (diff) |
Support for set compliment and universe set. Simplify approach for sep.nil nodes.
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/kinds | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 69 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 3 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 30 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 21 |
5 files changed, 97 insertions, 30 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index c92eab4bd..53905e47f 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -43,6 +43,7 @@ operator MEMBER 2 "set membership predicate; first parameter a member of 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 COMPLIMENT 1 "set compliment (with respect to finite universe)" operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" @@ -58,12 +59,14 @@ typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule typerule INSERT ::CVC4::theory::sets::InsertTypeRule typerule CARD ::CVC4::theory::sets::CardTypeRule +typerule COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +variable UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it." construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -71,6 +74,7 @@ construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule construle INSERT ::CVC4::theory::sets::InsertTypeRule construle CARD ::CVC4::theory::sets::CardTypeRule +construle COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index e78575791..e71333075 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -508,6 +508,7 @@ void TheorySetsPrivate::fullEffortCheck(){ d_set_eqc.clear(); d_set_eqc_list.clear(); d_eqc_emptyset.clear(); + d_eqc_univset.clear(); d_eqc_singleton.clear(); d_congruent.clear(); d_nvar_sets.clear(); @@ -557,7 +558,8 @@ void TheorySetsPrivate::fullEffortCheck(){ Assert( false ); } } - }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET ){ + }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION || + n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET || n.getKind()==kind::UNIVERSE_SET ){ if( n.getKind()==kind::SINGLETON ){ //singleton lemma getProxy( n ); @@ -571,6 +573,8 @@ void TheorySetsPrivate::fullEffortCheck(){ } }else if( n.getKind()==kind::EMPTYSET ){ d_eqc_emptyset[tn] = eqc; + }else if( n.getKind()==kind::UNIVERSE_SET ){ + d_eqc_univset[tn] = eqc; }else{ Node r1 = d_equalityEngine.getRepresentative( n[0] ); Node r2 = d_equalityEngine.getRepresentative( n[1] ); @@ -641,8 +645,9 @@ void TheorySetsPrivate::fullEffortCheck(){ checkUpwardsClosure( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ + std::vector< Node > intro_sets; + //for cardinality if( d_card_enabled ){ - //for cardinality checkCardBuildGraph( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ @@ -652,28 +657,27 @@ void TheorySetsPrivate::fullEffortCheck(){ checkCardCycles( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ - std::vector< Node > intro_sets; checkNormalForms( lemmas, intro_sets ); flushLemmas( lemmas ); - if( !hasProcessed() ){ - checkDisequalities( lemmas ); - flushLemmas( lemmas ); - if( !hasProcessed() && !intro_sets.empty() ){ - Assert( intro_sets.size()==1 ); - Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl; - Trace("sets-intro") << " Actual Intro : "; - debugPrintSet( intro_sets[0], "sets-nf" ); - Trace("sets-nf") << std::endl; - Node k = getProxy( intro_sets[0] ); - d_sentLemma = true; - } - } } } } - }else{ + } + if( !hasProcessed() ){ checkDisequalities( lemmas ); flushLemmas( lemmas ); + if( !hasProcessed() ){ + //introduce splitting on venn regions (absolute last resort) + if( d_card_enabled && !hasProcessed() && !intro_sets.empty() ){ + Assert( intro_sets.size()==1 ); + Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl; + Trace("sets-intro") << " Actual Intro : "; + debugPrintSet( intro_sets[0], "sets-nf" ); + Trace("sets-nf") << std::endl; + Node k = getProxy( intro_sets[0] ); + d_sentLemma = true; + } + } } } } @@ -682,7 +686,6 @@ void TheorySetsPrivate::fullEffortCheck(){ Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl; } - void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) { Trace("sets") << "Downwards closure..." << std::endl; //downwards closure @@ -837,6 +840,26 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { } } } + if( !hasProcessed() ){ + //universal sets + Trace("sets-debug") << "Check universe sets..." << std::endl; + //all elements must be in universal set + for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){ + TypeNode tn = it->first.getType(); + std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn ); + if( itu==d_eqc_univset.end() || itu->second!=it->first ){ + Node u = getUnivSet( tn ); + for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + Node mem = it2->second; + Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], u ); + assertInference( fact, mem, lemmas, "upuniv" ); + if( d_conflict ){ + return; + } + } + } + } + } } void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) { @@ -1493,6 +1516,16 @@ Node TheorySetsPrivate::getEmptySet( TypeNode tn ) { return it->second; } } +Node TheorySetsPrivate::getUnivSet( TypeNode tn ) { + std::map< TypeNode, Node >::iterator it = d_univset.find( tn ); + if( it==d_univset.end() ){ + Node n = NodeManager::currentNM()->mkUniqueVar(tn, kind::UNIVERSE_SET); + d_univset[tn] = n; + return n; + }else{ + return it->second; + } +} bool TheorySetsPrivate::hasLemmaCached( Node lem ) { return d_lemmas_produced.find(lem)!=d_lemmas_produced.end(); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 1c9a7e22a..6d7b57cc6 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -79,6 +79,7 @@ private: Node getProxy( Node n ); Node getCongruent( Node n ); Node getEmptySet( TypeNode tn ); + Node getUnivSet( TypeNode tn ); bool hasLemmaCached( Node lem ); bool hasProcessed(); @@ -119,8 +120,10 @@ private: std::map< Node, bool > d_set_eqc_relevant; std::map< Node, std::vector< Node > > d_set_eqc_list; std::map< TypeNode, Node > d_eqc_emptyset; + std::map< TypeNode, Node > d_eqc_univset; std::map< Node, Node > d_eqc_singleton; std::map< TypeNode, Node > d_emptyset; + std::map< TypeNode, Node > d_univset; std::map< Node, Node > d_congruent; std::map< Node, std::vector< Node > > d_nvar_sets; std::map< Node, std::map< Node, Node > > d_pol_mems[2]; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index aaf71e8fc..da4f8fb7a 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -219,7 +219,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::EMPTYSET) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; - return RewriteResponse(REWRITE_DONE, node[0]); + return RewriteResponse(REWRITE_AGAIN, node[0]); + }else if( node[1].getKind() == kind::UNIVERSE_SET ){ + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType()))); } else if(node[0].isConst() && node[1].isConst()) { std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); @@ -237,11 +239,11 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case kind::INTERSECTION: { if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; - return RewriteResponse(REWRITE_DONE, node[0]); - } else if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[0]); - } else if(node[1].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[1]); + return RewriteResponse(REWRITE_AGAIN, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[0]); + } else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[1]); } else if(node[0].isConst() && node[1].isConst()) { std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); @@ -276,11 +278,11 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { // NOTE: case where it is CONST is taken care of at the top if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; - return RewriteResponse(REWRITE_DONE, node[0]); - } else if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[1]); - } else if(node[1].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[0]); + return RewriteResponse(REWRITE_AGAIN, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[1]); + } else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[0]); } else if(node[0].isConst() && node[1].isConst()) { std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); @@ -303,7 +305,11 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } break; }//kind::UNION - + case kind::COMPLIMENT: { + Node univ = NodeManager::currentNM()->mkUniqueVar( node[0].getType(), kind::UNIVERSE_SET ); + return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) ); + } + break; case kind::CARD: { if(node[0].isConst()) { std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 89d481746..66e06b038 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -155,6 +155,27 @@ struct CardTypeRule { } };/* struct CardTypeRule */ +struct ComplimentTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::COMPLIMENT); + TypeNode setType = n[0].getType(check); + if( check ) { + if(!setType.isSet()) { + throw TypeCheckingExceptionPrivate(n, "compliment operates on a set, non-set object found"); + } + } + return setType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::COMPLIMENT); + return false; + } +};/* struct ComplimentTypeRule */ + + + struct InsertTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { |