diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 02:31:49 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-01 00:31:49 -0700 |
commit | 7291952f49ca93bbc98b419d72c20eb45f63c339 (patch) | |
tree | 1e633e865c0c02c0a4358ba6745be6d2ae1318c0 /src/theory/quantifiers/conjecture_generator.cpp | |
parent | def4b45fa41ddf128ab0b2e8f6bb3b8454974008 (diff) |
Make conjecture generator's uf term enumeration safer (#2172)
This ensures that the function getEnumerateUfTerm does not have out of bounds accesses. This is an alternative fix to the one brought up in #2158.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 31 |
1 files changed, 29 insertions, 2 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; } } |