Sets subtypes (#1095)

Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.

4 files changed, 52 insertions, 9 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 71857b7a5..93fca2324 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -738,22 +738,21 @@ void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) {
     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 ) ){          
+        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() ){
+          Node tc_k = getTypeConstraintSkolem(it2->first, mct);
+          if (!tc_k.isNull())
+          {
+            Node etc = tc_k.eqNode(it2->first);
             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;
+            }
           }
         }
       }
@@ -1686,6 +1685,18 @@ void TheorySetsPrivate::lastCallEffortCheck() {
 
 }
 
+Node TheorySetsPrivate::getTypeConstraintSkolem(Node n, TypeNode tn)
+{
+  std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
+  if (it == d_tc_skolem[n].end())
+  {
+    Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
+    d_tc_skolem[n][tn] = k;
+    return k;
+  }
+  return it->second;
+}
+
 /**************************** TheorySetsPrivate *****************************/
 /**************************** TheorySetsPrivate *****************************/
 /**************************** TheorySetsPrivate *****************************/
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index b57f208bd..e708ad539 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -158,7 +158,24 @@ private:
 private: //for universe set
   NodeBoolMap d_var_elim;
   void lastCallEffortCheck();
-public:
+
+ private:
+  /** type constraint skolems
+   *
+   * The sets theory solver outputs equality lemmas of the form:
+   *   n = d_tc_skolem[n][tn]
+   * where the type of d_tc_skolem[n][tn] is tn, and the type
+   * of n is not a subtype of tn. This is required to handle benchmarks like
+   *   test/regress/regress0/sets/sets-of-sets-subtypes.smt2
+   * where for s : (Set Int) and t : (Set Real), we have that
+   *   ( s = t ^ y in t ) implies ( exists k : Int. y = k )
+   * The type constraint Skolem for (y, Int) is the skolemization of k above.
+   */
+  std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
+  /** get type constraint skolem for n and tn */
+  Node getTypeConstraintSkolem(Node n, TypeNode tn);
+
+ public:
 
   /**
    * Constructs a new instance of TheorySetsPrivate w.r.t. the provided
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 48c81a13b..70cb56b8f 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -744,6 +744,7 @@ REG0_TESTS = \
 	regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 \
 	regress0/sets/sets-equal.smt2 \
 	regress0/sets/sets-inter.smt2 \
+	regress0/sets/sets-of-sets-subtypes.smt2 \
 	regress0/sets/sets-poly-int-real.smt2 \
 	regress0/sets/sets-poly-nonint.smt2 \
 	regress0/sets/sets-sample.smt2 \
diff --git a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2
new file mode 100644
index 000000000..86a1d93b4
--- /dev/null
+++ b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_LIRAFS)
+(set-info :status unsat)
+
+(declare-fun s () (Set (Set Real)))
+(declare-fun t () (Set (Set Int)))
+
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Real))
+
+(assert (member 0.5 y))
+(assert (member y s))
+(assert (or (= s t) (= s (singleton (singleton 1.0))) (= s (singleton (singleton 0.0)))))
+
+(check-sat)