Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.

5 files changed, 91 insertions, 57 deletions

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 256dcaef2..a514460c7 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -75,31 +75,10 @@ public:
     Debug("te") << "datatype is kind " << type.getKind() << std::endl;
     Debug("te") << "datatype is " << type << std::endl;
 
-    /* find the "zero" constructor (the first non-recursive one) */
-    /* FIXME: this isn't sufficient for mutually-recursive datatypes! */
-    while(d_zeroCtor < d_datatype.getNumConstructors()) {
-      bool recursive = false;
-      if( d_datatype.isParametric() ){
-        TypeNode tn = TypeNode::fromType( d_datatype[d_zeroCtor].getSpecializedConstructorType(d_type.toType()) );
-        for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
-          if( tn[i]==type ){
-            recursive = true;
-            break;
-          }
-        }
-      }else{
-        for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) {
-          if(Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type) {
-            recursive = true;
-            break;
-          }
-        }
-      }
-      if(!recursive) {
-        break;
-      }
-      ++d_zeroCtor;
-    }
+    /* find the "zero" constructor via mkGroundTerm */
+    Node t = type.mkGroundTerm();
+    Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
+    d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() );
 
     /* start with the non-recursive constructor */
     d_ctor = d_zeroCtor;
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index bf35db8f3..a2e3d4ce3 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -757,9 +757,18 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           }

         }

         Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;

-        Trace("sg-stats") << "--------> Total LHS of depth : " << rel_term_count << std::endl;

+        Trace("sg-stats") << "--------> Total LHS of depth " << depth << " : " << rel_term_count << std::endl;

         //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl;

-        //now generate right hand sides

+        

+        /* test...

+        for( unsigned i=0; i<rt_types.size(); i++ ){

+          Trace("sg-term-enum") << "Term enumeration for " << rt_types[i] << " : " << std::endl;

+          Trace("sg-term-enum") << "Ground term : " << rt_types[i].mkGroundTerm() << std::endl;

+          for( unsigned j=0; j<10; j++ ){

+            Trace("sg-term-enum") << "  " << getEnumerateTerm( rt_types[i], j ) << std::endl;

+          }

+        }

+        */

 

         //consider types from relevant terms

         for( unsigned rdepth=0; rdepth<=depth; rdepth++ ){

@@ -812,6 +821,9 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               }

             }

           }

+          if( (int)addedLemmas>=options::conjectureGenPerRound() ){

+            break;

+          }

         }

         if( (int)addedLemmas>=options::conjectureGenPerRound() ){

           break;

@@ -825,13 +837,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           TNode r = (*ueqcs_i);

           bool firstTime = true;

           TNode rr = getUniversalRepresentative( r );

-          Trace("thm-ee") << "  " << r;

-          if( rr!=r ){ Trace("thm-ee") << " [" << rr << "]"; }

+          Trace("thm-ee") << "  " << rr;

           Trace("thm-ee") << " : { ";

           eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine );

           while( !ueqc_i.isFinished() ){

             TNode n = (*ueqc_i);

-            if( r!=n ){

+            if( rr!=n ){

               if( firstTime ){

                 Trace("thm-ee") << std::endl;

                 firstTime = false;

@@ -879,32 +890,36 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
             //we have determined a relevant subgoal

             Node lhs = d_waiting_conjectures_lhs[indices[i]];

             Node rhs = d_waiting_conjectures_rhs[indices[i]];

-            Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;

-            Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[indices[i]] << std::endl;

-            std::vector< Node > bvs;

-            for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){

-              for( unsigned i=0; i<=it->second; i++ ){

-                bvs.push_back( getFreeVar( it->first, i ) );

-              }

-            }

-            Node rsg;

-            if( !bvs.empty() ){

-              Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );

-              rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );

+            if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){

+              //skip

             }else{

-              rsg = lhs.eqNode( rhs );

-            }

-            rsg = Rewriter::rewrite( rsg );

-            d_conjectures.push_back( rsg );

-            d_eq_conjectures[lhs].push_back( rhs );

-            d_eq_conjectures[rhs].push_back( lhs );

-

-            Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );

