From 7671fc17558dbb52df67838b3ad7166cb39d698a Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 18 Oct 2014 23:10:40 +0200
Subject: [PATCH] Add dt lemma: zero size implies nullary constructor.

---
 src/theory/datatypes/datatypes_rewriter.h | 19 +++++++++++-
 src/theory/datatypes/theory_datatypes.cpp | 37 +++++++++++++----------
 2 files changed, 39 insertions(+), 17 deletions(-)

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 3a41510dd..8214f23e2 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -260,7 +260,7 @@ public:
       }
     }else if( n1!=n2 ){
       if( n1.isConst() && n2.isConst() ){
-        return true;        
+        return true;
       }else{
         Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
         rew.push_back( eq );
@@ -319,6 +319,23 @@ public:
     }
     return false;
   }
+  static bool isNullaryApplyConstructor( Node n ){
+    Assert( n.getKind()==APPLY_CONSTRUCTOR );
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( n[i].getType().isDatatype() ){
+        return false;
+      }
+    }
+    return true;
+  }
+  static bool isNullaryConstructor( const DatatypeConstructor& c ){
+    for( unsigned j=0; j<c.getNumArgs(); j++ ){
+      if( c[j].getType().getRangeType().isDatatype() ){
+        return false;
+      }
+    }
+    return true;
+  }
 
   /** is this term a datatype */
   static bool isTermDatatype( TNode n ){
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index b7e2e5eb3..06d07f425 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1050,7 +1050,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
     Node eq_exp = c.eqNode( s[0] );
     Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
     Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl;
-    
+
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = eq_exp;
     d_infer.push_back( eq );
@@ -1385,20 +1385,6 @@ void TheoryDatatypes::collectTerms( Node n ) {
     }
     if( n.getKind() == APPLY_CONSTRUCTOR ){
       d_consTerms.push_back( n );
-      /*
-      //we must take into account subterm relation when checking for cycles
-      for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-        bool result = d_cycle_check.addEdgeNode( n, n[i] );
-        Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << " " << result << endl;
-        if( result && !d_hasSeenCycle.get() ){
-          Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl;
-        }
-        d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
-        //Node r = getRepresentative( n[i] );
-        //EqcInfo* eqc = getOrMakeEqcInfo( r, true );
-        //eqc->d_selectors = true;
-      }
-      */
     }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE ){
       d_selTerms.push_back( n );
       //we must also record which selectors exist
@@ -1413,7 +1399,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
       EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
       //add it to the eqc info
       addSelector( n, eqc, rep );
-      
+
       if( n.getKind() == DT_SIZE ){
         Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n );
         //must be non-negative
@@ -1421,6 +1407,23 @@ void TheoryDatatypes::collectTerms( Node n ) {
         d_pending.push_back( conc );
         d_pending_exp[ conc ] = d_true;
         d_infer.push_back( conc );
+
+        //add size = 0 lemma
+        Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) );
+        std::vector< Node > children;
+        children.push_back( nn.negate() );
+        const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
+        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+          if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
+            Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
+            children.push_back( test );
+          }
+        }
+        conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+        Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl;
+        d_pending.push_back( conc );
+        d_pending_exp[ conc ] = d_true;
+        d_infer.push_back( conc );
       }
     }
   }
@@ -1776,6 +1779,8 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
     addLemma = true;
   }else if( n.getKind()==LEQ ){
     addLemma = true;
+  }else if( n.getKind()==OR ){
+    addLemma = true;
   }
   if( addLemma ){
     //check if we have already added this lemma
-- 
2.30.2