Handle subtypes in sets. Bug fixes for tuples with subtypes.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index f11aa019e52ecc8f5600452b0ff114108b989824..720814aa8dfd803a5b08a2a2a46155f268c50071 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -539,6 +539,46 @@ TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){
   }
 }
 
+
+Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
+  TypeNode ntn = n.getType();
+  Assert( ntn.isComparableTo( tn ) );
+  if( !ntn.isSubtypeOf( tn ) ){
+    if( tn.isInteger() ){
+      if( tn.isSubtypeOf( ntn ) ){
+        return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n );
+      }
+    }else if( tn.isDatatype() && ntn.isDatatype() ){
+      if( tn.isTuple() && ntn.isTuple() ){
+        const Datatype& dt1 = tn.getDatatype();
+        const Datatype& dt2 = ntn.getDatatype();
+        if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
+          std::vector< Node > conds;
+          for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){
+            Node s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt2[0][i].getSelector() ), n );
+            Node etc = getEnsureTypeCondition( s, TypeNode::fromType( dt1[0][i].getRangeType() ) );
+            if( etc.isNull() ){
+              return Node::null();
+            }else{
+              conds.push_back( etc );
+            }
+          }
+          if( conds.empty() ){
+            return NodeManager::currentNM()->mkConst( true );
+          }else if( conds.size()==1 ){
+            return conds[0];
+          }else{
+            return NodeManager::currentNM()->mkNode( kind::AND, conds );
+          }
+        }
+      }
+    }
+    return Node::null();
+  }else{
+    return NodeManager::currentNM()->mkConst( true );
+  }
+}
+
 /** Is this a sort kind */
 bool TypeNode::isSort() const {
   return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0abbc9a1bcace2ad326a2500d590da12a2d99dd2..114b8a8eda5287b1985ad57991d1559b5d712209 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -651,6 +651,10 @@ public:
   static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
   static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
 
+  /** get ensure type condition 
+   *  Return value is a condition that implies that n has type tn.
+  */
+  static Node getEnsureTypeCondition( Node n, TypeNode tn );
 private:
   static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
 

diff --git a/src/options/sets_options b/src/options/sets_options
index 1c7e12a7d654bd05fd33fb3517e8abc7fea4a2d2..3e093cb8be376f95ba9ceca0c24768703c021514 100644 (file)
--- a/src/options/sets_options
+++ b/src/options/sets_options
@@ -14,4 +14,7 @@ option setsInferAsLemmas --sets-infer-as-lemmas bool :default true
 option setsRelEager --sets-rel-eager bool :default true
  standard effort checks for relations
  
+option setsExt --sets-ext bool :default false
+ enable extended symbols such as complement and universe in theory of sets
+ 
 endmodule

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 0d58233c9d82f111899627a044e41583fd21452b..30cdf8893d8c9ba1de6136e6f347d2bde18a5626 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -36,7 +36,8 @@ public:
     Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
 
     if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
-      Type t = in.getType().toType();
+      TypeNode tn = in.getType();
+      Type t = tn.toType();
       DatatypeType dt = DatatypeType(t);
       //check for parametric datatype constructors
       // to ensure a normal form, all parameteric datatype constructors must have a type ascription
@@ -58,6 +59,13 @@ public:
           return RewriteResponse(REWRITE_DONE, inr);
         }
       }
+      if( tn.isTuple() ){
+        Node nn = normalizeTupleConstructorApp( in );
+        if( nn!=in ){
+          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: Rewrite tuple constructor " << in << " to " << nn << std::endl;
+          return RewriteResponse(REWRITE_AGAIN_FULL, nn);
+        }
+      }
       if( in.isConst() ){
         Trace("datatypes-rewrite-debug") << "Normalizing constant " << in << std::endl;
         Node inn = normalizeConstant( in );
@@ -110,7 +118,7 @@ public:
       Expr constructorExpr = constructor.toExpr();
       size_t selectorIndex = Datatype::indexOf(selectorExpr);
       size_t constructorIndex = Datatype::indexOf(constructorExpr);
-      const Datatype& dt = Datatype::datatypeOf(constructorExpr);
+      const Datatype& dt = Datatype::datatypeOf(selectorExpr);
       const DatatypeConstructor& c = dt[constructorIndex];
       if(c.getNumArgs() > selectorIndex && c[selectorIndex].getSelector() == selectorExpr) {
         if( dt.isCodatatype() && in[0][selectorIndex].isConst() ){
@@ -235,15 +243,16 @@ public:
   static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
     Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
     if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
-      if( n1.getOperator() != n2.getOperator() ) {
-        Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
-        return true;
-      } else {
-        Assert( n1.getNumChildren() == n2.getNumChildren() );
-        for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
-          if( checkClash( n1[i], n2[i], rew ) ) {
-            return true;
-          }
+      if( n1.getOperator() != n2.getOperator()) {
+        if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){
+          Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
+          return true;
+        }
+      }
+      Assert( n1.getNumChildren() == n2.getNumChildren() );
+      for( unsigned i=0; i<n1.getNumChildren(); i++ ) {
+        if( checkClash( n1[i], n2[i], rew ) ) {
+          return true;
         }
       }
     }else if( n1!=n2 ){
@@ -601,11 +610,38 @@ public:
       return Node::null();
     }
   }
+  
+  static Node normalizeTupleConstructorApp( Node n ){
+    Assert( n.getType().isTuple() );
+    Assert( n.getKind()==kind::APPLY_CONSTRUCTOR );
+    const Datatype& dt = n.getType().getDatatype();
+    //may apply a different constructor based on child types
+    std::vector< TypeNode > cht;
+    std::vector< Node > ch;
+    bool childTypeChange = false;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      TypeNode tci = n[i].getType(); 
+      cht.push_back( tci );
+      ch.push_back( n[i] );
+      if( tci!=TypeNode::fromType( dt[0][i].getRangeType() ) ){
+        childTypeChange = true;
+      }
+    }
+    if( childTypeChange ){
+      TypeNode ttn = NodeManager::currentNM()->mkTupleType( cht );
+      const Datatype& dtt = ttn.getDatatype();
+      ch.insert( ch.begin(), Node::fromExpr( dtt[0].getConstructor() ) );
+      return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, ch );
+    }
+    return n;
+  }
   //normalize constant : apply to top-level codatatype constants
   static Node normalizeConstant( Node n ){
     TypeNode tn = n.getType();
     if( tn.isDatatype() ){
-      if( tn.isCodatatype() ){
+      if( tn.isTuple() ){
+        return normalizeTupleConstructorApp( n );
+      }else if( tn.isCodatatype() ){
         return normalizeCodatatypeConstant( n );
       }else{
         std::vector< Node > children;

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 8a440974da9c8038da64bac833a1f4fc6f5c14d4..412b3d7ecfdc1d9afed4953a27440957add38f5a 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -99,6 +99,19 @@ struct DatatypeConstructorTypeRule {
         return false;
       }
     }
+    //check whether it is in normal form?
+    TypeNode tn = n.getType();
+    if( tn.isTuple() ){
+      const Datatype& dt = tn.getDatatype();
+      //may be the wrong constructor, if children types are subtypes
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( n[i].getType()!=TypeNode::fromType( dt[0][i].getRangeType() ) ){
+          return false;
+        }
+      }
+    }else if( tn.isCodatatype() ){
+      //TODO?
+    }
     return true;
   }
 }; /* struct DatatypeConstructorTypeRule */

diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 96d682a774d8053ec74c391c2c2e857a19982075..636bfdb593fd602d3ccfe2c5d998567f5de74de8 100644 (file)
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -419,13 +419,16 @@ Node QuantifierMacros::simplify( Node n ){
           std::vector< Node > cond;
           TypeNode tno = op.getType();
           for( unsigned i=0; i<children.size(); i++ ){
-            if( !TermDb::getEnsureTypeCondition( children[i], tno[i], cond ) ){
+            Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] );
+            if( etc.isNull() ){
               //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, 
               //  and not ensuring it applies to n when its types are correct.
               //however, this should never fail: we never process types for which we cannot constuct conditions that ensure correct types, e.g. (is-int t).
               Assert( false );
               success = false;
               break;
+            }else if( !etc.isConst() ){
+              cond.push_back( etc );
             }
           }
           if( success ){

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 4f58f7a2e6c6e33aeaaffd07134c59e08890cfc5..5ac5ae0cceab802a98bb3ca59b997f97db5be6ff 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1839,20 +1839,6 @@ Node TermDb::ensureType( Node n, TypeNode tn ) {
   }
 }
 
-bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond ) {
-  TypeNode ntn = n.getType();
-  Assert( ntn.isComparableTo( tn ) );
-  if( !ntn.isSubtypeOf( tn ) ){
-    if( tn.isInteger() ){
-      cond.push_back( NodeManager::currentNM()->mkNode( IS_INTEGER, n ) );
-      return true;
-    }
-    return false;
-  }else{
-    return true;
-  }
-}
-
 void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) {
   if( n.getKind()==APPLY_SELECTOR_TOTAL ){
     unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr());

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5b29a72ce89758efb3f78a7a0d41d5128515aae7..c018172b520206e30614c4519d373ecf2460ab2e 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -473,8 +473,6 @@ public:
   bool containsVtsInfinity( Node n, bool isFree = false );
   /** ensure type */
   static Node ensureType( Node n, TypeNode tn );
-  /** get ensure type condition */
-  static bool getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond );
   /** get relevancy condition */
   static void getRelevancyCondition( Node n, std::vector< Node >& cond );
 private:

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index fe8f970c56a9a2103ed6775c681c35ef6fc26e7e..0338eb1b3c00b1d50e167426a57bf47f7b472c05 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -157,7 +157,7 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
         }
         if( add ){
           if( !s1.isNull() && s2.isNull() ){
-            Assert( m2[1].getType()==s1.getType() );
+            Assert( m2[1].getType().isComparableTo( s1.getType() ) );
             Assert( ee_areEqual( m2[1], s1 ) );
             Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 );
             if( s1.getKind()==kind::SINGLETON ){
@@ -518,6 +518,7 @@ void TheorySetsPrivate::fullEffortCheck(){
     Assert( d_equalityEngine.consistent() );
     d_sentLemma = false;
     d_addedFact = false;
+    d_full_check_incomplete = false;
     d_set_eqc.clear();
     d_set_eqc_list.clear();
     d_eqc_emptyset.clear();
@@ -526,6 +527,8 @@ void TheorySetsPrivate::fullEffortCheck(){
     d_congruent.clear();
     d_nvar_sets.clear();
     d_var_set.clear();
+    d_most_common_type.clear();
+    d_most_common_type_term.clear();
     d_pol_mems[0].clear();
     d_pol_mems[1].clear();
     d_members_index.clear();
@@ -543,9 +546,14 @@ void TheorySetsPrivate::fullEffortCheck(){
       Node eqc = (*eqcs_i);
       bool isSet = false;
       TypeNode tn = eqc.getType();
+      //common type node and term
+      TypeNode tnc;
+      Node tnct;
       if( tn.isSet() ){
         isSet = true;
         d_set_eqc.push_back( eqc );
+        tnc = tn.getSetElementType();
+        tnct = eqc;
       }
       Trace("sets-eqc") << "[" << eqc << "] : ";
       eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
@@ -554,6 +562,17 @@ void TheorySetsPrivate::fullEffortCheck(){
         if( n!=eqc ){
           Trace("sets-eqc") << n << " ";
         }
+        TypeNode tnn = n.getType();
+        if( isSet ){
+          Assert( tnn.isSet() );
+          TypeNode tnnel = tnn.getSetElementType();
+          tnc = TypeNode::mostCommonTypeNode( tnc, tnnel );
+          Assert( !tnc.isNull() );
+          //update the common type term
+          if( tnc==tnnel ){
+            tnct = n;
+          }
+        }
         if( n.getKind()==kind::MEMBER ){
           if( eqc.isConst() ){
             Node s = d_equalityEngine.getRepresentative( n[1] );
@@ -586,9 +605,15 @@ void TheorySetsPrivate::fullEffortCheck(){
               d_congruent[n] = d_singleton_index[r];
             }
           }else if( n.getKind()==kind::EMPTYSET ){
-            d_eqc_emptyset[tn] = eqc;
+            d_eqc_emptyset[tnn] = eqc;
           }else if( n.getKind()==kind::UNIVERSE_SET ){
-            d_eqc_univset[tn] = eqc;
+            if( options::setsExt() ){
+              d_eqc_univset[tnn] = eqc;
+            }else{
+              std::stringstream ss;
+              ss << "Symbols complement and universe set are not supported in default mode, try --sets-ext." << std::endl;
+              throw LogicException(ss.str());
+            }
           }else{
             Node r1 = d_equalityEngine.getRepresentative( n[0] );
             Node r2 = d_equalityEngine.getRepresentative( n[1] );
@@ -604,8 +629,8 @@ void TheorySetsPrivate::fullEffortCheck(){
           d_set_eqc_list[eqc].push_back( n );
         }else if( n.getKind()==kind::CARD ){
           d_card_enabled = true;
-          TypeNode tn = n[0].getType().getSetElementType();
-          if( tn.isInterpretedFinite() ){
+          TypeNode tnc = n[0].getType().getSetElementType();
+          if( tnc.isInterpretedFinite() ){
             std::stringstream ss;
             ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl;
             throw LogicException(ss.str());
@@ -631,6 +656,11 @@ void TheorySetsPrivate::fullEffortCheck(){
         }
         ++eqc_i;
       }
+      if( isSet ){
+        Assert( tnct.getType().getSetElementType()==tnc );
+        d_most_common_type[eqc] = tnc;
+        d_most_common_type_term[eqc] = tnct;
+      }
       Trace("sets-eqc") << std::endl;
       ++eqcs_i;
     }
@@ -655,46 +685,50 @@ void TheorySetsPrivate::fullEffortCheck(){
           Trace("sets-mem") << std::endl;
         }
       }
-    
-      checkDownwardsClosure( lemmas );
-      if( options::setsInferAsLemmas() ){
-        flushLemmas( lemmas );
-      }
+      checkSubtypes( lemmas );
+      flushLemmas( lemmas, true );
       if( !hasProcessed() ){
-        checkUpwardsClosure( lemmas );
-        flushLemmas( lemmas );
+      
+        checkDownwardsClosure( lemmas );
+        if( options::setsInferAsLemmas() ){
+          flushLemmas( lemmas );
+        }
         if( !hasProcessed() ){
-          std::vector< Node > intro_sets;
-          //for cardinality
-          if( d_card_enabled ){
-            checkCardBuildGraph( lemmas );
-            flushLemmas( lemmas );
-            if( !hasProcessed() ){
-              checkMinCard( lemmas );
+          checkUpwardsClosure( lemmas );
+          flushLemmas( lemmas );
+          if( !hasProcessed() ){
+            std::vector< Node > intro_sets;
+            //for cardinality
+            if( d_card_enabled ){
+              checkCardBuildGraph( lemmas );
               flushLemmas( lemmas );
               if( !hasProcessed() ){
-                checkCardCycles( lemmas );
+                checkMinCard( lemmas );
                 flushLemmas( lemmas );
                 if( !hasProcessed() ){
-                  checkNormalForms( lemmas, intro_sets );
+                  checkCardCycles( lemmas );
                   flushLemmas( lemmas );
+                  if( !hasProcessed() ){
+                    checkNormalForms( lemmas, intro_sets );
+                    flushLemmas( lemmas );
+                  }
                 }
               }
             }
-          }
-          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;
+              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;
+                }
               }
             }
           }
@@ -705,6 +739,36 @@ void TheorySetsPrivate::fullEffortCheck(){
   Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl;
 }
 
+void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) {
+ for( unsigned i=0; i<d_set_eqc.size(); i++ ){
+    Node s = d_set_eqc[i];
+    TypeNode mct = d_most_common_type[s];
+    std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
+    if( it!=d_pol_mems[0].end() ){
+      for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        if( !it2->first.getType().isSubtypeOf( mct ) ){          
+          Node mctt = d_most_common_type_term[s];
+          std::vector< Node > exp;
+          exp.push_back( it2->second );
+          Assert( ee_areEqual( mctt, it2->second[1] ) );
+          exp.push_back( mctt.eqNode( it2->second[1] ) );
+          Node etc = TypeNode::getEnsureTypeCondition( it2->first, mct );
+          if( !etc.isNull() ){
+            assertInference( etc, exp, lemmas, "subtype-clash" );
+            if( d_conflict ){
+              return;
+            } 
+          }else{
+            // very strange situation : we have a member in a set that is not a subtype, and we do not have a type condition for it
+            d_full_check_incomplete = true;
+            Trace("sets-incomplete") << "Sets : incomplete because of unknown type constraint." << std::endl;
+          }
+        }
+      }
+    }
+  }
+}
+
 void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
   Trace("sets") << "Downwards closure..." << std::endl;
   //downwards closure
@@ -869,30 +933,44 @@ 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 ){
-      //if equivalence class contains a variable
-      std::map< Node, Node >::iterator itv = d_var_set.find( it->first );
-      if( itv!=d_var_set.end() ){
-        TypeNode tn = it->first.getType();
-        std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn );
-        // if the universe does not yet exist, or is not in this equivalence class
-        if( itu==d_eqc_univset.end() || itu->second!=it->first ){
-          Node u = getUnivSet( tn );
+    if( options::setsExt() ){
+      //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 ){
+        //if equivalence class contains a variable
+        std::map< Node, Node >::iterator itv = d_var_set.find( it->first );
+        if( itv!=d_var_set.end() ){
+          //the variable in the equivalence class
           Node v = itv->second;
+          std::map< TypeNode, Node > univ_set;
           for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-            Assert( it2->second.getKind()==kind::MEMBER );
-            std::vector< Node > exp;
-            exp.push_back( it2->second );
-            if( v!=it2->second[1] ){
-              exp.push_back( v.eqNode( it2->second[1] ) );
+            Node e = it2->second[0];
+            TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() );
+            Node u;
+            std::map< TypeNode, Node >::iterator itu = univ_set.find( tn );
+            if( itu==univ_set.end() ){
+              std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn );
+              // if the universe does not yet exist, or is not in this equivalence class
+              if( itu==d_eqc_univset.end() || itu->second!=it->first ){
+                u = getUnivSet( tn );
+              }
+              univ_set[tn] = u;
+            }else{
+              u = itu->second;
             }
-            Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u );
-            assertInference( fact, exp, lemmas, "upuniv" );
-            if( d_conflict ){
-              return;
+            if( !u.isNull() ){
+              Assert( it2->second.getKind()==kind::MEMBER );
+              std::vector< Node > exp;
+              exp.push_back( it2->second );
+              if( v!=it2->second[1] ){
+                exp.push_back( v.eqNode( it2->second[1] ) );
+              }
+              Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u );
+              assertInference( fact, exp, lemmas, "upuniv" );
+              if( d_conflict ){
+                return;
+              }
             }
           }
         }
@@ -1494,22 +1572,24 @@ void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) {
   }
 }
 
-void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas ) {
-  //do lemmas
+void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas, bool preprocess ) {
   for( unsigned i=0; i<lemmas.size(); i++ ){
-    Node lem = lemmas[i];
-    if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){
-      Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
-      d_lemmas_produced.insert(lem);
-      d_external.d_out->lemma(lem);
-      d_sentLemma = true;
-    }else{
-      Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
-    }
+    flushLemma( lemmas[i], preprocess );
   }
   lemmas.clear();
 }
 
+void TheorySetsPrivate::flushLemma( Node lem, bool preprocess ) {
+  if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){
+    Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
+    d_lemmas_produced.insert(lem);
+    d_external.d_out->lemma(lem, false, preprocess);
+    d_sentLemma = true;
+  }else{
+    Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
+  }
+}
+
 Node TheorySetsPrivate::getProxy( Node n ) {
   if( n.getKind()==kind::EMPTYSET || n.getKind()==kind::SINGLETON || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::UNION ){
     NodeMap::const_iterator it = d_proxy.find( n );
@@ -1559,6 +1639,23 @@ Node TheorySetsPrivate::getUnivSet( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator it = d_univset.find( tn );
   if( it==d_univset.end() ){
     Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET);
+    for( it = d_univset.begin(); it != d_univset.end(); ++it ){
+      Node n1;
+      Node n2;
+      if( tn.isSubtypeOf( it->first ) ){
+        n1 = n;
+        n2 = it->second;
+      }else if( it->first.isSubtypeOf( tn ) ){
+        n1 = it->second;
+        n2 = n;
+      }
+      if( !n1.isNull() ){
+        Node ulem = NodeManager::currentNM()->mkNode( kind::SUBSET, n1, n2 );
+        Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl;
+        d_external.d_out->lemma( ulem );
+        d_sentLemma = true;
+      }
+    }
     d_univset[tn] = n;
     return n;
   }else{
@@ -1594,41 +1691,7 @@ void TheorySetsPrivate::debugPrintSet( Node s, const char * c ) {
 
 void TheorySetsPrivate::lastCallEffortCheck() {
   Trace("sets") << "----- Last call effort check ------" << std::endl;
-  /*
-  //FIXME : this is messy, have to see if constants are handled by the decision procedure, and not UF
-  TheoryModel * m = d_external.d_valuation.getModel();
-  //must process eliminated variables at last call effort when model is available
-  std::vector< Node > lemmas;
-  for(NodeBoolMap::const_iterator it=d_var_elim.begin(); it !=d_var_elim.end(); ++it) {
-    if( (*it).second ){
-      Node v = (*it).first;
-      Trace("sets-var-elim") << "Process eliminated variable : " << v << std::endl;
-      Node mv = m->getValue( v );
-      Trace("sets-var-elim") << "...value in model is : " << mv << std::endl;
-      Node u = getUnivSet( mv.getType() );
-      Node mvc = mv;
-      std::vector< Node > conj;
-      while( mvc.getKind()==kind::UNION ){
-        Node s = mvc[1];
-        Assert( s.getKind()==kind::SINGLETON );
-        conj.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, s[0], u ) );
-        mvc = mvc[0];
-      }
-      if( mvc.getKind()==kind::SINGLETON ){
-        conj.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, mvc[0], u ) );
-      }
-      if( !conj.empty() ){
-        Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::AND, conj );
-        // cannot add antecedant here since the eliminated variable v should not be reintroduced
-        //lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, v.eqNode(mv), lem );
-        Trace("sets-var-elim") << "...lemma is : " << lem << std::endl;
-        lemmas.push_back( lem );
-      }
-      d_var_elim[v] = false;
-    }
-  }
-  flushLemmas( lemmas );
-  */
+
 }
 
 /**************************** TheorySetsPrivate *****************************/
@@ -1659,12 +1722,17 @@ void TheorySetsPrivate::check(Theory::Effort level) {
         if( !d_conflict && !d_sentLemma ){
           //invoke relations solver
           d_rels->check(level);  
-          if( d_card_enabled && d_rels_enabled ){
-            //incomplete if we have both cardinality constraints and relational operators?
+          if( d_card_enabled && ( d_rels_enabled || options::setsExt() ) ){
+            //if cardinality constraints are enabled,
+            //  then model construction may fail in there are relational operators, or universe set.
             // TODO: should internally check model, return unknown if fail
-            d_external.d_out->setIncomplete();
+            d_full_check_incomplete = true;
+            Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl;
           }
         }
+        if( d_full_check_incomplete ){
+          d_external.d_out->setIncomplete();
+        }
       }
     }else{
       if( options::setsRelEager() ){
@@ -2094,22 +2162,21 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
 Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
   
-  //TODO: should allow variable elimination for sets
-  //      however, this makes universe set incorrect
+  //TODO: allow variable elimination for sets when setsExt = true
   
   //this is based off of Theory::ppAssert
   Node var;
   if (in.getKind() == kind::EQUAL) {
     if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
         (in[1].getType()).isSubtypeOf(in[0].getType()) ){
-      if( !in[0].getType().isSet() ){
+      if( !in[0].getType().isSet() || !options::setsExt() ){
         outSubstitutions.addSubstitution(in[0], in[1]);
         var = in[0];
         status = Theory::PP_ASSERT_STATUS_SOLVED;
       }
     }else if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
         (in[0].getType()).isSubtypeOf(in[1].getType())){
-      if( !in[1].getType().isSet() ){
+      if( !in[1].getType().isSet() || !options::setsExt() ){
         outSubstitutions.addSubstitution(in[1], in[0]);
         var = in[1];
         status = Theory::PP_ASSERT_STATUS_SOLVED;
@@ -2129,7 +2196,9 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
       d_var_elim[var] = true;
     } 
     */
-    Assert( !var.getType().isSet() ); 
+    if( options::setsExt() ){
+      Assert( !var.getType().isSet() ); 
+    }
   }
   return status;
 }

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index d11dff2afa9cde149094d15b6629386d42963330..667b7f2535c183d974a32191ed6426010d496b13 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -70,13 +70,15 @@ private:
   // send lemma ( n OR (NOT n) ) immediately
   void split( Node n, int reqPol=0 );
   void fullEffortCheck();
+  void checkSubtypes( std::vector< Node >& lemmas );
   void checkDownwardsClosure( std::vector< Node >& lemmas );
   void checkUpwardsClosure( std::vector< Node >& lemmas );
   void checkDisequalities( std::vector< Node >& lemmas );
   bool isMember( Node x, Node s );
   bool isSetDisequalityEntailed( Node s, Node t );
   
-  void flushLemmas( std::vector< Node >& lemmas );
+  void flushLemmas( std::vector< Node >& lemmas, bool preprocess = false );
+  void flushLemma( Node lem, bool preprocess = false );
   Node getProxy( Node n );
   Node getCongruent( Node n );
   Node getEmptySet( TypeNode tn );
@@ -114,6 +116,7 @@ private:
   
   bool d_sentLemma;
   bool d_addedFact;
+  bool d_full_check_incomplete;
   NodeMap d_proxy;  
   NodeMap d_proxy_to_term;  
   NodeSet d_lemmas_produced;
@@ -128,6 +131,8 @@ private:
   std::map< Node, Node > d_congruent;
   std::map< Node, std::vector< Node > > d_nvar_sets;
   std::map< Node, Node > d_var_set;
+  std::map< Node, TypeNode > d_most_common_type;
+  std::map< Node, Node > d_most_common_type_term;
   std::map< Node, std::map< Node, Node > > d_pol_mems[2];
   std::map< Node, std::map< Node, Node > > d_members_index;
   std::map< Node, Node > d_singleton_index;

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index a3abdf508356772fbd14da5ad4d328fee7ba5aad..7462847b69f2ac3ae10aae91a42c5dede5bedd4d 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -59,7 +59,15 @@ struct SetsBinaryOperatorTypeRule {
       }
       TypeNode secondSetType = n[1].getType(check);
       if(secondSetType != setType) {
-        throw TypeCheckingExceptionPrivate(n, "operator expects two sets of the same type");
+        if( n.getKind() == kind::INTERSECTION ){
+          setType = TypeNode::mostCommonTypeNode( secondSetType, setType );
+        }else{
+          setType = TypeNode::leastCommonTypeNode( secondSetType, setType );
+        }
+        if( setType.isNull() ){
+          throw TypeCheckingExceptionPrivate(n, "operator expects two sets of comparable types");
+        }
+        
       }
     }
     return setType;
@@ -88,7 +96,9 @@ struct SubsetTypeRule {
       }
       TypeNode secondSetType = n[1].getType(check);
       if(secondSetType != setType) {
-        throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types");
+        if( !setType.isComparableTo( secondSetType ) ){
+          throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types");
+        }
       }
     }
     return nodeManager->booleanType();
@@ -105,7 +115,7 @@ struct MemberTypeRule {
         throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
       }
       TypeNode elementType = n[0].getType(check);
-      if(!setType.getSetElementType().isSubtypeOf(elementType)) {
+      if(!elementType.isComparableTo(setType.getSetElementType())) {
         throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types");
       }
     }

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index d9db39b40ed52bf516bcdf781ef22bf21da6635d..caf1fc61c8dfeb7da97aed605b02dabad0c6cf40 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -79,7 +79,8 @@ TESTS =       \
        dt-sel-2.6.smt2 \
        dt-param-2.6.smt2 \
        dt-color-2.6.smt2 \
-       dt-match-pat-param-2.6.smt2
+       dt-match-pat-param-2.6.smt2 \
+       tuple-no-clash.cvc
 
 FAILING_TESTS = \
        datatype-dump.cvc

diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc b/test/regress/regress0/datatypes/tuple-no-clash.cvc
new file mode 100644 (file)
index 0000000..4d7345a
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc
@@ -0,0 +1,11 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+
+x : [ REAL, REAL ];
+y : REAL;
+z : REAL;
+
+ASSERT x = (y, z) OR x = (z, y);
+ASSERT x = (0,0) OR x = (1,1);
+
+CHECKSAT;

diff --git a/test/regress/regress0/rels/atom_univ2.cvc b/test/regress/regress0/rels/atom_univ2.cvc
index 9901ce630f2f9e329ee205539ea98e738cda215b..e01d99dee3fea0480388fb69cb7c65c1987b3c83 100644 (file)
--- a/test/regress/regress0/rels/atom_univ2.cvc
+++ b/test/regress/regress0/rels/atom_univ2.cvc
@@ -1,4 +1,5 @@
 % EXPECT: unsat\r
+OPTION "sets-ext";\r
 OPTION "logic" "ALL_SUPPORTED";\r
 Atom: TYPE;\r
 \r

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 9413dfba3c68b2eef8dd91364c76e8decd65f948..5ff24f1ff4ad5577220fbd88cffb0f51492e5a7f 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -81,7 +81,12 @@ TESTS =      \
   complement3.cvc \
   sharing-simp.smt2 \
   pre-proc-univ.smt2 \
-  nonvar-univ.smt2
+  nonvar-univ.smt2 \
+  sets-poly-int-real.smt2 \
+  sets-poly-nonint.smt2 \
+  int-real-univ.smt2 \
+  int-real-univ-unsat.smt2 \
+  sets-tuple-poly.cvc
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc
index 73eeb2cbd1775b6316035e324b0a4fb6a456943f..91388a56cad4ee239d510b2a3b76d1b4f9b771cf 100644 (file)
--- a/test/regress/regress0/sets/complement.cvc
+++ b/test/regress/regress0/sets/complement.cvc
@@ -1,4 +1,5 @@
 % EXPECT: sat
+OPTION "sets-ext";
 OPTION "logic" "ALL_SUPPORTED";
 Atom: TYPE;
 a : SET OF [Atom];

diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc
index 22dde0338eb0fb727d13dbaf9f2caa55f75ad814..b8100bf5f1b842805341d5f078fef5910f8926fa 100644 (file)
--- a/test/regress/regress0/sets/complement2.cvc
+++ b/test/regress/regress0/sets/complement2.cvc
@@ -1,4 +1,5 @@
 % EXPECT: unsat\r
+OPTION "sets-ext";\r
 OPTION "logic" "ALL_SUPPORTED";\r
 Atom: TYPE;\r
 a : SET OF Atom;\r

diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc
index ff527a9b3ca434a913e60b3ff4e5971b884cfe02..fa0a31e408d50592e27a92b7d8a8f076f6f4ad35 100644 (file)
--- a/test/regress/regress0/sets/complement3.cvc
+++ b/test/regress/regress0/sets/complement3.cvc
@@ -1,4 +1,5 @@
 % EXPECT: sat
+OPTION "sets-ext";
 OPTION "logic" "ALL_SUPPORTED";
 Atom : TYPE;
 C32 : SET OF [Atom];
@@ -11,4 +12,4 @@ ASSERT TUPLE(V1) IS_IN ~(C32);
 ASSERT ATOM_UNIV = UNIVERSE :: SET OF [Atom];
 ASSERT TUPLE(V1) IS_IN ATOM_UNIV;
 ASSERT TUPLE(V1) IS_IN ~(C2);
-CHECKSAT;
\ No newline at end of file
+CHECKSAT;

diff --git a/test/regress/regress0/sets/int-real-univ-unsat.smt2 b/test/regress/regress0/sets/int-real-univ-unsat.smt2
new file mode 100644 (file)
index 0000000..56f7e8c
--- /dev/null
+++ b/test/regress/regress0/sets/int-real-univ-unsat.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun a () (Set Real))
+
+(declare-fun x () Real)
+
+(assert (= (as univset (Set Real)) (as univset (Set Int))))
+
+(assert (member x a))
+
+(assert (and (<= 5.5 x) (< x 5.8)))
+
+(check-sat)

diff --git a/test/regress/regress0/sets/int-real-univ.smt2 b/test/regress/regress0/sets/int-real-univ.smt2
new file mode 100644 (file)
index 0000000..afe20b9
--- /dev/null
+++ b/test/regress/regress0/sets/int-real-univ.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun a () (Set Real))
+
+(declare-fun x () Real)
+
+(assert (= (as univset (Set Real)) (as univset (Set Int))))
+
+(assert (member x a))
+
+(assert (and (<= 5.5 x) (< x 6.1)))
+
+(check-sat)

diff --git a/test/regress/regress0/sets/nonvar-univ.smt2 b/test/regress/regress0/sets/nonvar-univ.smt2
index c71c984a238457a82ee94e4678bcbd43efc6b577..5c3bc567ca84537d6c9a3959f5a4a899a700c89f 100644 (file)
--- a/test/regress/regress0/sets/nonvar-univ.smt2
+++ b/test/regress/regress0/sets/nonvar-univ.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () (Set Int))

diff --git a/test/regress/regress0/sets/pre-proc-univ.smt2 b/test/regress/regress0/sets/pre-proc-univ.smt2
index 1b4bf8b41cdd77abb0b0c932fb4fe09ce61054f4..f184ebf9254c2250742b30578c86c92a51e1ba4f 100644 (file)
--- a/test/regress/regress0/sets/pre-proc-univ.smt2
+++ b/test/regress/regress0/sets/pre-proc-univ.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () (Set Int))

diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2
new file mode 100644 (file)
index 0000000..407e95d
--- /dev/null
+++ b/test/regress/regress0/sets/sets-poly-int-real.smt2
@@ -0,0 +1,17 @@
+(set-logic QF_UFLIRAFS)
+(set-info :status sat)
+(declare-fun s () (Set Real))
+(declare-fun t1 () (Set Real))
+(declare-fun t2 () (Set Real))
+(declare-fun t3 () (Set Real))
+(declare-fun r1 () (Set Int))
+(declare-fun r2 () (Set Int))
+(declare-fun r3 () (Set Int))
+(assert (and (member 1.5 s) (member 0 s)))
+(assert (= t1 (union s (singleton 2.5))))
+(assert (= t2 (union s (singleton 2))))
+(assert (= t3 (union r3 (singleton 2.5))))
+(assert (= (intersection r1 r2) (intersection s (singleton 0))))
+(assert (not (= r1 (as emptyset (Set Real)))))
+
+(check-sat)

diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2
new file mode 100644 (file)
index 0000000..441716d
--- /dev/null
+++ b/test/regress/regress0/sets/sets-poly-nonint.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UFLIRAFS)
+(set-info :status unsat)
+(declare-fun s () (Set Int))
+(declare-fun t () (Set Real))
+(declare-fun r () (Set Real))
+(declare-fun u () (Set Real))
+(assert (member 1.5 t))
+(assert (member 2.5 r))
+(assert (member 3.5 u))
+(assert (or (member 4.5 s) (= s t) (= s r) (= s u) (= s (singleton 6.5))))
+(check-sat)

diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc
new file mode 100644 (file)
index 0000000..8d87345
--- /dev/null
+++ b/test/regress/regress0/sets/sets-tuple-poly.cvc
@@ -0,0 +1,18 @@
+% EXPECT: sat
+OPTION "sets-ext";
+OPTION "logic" "ALL_SUPPORTED";
+
+a : SET OF [REAL, INT];
+b : SET OF [INT, REAL];
+
+x : [ REAL, REAL ];
+
+
+ASSERT NOT x = (0,0);
+
+ASSERT x IS_IN a;
+ASSERT x IS_IN b;
+
+ASSERT NOT x.0 = x.1;
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2
index ec975077632074453043ef7181cfb4b91545eb6c..a8875cc413d782112071cc1f56c6a6a13a74d02f 100644 (file)
--- a/test/regress/regress0/sets/univset-simp.smt2
+++ b/test/regress/regress0/sets/univset-simp.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sets-ext
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)