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 256dcaef266afbb2565b4aace1b9bea3b7b227a3..a514460c7050715192e64bfa3ff73541ffc2b4c8 100644 (file)
--- 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 bf35db8f395f31eb7fea1f9e02e158e6d39a907c..a2e3d4ce3ab319161e5c0e27b009d7c91662ab66 100755 (executable)
--- 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 ) {
           }\r
         }\r
         Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;\r
-        Trace("sg-stats") << "--------> Total LHS of depth : " << rel_term_count << std::endl;\r
+        Trace("sg-stats") << "--------> Total LHS of depth " << depth << " : " << rel_term_count << std::endl;\r
         //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl;\r
-        //now generate right hand sides\r
+        \r
+        /* test...\r
+        for( unsigned i=0; i<rt_types.size(); i++ ){\r
+          Trace("sg-term-enum") << "Term enumeration for " << rt_types[i] << " : " << std::endl;\r
+          Trace("sg-term-enum") << "Ground term : " << rt_types[i].mkGroundTerm() << std::endl;\r
+          for( unsigned j=0; j<10; j++ ){\r
+            Trace("sg-term-enum") << "  " << getEnumerateTerm( rt_types[i], j ) << std::endl;\r
+          }\r
+        }\r
+        */\r
 \r
         //consider types from relevant terms\r
         for( unsigned rdepth=0; rdepth<=depth; rdepth++ ){\r
@@ -812,6 +821,9 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               }\r
             }\r
           }\r
+          if( (int)addedLemmas>=options::conjectureGenPerRound() ){\r
+            break;\r
+          }\r
         }\r
         if( (int)addedLemmas>=options::conjectureGenPerRound() ){\r
           break;\r
@@ -825,13 +837,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           TNode r = (*ueqcs_i);\r
           bool firstTime = true;\r
           TNode rr = getUniversalRepresentative( r );\r
-          Trace("thm-ee") << "  " << r;\r
-          if( rr!=r ){ Trace("thm-ee") << " [" << rr << "]"; }\r
+          Trace("thm-ee") << "  " << rr;\r
           Trace("thm-ee") << " : { ";\r
           eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine );\r
           while( !ueqc_i.isFinished() ){\r
             TNode n = (*ueqc_i);\r
-            if( r!=n ){\r
+            if( rr!=n ){\r
               if( firstTime ){\r
                 Trace("thm-ee") << std::endl;\r
                 firstTime = false;\r
@@ -879,32 +890,36 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
             //we have determined a relevant subgoal\r
             Node lhs = d_waiting_conjectures_lhs[indices[i]];\r
             Node rhs = d_waiting_conjectures_rhs[indices[i]];\r
-            Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;\r
-            Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[indices[i]] << std::endl;\r
-            std::vector< Node > bvs;\r
-            for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){\r
-              for( unsigned i=0; i<=it->second; i++ ){\r
-                bvs.push_back( getFreeVar( it->first, i ) );\r
-              }\r
-            }\r
-            Node rsg;\r
-            if( !bvs.empty() ){\r
-              Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );\r
-              rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );\r
+            if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){\r
+              //skip\r
             }else{\r
-              rsg = lhs.eqNode( rhs );\r
-            }\r
-            rsg = Rewriter::rewrite( rsg );\r
-            d_conjectures.push_back( rsg );\r
-            d_eq_conjectures[lhs].push_back( rhs );\r
-            d_eq_conjectures[rhs].push_back( lhs );\r
-\r
-            Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );\r
-            d_quantEngine->addLemma( lem, false );\r
-            d_quantEngine->addRequirePhase( rsg, false );\r
-            addedLemmas++;\r
-            if( (int)addedLemmas>=options::conjectureGenPerRound() ){\r
-              break;\r
+              Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;\r
+              Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[indices[i]] << std::endl;\r
+              std::vector< Node > bvs;\r
+              for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){\r
+                for( unsigned i=0; i<=it->second; i++ ){\r
+                  bvs.push_back( getFreeVar( it->first, i ) );\r
+                }\r
+              }\r
+              Node rsg;\r
+              if( !bvs.empty() ){\r
+                Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );\r
+                rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );\r
+              }else{\r
+                rsg = lhs.eqNode( rhs );\r
+              }\r
+              rsg = Rewriter::rewrite( rsg );\r
+              d_conjectures.push_back( rsg );\r
+              d_eq_conjectures[lhs].push_back( rhs );\r
+              d_eq_conjectures[rhs].push_back( lhs );\r
+\r
+              Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );\r
+              d_quantEngine->addLemma( lem, false );\r
+              d_quantEngine->addRequirePhase( rsg, false );\r
+              addedLemmas++;\r
+              if( (int)addedLemmas>=options::conjectureGenPerRound() ){\r
+                break;\r
+              }\r
             }\r
           }else{\r
             if( doSort ){\r
@@ -1059,6 +1074,26 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo
   }\r
 }\r
 \r
+Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) {\r
+  std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );\r
+  unsigned teIndex;\r
+  if( it==d_typ_enum_map.end() ){\r
+    teIndex = (int)d_typ_enum.size();\r
+    d_typ_enum_map[tn] = teIndex;\r
+    d_typ_enum.push_back( TypeEnumerator(tn) );\r
+  }else{\r
+    teIndex = it->second;\r
+  }\r
+  while( index>=d_enum_terms[tn].size() ){\r
+    if( d_typ_enum[teIndex].isFinished() ){\r
+      return Node::null();\r
+    }\r
+    d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );\r
+    ++d_typ_enum[teIndex];\r
+  }\r
+  return d_enum_terms[tn][index];\r
+}\r
+\r
 void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {\r
   int score = considerCandidateConjecture( lhs, rhs ); \r
   if( score>0 ){\r

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index b0f25bd641626316b07a0f735520a7bc130790e1..eb7f4b2aa2041e081d4ddbc4c6b94cd88756de94 100755 (executable)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -20,6 +20,7 @@
 #include "context/cdhashmap.h"\r
 #include "context/cdchunk_list.h"\r
 #include "theory/quantifiers_engine.h"\r
+#include "theory/type_enumerator.h"\r
 \r
 namespace CVC4 {\r
 namespace theory {\r
@@ -355,6 +356,14 @@ public:  //for generalization
   bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );\r
   // get generalization depth\r
   int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );\r
+private:\r
+  //ground term enumeration\r
+  std::map< TypeNode, std::vector< Node > > d_enum_terms;\r
+  //type enumerators\r
+  std::map< TypeNode, unsigned > d_typ_enum_map;\r
+  std::vector< TypeEnumerator > d_typ_enum;\r
+  //get nth term for type\r
+  Node getEnumerateTerm( TypeNode tn, unsigned index );\r
 public:  //for property enumeration\r
   //process this candidate conjecture\r
   void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );\r
@@ -404,7 +413,6 @@ public:
   void assertNode( Node n );\r
   /** Identify this module (for debugging, dynamic configuration, etc..) */\r
   std::string identify() const { return "ConjectureGenerator"; }\r
-\r
 //options\r
 private:\r
   bool optReqDistinctVarPatterns();\r

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index e8a8f16f593e4723663d768944aaf420d60043e8..a3a984682fc2cba91d224a026b924f0eb92a973d 100644 (file)
--- 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 (file)
index 0000000..bf82c7b
--- /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