-            d_quantEngine->addLemma( lem, false );

-            d_quantEngine->addRequirePhase( rsg, false );

-            addedLemmas++;

-            if( (int)addedLemmas>=options::conjectureGenPerRound() ){

-              break;

+              Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;

+              Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[indices[i]] << std::endl;

+              std::vector< Node > bvs;

+              for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){

+                for( unsigned i=0; i<=it->second; i++ ){

+                  bvs.push_back( getFreeVar( it->first, i ) );

+                }

+              }

+              Node rsg;

+              if( !bvs.empty() ){

+                Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );

+                rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );

+              }else{

+                rsg = lhs.eqNode( rhs );

+              }

+              rsg = Rewriter::rewrite( rsg );

+              d_conjectures.push_back( rsg );

+              d_eq_conjectures[lhs].push_back( rhs );

+              d_eq_conjectures[rhs].push_back( lhs );

+

+              Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );

+              d_quantEngine->addLemma( lem, false );

+              d_quantEngine->addRequirePhase( rsg, false );

+              addedLemmas++;

+              if( (int)addedLemmas>=options::conjectureGenPerRound() ){

+                break;

+              }

             }

           }else{

             if( doSort ){

@@ -1059,6 +1074,26 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo
   }

 }

 

+Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) {

+  std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );

+  unsigned teIndex;

+  if( it==d_typ_enum_map.end() ){

+    teIndex = (int)d_typ_enum.size();

+    d_typ_enum_map[tn] = teIndex;

+    d_typ_enum.push_back( TypeEnumerator(tn) );

+  }else{

+    teIndex = it->second;

+  }

+  while( index>=d_enum_terms[tn].size() ){

+    if( d_typ_enum[teIndex].isFinished() ){

+      return Node::null();

+    }

+    d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );

+    ++d_typ_enum[teIndex];

+  }

+  return d_enum_terms[tn][index];

+}

+

 void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {

   int score = considerCandidateConjecture( lhs, rhs ); 

   if( score>0 ){

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index b0f25bd64..eb7f4b2aa 100755
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -20,6 +20,7 @@
 #include "context/cdhashmap.h"

 #include "context/cdchunk_list.h"

 #include "theory/quantifiers_engine.h"

+#include "theory/type_enumerator.h"

 

 namespace CVC4 {

 namespace theory {

@@ -355,6 +356,14 @@ public:  //for generalization
   bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );

   // get generalization depth

   int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );

+private:

+  //ground term enumeration

+  std::map< TypeNode, std::vector< Node > > d_enum_terms;

+  //type enumerators

+  std::map< TypeNode, unsigned > d_typ_enum_map;

+  std::vector< TypeEnumerator > d_typ_enum;

+  //get nth term for type

+  Node getEnumerateTerm( TypeNode tn, unsigned index );

 public:  //for property enumeration

   //process this candidate conjecture

   void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );

@@ -404,7 +413,6 @@ public:
   void assertNode( Node n );

   /** Identify this module (for debugging, dynamic configuration, etc..) */

   std::string identify() const { return "ConjectureGenerator"; }

-

 //options

 private:

   bool optReqDistinctVarPatterns();

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index e8a8f16f5..a3a984682 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -58,7 +58,8 @@ TESTS =	\
 	bug286.cvc \
 	bug438.cvc \
 	bug438b.cvc \
-	wrong-sel-simp.cvc
+	wrong-sel-simp.cvc \
+	tenum-bug.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/tenum-bug.smt2 b/test/regress/regress0/datatypes/tenum-bug.smt2
new file mode 100644
index 000000000..bf82c7b8c
--- /dev/null
+++ b/test/regress/regress0/datatypes/tenum-bug.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-datatypes () ((DNat (dnat (data Nat)))
+                       (Nat (succ (pred DNat)) (zero))))
+
+(declare-fun x () Nat)
+
+(assert (not (= x zero)))
+
+(check-sat)
\ No newline at end of file