Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.

5 files changed, 160 insertions, 80 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 29a95b38f..ec9318e99 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -146,14 +146,14 @@ public:
           gt = *te;
         }else{
           //check whether well-founded
-          bool isWellFounded = true;
-          if( isTypeDatatype( tn ) ){
-            const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
-            isWellFounded = dta.isWellFounded();
-          }
-          if( isWellFounded || in[0].isConst() ){
-            gt = tn.mkGroundTerm();
-          }
+          //bool isWf = true;
+          //if( isTypeDatatype( tn ) ){
+          //  const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
+          //  isWf = dta.isWellFounded();
+          //}
+          //if( isWf || in[0].isConst() ){
+          gt = tn.mkGroundTerm();
+          //}
         }
         if( !gt.isNull() ){
           //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 24bd69854..299ae5678 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -56,7 +56,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_conflict( c, false ),
   d_collectTermsCache( c ),
   d_consTerms( c ),
-  d_selTerms( c ){
+  d_selTerms( c ),
+  d_singleton_eq( u ){
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -175,6 +176,7 @@ void TheoryDatatypes::check(Effort e) {
     Debug("datatypes-split") << "Check for splits " << e << endl;
     addedFact = false;
     do {
+      std::map< TypeNode, Node > rec_singletons;
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       while( !eqcs_i.isFinished() ){
         Node n = (*eqcs_i);
@@ -186,89 +188,128 @@ void TheoryDatatypes::check(Effort e) {
           if( !hasLabel( eqc, n ) ){
             Trace("datatypes-debug") << "No constructor..." << std::endl;
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-
-            std::vector< bool > pcons;
-            getPossibleCons( eqc, n, pcons );
-            //std::cout << "pcons " << n << " = ";
-            //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
-            //std::cout << std::endl;
-            //check if we do not need to resolve the constructor type for this equivalence class.
-            // this is if there are no selectors for this equivalence class, its possible values are infinite,
-            //  and we are not producing a model, then do not split.
-            int consIndex = -1;
-            bool needSplit = true;
-            for( unsigned int j=0; j<pcons.size(); j++ ) {
-              if( pcons[j] ) {
-                if( consIndex==-1 ){
-                  consIndex = j;
-                }
-                if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_selectors ) ) {
-                  needSplit = false;
+            bool continueProc = true;
+            if( dt.isRecursiveSingleton() ){
+              //handle recursive singleton case
+              std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn );
+              if( itrs!=rec_singletons.end() ){
+                Node eq = n.eqNode( itrs->second );
+                if( d_singleton_eq.find( eq )==d_singleton_eq.end() ){
+                  d_singleton_eq[eq] = true;
+                  // get assumptions
+                  bool success = true;
+                  std::vector< Node > assumptions;
+                  //if there is at least one uninterpreted sort occurring within the datatype and the logic is not quantified, add lemmas ensuring cardinality is more than one,
+                  //  do not infer the equality if at least one sort was processed.
+                  //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one,
+                  //  infer the equality.
+                  for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes(); i++ ){
+                    TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( i ) );
+                    if( getQuantifiersEngine() ){
+                      // under the assumption that the cardinality of this type is one
+                      Node a = getSingletonLemma( tn, true );
+                      assumptions.push_back( a.negate() );
+                    }else{
+                      success = false;
+                      // assert that the cardinality of this type is more than one
+                      getSingletonLemma( tn, false );
+                    }
+                  }
+                  if( success ){
+                    Node eq = n.eqNode( itrs->second );
+                    assumptions.push_back( eq );
+                    Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
+                    Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
+                    d_out->lemma( lemma );
+                  }
                 }
+              }else{
+                rec_singletons[tn] = n;
               }
+              //do splitting for quantified logics (incomplete anyways)
+              continueProc = ( getQuantifiersEngine()!=NULL );
             }
-            //d_dtfCounter++;
-            if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
-              //for the sake of termination, we must choose the constructor of a ground term
-              //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
-              // TODO: this is probably not good enough, actually need fair enumeration strategy
-              if( !n.getType().isRecord() ){ //FIXME
-                Node groundTerm = n.getType().mkGroundTerm();
-                if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME
-                  int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
-                  if( pcons[index] ){
-                    consIndex = index;
+            if( continueProc ){
+              //all other cases
+              std::vector< bool > pcons;
+              getPossibleCons( eqc, n, pcons );
+              //check if we do not need to resolve the constructor type for this equivalence class.
+              // this is if there are no selectors for this equivalence class, its possible values are infinite,
+              //  and we are not producing a model, then do not split.
+              int consIndex = -1;
+              bool needSplit = true;
+              for( unsigned int j=0; j<pcons.size(); j++ ) {
+                if( pcons[j] ) {
+                  if( consIndex==-1 ){
+                    consIndex = j;
+                  }
+                  if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_selectors ) ) {
+                    needSplit = false;
+                  }
+                }
+              }
+              //d_dtfCounter++;
+              if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
+                //for the sake of termination, we must choose the constructor of a ground term
+                //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
+                // TODO: this is probably not good enough, actually need fair enumeration strategy
+                if( !n.getType().isRecord() ){ //FIXME
+                  Node groundTerm = n.getType().mkGroundTerm();
+                  if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME
+                    int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
+                    if( pcons[index] ){
+                      consIndex = index;
+                    }
+                    needSplit = true;
                   }
-                  needSplit = true;
                 }
               }
-            }
 
-            if( needSplit && consIndex!=-1 ) {
-              //if only one constructor, then this term must be this constructor
-              if( dt.getNumConstructors()==1 ){
-                Node t = DatatypesRewriter::mkTester( n, 0, dt );
-                d_pending.push_back( t );
-                d_pending_exp[ t ] = d_true;
-                Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
-                d_infer.push_back( t );
-              }else{
-                if( options::dtBinarySplit() ){
-                  Node test = DatatypesRewriter::mkTester( n, consIndex, dt );
-                  Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
-                  test = Rewriter::rewrite( test );
-                  NodeBuilder<> nb(kind::OR);
-                  nb << test << test.notNode();
-                  Node lemma = nb;
-                  d_out->lemma( lemma );
-                  d_out->requirePhase( test, true );
+              if( needSplit && consIndex!=-1 ) {
+                //if only one constructor, then this term must be this constructor
+                if( dt.getNumConstructors()==1 ){
+                  Node t = DatatypesRewriter::mkTester( n, 0, dt );
+                  d_pending.push_back( t );
+                  d_pending_exp[ t ] = d_true;
+                  Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
+                  d_infer.push_back( t );
                 }else{
-                  Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
-                  std::vector< Node > children;
-                  if( dt.isSygus() && d_sygus_split ){
-                    std::vector< Node > lemmas;
-                    d_sygus_split->getSygusSplits( n, dt, children, lemmas );
-                    for( unsigned i=0; i<lemmas.size(); i++ ){
-                      Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
-                      d_out->lemma( lemmas[i] );
-                    }
+                  if( options::dtBinarySplit() ){
+                    Node test = DatatypesRewriter::mkTester( n, consIndex, dt );
+                    Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
+                    test = Rewriter::rewrite( test );
+                    NodeBuilder<> nb(kind::OR);
+                    nb << test << test.notNode();
+                    Node lemma = nb;
+                    d_out->lemma( lemma );
+                    d_out->requirePhase( test, true );
                   }else{
-                    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                      Node test = DatatypesRewriter::mkTester( n, i, dt );
-                      children.push_back( test );
+                    Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
+                    std::vector< Node > children;
+                    if( dt.isSygus() && d_sygus_split ){
+                      std::vector< Node > lemmas;
+                      d_sygus_split->getSygusSplits( n, dt, children, lemmas );
+                      for( unsigned i=0; i<lemmas.size(); i++ ){
+                        Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
+                        d_out->lemma( lemmas[i] );
+                      }
+                    }else{
+                      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+                        Node test = DatatypesRewriter::mkTester( n, i, dt );
+                        children.push_back( test );
+                      }
                     }
+                    Assert( !children.empty() );
+                    Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
+                    Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
+                    d_out->lemma( lemma );
                   }
-                  Assert( !children.empty() );
-                  Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
-                  Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
-                  d_out->lemma( lemma );
+                  return;
                 }
-                return;
+              }else{
+                Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
               }
-            }else{
-              Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
             }
-
           }else{
             Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl;
           }
@@ -1415,6 +1456,30 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c
   }
 }
 
+Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
+  int index = pol ? 0 : 1;
+  std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn );
+  if( it==d_singleton_lemma[index].end() ){
+    Node a;
+    if( pol ){
+      Node v1 = NodeManager::currentNM()->mkBoundVar( tn );
+      Node v2 = NodeManager::currentNM()->mkBoundVar( tn );
+      a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) );
+    }else{
+      Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn );
+      Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
+      a = v1.eqNode( v2 ).negate();
+      //send out immediately as lemma
+      d_out->lemma( a );
+      Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
+    }
+    d_singleton_lemma[index][tn] = a;
+    return a;
+  }else{
+    return it->second;
+  } 
+}
+
 void TheoryDatatypes::collectTerms( Node n ) {
   if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
     d_collectTermsCache[n] = true;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 6604e5548..ab40f07db 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -181,6 +181,11 @@ private:
   SygusSplit * d_sygus_split;
   SygusSymBreak * d_sygus_sym_break;
 private:
+  /** singleton lemmas (for degenerate co-datatype case) */
+  std::map< TypeNode, Node > d_singleton_lemma[2];
+  /** Cache for singleton equalities processed */
+  BoolMap d_singleton_eq;
+private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
   /** flush pending facts */
@@ -262,6 +267,8 @@ private:
                           std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp );
   /** build model */
   Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv );
+  /** get singleton lemma */
+  Node getSingletonLemma( TypeNode tn, bool pol );
   /** collect terms */
   void collectTerms( Node n );
   /** get instantiate cons */
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 616c51f54..f9c8e42fd 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -528,7 +528,7 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
                     for( unsigned k=0; k<vars[lhs].size(); k++ ){
                       int v = vars[lhs][k];
                       Trace("cegqi-si-debug") << "        variable " << v << std::endl;
-                      Assert( vars[lhs].size()==vn );
+                      Assert( (int)vars[lhs].size()==vn );
                       //check if already processed
                       bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end();
                       if( proc==(p==1) ){
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index d37aa1b7d..244cb303d 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Clark Barrett
  ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne
+ ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -197,6 +197,14 @@ void UnconstrainedSimplifier::processUnconstrained()
               break;
             }
           }
+          if( parent[0].getType().isDatatype() ){
+            TypeNode tn = parent[0].getType();
+            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+            if( dt.isRecursiveSingleton() ){
+              //domain size may be 1
+              break;
+            }
+          }
         case kind::BITVECTOR_COMP:
         case kind::LT:
         case kind::LEQ: