+\r
+Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {\r
+ std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );\r
+ if( it==d_typ_pred.end() ){\r
+ TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );\r
+ Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." );\r
+ d_typ_pred[tn] = op;\r
+ return op;\r
+ }else{\r
+ return it->second;\r
+ }\r
+}\r
+\r
+void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {\r
+ if( n.getNumChildren()>0 ){\r
+ std::vector< int > vec;\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ vec.push_back( 0 );\r
+ }\r
+ vec.pop_back();\r
+ int size_limit = 0;\r
+ int vec_sum = -1;\r
+ unsigned index = 0;\r
+ unsigned last_size = terms.size();\r
+ while( terms.size()<num ){\r
+ bool success = true;\r
+ if( vec_sum==-1 ){\r
+ vec_sum = 0;\r
+ vec.push_back( size_limit );\r
+ }else{\r
+ //see if we can iterate current\r
+ if( vec_sum<size_limit && !getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){\r
+ vec[index]++;\r
+ vec_sum++;\r
+ vec.push_back( size_limit - vec_sum );\r
+ }else{\r
+ vec_sum -= vec[index];\r
+ vec[index] = 0;\r
+ index++;\r
+ if( index==n.getNumChildren() ){\r
+ success = false;\r
+ }\r
+ }\r
+ }\r
+ if( success ){\r
+ if( vec.size()==n.getNumChildren() ){\r
+ Node lc = getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );\r
+ if( !lc.isNull() ){\r
+ for( unsigned i=0; i<vec.size(); i++ ){\r
+ Trace("sg-gt-enum-debug") << vec[i] << " ";\r
+ }\r
+ Trace("sg-gt-enum-debug") << " / " << size_limit << std::endl;\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ Trace("sg-gt-enum-debug") << n[i].getType() << " ";\r
+ }\r
+ Trace("sg-gt-enum-debug") << std::endl;\r
+ std::vector< Node > children;\r
+ children.push_back( n.getOperator() );\r
+ for( unsigned i=0; i<(vec.size()-1); i++ ){\r
+ Node nn = getEnumerateTerm( n[i].getType(), vec[i] );\r
+ Assert( !nn.isNull() );\r
+ Assert( nn.getType()==n[i].getType() );\r
+ children.push_back( nn );\r
+ }\r
+ children.push_back( lc );\r
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
+ Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl;\r
+ terms.push_back( n );\r
+ }\r
+ vec.pop_back();\r
+ index = 0;\r
+ }\r
+ }else{\r
+ if( terms.size()>last_size ){\r
+ last_size = terms.size();\r
+ size_limit++;\r
+ for( unsigned i=0; i<vec.size(); i++ ){\r
+ vec[i] = 0;\r
+ }\r
+ vec_sum = -1;\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ terms.push_back( n );\r
+ }\r
+}\r
+\r
+void ConjectureGenerator::getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {\r
+ std::vector< Node > uf_terms;\r
+ getEnumerateUfTerm( n, num, uf_terms );\r
+ Node p = getPredicateForType( n.getType() );\r
+ for( unsigned i=0; i<uf_terms.size(); i++ ){\r
+ terms.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, p, uf_terms[i] ) );\r
+ }\r
+}\r
+\r