Support for set compliment and universe set. Simplify approach for sep.nil nodes.

9 files changed, 99 insertions, 48 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d394c8fef..6b4b67a26 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -137,7 +137,7 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
 Node TermDb::getMatchOperator( Node n ) {
   Kind k = n.getKind();
   //datatype operators may be parametric, always assume they are
-  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
+  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT ||
       k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index cca6543b6..efd80a83c 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -353,7 +353,7 @@ bool Trigger::isAtomicTrigger( Node n ){
 bool Trigger::isAtomicTriggerKind( Kind k ) {
   return k==APPLY_UF || k==SELECT || k==STORE ||
          k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
-         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
+         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT ||
          k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR;
 }
 
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 5cd9093f4..358c63f55 100644
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -12,13 +12,6 @@ properties check propagate presolve getNextDecisionRequest
 
 rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h"
 
-# constants
-constant SEP_NIL_REF \
-    ::CVC4::NilRef \
-    ::CVC4::NilRefHashFunction \
-    "expr/sepconst.h" \
-    "the nil reference constant; payload is an instance of the CVC4::NilRef class"
-
 variable SEP_NIL "separation nil"
 
 operator SEP_EMP 2 "separation empty heap"
@@ -27,7 +20,6 @@ operator SEP_STAR 2: "separation star"
 operator SEP_WAND 2 "separation magic wand"
 operator SEP_LABEL 2 "separation label (internal use only)"
 
-typerule SEP_NIL_REF ::CVC4::theory::sep::SepNilRefTypeRule
 typerule SEP_EMP ::CVC4::theory::sep::SepEmpTypeRule
 typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule
 typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule
diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index 7d4eb303e..23e725a25 100644
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -25,14 +25,6 @@ namespace CVC4 {
 namespace theory {
 namespace sep {
 
-class SepNilRefTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
-    return TypeNode::fromType( n.getConst<NilRef>().getType() );
-  }
-};
-
 class SepEmpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
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) {