if( n.getKind()!=EQUAL ){\r
if( n.hasOperator() ){\r
TNode op = n.getOperator();\r
- if( !isRelevantFunc( op ) ){\r
+ if( !d_tge.isRelevantFunc( op ) ){\r
return Node::null();\r
}\r
children.push_back( op );\r
return std::find( d_ground_terms.begin(), d_ground_terms.end(), n )!=d_ground_terms.end();\r
}\r
\r
-bool ConjectureGenerator::isRelevantFunc( Node f ) {\r
- return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end();\r
-}\r
-\r
bool ConjectureGenerator::needsCheck( Theory::Effort e ) {\r
return e==Theory::EFFORT_FULL;\r
}\r
if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){\r
d_fullEffortCount++;\r
if( d_fullEffortCount%optFullCheckFrequency()==0 ){\r
+ d_tge.d_cg = this;\r
Trace("sg-engine") << "---Conjecture generator, effort = " << e << "--- " << std::endl;\r
eq::EqualityEngine * ee = getEqualityEngine();\r
\r
}\r
\r
Trace("sg-proc") << "Compute relevant eqc..." << std::endl;\r
- d_relevant_eqc[0].clear();\r
- d_relevant_eqc[1].clear();\r
+ d_tge.d_relevant_eqc[0].clear();\r
+ d_tge.d_relevant_eqc[1].clear();\r
for( unsigned i=0; i<eqcs.size(); i++ ){\r
TNode r = eqcs[i];\r
std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );\r
index = 0;\r
}\r
//based on unproven conjectures? TODO\r
- d_relevant_eqc[index].push_back( r );\r
+ d_tge.d_relevant_eqc[index].push_back( r );\r
}\r
Trace("sg-gen-tg-debug") << "Initial relevant eqc : ";\r
- for( unsigned i=0; i<d_relevant_eqc[0].size(); i++ ){\r
- Trace("sg-gen-tg-debug") << "e" << d_em[d_relevant_eqc[0][i]] << " ";\r
+ for( unsigned i=0; i<d_tge.d_relevant_eqc[0].size(); i++ ){\r
+ Trace("sg-gen-tg-debug") << "e" << d_em[d_tge.d_relevant_eqc[0][i]] << " ";\r
}\r
Trace("sg-gen-tg-debug") << std::endl;\r
Trace("sg-proc") << "...done compute relevant eqc" << std::endl;\r
\r
\r
Trace("sg-proc") << "Collect signature information..." << std::endl;\r
- d_funcs.clear();\r
- d_typ_funcs.clear();\r
- d_func_kind.clear();\r
- d_func_args.clear();\r
- TypeNode tnull;\r
- for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){\r
- if( !getTermDatabase()->d_op_map[it->first].empty() ){\r
- Node nn = getTermDatabase()->d_op_map[it->first][0];\r
- if( isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){\r
- d_funcs.push_back( it->first );\r
- d_typ_funcs[tnull].push_back( it->first );\r
- d_typ_funcs[nn.getType()].push_back( it->first );\r
- for( unsigned i=0; i<nn.getNumChildren(); i++ ){\r
- d_func_args[it->first].push_back( nn[i].getType() );\r
- }\r
- d_func_kind[it->first] = nn.getKind();\r
- Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;\r
- getTermDatabase()->computeUfEqcTerms( it->first );\r
- }\r
- }\r
- }\r
- //shuffle functions\r
- for( std::map< TypeNode, std::vector< TNode > >::iterator it = d_typ_funcs.begin(); it !=d_typ_funcs.end(); ++it ){\r
- std::random_shuffle( it->second.begin(), it->second.end() );\r
- if( it->first.isNull() ){\r
- Trace("sg-gen-tg-debug") << "In this order : ";\r
- for( unsigned i=0; i<it->second.size(); i++ ){\r
- Trace("sg-gen-tg-debug") << it->second[i] << " ";\r
- }\r
- Trace("sg-gen-tg-debug") << std::endl;\r
- }\r
- }\r
+ d_tge.collectSignatureInformation();\r
Trace("sg-proc") << "...done collect signature information" << std::endl;\r
+ \r
\r
\r
Trace("sg-proc") << "Build theorem index..." << std::endl;\r
d_thm_index.debugPrint( "thm-db" );\r
Trace("thm-db") << std::endl;\r
Trace("sg-proc") << "...done build theorem index" << std::endl;\r
+ \r
\r
//clear patterns\r
d_patterns.clear();\r
d_rel_pattern_var_sum.clear();\r
d_rel_pattern_typ_index.clear();\r
d_rel_pattern_subs_index.clear();\r
- //d_gen_lat_maximal.clear();\r
- //d_gen_lat_child.clear();\r
- //d_gen_lat_parent.clear();\r
- //d_gen_depth.clear();\r
\r
unsigned rel_term_count = 0;\r
- //consider all functions from relevant signature\r
- d_typ_tg_funcs.clear();\r
- for( std::map< TypeNode, std::vector< TNode > >::iterator it = d_typ_funcs.begin(); it != d_typ_funcs.end(); ++it ){\r
- d_typ_tg_funcs[it->first].insert( d_typ_tg_funcs[it->first].end(), it->second.begin(), it->second.end() );\r
- }\r
std::map< TypeNode, unsigned > rt_var_max;\r
std::vector< TypeNode > rt_types;\r
std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs;\r
for( unsigned depth=1; depth<=3; depth++ ){\r
- Assert( d_tg_alloc.empty() );\r
Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl;\r
Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl;\r
//set up environment\r
- for( unsigned i=0; i<2; i++ ){\r
- d_ccand_eqc[i].clear();\r
- d_ccand_eqc[i].push_back( d_relevant_eqc[i] );\r
- }\r
- d_var_id.clear();\r
- d_var_limit.clear();\r
- d_tg_id = 0;\r
- d_tg_gdepth = 0;\r
- d_tg_gdepth_limit = depth;\r
- d_gen_relevant_terms = true; \r
- //consider all types\r
- d_tg_alloc[0].reset( this, TypeNode::null() );\r
- while( d_tg_alloc[0].getNextTerm( this, depth ) ){\r
- //Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );\r
- //if( d_tg_alloc[0].getDepth( this )==depth ){\r
- if( d_tg_alloc[0].getGeneralizationDepth( this )==depth ){\r
- //construct term\r
- Node nn = d_tg_alloc[0].getTerm( this );\r
- if( getUniversalRepresentative( nn )==nn ){\r
- rel_term_count++;\r
- Trace("sg-rel-term") << "*** Relevant term : ";\r
- d_tg_alloc[0].debugPrint( this, "sg-rel-term", "sg-rel-term-debug2" );\r
- Trace("sg-rel-term") << std::endl;\r
-\r
- for( unsigned r=0; r<2; r++ ){\r
- Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";\r
- int index = d_ccand_eqc[r].size()-1;\r
- for( unsigned j=0; j<d_ccand_eqc[r][index].size(); j++ ){\r
- Trace("sg-rel-term-debug") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";\r
- }\r
- Trace("sg-rel-term-debug") << std::endl;\r
- }\r
- TypeNode tnn = nn.getType();\r
- Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;\r
- conj_lhs[tnn][depth].push_back( nn );\r
-\r
- //add information about pattern\r
- Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl;\r
- Assert( std::find( d_rel_patterns[tnn].begin(), d_rel_patterns[tnn].end(), nn )==d_rel_patterns[tnn].end() );\r
- d_rel_patterns[tnn].push_back( nn );\r
- //build information concerning the variables in this pattern\r
- unsigned sum = 0;\r
- std::map< TypeNode, unsigned > typ_to_subs_index;\r
- std::vector< TNode > gsubs_vars;\r
- for( std::map< TypeNode, unsigned >::iterator it = d_var_id.begin(); it != d_var_id.end(); ++it ){\r
- if( it->second>0 ){\r
- typ_to_subs_index[it->first] = sum;\r
- sum += it->second;\r
- for( unsigned i=0; i<it->second; i++ ){\r
- gsubs_vars.push_back( getFreeVar( it->first, i ) );\r
- }\r
- }\r
+ d_tge.d_var_id.clear();\r
+ d_tge.d_var_limit.clear();\r
+ d_tge.reset( depth, true, TypeNode::null() );\r
+ while( d_tge.getNextTerm() ){\r
+ //construct term\r
+ Node nn = d_tge.getTerm();\r
+ if( !options::conjectureFilterCanonical() || getUniversalRepresentative( nn )==nn ){\r
+ rel_term_count++;\r
+ Trace("sg-rel-term") << "*** Relevant term : ";\r
+ d_tge.debugPrint( "sg-rel-term", "sg-rel-term-debug2" );\r
+ Trace("sg-rel-term") << std::endl;\r
+\r
+ for( unsigned r=0; r<2; r++ ){\r
+ Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";\r
+ int index = d_tge.d_ccand_eqc[r].size()-1;\r
+ for( unsigned j=0; j<d_tge.d_ccand_eqc[r][index].size(); j++ ){\r
+ Trace("sg-rel-term-debug") << "e" << d_em[d_tge.d_ccand_eqc[r][index][j]] << " ";\r
}\r
- d_rel_pattern_var_sum[nn] = sum;\r
- //register the pattern\r
- registerPattern( nn, tnn );\r
- Assert( d_pattern_is_normal[nn] );\r
- Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl;\r
-\r
- //record information about types\r
- Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl;\r
- PatternTypIndex * pti = &d_rel_pattern_typ_index;\r
- for( std::map< TypeNode, unsigned >::iterator it = d_var_id.begin(); it != d_var_id.end(); ++it ){\r
- pti = &pti->d_children[it->first][it->second];\r
- //record maximum\r
- if( rt_var_max.find( it->first )==rt_var_max.end() || it->second>rt_var_max[it->first] ){\r
- rt_var_max[it->first] = it->second;\r
+ Trace("sg-rel-term-debug") << std::endl;\r
+ }\r
+ TypeNode tnn = nn.getType();\r
+ Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;\r
+ conj_lhs[tnn][depth].push_back( nn );\r
+\r
+ //add information about pattern\r
+ Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl;\r
+ Assert( std::find( d_rel_patterns[tnn].begin(), d_rel_patterns[tnn].end(), nn )==d_rel_patterns[tnn].end() );\r
+ d_rel_patterns[tnn].push_back( nn );\r
+ //build information concerning the variables in this pattern\r
+ unsigned sum = 0;\r
+ std::map< TypeNode, unsigned > typ_to_subs_index;\r
+ std::vector< TNode > gsubs_vars;\r
+ for( std::map< TypeNode, unsigned >::iterator it = d_tge.d_var_id.begin(); it != d_tge.d_var_id.end(); ++it ){\r
+ if( it->second>0 ){\r
+ typ_to_subs_index[it->first] = sum;\r
+ sum += it->second;\r
+ for( unsigned i=0; i<it->second; i++ ){\r
+ gsubs_vars.push_back( getFreeVar( it->first, i ) );\r
}\r
}\r
- if( std::find( rt_types.begin(), rt_types.end(), tnn )==rt_types.end() ){\r
- rt_types.push_back( tnn );\r
+ }\r
+ d_rel_pattern_var_sum[nn] = sum;\r
+ //register the pattern\r
+ registerPattern( nn, tnn );\r
+ Assert( d_pattern_is_normal[nn] );\r
+ Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl;\r
+\r
+ //record information about types\r
+ Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl;\r
+ PatternTypIndex * pti = &d_rel_pattern_typ_index;\r
+ for( std::map< TypeNode, unsigned >::iterator it = d_tge.d_var_id.begin(); it != d_tge.d_var_id.end(); ++it ){\r
+ pti = &pti->d_children[it->first][it->second];\r
+ //record maximum\r
+ if( rt_var_max.find( it->first )==rt_var_max.end() || it->second>rt_var_max[it->first] ){\r
+ rt_var_max[it->first] = it->second;\r
}\r
- pti->d_terms.push_back( nn );\r
- Trace("sg-gen-tg-debug") << "...done collect type information" << std::endl;\r
-\r
- Trace("sg-gen-tg-debug") << "Build substitutions for ground EQC..." << std::endl;\r
- std::vector< TNode > gsubs_terms;\r
- gsubs_terms.resize( gsubs_vars.size() );\r
- int index = d_ccand_eqc[1].size()-1;\r
- for( unsigned j=0; j<d_ccand_eqc[1][index].size(); j++ ){\r
- TNode r = d_ccand_eqc[1][index][j];\r
- Trace("sg-rel-term-debug") << " Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;\r
- std::map< TypeNode, std::map< unsigned, TNode > > subs;\r
- std::map< TNode, bool > rev_subs;\r
- //only get ground terms\r
- unsigned mode = optFilterConfirmationOnlyGround() ? 2 : 0;\r
- d_tg_alloc[0].resetMatching( this, r, mode );\r
- while( d_tg_alloc[0].getNextMatch( this, r, subs, rev_subs ) ){\r
- //we will be building substitutions\r
- bool firstTime = true;\r
- for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator it = subs.begin(); it != subs.end(); ++it ){\r
- unsigned tindex = typ_to_subs_index[it->first];\r
- for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
- if( !firstTime ){\r
- Trace("sg-rel-term-debug") << ", ";\r
- }else{\r
- firstTime = false;\r
- Trace("sg-rel-term-debug") << " ";\r
- }\r
- Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;\r
- Assert( tindex+it2->first<gsubs_terms.size() );\r
- gsubs_terms[tindex+it2->first] = it2->second;\r
+ }\r
+ if( std::find( rt_types.begin(), rt_types.end(), tnn )==rt_types.end() ){\r
+ rt_types.push_back( tnn );\r
+ }\r
+ pti->d_terms.push_back( nn );\r
+ Trace("sg-gen-tg-debug") << "...done collect type information" << std::endl;\r
+\r
+ Trace("sg-gen-tg-debug") << "Build substitutions for ground EQC..." << std::endl;\r
+ std::vector< TNode > gsubs_terms;\r
+ gsubs_terms.resize( gsubs_vars.size() );\r
+ int index = d_tge.d_ccand_eqc[1].size()-1;\r
+ for( unsigned j=0; j<d_tge.d_ccand_eqc[1][index].size(); j++ ){\r
+ TNode r = d_tge.d_ccand_eqc[1][index][j];\r
+ Trace("sg-rel-term-debug") << " Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;\r
+ std::map< TypeNode, std::map< unsigned, TNode > > subs;\r
+ std::map< TNode, bool > rev_subs;\r
+ //only get ground terms\r
+ unsigned mode = optFilterConfirmationOnlyGround() ? 2 : 0;\r
+ d_tge.resetMatching( r, mode );\r
+ while( d_tge.getNextMatch( r, subs, rev_subs ) ){\r
+ //we will be building substitutions\r
+ bool firstTime = true;\r
+ for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator it = subs.begin(); it != subs.end(); ++it ){\r
+ unsigned tindex = typ_to_subs_index[it->first];\r
+ for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+ if( !firstTime ){\r
+ Trace("sg-rel-term-debug") << ", ";\r
+ }else{\r
+ firstTime = false;\r
+ Trace("sg-rel-term-debug") << " ";\r
}\r
+ Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;\r
+ Assert( tindex+it2->first<gsubs_terms.size() );\r
+ gsubs_terms[tindex+it2->first] = it2->second;\r
}\r
- Trace("sg-rel-term-debug") << std::endl;\r
- d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );\r
}\r
+ Trace("sg-rel-term-debug") << std::endl;\r
+ d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );\r
}\r
- Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl;\r
- }else{\r
- Trace("sg-gen-tg-debug") << "> not canonical : " << nn << std::endl;\r
}\r
+ Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl;\r
}else{\r
- Trace("sg-gen-tg-debug") << "> produced term at previous depth : ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
- Trace("sg-gen-tg-debug") << std::endl;\r
+ Trace("sg-gen-tg-debug") << "> not canonical : " << nn << std::endl;\r
}\r
}\r
Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;\r
//consider types from relevant terms\r
for( unsigned rdepth=0; rdepth<=depth; rdepth++ ){\r
//set up environment\r
- d_gen_relevant_terms = false;\r
- d_var_id.clear();\r
- d_var_limit.clear();\r
+ d_tge.d_var_id.clear();\r
+ d_tge.d_var_limit.clear();\r
for( std::map< TypeNode, unsigned >::iterator it = rt_var_max.begin(); it != rt_var_max.end(); ++it ){\r
- d_var_id[ it->first ] = it->second;\r
- d_var_limit[ it->first ] = it->second;\r
+ d_tge.d_var_id[ it->first ] = it->second;\r
+ d_tge.d_var_limit[ it->first ] = it->second;\r
}\r
std::random_shuffle( rt_types.begin(), rt_types.end() );\r
std::map< TypeNode, std::vector< Node > > conj_rhs;\r
for( unsigned i=0; i<rt_types.size(); i++ ){\r
- Assert( d_tg_alloc.empty() );\r
+\r
Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types[i] << " at depth " << rdepth << "..." << std::endl;\r
- d_tg_id = 0;\r
- d_tg_gdepth = 0;\r
- d_tg_gdepth_limit = rdepth;\r
- d_tg_alloc[0].reset( this, rt_types[i] );\r
- while( d_tg_alloc[0].getNextTerm( this, rdepth ) ){\r
- if( d_tg_alloc[0].getGeneralizationDepth( this )==rdepth ){\r
- Node rhs = d_tg_alloc[0].getTerm( this );\r
- Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;\r
- //register pattern\r
- Assert( rhs.getType()==rt_types[i] );\r
- registerPattern( rhs, rt_types[i] );\r
- if( rdepth<depth ){\r
- //consider against all LHS at depth\r
- for( unsigned j=0; j<conj_lhs[rt_types[i]][depth].size(); j++ ){\r
- processCandidateConjecture( conj_lhs[rt_types[i]][depth][j], rhs, depth, rdepth );\r
- }\r
- }else{\r
- conj_rhs[rt_types[i]].push_back( rhs );\r
+ d_tge.reset( rdepth, false, rt_types[i] );\r
+ \r
+ while( d_tge.getNextTerm() ){\r
+ Node rhs = d_tge.getTerm();\r
+ Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;\r
+ //register pattern\r
+ Assert( rhs.getType()==rt_types[i] );\r
+ registerPattern( rhs, rt_types[i] );\r
+ if( rdepth<depth ){\r
+ //consider against all LHS at depth\r
+ for( unsigned j=0; j<conj_lhs[rt_types[i]][depth].size(); j++ ){\r
+ processCandidateConjecture( conj_lhs[rt_types[i]][depth][j], rhs, depth, rdepth );\r
}\r
+ }else{\r
+ conj_rhs[rt_types[i]].push_back( rhs );\r
}\r
}\r
- //could have been partial, we must clear\r
- //REMOVE_THIS?\r
- d_tg_alloc.clear();\r
}\r
//consider against all LHS up to depth\r
if( rdepth==depth ){\r
\r
}\r
\r
-\r
-unsigned ConjectureGenerator::getNumTgVars( TypeNode tn ) {\r
- //return d_var_tg.size();\r
- return d_var_id[tn];\r
-}\r
-\r
-bool ConjectureGenerator::allowVar( TypeNode tn ) {\r
- std::map< TypeNode, unsigned >::iterator it = d_var_limit.find( tn );\r
- if( it==d_var_limit.end() ){\r
- return true;\r
- }else{\r
- return d_var_id[tn]<it->second;\r
- }\r
-}\r
-\r
-void ConjectureGenerator::addVar( TypeNode tn ) {\r
- //d_var_tg.push_back( v );\r
- d_var_id[tn]++;\r
- //d_var_eq_tg.push_back( std::vector< unsigned >() );\r
-}\r
-\r
-void ConjectureGenerator::removeVar( TypeNode tn ) {\r
- d_var_id[tn]--;\r
- //d_var_eq_tg.pop_back();\r
- //d_var_tg.pop_back();\r
-}\r
-\r
-unsigned ConjectureGenerator::getNumTgFuncs( TypeNode tn ) {\r
- return d_typ_tg_funcs[tn].size();\r
-}\r
-\r
-TNode ConjectureGenerator::getTgFunc( TypeNode tn, unsigned i ) {\r
- return d_typ_tg_funcs[tn][i];\r
-}\r
-\r
-bool ConjectureGenerator::considerCurrentTerm() {\r
- Assert( !d_tg_alloc.empty() );\r
-\r
- //if generalization depth is too large, don't consider it\r
- unsigned i = d_tg_alloc.size();\r
- Trace("sg-gen-tg-debug") << "Consider term ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
- Trace("sg-gen-tg-debug") << "? curr term size = " << d_tg_alloc.size() << ", last status = " << d_tg_alloc[i-1].d_status;\r
- Trace("sg-gen-tg-debug") << std::endl;\r
-\r
- if( d_tg_gdepth_limit>=0 && d_tg_alloc[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit ){\r
- Trace("sg-gen-consider-term") << "-> generalization depth of ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );\r
- Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth << " " << d_tg_alloc[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl;\r
- return false;\r
- }\r
-\r
- //----optimizations\r
- /*\r
- if( d_tg_alloc[i-1].d_status==1 ){\r
- }else if( d_tg_alloc[i-1].d_status==2 ){\r
- }else if( d_tg_alloc[i-1].d_status==5 ){\r
- }else{\r
- Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl;\r
- Assert( false );\r
- }\r
- */\r
- //if equated two variables, first check if context-independent TODO\r
- //----end optimizations\r
-\r
-\r
- //check based on which candidate equivalence classes match\r
- if( d_gen_relevant_terms ){\r
- Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";\r
- Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl;\r
-\r
- Assert( d_ccand_eqc[0].size()>=2 );\r
- Assert( d_ccand_eqc[0].size()==d_ccand_eqc[1].size() );\r
- Assert( d_ccand_eqc[0].size()==d_tg_id+1 );\r
- Assert( d_tg_id==d_tg_alloc.size() );\r
- for( unsigned r=0; r<2; r++ ){\r
- d_ccand_eqc[r][i].clear();\r
- }\r
-\r
- //re-check feasibility of EQC\r
- for( unsigned r=0; r<2; r++ ){\r
- for( unsigned j=0; j<d_ccand_eqc[r][i-1].size(); j++ ){\r
- std::map< TypeNode, std::map< unsigned, TNode > > subs;\r
- std::map< TNode, bool > rev_subs;\r
- unsigned mode;\r
- if( r==0 ){\r
- mode = optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;\r
- mode = mode | (1 << 2 );\r
- }else{\r
- mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? ( 1 << 1 ) : 0;\r
- }\r
- d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );\r
- if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){\r
- d_ccand_eqc[r][i].push_back( d_ccand_eqc[r][i-1][j] );\r
- }\r
- }\r
- }\r
- for( unsigned r=0; r<2; r++ ){\r
- Trace("sg-gen-tg-debug") << "Current eqc of type " << r << " : ";\r
- for( unsigned j=0; j<d_ccand_eqc[r][i].size(); j++ ){\r
- Trace("sg-gen-tg-debug") << "e" << d_em[d_ccand_eqc[r][i][j]] << " ";\r
- }\r
- Trace("sg-gen-tg-debug") << std::endl;\r
- }\r
- if( options::conjectureFilterActiveTerms() && d_ccand_eqc[0][i].empty() ){\r
- Trace("sg-gen-consider-term") << "Do not consider term of form ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );\r
- Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl;\r
- return false;\r
- }\r
- if( options::conjectureFilterModel() && d_ccand_eqc[1][i].empty() && optFilterConfirmation() ){\r
- Trace("sg-gen-consider-term") << "Do not consider term of form ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );\r
- Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl;\r
+bool ConjectureGenerator::considerCurrentTermCanon( Node ln, bool genRelevant ){\r
+ if( !ln.isNull() ){\r
+ //do not consider if it is non-canonical, and either:\r
+ // (1) we are not generating relevant terms, or\r
+ // (2) its canonical form is a generalization.\r
+ TNode lnr = getUniversalRepresentative( ln, true );\r
+ if( lnr==ln ){\r
+ markReportedCanon( ln );\r
+ }else if( !genRelevant || isGeneralization( lnr, ln ) ){\r
+ Trace("sg-gen-consider-term") << "Do not consider term, " << ln << " is not canonical representation (which is " << lnr << ")." << std::endl;\r
return false;\r
}\r
}\r
- Trace("sg-gen-tg-debug") << "Will consider term ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
- Trace("sg-gen-tg-debug") << std::endl;\r
+ Trace("sg-gen-tg-debug") << "Will consider term canon " << ln << std::endl;\r
Trace("sg-gen-consider-term-debug") << std::endl;\r
return true;\r
}\r
\r
-bool ConjectureGenerator::considerCurrentTermCanon( unsigned tg_id ){\r
- Assert( tg_id<d_tg_alloc.size() );\r
- if( options::conjectureFilterCanonical() ){\r
- //check based on a canonicity of the term (if there is one)\r
- Trace("sg-gen-tg-debug") << "Consider term canon ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
- Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl;\r
-\r
- Node ln = d_tg_alloc[tg_id].getTerm( this );\r
- Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl;\r
- if( !ln.isNull() ){\r
- //do not consider if it is non-canonical, and either:\r
- // (1) we are not generating relevant terms, or\r
- // (2) its canonical form is a generalization.\r
- TNode lnr = getUniversalRepresentative( ln, true );\r
- if( lnr==ln ){\r
- markReportedCanon( ln );\r
- }else if( !d_gen_relevant_terms || isGeneralization( lnr, ln ) ){\r
- Trace("sg-gen-consider-term") << "Do not consider term of form ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );\r
- Trace("sg-gen-consider-term") << " since sub-term " << ln << " is not canonical representation (which is " << lnr << ")." << std::endl;\r
- return false;\r
- }\r
- }\r
- Trace("sg-gen-tg-debug") << "Will consider term canon ";\r
- d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
- Trace("sg-gen-tg-debug") << std::endl;\r
- Trace("sg-gen-consider-term-debug") << std::endl;\r
- }\r
- return true;\r
-}\r
-\r
-void ConjectureGenerator::changeContext( bool add ) {\r
- if( add ){\r
- for( unsigned r=0; r<2; r++ ){\r
- d_ccand_eqc[r].push_back( std::vector< TNode >() );\r
- }\r
- d_tg_id++;\r
- }else{\r
- for( unsigned r=0; r<2; r++ ){\r
- d_ccand_eqc[r].pop_back();\r
- }\r
- d_tg_id--;\r
- Assert( d_tg_alloc.find( d_tg_id )!=d_tg_alloc.end() );\r
- d_tg_alloc.erase( d_tg_id );\r
- }\r
-}\r
-\r
unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,\r
std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn ){\r
if( pat.hasOperator() ){\r
funcs[pat.getOperator()]++;\r
- if( !isRelevantFunc( pat.getOperator() ) ){\r
+ if( !d_tge.isRelevantFunc( pat.getOperator() ) ){\r
d_pattern_is_relevant[opat] = false;\r
}\r
unsigned sum = 1;\r
}\r
\r
\r
-void TermGenerator::reset( ConjectureGenerator * s, TypeNode tn ) {\r
+\r
+\r
+\r
+\r
+void TermGenerator::reset( TermGenEnv * s, TypeNode tn ) {\r
Assert( d_children.empty() );\r
d_typ = tn;\r
d_status = 0;\r
s->changeContext( true );\r
}\r
\r
-bool TermGenerator::getNextTerm( ConjectureGenerator * s, unsigned depth ) {\r
+bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {\r
if( Trace.isOn("sg-gen-tg-debug2") ){\r
Trace("sg-gen-tg-debug2") << this << " getNextTerm depth " << depth << " : status = " << d_status << ", num = " << d_status_num;\r
if( d_status==5 ){\r
}\r
}\r
\r
-void TermGenerator::resetMatching( ConjectureGenerator * s, TNode eqc, unsigned mode ) {\r
+void TermGenerator::resetMatching( TermGenEnv * s, TNode eqc, unsigned mode ) {\r
d_match_status = 0;\r
d_match_status_child_num = 0;\r
d_match_children.clear();\r
//}\r
}\r
\r
-bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {\r
+bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {\r
if( d_match_status<0 ){\r
return false;\r
}\r
if( Trace.isOn("sg-gen-tg-match") ){\r
Trace("sg-gen-tg-match") << "Matching ";\r
debugPrint( s, "sg-gen-tg-match", "sg-gen-tg-match" );\r
- Trace("sg-gen-tg-match") << " with eqc e" << s->d_em[eqc] << "..." << std::endl;\r
+ Trace("sg-gen-tg-match") << " with eqc e" << s->d_cg->d_em[eqc] << "..." << std::endl;\r
Trace("sg-gen-tg-match") << " mstatus = " << d_match_status;\r
if( d_status==5 ){\r
TNode f = s->getTgFunc( d_typ, d_status_num );\r
Trace("sg-gen-tg-debug2") << ", current substitution : {";\r
for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator itt = subs.begin(); itt != subs.end(); ++itt ){\r
for( std::map< unsigned, TNode >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){\r
- Trace("sg-gen-tg-debug2") << " " << it->first << " -> e" << s->d_em[it->second];\r
+ Trace("sg-gen-tg-debug2") << " " << it->first << " -> e" << s->d_cg->d_em[it->second];\r
}\r
}\r
Trace("sg-gen-tg-debug2") << " } " << std::endl;\r
return false;\r
}\r
\r
-unsigned TermGenerator::getDepth( ConjectureGenerator * s ) {\r
+unsigned TermGenerator::getDepth( TermGenEnv * s ) {\r
if( d_status==5 ){\r
unsigned maxd = 0;\r
for( unsigned i=0; i<d_children.size(); i++ ){\r
}\r
}\r
\r
-unsigned TermGenerator::calculateGeneralizationDepth( ConjectureGenerator * s, std::map< TypeNode, std::vector< int > >& fvs ) {\r
+unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ) {\r
if( d_status==5 ){\r
unsigned sum = 1;\r
for( unsigned i=0; i<d_children.size(); i++ ){\r
}\r
}\r
\r
-unsigned TermGenerator::getGeneralizationDepth( ConjectureGenerator * s ) {\r
+unsigned TermGenerator::getGeneralizationDepth( TermGenEnv * s ) {\r
//if( s->d_gen_relevant_terms ){\r
// return s->d_tg_gdepth;\r
//}else{\r
//}\r
}\r
\r
-Node TermGenerator::getTerm( ConjectureGenerator * s ) {\r
+Node TermGenerator::getTerm( TermGenEnv * s ) {\r
if( d_status==1 || d_status==2 ){\r
Assert( !d_typ.isNull() );\r
return s->getFreeVar( d_typ, d_status_num );\r
return Node::null();\r
}\r
\r
-void TermGenerator::debugPrint( ConjectureGenerator * s, const char * c, const char * cd ) {\r
+void TermGenerator::debugPrint( TermGenEnv * s, const char * c, const char * cd ) {\r
Trace(cd) << "[*" << d_id << "," << d_status << "]:";\r
if( d_status==1 || d_status==2 ){\r
Trace(c) << s->getFreeVar( d_typ, d_status_num );\r
}\r
}\r
\r
+void TermGenEnv::collectSignatureInformation() {\r
+ d_typ_tg_funcs.clear();\r
+ d_funcs.clear();\r
+ d_func_kind.clear();\r
+ d_func_args.clear();\r
+ TypeNode tnull;\r
+ for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){\r
+ if( !getTermDatabase()->d_op_map[it->first].empty() ){\r
+ Node nn = getTermDatabase()->d_op_map[it->first][0];\r
+ if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){\r
+ d_funcs.push_back( it->first );\r
+ for( unsigned i=0; i<nn.getNumChildren(); i++ ){\r
+ d_func_args[it->first].push_back( nn[i].getType() );\r
+ }\r
+ d_func_kind[it->first] = nn.getKind();\r
+ d_typ_tg_funcs[tnull].push_back( it->first );\r
+ d_typ_tg_funcs[nn.getType()].push_back( it->first );\r
+ Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;\r
+ getTermDatabase()->computeUfEqcTerms( it->first );\r
+ }\r
+ }\r
+ }\r
+ //shuffle functions\r
+ for( std::map< TypeNode, std::vector< TNode > >::iterator it = d_typ_tg_funcs.begin(); it != d_typ_tg_funcs.end(); ++it ){\r
+ std::random_shuffle( it->second.begin(), it->second.end() );\r
+ if( it->first.isNull() ){\r
+ Trace("sg-gen-tg-debug") << "In this order : ";\r
+ for( unsigned i=0; i<it->second.size(); i++ ){\r
+ Trace("sg-gen-tg-debug") << it->second[i] << " ";\r
+ }\r
+ Trace("sg-gen-tg-debug") << std::endl;\r
+ }\r
+ }\r
+}\r
+\r
+void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) {\r
+ Assert( d_tg_alloc.empty() );\r
+ d_tg_alloc.clear();\r
+ \r
+ if( genRelevant ){\r
+ for( unsigned i=0; i<2; i++ ){\r
+ d_ccand_eqc[i].clear();\r
+ d_ccand_eqc[i].push_back( d_relevant_eqc[i] );\r
+ }\r
+ }\r
+ \r
+ d_tg_id = 0;\r
+ d_tg_gdepth = 0;\r
+ d_tg_gdepth_limit = depth;\r
+ d_gen_relevant_terms = genRelevant; \r
+ d_tg_alloc[0].reset( this, tn );\r
+}\r
+\r
+bool TermGenEnv::getNextTerm() {\r
+ if( d_tg_alloc[0].getNextTerm( this, d_tg_gdepth_limit ) ){\r
+ Assert( (int)d_tg_alloc[0].getGeneralizationDepth( this )<=d_tg_gdepth_limit );\r
+ if( (int)d_tg_alloc[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit ){\r
+ return getNextTerm();\r
+ }else{\r
+ return true;\r
+ }\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+//reset matching\r
+void TermGenEnv::resetMatching( TNode eqc, unsigned mode ) { \r
+ d_tg_alloc[0].resetMatching( this, eqc, mode ); \r
+}\r
+\r
+//get next match\r
+bool TermGenEnv::getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {\r
+ return d_tg_alloc[0].getNextMatch( this, eqc, subs, rev_subs );\r
+}\r
+\r
+//get term\r
+Node TermGenEnv::getTerm() { \r
+ return d_tg_alloc[0].getTerm( this ); \r
+}\r
+\r
+void TermGenEnv::debugPrint( const char * c, const char * cd ) {\r
+ d_tg_alloc[0].debugPrint( this, c, cd );\r
+}\r
+\r
+unsigned TermGenEnv::getNumTgVars( TypeNode tn ) {\r
+ return d_var_id[tn];\r
+}\r
+\r
+bool TermGenEnv::allowVar( TypeNode tn ) {\r
+ std::map< TypeNode, unsigned >::iterator it = d_var_limit.find( tn );\r
+ if( it==d_var_limit.end() ){\r
+ return true;\r
+ }else{\r
+ return d_var_id[tn]<it->second;\r
+ }\r
+}\r
+\r
+void TermGenEnv::addVar( TypeNode tn ) {\r
+ d_var_id[tn]++;\r
+}\r
+\r
+void TermGenEnv::removeVar( TypeNode tn ) {\r
+ d_var_id[tn]--;\r
+ //d_var_eq_tg.pop_back();\r
+ //d_var_tg.pop_back();\r
+}\r
+\r
+unsigned TermGenEnv::getNumTgFuncs( TypeNode tn ) {\r
+ return d_typ_tg_funcs[tn].size();\r
+}\r
+\r
+TNode TermGenEnv::getTgFunc( TypeNode tn, unsigned i ) {\r
+ return d_typ_tg_funcs[tn][i];\r
+}\r
+\r
+Node TermGenEnv::getFreeVar( TypeNode tn, unsigned i ) {\r
+ return d_cg->getFreeVar( tn, i );\r
+}\r
+\r
+bool TermGenEnv::considerCurrentTerm() {\r
+ Assert( !d_tg_alloc.empty() );\r
+\r
+ //if generalization depth is too large, don't consider it\r
+ unsigned i = d_tg_alloc.size();\r
+ Trace("sg-gen-tg-debug") << "Consider term ";\r
+ d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
+ Trace("sg-gen-tg-debug") << "? curr term size = " << d_tg_alloc.size() << ", last status = " << d_tg_alloc[i-1].d_status;\r
+ Trace("sg-gen-tg-debug") << std::endl;\r
+\r
+ if( d_tg_gdepth_limit>=0 && d_tg_alloc[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit ){\r
+ Trace("sg-gen-consider-term") << "-> generalization depth of ";\r
+ d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );\r
+ Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth << " " << d_tg_alloc[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl;\r
+ return false;\r
+ }\r
+\r
+ //----optimizations\r
+ /*\r
+ if( d_tg_alloc[i-1].d_status==1 ){\r
+ }else if( d_tg_alloc[i-1].d_status==2 ){\r
+ }else if( d_tg_alloc[i-1].d_status==5 ){\r
+ }else{\r
+ Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl;\r
+ Assert( false );\r
+ }\r
+ */\r
+ //if equated two variables, first check if context-independent TODO\r
+ //----end optimizations\r
+\r
+\r
+ //check based on which candidate equivalence classes match\r
+ if( d_gen_relevant_terms ){\r
+ Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";\r
+ Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl;\r
+\r
+ Assert( d_ccand_eqc[0].size()>=2 );\r
+ Assert( d_ccand_eqc[0].size()==d_ccand_eqc[1].size() );\r
+ Assert( d_ccand_eqc[0].size()==d_tg_id+1 );\r
+ Assert( d_tg_id==d_tg_alloc.size() );\r
+ for( unsigned r=0; r<2; r++ ){\r
+ d_ccand_eqc[r][i].clear();\r
+ }\r
+\r
+ //re-check feasibility of EQC\r
+ for( unsigned r=0; r<2; r++ ){\r
+ for( unsigned j=0; j<d_ccand_eqc[r][i-1].size(); j++ ){\r
+ std::map< TypeNode, std::map< unsigned, TNode > > subs;\r
+ std::map< TNode, bool > rev_subs;\r
+ unsigned mode;\r
+ if( r==0 ){\r
+ mode = d_cg->optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;\r
+ mode = mode | (1 << 2 );\r
+ }else{\r
+ mode = (d_cg->optFilterConfirmation() && d_cg->optFilterConfirmationOnlyGround() ) ? ( 1 << 1 ) : 0;\r
+ }\r
+ d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );\r
+ if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){\r
+ d_ccand_eqc[r][i].push_back( d_ccand_eqc[r][i-1][j] );\r
+ }\r
+ }\r
+ }\r
+ for( unsigned r=0; r<2; r++ ){\r
+ Trace("sg-gen-tg-debug") << "Current eqc of type " << r << " : ";\r
+ for( unsigned j=0; j<d_ccand_eqc[r][i].size(); j++ ){\r
+ Trace("sg-gen-tg-debug") << "e" << d_cg->d_em[d_ccand_eqc[r][i][j]] << " ";\r
+ }\r
+ Trace("sg-gen-tg-debug") << std::endl;\r
+ }\r
+ if( options::conjectureFilterActiveTerms() && d_ccand_eqc[0][i].empty() ){\r
+ Trace("sg-gen-consider-term") << "Do not consider term of form ";\r
+ d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );\r
+ Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl;\r
+ return false;\r
+ }\r
+ if( options::conjectureFilterModel() && d_ccand_eqc[1][i].empty() && d_cg->optFilterConfirmation() ){\r
+ Trace("sg-gen-consider-term") << "Do not consider term of form ";\r
+ d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );\r
+ Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl;\r
+ return false;\r
+ }\r
+ }\r
+ Trace("sg-gen-tg-debug") << "Will consider term ";\r
+ d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
+ Trace("sg-gen-tg-debug") << std::endl;\r
+ Trace("sg-gen-consider-term-debug") << std::endl;\r
+ return true;\r
+}\r
+\r
+void TermGenEnv::changeContext( bool add ) {\r
+ if( add ){\r
+ for( unsigned r=0; r<2; r++ ){\r
+ d_ccand_eqc[r].push_back( std::vector< TNode >() );\r
+ }\r
+ d_tg_id++;\r
+ }else{\r
+ for( unsigned r=0; r<2; r++ ){\r
+ d_ccand_eqc[r].pop_back();\r
+ }\r
+ d_tg_id--;\r
+ Assert( d_tg_alloc.find( d_tg_id )!=d_tg_alloc.end() );\r
+ d_tg_alloc.erase( d_tg_id );\r
+ }\r
+}\r
+\r
+bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){\r
+ Assert( tg_id<d_tg_alloc.size() );\r
+ if( options::conjectureFilterCanonical() ){\r
+ //check based on a canonicity of the term (if there is one)\r
+ Trace("sg-gen-tg-debug") << "Consider term canon ";\r
+ d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );\r
+ Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl;\r
+\r
+ Node ln = d_tg_alloc[tg_id].getTerm( this );\r
+ Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl;\r
+ return d_cg->considerCurrentTermCanon( ln, d_gen_relevant_terms );\r
+ }\r
+ return true;\r
+}\r
+\r
+bool TermGenEnv::isRelevantFunc( Node f ) {\r
+ return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end();\r
+}\r
+TermDb * TermGenEnv::getTermDatabase() {\r
+ return d_cg->getTermDatabase();\r
+}\r
+Node TermGenEnv::getGroundEqc( TNode r ) {\r
+ return d_cg->getGroundEqc( r );\r
+}\r
+bool TermGenEnv::isGroundEqc( TNode r ){\r
+ return d_cg->isGroundEqc( r );\r
+}\r
+bool TermGenEnv::isGroundTerm( TNode n ){\r
+ return d_cg->isGroundTerm( n );\r
+}\r
+\r
+\r
\r
void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i ) {\r
if( i==vars.size() ){\r
bool notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i = 0 );\r
};\r
\r
+class TermGenEnv;\r
+\r
class TermGenerator\r
{\r
private:\r
- unsigned calculateGeneralizationDepth( ConjectureGenerator * s, std::map< TypeNode, std::vector< int > >& fvs );\r
+ unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs );\r
public:\r
TermGenerator(){}\r
TypeNode d_typ;\r
std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;\r
std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end;\r
\r
- void reset( ConjectureGenerator * s, TypeNode tn );\r
- bool getNextTerm( ConjectureGenerator * s, unsigned depth );\r
- void resetMatching( ConjectureGenerator * s, TNode eqc, unsigned mode );\r
- bool getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );\r
+ void reset( TermGenEnv * s, TypeNode tn );\r
+ bool getNextTerm( TermGenEnv * s, unsigned depth );\r
+ void resetMatching( TermGenEnv * s, TNode eqc, unsigned mode );\r
+ bool getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );\r
+\r
+ unsigned getDepth( TermGenEnv * s );\r
+ unsigned getGeneralizationDepth( TermGenEnv * s );\r
+ Node getTerm( TermGenEnv * s );\r
\r
- unsigned getDepth( ConjectureGenerator * s );\r
- unsigned getGeneralizationDepth( ConjectureGenerator * s );\r
- Node getTerm( ConjectureGenerator * s );\r
+ void debugPrint( TermGenEnv * s, const char * c, const char * cd );\r
+};\r
\r
- void debugPrint( ConjectureGenerator * s, const char * c, const char * cd );\r
+\r
+class TermGenEnv\r
+{\r
+public:\r
+ //collect signature information\r
+ void collectSignatureInformation();\r
+ //reset function\r
+ void reset( unsigned gdepth, bool genRelevant, TypeNode tgen );\r
+ //get next term\r
+ bool getNextTerm();\r
+ //reset matching\r
+ void resetMatching( TNode eqc, unsigned mode );\r
+ //get next match\r
+ bool getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );\r
+ //get term\r
+ Node getTerm();\r
+ //debug print\r
+ void debugPrint( const char * c, const char * cd );\r
+ \r
+ //conjecture generation\r
+ ConjectureGenerator * d_cg;\r
+ //the current number of enumerated variables per type\r
+ std::map< TypeNode, unsigned > d_var_id;\r
+ //the limit of number of variables per type to enumerate\r
+ std::map< TypeNode, unsigned > d_var_limit;\r
+ //the functions we can currently generate\r
+ std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;\r
+ //the equivalence classes (if applicable) that match the currently generated term\r
+ bool d_gen_relevant_terms;\r
+ //relevant equivalence classes\r
+ std::vector< TNode > d_relevant_eqc[2];\r
+ //candidate equivalence classes\r
+ std::vector< std::vector< TNode > > d_ccand_eqc[2];\r
+ //the term generation objects\r
+ unsigned d_tg_id;\r
+ std::map< unsigned, TermGenerator > d_tg_alloc;\r
+ unsigned d_tg_gdepth;\r
+ int d_tg_gdepth_limit;\r
+ \r
+ //all functions\r
+ std::vector< TNode > d_funcs;\r
+ //function to kind map\r
+ std::map< TNode, Kind > d_func_kind;\r
+ //type of each argument of the function\r
+ std::map< TNode, std::vector< TypeNode > > d_func_args;\r
+ \r
+ //access functions\r
+ unsigned getNumTgVars( TypeNode tn );\r
+ bool allowVar( TypeNode tn );\r
+ void addVar( TypeNode tn );\r
+ void removeVar( TypeNode tn );\r
+ unsigned getNumTgFuncs( TypeNode tn );\r
+ TNode getTgFunc( TypeNode tn, unsigned i );\r
+ Node getFreeVar( TypeNode tn, unsigned i );\r
+ bool considerCurrentTerm();\r
+ bool considerCurrentTermCanon( unsigned tg_id );\r
+ void changeContext( bool add );\r
+ bool isRelevantFunc( Node f );\r
+ //carry\r
+ TermDb * getTermDatabase();\r
+ Node getGroundEqc( TNode r );\r
+ bool isGroundEqc( TNode r );\r
+ bool isGroundTerm( TNode n );\r
};\r
\r
\r
+\r
class TheoremIndex\r
{\r
private:\r
friend class PatternGen;\r
friend class SubsEqcIndex;\r
friend class TermGenerator;\r
+ friend class TermGenEnv;\r
typedef context::CDChunkList<Node> NodeList;\r
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;\r
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;\r
BoolMap d_ee_conjectures;\r
/** conjecture index */\r
TheoremIndex d_thm_index;\r
- /** the relevant equivalence classes based on the conjectures */\r
- std::vector< TNode > d_relevant_eqc[2];\r
-private: //information regarding the signature we are enumerating conjectures for\r
- //all functions\r
- std::vector< TNode > d_funcs;\r
- //functions per type\r
- std::map< TypeNode, std::vector< TNode > > d_typ_funcs;\r
- //function to kind map\r
- std::map< TNode, Kind > d_func_kind;\r
- //type of each argument of the function\r
- std::map< TNode, std::vector< TypeNode > > d_func_args;\r
+private: //free variable list\r
//free variables\r
std::map< TypeNode, std::vector< Node > > d_free_var;\r
//map from free variable to FV#\r
std::map< TNode, unsigned > d_free_var_num;\r
// get canonical free variable #i of type tn\r
Node getFreeVar( TypeNode tn, unsigned i );\r
- // get maximum free variable numbers\r
- void getMaxFreeVarNum( TNode n, std::map< TypeNode, unsigned >& mvn );\r
// get canonical term, return null if it contains a term apart from handled signature\r
Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs );\r
private: //information regarding the terms\r
void registerPattern( Node pat, TypeNode tpat );\r
private: //for debugging\r
std::map< TNode, unsigned > d_em;\r
-public: //environment for term enumeration\r
- //the current number of enumerated variables per type\r
- std::map< TypeNode, unsigned > d_var_id;\r
- //the limit of number of variables per type to enumerate\r
- std::map< TypeNode, unsigned > d_var_limit;\r
- //the functions we can currently generate\r
- std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;\r
- //the equivalence classes (if applicable) that match the currently generated term\r
- bool d_gen_relevant_terms;\r
- std::vector< std::vector< TNode > > d_ccand_eqc[2];\r
- //the term generation objects\r
- unsigned d_tg_id;\r
- std::map< unsigned, TermGenerator > d_tg_alloc;\r
- unsigned d_tg_gdepth;\r
- int d_tg_gdepth_limit;\r
- //access functions\r
- unsigned getNumTgVars( TypeNode tn );\r
- bool allowVar( TypeNode tn );\r
- void addVar( TypeNode tn );\r
- void removeVar( TypeNode tn );\r
- unsigned getNumTgFuncs( TypeNode tn );\r
- TNode getTgFunc( TypeNode tn, unsigned i );\r
- bool considerCurrentTerm();\r
- bool considerCurrentTermCanon( unsigned tg_id );\r
- void changeContext( bool add );\r
+public:\r
+ //term generation environment\r
+ TermGenEnv d_tge;\r
+ //consider term canon\r
+ bool considerCurrentTermCanon( Node ln, bool genRelevant );\r
public: //for generalization\r
//generalizations\r
bool isGeneralization( TNode patg, TNode pat ) {\r
Node getGroundEqc( TNode r );\r
bool isGroundEqc( TNode r );\r
bool isGroundTerm( TNode n );\r
- bool isRelevantFunc( Node f );\r
// count of full effort checks\r
unsigned d_fullEffortCount;\r
public:\r
projects / cvc5.git / commitdiff