diff options
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 31 | ||||
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 18 |
2 files changed, 46 insertions, 3 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index ad278f8c5..8c6b5afbc 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1066,6 +1066,8 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) { if( n.getNumChildren()>0 ){ TermEnumeration* te = d_quantEngine->getTermEnumeration(); + // below, we do a fair enumeration of vectors vec of indices whose sum is + // 1,2,3, ... std::vector< int > vec; std::vector< TypeNode > types; for( unsigned i=0; i<n.getNumChildren(); i++ ){ @@ -1078,6 +1080,10 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< return; } } + // the index of the last child is determined by the limit of the sum + // of indices of children (size_limit) and the sum of the indices of the + // other children (vec_sum). Hence, we pop here and add this value at each + // iteration of the loop. vec.pop_back(); int size_limit = 0; int vec_sum = -1; @@ -1087,25 +1093,44 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< bool success = true; if( vec_sum==-1 ){ vec_sum = 0; + // we will construct a new child below + // since sum is 0, the index of last child is limit vec.push_back( size_limit ); - }else{ + } + else if (index < vec.size()) + { + Assert(index < types.size()); //see if we can iterate current if (vec_sum < size_limit && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull()) { vec[index]++; vec_sum++; + // we will construct a new child below + // add the index of the last child, its index is (limit-sum) vec.push_back( size_limit - vec_sum ); }else{ + // reset the index vec_sum -= vec[index]; vec[index] = 0; index++; - if( index==n.getNumChildren() ){ + if (index == vec.size()) + { + // no more indices to iterate, we increment limit and reset below success = false; } } } + else + { + // This should never happen due to invariants of this loop. + // However, if it does, we simply abort while not fully enumerating the + // full set of terms. + Assert(false); + return; + } if( success ){ + // if we are ready to construct the term if( vec.size()==n.getNumChildren() ){ Node lc = te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]); @@ -1131,6 +1156,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl; terms.push_back( n ); } + // pop the index for the last child vec.pop_back(); index = 0; } @@ -1143,6 +1169,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< } vec_sum = -1; }else{ + // we've saturated, no more terms can be enumerated return; } } diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index b0363c59b..6d626038d 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -378,7 +378,23 @@ private: std::map< TypeNode, Node > d_typ_pred; //get predicate for type Node getPredicateForType( TypeNode tn ); - // + /** get enumerate uf term + * + * This function adds up to #num f-applications to terms, where f is + * n.getOperator(). These applications are enumerated in a fair manner based + * on an iterative deepening of the sum of indices of the arguments. For + * example, if f : U x U -> U, an the term enumerator for U gives t1, t2, t3 + * ..., then we add f-applications to terms in this order: + * f( t1, t1 ) + * f( t2, t1 ) + * f( t1, t2 ) + * f( t1, t3 ) + * f( t2, t2 ) + * f( t3, t1 ) + * ... + * This function may add fewer than #num terms to terms if the enumeration is + * exhausted, or if an internal error occurs. + */ void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ); // void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ); |