Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction.

5 files changed, 88 insertions, 28 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 4ca631184..1a466ff8a 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1222,6 +1222,42 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
   eqc->d_constructor.set( c );
 }
 
+Node TheoryDatatypes::removeUninterpretedConstants( Node n, std::map< Node, Node >& visited ){
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( it==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==UNINTERPRETED_CONSTANT ){
+      std::map< Node, Node >::iterator itu = d_uc_to_fresh_var.find( n );
+      if( itu==d_uc_to_fresh_var.end() ){
+        Node k = NodeManager::currentNM()->mkSkolem( "w", n.getType(), "Skolem for wrongly applied selector." );
+        d_uc_to_fresh_var[n] = k;
+        ret = k;
+      }else{
+        ret = itu->second;
+      }
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = removeUninterpretedConstants( n[i], visited ); 
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
+} 
+
+
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   Assert( c.getKind()==APPLY_CONSTRUCTOR );
   Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
@@ -1268,8 +1304,16 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   }
   if( !r.isNull() ){
     Node rr = Rewriter::rewrite( r );
-    if( use_s!=rr ){
-      Node eq = use_s.eqNode( rr );
+    Node rrs = rr;
+    if( wrong ){
+      // we have inference S_i( C_j( t ) ) = t' for i != j, where t' is result of mkGroundTerm.
+      // we must eliminate uninterpreted constants for datatypes that have uninterpreted sort subfields,
+      // since uninterpreted constants should not appear in lemmas
+      std::map< Node, Node > visited;
+      rrs = removeUninterpretedConstants( rr, visited );
+    }
+    if( use_s!=rrs ){
+      Node eq = use_s.eqNode( rrs );
       Node eq_exp;
       if( options::dtRefIntro() ){
         eq_exp = d_true;
@@ -1654,19 +1698,6 @@ void TheoryDatatypes::collectTerms( Node n ) {
   }
 }
 
-void TheoryDatatypes::processNewTerm( Node n ){
-  Trace("dt-terms") << "Created term : " << n << std::endl;
-  //see if it is rewritten to be something different
-  Node rn = Rewriter::rewrite( n );
-  if( rn!=n && !areEqual( rn, n ) ){
-    Node eq = rn.eqNode( n );
-    d_pending.push_back( eq );
-    d_pending_exp[ eq ] = d_true;
-    Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
-    d_infer.push_back( eq );
-  }
-}
-
 Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){
   std::map< int, Node >::iterator it = d_inst_map[n].find( index );
   if( it!=d_inst_map[n].end() ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 6a26352ad..98d8d53b1 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -192,7 +192,8 @@ private:
   /** sygus utilities */
   SygusSplit * d_sygus_split;
   SygusSymBreak * d_sygus_sym_break;
-
+  /** uninterpreted constant to variable map */
+  std::map< Node, Node > d_uc_to_fresh_var;
 private:
   /** singleton lemmas (for degenerate co-datatype case) */
   std::map< TypeNode, Node > d_singleton_lemma[2];
@@ -284,6 +285,8 @@ private:
   void merge( Node t1, Node t2 );
   /** collapse selector, s is of the form sel( n ) where n = c */
   void collapseSelector( Node s, Node c );
+  /** remove uninterpreted constants */
+  Node removeUninterpretedConstants( Node n, std::map< Node, Node >& visited );
   /** for checking if cycles exist */
   void checkCycles();
   Node searchForCycle( TNode n, TNode on,
@@ -302,8 +305,6 @@ private:
   void collectTerms( Node n );
   /** get instantiate cons */
   Node getInstantiateCons( Node n, const Datatype& dt, int index );
-  /** process new term that was created internally */
-  void processNewTerm( Node n );
   /** check instantiate */
   void instantiate( EqcInfo* eqc, Node n );
   /** must communicate fact */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 084912f5a..612646b42 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -734,8 +734,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
           if( !isStar(cond[j][1]) ){
             children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
           }
-        }else if ( !isStar(cond[j]) &&  //handle the case where there are 0 or 1 ground eqc of this type
-                   d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
+        }else if( !isStar(cond[j]) ){
           Node c = getRepresentative( cond[j] );
           c = getRepresentative( c );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 88f8e2484..58bebef35 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -496,21 +496,49 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
   }
   return false;
 }
-int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
-  int hmin = 1;
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    TypeNode tn = q[0][i].getType();
-    int handled = -1;
+
+// -1 : not cbqi sort, 0 : cbqi sort, 1 : cbqi sort regardless of quantifier body
+int InstStrategyCbqi::isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited ) {
+  std::map< TypeNode, int >::iterator itv = visited.find( tn );
+  if( itv==visited.end() ){
+    visited[tn] = 0;
+    int ret = -1;
     if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){
-      handled = 0;
+      ret = 0;
     }else if( tn.isDatatype() ){
-      handled = 0;
+      ret = 1;
+      const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+          TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
+          int cret = isCbqiSort( crange, visited );
+          if( cret==-1 ){
+            visited[tn] = -1;
+            return -1;
+          }else if( cret<ret ){
+            ret = cret;
+          }
+        }
+      }
     }else if( tn.isSort() ){
       QuantEPR * qepr = d_quantEngine->getQuantEPR();
       if( qepr!=NULL ){
-        handled = qepr->isEPR( tn ) ? 1 : -1;
+        ret = qepr->isEPR( tn ) ? 1 : -1;
       }
     }
+    visited[tn] = ret;
+    return ret;
+  }else{
+    return itv->second;
+  }
+}
+
+int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
+  int hmin = 1;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    TypeNode tn = q[0][i].getType();
+    std::map< TypeNode, int > visited;
+    int handled = isCbqiSort( tn, visited );
     if( handled==-1 ){
       return -1;
     }else if( handled<hmin ){
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 2cd5f6e1c..6c2dc9275 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -58,6 +58,7 @@ protected:
   /** helper functions */
   int hasNonCbqiVariable( Node q );
   bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+  int isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited );
   /** get next decision request with dependency checking */
   Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );  
   /** process functions */