From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 24 Sep 2014 14:42:31 +0000 (+0200)
Subject: Fix infinite loop in datatypes enumerator.  Minor work on conjecture generator.
X-Git-Tag: cvc5-1.0.0~6620
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d38d41b3f3604fc728ec71499d1f3af3dfb46ccd;p=cvc5.git

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

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