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.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 71857b7a58a2609b8e842fcc9fd01fa4019bb2e3..93fca232499131d017733c341a83f257a41d6797 100644 (file)
--- 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 b57f208bda9e60f7985e63146167a6973b9beb77..e708ad539a345dfb55e3653a7727df7de729cc70 100644 (file)
--- 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 48c81a13b9afab99c494dcaf78341f90131ece32..70cb56b8f57eab9806ff983fc5207fcdb43b52fa 100644 (file)
--- 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 (file)
index 0000000..86a1d93
--- /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)