Handle parametric datatypes with --quant-ind. Minor updates.

3 files changed, 25 insertions, 11 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index cd31778ec..dd2803d30 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -260,10 +260,6 @@ public:
   /** get instantiate cons */
   static Node getInstCons( Node n, const Datatype& dt, int index ) {
     Assert( index>=0 && index<(int)dt.getNumConstructors() );
-    Type tspec;
-    if( dt.isParametric() ){
-      tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
-    }
     std::vector< Node > children;
     children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
     for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 27bbb0f5f..2cc49ef5a 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -605,7 +605,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
       std::vector< TypeNode > rt_types;
       std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs;
       unsigned addedLemmas = 0;
-      for( unsigned depth=1; depth<=3; depth++ ){
+      unsigned maxDepth = options::conjectureGenMaxDepth();
+      for( unsigned depth=1; depth<=maxDepth; depth++ ){
         Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl;
         Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl;
         //set up environment
@@ -1167,6 +1168,8 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi
     d_waiting_conjectures_score.push_back( score );
     d_waiting_conjectures[lhs].push_back( rhs );
     d_waiting_conjectures[rhs].push_back( lhs );
+  }else{
+    Trace("sg-conjecture-debug2") << "...do not consider " << lhs << " == " << rhs << ", score = " << score << std::endl;
   }
 }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 51c72d7bb..8b09d8e5d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1016,14 +1016,29 @@ Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
 }
 
 
-void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
+void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
+  TypeNode tspec;
+  if( dt.isParametric() ){
+    tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) );
+    Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl;
+    Assert( tspec.getNumChildren()==dc.getNumArgs() );
+  }
+  Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl;
   for( unsigned j=0; j<dc.getNumArgs(); j++ ){
-    TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
     std::vector< Node > ssc;
-    if( tn==ntn ){
-      ssc.push_back( n );
+    if( dt.isParametric() ){
+      Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl;
+      if( tspec[j]==ntn ){
+        ssc.push_back( n );
+      }
+    }else{
+      TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
+      Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
+      if( tn==ntn ){
+        ssc.push_back( n );
+      }
     }
-    /* TODO
+    /* TODO: more than weak structural induction
     else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
       visited.push_back( tn );
       const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
@@ -1101,7 +1116,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
       std::vector< Node > disj;
       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
         std::vector< Node > selfSel;
-        getSelfSel( dt[i], k, tn, selfSel );
+        getSelfSel( dt, dt[i], k, tn, selfSel );
         std::vector< Node > conj;
         conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
         for( unsigned j=0; j<selfSel.size(); j++ ){