Generalize finite bound inference to unifiable variables in set membership literals.

6 files changed, 113 insertions, 10 deletions

diff --git a/src/options/sets_options b/src/options/sets_options
index 52a8f78ba..1c7e12a7d 100644
--- a/src/options/sets_options
+++ b/src/options/sets_options
@@ -11,4 +11,7 @@ option setsProxyLemmas --sets-proxy-lemmas bool :default false
 option setsInferAsLemmas --sets-infer-as-lemmas bool :default true
  send inferences as lemmas
  
+option setsRelEager --sets-rel-eager bool :default true
+ standard effort checks for relations
+ 
 endmodule
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 1e8449dbf..09bb2dab3 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -212,6 +212,20 @@ bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< N
   return false;
 }
 
+void BoundedIntegers::processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==BOUND_VARIABLE && !isBound( q, n ) ){
+      bvs.push_back( n );
+    //injective operators
+    }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        processMatchBoundVars( q, n[i], bvs, visited );
+      }
+    }    
+  }
+}
+
 void BoundedIntegers::process( Node q, Node n, bool pol,
                                std::map< Node, unsigned >& bound_lit_type_map,
                                std::map< int, std::map< Node, Node > >& bound_lit_map,
@@ -314,11 +328,17 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
       }
     }
   }else if( n.getKind()==MEMBER ){
-    if( !pol && n[0].getKind()==BOUND_VARIABLE && !isBound( q, n[0] ) && !hasNonBoundVar( q, n[1] ) ){
-      Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
-      bound_lit_type_map[n[0]] = BOUND_SET_MEMBER;
-      bound_lit_map[2][n[0]] = n;
-      bound_lit_pol_map[2][n[0]] = pol;
+    if( !pol && !hasNonBoundVar( q, n[1] ) ){
+      std::vector< Node > bound_vars;
+      std::map< Node, bool > visited;
+      processMatchBoundVars( q, n[0], bound_vars, visited );
+      for( unsigned i=0; i<bound_vars.size(); i++ ){
+        Node v = bound_vars[i];
+        Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
+        bound_lit_type_map[v] = BOUND_SET_MEMBER;
+        bound_lit_map[2][v] = n;
+        bound_lit_pol_map[2][v] = pol;
+      }
     }
   }else{
     Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT );
@@ -450,7 +470,11 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
         if( d_bound_type[f][v]==BOUND_INT_RANGE ){
           Trace("bound-int") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
         }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
-          Trace("bound-int") << "  " << v << " in " << d_setm_range[f][v] << std::endl;
+          if( d_setm_range_lit[f][v][0]==v ){
+            Trace("bound-int") << "  " << v << " in " << d_setm_range[f][v] << std::endl;
+          }else{
+            Trace("bound-int") << "  " << v << " unifiable in " << d_setm_range_lit[f][v] << std::endl;
+          }
         }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
           Trace("bound-int") << "  " << v << " in { ";
           for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){ 
@@ -729,6 +753,33 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
   }
 }
 
+Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
+  if( t==v ){
+    return e;
+  }else if( t.getKind()==kind::APPLY_CONSTRUCTOR ){
+    if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
+      if( t.getOperator() != e.getOperator() ) {
+        return Node::null();
+      }
+    }
+    const Datatype& dt = Datatype::datatypeOf( t.getOperator().toExpr() );
+    unsigned index = Datatype::indexOf( t.getOperator().toExpr() );
+    for( unsigned i=0; i<t.getNumChildren(); i++ ){
+      Node u;
+      if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
+        u = matchBoundVar( v, t[i], e[i] );
+      }else{
+        Node se = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), e );
+        u = matchBoundVar( v, t[i], se );
+      }
+      if( !u.isNull() ){
+        return u;
+      }
+    }
+  }
+  return Node::null();
+}
+
 bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
   if( initial || !isGroundRange( q, v ) ){
     elements.clear();
@@ -768,6 +819,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
       }else{
         Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
         if( srv.getKind()!=EMPTYSET ){
+          //collect the elements
           while( srv.getKind()==UNION ){
             Assert( srv[1].getKind()==kind::SINGLETON );
             elements.push_back( srv[1][0] );
@@ -775,6 +827,21 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
           }
           Assert( srv.getKind()==kind::SINGLETON );
           elements.push_back( srv[0] );
+          //check if we need to do matching, for literals like ( tuple( v ) in S )
+          Node t = d_setm_range_lit[q][v][0];
+          if( t!=v ){
+            std::vector< Node > elements_tmp;
+            elements_tmp.insert( elements_tmp.end(), elements.begin(), elements.end() );
+            elements.clear();
+            for( unsigned i=0; i<elements_tmp.size(); i++ ){
+              //do matching to determine v -> u
+              Node u = matchBoundVar( v, t, elements_tmp[i] );
+              Trace("bound-int-rsi-debug") << "  unification : " << elements_tmp[i] << " = " << t << " yields " << v << " -> " << u << std::endl;
+              if( !u.isNull() ){
+                elements.push_back( u );
+              }
+            }
+          }
         }
         return true;
       }
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 5c5a52855..f367b328c 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -74,6 +74,7 @@ private:
                 std::map< int, std::map< Node, Node > >& bound_int_range_term,
                 std::map< Node, std::vector< Node > >& bound_fixed_set );
   bool processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases );
+  void processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited );
   std::vector< Node > d_bound_quants;
 private:
   class RangeModel {
@@ -164,6 +165,7 @@ private:
   //for set range
   Node getSetRange( Node q, Node v, RepSetIterator * rsi );
   Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi );
+  Node matchBoundVar( Node v, Node t, Node e );
   
   bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
 public:
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 40da5d7d0..d3c596664 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -90,7 +90,9 @@ void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
     EqcInfo * e = getOrMakeEqcInfo( t, true );
     e->d_singleton = t;
   }
-  d_rels->eqNotifyNewClass( t );
+  if( options::setsRelEager() ){
+    d_rels->eqNotifyNewClass( t );
+  }
 }
 
 void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){
@@ -183,7 +185,9 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
       }
       d_members[t1] = n_members;
     }
-    d_rels->eqNotifyPostMerge( t1, t2 );
+    if( options::setsRelEager() ){
+      d_rels->eqNotifyPostMerge( t1, t2 );
+    }
   }
 }
 
@@ -1532,7 +1536,7 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     fullEffortCheck();
   }
   // invoke the relational solver
-  if( !d_conflict && !d_sentLemma ){
+  if( !d_conflict && !d_sentLemma && ( level == Theory::EFFORT_FULL || options::setsRelEager() ) ){
     d_rels->check(level);  
     //incomplete if we have both cardinality constraints and relational operators?
     // TODO: should internally check model, return unknown if fail
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 03fe780b8..af8776ace 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -64,7 +64,8 @@ TESTS =	\
 	fmf-bound-2dim.smt2 \
 	memory_model-R_cpp-dd.cvc \
 	bug764.smt2 \
-	ko-bound-set.cvc
+	ko-bound-set.cvc \
+	cons-sets-bounds.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/cons-sets-bounds.smt2 b/test/regress/regress0/fmf/cons-sets-bounds.smt2
new file mode 100644
index 000000000..db9788a61
--- /dev/null
+++ b/test/regress/regress0/fmf/cons-sets-bounds.smt2
@@ -0,0 +1,26 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(declare-datatypes () ((list (cons (head Int) (tail list)) (nil))))
+
+(declare-fun P (Int) Bool)
+(declare-fun S () (Set list))
+
+; can use simple unification to infer bounds on x and y
+(assert (forall ((x Int) (y list)) (=> (member (cons x y) S) (P x))))
+
+(assert (member (cons 4 (cons 1 nil)) S))
+(assert (member (cons 2 nil) S))
+
+; should construct instantiation involving selectors for l 
+(declare-fun l () list)
+(assert (is-cons l))
+(assert (member l S))
+
+; should not contribute to instantiations
+(assert (member nil S))
+
+(assert (not (P 1)))
+(assert (not (P 0)))
+
+(check-sat)