}\r
Trace("thm-ee-debug") << "UEE : equality holds : " << t1 << " == " << t2 << std::endl;\r
Trace("thm-ee-debug") << " ureps : " << rt1 << " == " << rt2 << std::endl;\r
+ Trace("thm-ee-debug") << " relevant : " << d_pattern_is_relevant[rt1] << " " << d_pattern_is_relevant[rt2] << std::endl;\r
Trace("thm-ee-debug") << " normal : " << d_pattern_is_normal[rt1] << " " << d_pattern_is_normal[rt2] << std::endl;\r
Trace("thm-ee-debug") << " size : " << d_pattern_fun_sum[rt1] << " " << d_pattern_fun_sum[rt2] << std::endl;\r
\r
}\r
}\r
\r
-void ConjectureGenerator::doPendingAddUniversalTerms() {\r
- //merge all pending equalities\r
- while( !d_upendingAdds.empty() ){\r
- Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl;\r
- std::vector< Node > pending;\r
- pending.insert( pending.end(), d_upendingAdds.begin(), d_upendingAdds.end() );\r
- d_upendingAdds.clear();\r
- for( unsigned i=0; i<pending.size(); i++ ){\r
- Node t = pending[i];\r
- TypeNode tn = t.getType();\r
- Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;\r
- //get all equivalent terms based on theorem database\r
- std::vector< Node > eq_terms;\r
- d_thm_index.getEquivalentTerms( t, eq_terms );\r
- if( !eq_terms.empty() ){\r
- Trace("thm-ee-add") << "UEE : Based on theorem database, it is equivalent to " << eq_terms.size() << " terms : " << std::endl;\r
- //add equivalent terms as equalities to universal engine\r
- for( unsigned i=0; i<eq_terms.size(); i++ ){\r
- Trace("thm-ee-add") << " " << eq_terms[i] << std::endl;\r
- //if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){\r
- bool assertEq = false;\r
- if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){\r
- assertEq = true;\r
- }else{\r
- Assert( eq_terms[i].getType()==tn );\r
- registerPattern( eq_terms[i], tn );\r
- if( isUniversalLessThan( eq_terms[i], t ) ){\r
- setUniversalRelevant( eq_terms[i] );\r
- assertEq = true;\r
- }\r
- }\r
- if( assertEq ){\r
- Node exp;\r
- d_uequalityEngine.assertEquality( t.eqNode( eq_terms[i] ), true, exp );\r
- }\r
- }\r
- }else{\r
- Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;\r
- }\r
- //if occurs at ground level, merge with representative of ground equality engine\r
- /*\r
- eq::EqualityEngine * ee = getEqualityEngine();\r
- if( ee->hasTerm( t ) ){\r
- TNode grt = ee->getRepresentative( t );\r
- if( t!=grt ){\r
- Node exp;\r
- d_uequalityEngine.assertEquality( t.eqNode( grt ), true, exp );\r
- }\r
- }\r
- */\r
- }\r
- }\r
-}\r
-\r
void ConjectureGenerator::setUniversalRelevant( TNode n ) {\r
//add pattern information\r
registerPattern( n, n.getType() );\r
\r
bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) {\r
//prefer the one that is (normal, smaller) lexographically\r
+ Assert( d_pattern_is_relevant.find( rt1 )!=d_pattern_is_relevant.end() );\r
+ Assert( d_pattern_is_relevant.find( rt2 )!=d_pattern_is_relevant.end() );\r
Assert( d_pattern_is_normal.find( rt1 )!=d_pattern_is_normal.end() );\r
Assert( d_pattern_is_normal.find( rt2 )!=d_pattern_is_normal.end() );\r
Assert( d_pattern_fun_sum.find( rt1 )!=d_pattern_fun_sum.end() );\r
Assert( d_pattern_fun_sum.find( rt2 )!=d_pattern_fun_sum.end() );\r
\r
- if( d_pattern_is_normal[rt1] && !d_pattern_is_normal[rt2] ){\r
- Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl;\r
+ if( d_pattern_is_relevant[rt1] && !d_pattern_is_relevant[rt2] ){\r
+ Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl;\r
return true;\r
- }else if( d_pattern_is_normal[rt1]==d_pattern_is_normal[rt2] ){\r
- if( d_pattern_fun_sum[rt1]<d_pattern_fun_sum[rt2] ){\r
- Trace("thm-ee-debug") << "UEE : LT due to size." << std::endl;\r
- //decide which representative to use : based on size of the term\r
+ }else if( d_pattern_is_relevant[rt1]==d_pattern_is_relevant[rt2] ){\r
+ if( d_pattern_is_normal[rt1] && !d_pattern_is_normal[rt2] ){\r
+ Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl;\r
return true;\r
- }else if( d_pattern_fun_sum[rt1]==d_pattern_fun_sum[rt2] ){\r
- //same size : tie goes to term that has already been reported\r
- return isReportedCanon( rt1 ) && !isReportedCanon( rt2 );\r
+ }else if( d_pattern_is_normal[rt1]==d_pattern_is_normal[rt2] ){\r
+ if( d_pattern_fun_sum[rt1]<d_pattern_fun_sum[rt2] ){\r
+ Trace("thm-ee-debug") << "UEE : LT due to size." << std::endl;\r
+ //decide which representative to use : based on size of the term\r
+ return true;\r
+ }else if( d_pattern_fun_sum[rt1]==d_pattern_fun_sum[rt2] ){\r
+ //same size : tie goes to term that has already been reported\r
+ return isReportedCanon( rt1 ) && !isReportedCanon( rt2 );\r
+ }\r
}\r
}\r
return false;\r
setUniversalRelevant( n );\r
//add term to universal equality engine\r
d_uequalityEngine.addTerm( n );\r
- Trace("thm-ee-debug") << "Merge equivalence classes based on terms..." << std::endl;\r
- doPendingAddUniversalTerms();\r
+ // addding this term to equality engine will lead to a set of new terms (the new subterms of n)\r
+ // now, do instantiation-based merging for each of these terms\r
+ Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl;\r
+ //merge all pending equalities\r
+ while( !d_upendingAdds.empty() ){\r
+ Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl;\r
+ std::vector< Node > pending;\r
+ pending.insert( pending.end(), d_upendingAdds.begin(), d_upendingAdds.end() );\r
+ d_upendingAdds.clear();\r
+ for( unsigned i=0; i<pending.size(); i++ ){\r
+ Node t = pending[i];\r
+ TypeNode tn = t.getType();\r
+ Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;\r
+ std::vector< Node > eq_terms;\r
+ //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine\r
+ TNode gt = getTermDatabase()->evaluateTerm( t );\r
+ if( !gt.isNull() && gt!=t ){\r
+ eq_terms.push_back( gt );\r
+ }\r
+ //get all equivalent terms based on theorem database\r
+ d_thm_index.getEquivalentTerms( t, eq_terms );\r
+ if( !eq_terms.empty() ){\r
+ Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms.size() << " terms : " << std::endl;\r
+ //add equivalent terms as equalities to universal engine\r
+ for( unsigned i=0; i<eq_terms.size(); i++ ){\r
+ Trace("thm-ee-add") << " " << eq_terms[i] << std::endl;\r
+ bool assertEq = false;\r
+ if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){\r
+ assertEq = true;\r
+ }else{\r
+ Assert( eq_terms[i].getType()==tn );\r
+ registerPattern( eq_terms[i], tn );\r
+ if( isUniversalLessThan( eq_terms[i], t ) ){\r
+ setUniversalRelevant( eq_terms[i] );\r
+ assertEq = true;\r
+ }\r
+ }\r
+ if( assertEq ){\r
+ Node exp;\r
+ d_uequalityEngine.assertEquality( t.eqNode( eq_terms[i] ), true, exp );\r
+ }\r
+ }\r
+ }else{\r
+ Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;\r
+ }\r
+ }\r
+ }\r
}\r
}\r
+ \r
if( d_uequalityEngine.hasTerm( n ) ){\r
Node r = d_uequalityEngine.getRepresentative( n );\r
EqcInfo * ei = getOrMakeEqcInfo( r );\r
if( n.getKind()!=EQUAL ){\r
if( n.hasOperator() ){\r
TNode op = n.getOperator();\r
- if( std::find( d_funcs.begin(), d_funcs.end(), op )==d_funcs.end() ){\r
+ if( !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
d_pattern_var_id.clear();\r
d_pattern_var_duplicate.clear();\r
d_pattern_is_normal.clear();\r
+ d_pattern_is_relevant.clear();\r
d_pattern_fun_id.clear();\r
d_pattern_fun_sum.clear();\r
d_rel_patterns.clear();\r
//d_gen_lat_parent.clear();\r
//d_gen_depth.clear();\r
\r
- //the following generates a set of relevant terms\r
- d_use_ccand_eqc = true;\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_rel_term_count = 0;\r
- //consider all functions\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< int, std::vector< Node > > conj_lhs;\r
- std::map< int, std::vector< Node > > conj_rhs;\r
- //map from generalization depth to maximum depth\r
- //std::map< unsigned, unsigned > gdepth_to_tdepth;\r
- for( unsigned depth=1; depth<3; depth++ ){\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 terms at depth " << depth << "..." << std::endl;\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
+ //Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );\r
//if( d_tg_alloc[0].getDepth( this )==depth ){\r
- if( (int)d_tg_gdepth==d_tg_gdepth_limit ){\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
- d_rel_term_count++;\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
TypeNode tnn = nn.getType();\r
Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;\r
- conj_lhs[depth].push_back( nn );\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
}\r
}\r
Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;\r
-\r
+ Trace("sg-stats") << "--------> Total LHS of 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
-\r
- }\r
- Trace("sg-stats") << "--------> Total relevant patterns : " << d_rel_term_count << std::endl;\r
-\r
- Trace("sg-proc") << "Generate properties..." << std::endl;\r
- //set up environment\r
- d_use_ccand_eqc = false;\r
- d_var_id.clear();\r
- 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
- }\r
- //set up environment for candidate conjectures\r
- //d_cconj_at_depth.clear();\r
- //for( unsigned i=0; i<2; i++ ){\r
- // d_cconj[i].clear();\r
- //}\r
- //d_cconj_rhs_paired.clear();\r
- unsigned totalCount = 0;\r
- for( unsigned depth=0; depth<5; depth++ ){\r
//consider types from relevant terms\r
- std::random_shuffle( rt_types.begin(), rt_types.end() );\r
- for( unsigned i=0; i<rt_types.size(); i++ ){\r
- Assert( d_tg_alloc.empty() );\r
- Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types[i] << " at depth " << depth << "..." << std::endl;\r
- d_tg_id = 0;\r
- d_tg_gdepth = 0;\r
- d_tg_gdepth_limit = -1;\r
- d_tg_alloc[0].reset( this, rt_types[i] );\r
- while( d_tg_alloc[0].getNextTerm( this, depth ) && totalCount<100 ){\r
- if( d_tg_alloc[0].getDepth( this )==depth ){\r
- Node rhs = d_tg_alloc[0].getTerm( this );\r
- Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;\r
- conj_rhs[depth].push_back( rhs );\r
- //register pattern\r
- Assert( rhs.getType()==rt_types[i] );\r
- registerPattern( rhs, rt_types[i] );\r
- totalCount++;\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
+ 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
+ }\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
+ 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
+ }\r
+ }\r
}\r
+ //could have been partial, we must clear\r
+ //REMOVE_THIS?\r
+ d_tg_alloc.clear();\r
}\r
- //could have been partial, we must clear\r
- d_tg_alloc.clear();\r
- }\r
- Trace("sg-proc") << "Process candidate conjectures up to RHS term depth " << depth << "..." << std::endl;\r
- for( int rhs_d=depth; rhs_d>=0; rhs_d-- ){\r
- int lhs_d = (depth-rhs_d)+1;\r
- for( unsigned i=0; i<conj_rhs[rhs_d].size(); i++ ){\r
- for( unsigned j=0; j<conj_lhs[lhs_d].size(); j++ ){\r
- processCandidateConjecture( conj_lhs[lhs_d][j], conj_rhs[rhs_d][i], lhs_d, rhs_d );\r
+ //consider against all LHS up to depth\r
+ if( rdepth==depth ){\r
+ for( unsigned lhs_depth = 1; lhs_depth<=depth; lhs_depth++ ){\r
+ if( !optStatsOnly() && d_waiting_conjectures_lhs.size()>=optFullCheckConjectures() ){\r
+ break;\r
+ }\r
+ Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth << ", " << rdepth << ")..." << std::endl;\r
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = conj_rhs.begin(); it != conj_rhs.end(); ++it ){\r
+ for( unsigned j=0; j<it->second.size(); j++ ){\r
+ for( unsigned k=0; k<conj_lhs[it->first][lhs_depth].size(); k++ ){\r
+ processCandidateConjecture( conj_lhs[it->first][lhs_depth][k], it->second[j], lhs_depth, rdepth );\r
+ }\r
+ }\r
+ }\r
}\r
}\r
}\r
- Trace("sg-proc") << "...done process candidate conjectures at RHS term depth " << depth << std::endl;\r
+ if( optStatsOnly() ){\r
+ Trace("conjecture-count") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures for depth " << depth << "." << std::endl;\r
+ d_waiting_conjectures_lhs.clear();\r
+ d_waiting_conjectures_rhs.clear();\r
+ }else if( d_waiting_conjectures_lhs.size()>=optFullCheckConjectures() ){\r
+ break;\r
+ }\r
}\r
- Trace("sg-proc") << "...done generate properties" << std::endl;\r
-\r
- if( !d_waiting_conjectures.empty() ){\r
- Trace("sg-proc") << "Generated " << d_waiting_conjectures.size() << " conjectures." << std::endl;\r
- d_conjectures.insert( d_conjectures.end(), d_waiting_conjectures.begin(), d_waiting_conjectures.end() );\r
- for( unsigned i=0; i<d_waiting_conjectures.size(); i++ ){\r
- Assert( d_waiting_conjectures[i].getKind()==FORALL );\r
- Node lem = NodeManager::currentNM()->mkNode( OR, d_waiting_conjectures[i].negate(), d_waiting_conjectures[i] );\r
- d_quantEngine->addLemma( lem, false );\r
- d_quantEngine->addRequirePhase( d_waiting_conjectures[i], false );\r
+\r
+ if( !d_waiting_conjectures_lhs.empty() ){\r
+ Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures." << std::endl;\r
+ //TODO: prune conjectures in a smart way\r
+ for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){\r
+ if( i>optFullCheckConjectures() ){\r
+ break;\r
+ }else{\r
+ //we have determined a relevant subgoal\r
+ Node lhs = d_waiting_conjectures_lhs[i];\r
+ Node rhs = d_waiting_conjectures_rhs[i];\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
+ Trace("sg-lemma") << "Constructed : " << rsg << std::endl;\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
+ }\r
}\r
+ d_waiting_conjectures_lhs.clear();\r
+ d_waiting_conjectures_rhs.clear();\r
d_waiting_conjectures.clear();\r
}\r
\r
- Trace("thm-ee") << "Universal equality engine is : " << std::endl;\r
- eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine );\r
- while( !ueqcs_i.isFinished() ){\r
- 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") << " : { ";\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( firstTime ){\r
- Trace("thm-ee") << std::endl;\r
- firstTime = false;\r
+ if( Trace.isOn("thm-ee") ){\r
+ Trace("thm-ee") << "Universal equality engine is : " << std::endl;\r
+ eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine );\r
+ while( !ueqcs_i.isFinished() ){\r
+ 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") << " : { ";\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( firstTime ){\r
+ Trace("thm-ee") << std::endl;\r
+ firstTime = false;\r
+ }\r
+ Trace("thm-ee") << " " << n << std::endl;\r
}\r
- Trace("thm-ee") << " " << n << std::endl;\r
+ ++ueqc_i;\r
}\r
- ++ueqc_i;\r
+ if( !firstTime ){ Trace("thm-ee") << " "; }\r
+ Trace("thm-ee") << "}" << std::endl;\r
+ ++ueqcs_i;\r
}\r
- if( !firstTime ){ Trace("thm-ee") << " "; }\r
- Trace("thm-ee") << "}" << std::endl;\r
- ++ueqcs_i;\r
+ Trace("thm-ee") << std::endl;\r
}\r
- Trace("thm-ee") << std::endl;\r
}\r
}\r
}\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
- Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );\r
-\r
- if( d_tg_gdepth_limit>=0 && d_tg_gdepth>(unsigned)d_tg_gdepth_limit ){\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
}\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
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_use_ccand_eqc ){\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
}\r
Trace("sg-gen-tg-debug") << std::endl;\r
}\r
- if( d_ccand_eqc[0][i].empty() ){\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( d_ccand_eqc[1][i].empty() && optFilterConfirmation() ){\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
return true;\r
}\r
\r
-bool ConjectureGenerator::considerTermCanon( unsigned tg_id ){\r
+bool ConjectureGenerator::considerCurrentTermCanon( unsigned tg_id ){\r
Assert( tg_id<d_tg_alloc.size() );\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 filtering based on matching candidate eqc, 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_use_ccand_eqc || 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
+ 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
- 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
return true;\r
}\r
\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
+ d_pattern_is_relevant[opat] = false;\r
+ }\r
unsigned sum = 1;\r
for( unsigned i=0; i<pat.getNumChildren(); i++ ){\r
sum += collectFunctions( opat, pat[i], funcs, mnvn, mxvn );\r
mxvn[tn] = vn;\r
}\r
}\r
+ }else{\r
+ d_pattern_is_relevant[opat] = false;\r
}\r
return 1;\r
}\r
if( d_pattern_is_normal.find( pat )==d_pattern_is_normal.end() ){\r
d_pattern_is_normal[pat] = true;\r
}\r
+ if( d_pattern_is_relevant.find( pat )==d_pattern_is_relevant.end() ){\r
+ d_pattern_is_relevant[pat] = true;\r
+ }\r
}\r
}\r
\r
}\r
}\r
\r
-void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {\r
- if( d_waiting_conjectures.size()>=optFullCheckConjectures() ){\r
- return;\r
+int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ) {\r
+ if( n.getKind()==BOUND_VARIABLE ){\r
+ if( std::find( fv.begin(), fv.end(), n )==fv.end() ){\r
+ fv.push_back( n );\r
+ return 0;\r
+ }else{\r
+ return 1;\r
+ }\r
+ }else{\r
+ int depth = 1;\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ depth += calculateGeneralizationDepth( n[i], fv );\r
+ }\r
+ return depth;\r
}\r
+}\r
+\r
+void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {\r
if( considerCandidateConjecture( lhs, rhs ) ){\r
Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;\r
Trace("sg-conjecture-debug") << " LHS, RHS generalization depth : " << lhs_depth << ", " << rhs_depth << std::endl;\r
Trace("sg-conjecture-debug") << std::endl;\r
Trace("sg-conjecture-debug") << " unknown = " << d_subs_unkCount << std::endl;\r
}\r
- Assert( getUniversalRepresentative( rhs )==rhs );\r
- Assert( getUniversalRepresentative( lhs )==lhs );\r
- //make universal quantified formula\r
- Assert( std::find( d_eq_conjectures[lhs].begin(), d_eq_conjectures[lhs].end(), rhs )==d_eq_conjectures[lhs].end() );\r
- d_eq_conjectures[lhs].push_back( rhs );\r
- d_eq_conjectures[rhs].push_back( lhs );\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 bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );\r
- Node conj = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );\r
- conj = Rewriter::rewrite( conj );\r
- d_waiting_conjectures.push_back( conj );\r
+ //Assert( getUniversalRepresentative( rhs )==rhs );\r
+ //Assert( getUniversalRepresentative( lhs )==lhs );\r
+ d_waiting_conjectures_lhs.push_back( lhs );\r
+ d_waiting_conjectures_rhs.push_back( rhs );\r
+ d_waiting_conjectures[lhs].push_back( rhs );\r
+ d_waiting_conjectures[rhs].push_back( lhs );\r
}\r
}\r
\r
bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {\r
+ if( lhs.getType()!=rhs.getType() ){\r
+ std::cout << "BAD TYPE" << std::endl;\r
+ }\r
Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;\r
if( lhs==rhs ){\r
Trace("sg-cconj-debug") << " -> trivial." << std::endl;\r
return false;\r
}\r
}\r
+\r
//currently active conjecture?\r
std::map< Node, std::vector< Node > >::iterator iteq = d_eq_conjectures.find( lhs );\r
if( iteq!=d_eq_conjectures.end() ){\r
if( std::find( iteq->second.begin(), iteq->second.end(), rhs )!=iteq->second.end() ){\r
+ Trace("sg-cconj-debug") << " -> this conjecture is already active." << std::endl;\r
+ return false;\r
+ }\r
+ }\r
+ //current a waiting conjecture?\r
+ std::map< Node, std::vector< Node > >::iterator itw = d_waiting_conjectures.find( lhs );\r
+ if( itw!=d_waiting_conjectures.end() ){\r
+ if( std::find( itw->second.begin(), itw->second.end(), rhs )!=itw->second.end() ){\r
Trace("sg-cconj-debug") << " -> already are considering this conjecture." << std::endl;\r
return false;\r
}\r
}\r
+\r
+\r
Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;\r
//find witness for counterexample, if possible\r
- if( optFilterConfirmation() || optFilterFalsification() ){\r
+ if( options::conjectureFilterModel() && ( optFilterConfirmation() || optFilterFalsification() ) ){\r
Assert( d_rel_pattern_var_sum.find( lhs )!=d_rel_pattern_var_sum.end() );\r
Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl;\r
std::map< TNode, TNode > subs;\r
return false;\r
}\r
}\r
- if( optFilterConfirmationDomain() ){\r
+ if( optFilterConfirmationDomainThreshold()>0 ){\r
std::vector< TNode > vars;\r
std::vector< TNode > subs;\r
for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){\r
Assert( d_pattern_fun_id[lhs].find( it->first )!=d_pattern_fun_id[lhs].end() );\r
- unsigned req = d_pattern_fun_id[lhs][it->first];\r
+ unsigned req = optFilterConfirmationDomainThreshold() + (d_pattern_fun_id[lhs][it->first]-1);\r
std::map< TNode, unsigned >::iterator itrf = d_pattern_fun_id[rhs].find( it->first );\r
if( itrf!=d_pattern_fun_id[rhs].end() ){\r
req = itrf->second>req ? itrf->second : req;\r
subs.push_back( it->second[0] );\r
}\r
}\r
- if( optFilterConfirmationNonCanonical() && !vars.empty() ){\r
- Node slhs = lhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
- Node srhs = rhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
- TNode slhsr = getUniversalRepresentative( slhs, true );\r
- TNode srhsr = getUniversalRepresentative( srhs, true );\r
- if( areUniversalEqual( slhsr, srhsr ) ){\r
- Trace("sg-cconj") << " -> all ground witnesses can be proven by other theorems." << std::endl;\r
- return false;\r
- }else{\r
- Trace("sg-cconj-debug") << "Checked if " << slhsr << " and " << srhsr << " were equal." << std::endl;\r
- }\r
- }\r
}\r
- }\r
-\r
- Trace("sg-cconj") << " -> SUCCESS." << std::endl;\r
- if( optFilterConfirmation() || optFilterFalsification() ){\r
+ Trace("sg-cconj") << " -> SUCCESS." << std::endl;\r
Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;\r
for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){\r
Trace("sg-cconj") << " #witnesses for " << it->first << " : " << it->second.size() << std::endl;\r
}\r
}\r
\r
- /*\r
- if( getUniversalRepresentative( lhs )!=lhs ){\r
- std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;\r
- exit(0);\r
- }\r
- if( getUniversalRepresentative( rhs )!=rhs ){\r
- std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;\r
- exit(0);\r
- }\r
- */\r
-\r
//check if still canonical representation (should be, but for efficiency this is not guarenteed)\r
- if( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ){\r
+ if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){\r
Trace("sg-cconj") << " -> after processing, not canonical." << std::endl;\r
+ return false;\r
}\r
\r
return true;\r
}else{\r
d_subs_unkCount++;\r
if( optFilterUnknown() ){\r
+ Trace("sg-cconj-debug") << "...ground substitution giving terms that are neither equal nor disequal." << std::endl;\r
return false;\r
}\r
}\r
}\r
}\r
}\r
- /*\r
- if( getEqualityEngine()->areDisequal( glhs, grhs, false ) ){\r
- Trace("sg-cconj-debug") << "..." << glhs << " and " << grhs << " are disequal." << std::endl;\r
- return false;\r
- }else{\r
- Trace("sg-cconj-debug") << "..." << glhs << " and " << grhs << " are not disequal." << std::endl;\r
- }\r
- */\r
}else{\r
Trace("sg-cconj-witness") << " Witnessed " << glhs << " == " << grhs << ", substutition is : " << std::endl;\r
for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){\r
//check allocating new variable\r
d_status++;\r
d_status_num = -1;\r
- s->d_tg_gdepth++;\r
+ if( s->d_gen_relevant_terms ){\r
+ s->d_tg_gdepth++;\r
+ }\r
return getNextTerm( s, depth );\r
}\r
}else{\r
Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num << std::endl;\r
return s->considerCurrentTerm() ? true : getNextTerm( s, depth );\r
}else{\r
- s->d_tg_gdepth--;\r
+ if( s->d_gen_relevant_terms ){\r
+ s->d_tg_gdepth--;\r
+ }\r
d_status++;\r
return getNextTerm( s, depth );\r
}\r
return getNextTerm( s, depth );\r
}else if( d_status_child_num==(int)s->d_func_args[f].size() ){\r
d_status_child_num--;\r
- return s->considerTermCanon( d_id ) ? true : getNextTerm( s, depth );\r
+ return s->considerCurrentTermCanon( d_id ) ? true : getNextTerm( s, depth );\r
//return true;\r
}else{\r
Assert( d_status_child_num<(int)s->d_func_args[f].size() );\r
}\r
}\r
\r
-unsigned TermGenerator::getGeneralizationDepth( ConjectureGenerator * s ) {\r
+unsigned TermGenerator::calculateGeneralizationDepth( ConjectureGenerator * 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
- sum += s->d_tg_alloc[d_children[i]].getGeneralizationDepth( s );\r
+ sum += s->d_tg_alloc[d_children[i]].calculateGeneralizationDepth( s, fvs );\r
}\r
return sum;\r
- }else if( d_status==2 ){\r
- return 1;\r
}else{\r
- Assert( d_status==1 );\r
+ Assert( d_status==2 || d_status==1 );\r
+ std::map< TypeNode, std::vector< int > >::iterator it = fvs.find( d_typ );\r
+ if( it!=fvs.end() ){\r
+ if( std::find( it->second.begin(), it->second.end(), d_status_num )!=it->second.end() ){\r
+ return 1;\r
+ }\r
+ }\r
+ fvs[d_typ].push_back( d_status_num );\r
return 0;\r
}\r
}\r
\r
+unsigned TermGenerator::getGeneralizationDepth( ConjectureGenerator * s ) {\r
+ //if( s->d_gen_relevant_terms ){\r
+ // return s->d_tg_gdepth;\r
+ //}else{\r
+ std::map< TypeNode, std::vector< int > > fvs;\r
+ return calculateGeneralizationDepth( s, fvs );\r
+ //}\r
+}\r
+\r
Node TermGenerator::getTerm( ConjectureGenerator * s ) {\r
if( d_status==1 || d_status==2 ){\r
Assert( !d_typ.isNull() );\r
d_children[curr.getOperator()].addTheorem( lhs_v, lhs_arg, rhs );\r
}else{\r
Assert( curr.getKind()==kind::BOUND_VARIABLE );\r
- Assert( d_var.isNull() || d_var==curr );\r
- d_var = curr;\r
+ TypeNode tn = curr.getType();\r
+ Assert( d_var[tn].isNull() || d_var[tn]==curr );\r
+ d_var[tn] = curr;\r
d_children[curr].addTheorem( lhs_v, lhs_arg, rhs );\r
}\r
}\r
}\r
Trace("thm-db-debug") << "...done check based on operator" << std::endl;\r
}\r
- if( !d_var.isNull() ){\r
- Trace("thm-db-debug") << "Check for substitution with " << d_var << "..." << std::endl;\r
- if( curr.getType()==d_var.getType() ){\r
- //add to substitution if possible\r
- bool success = false;\r
- std::map< TNode, TNode >::iterator it = smap.find( d_var );\r
- if( it==smap.end() ){\r
- smap[d_var] = curr;\r
- vars.push_back( d_var );\r
- subs.push_back( curr );\r
- success = true;\r
- }else if( it->second==curr ){\r
- success = true;\r
- }else{\r
- //also check modulo equality (in universal equality engine)\r
- }\r
- Trace("thm-db-debug") << "...check for substitution with " << d_var << ", success = " << success << "." << std::endl;\r
- if( success ){\r
- d_children[d_var].getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );\r
- }\r
+ TypeNode tn = curr.getType();\r
+ std::map< TypeNode, TNode >::iterator itt = d_var.find( tn );\r
+ if( itt!=d_var.end() ){\r
+ Trace("thm-db-debug") << "Check for substitution with " << itt->second << "..." << std::endl;\r
+ Assert( curr.getType()==itt->second.getType() );\r
+ //add to substitution if possible\r
+ bool success = false;\r
+ std::map< TNode, TNode >::iterator it = smap.find( itt->second );\r
+ if( it==smap.end() ){\r
+ smap[itt->second] = curr;\r
+ vars.push_back( itt->second );\r
+ subs.push_back( curr );\r
+ success = true;\r
+ }else if( it->second==curr ){\r
+ success = true;\r
+ }else{\r
+ //also check modulo equality (in universal equality engine)\r
+ }\r
+ Trace("thm-db-debug") << "...check for substitution with " << itt->second << ", success = " << success << "." << std::endl;\r
+ if( success ){\r
+ d_children[itt->second].getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );\r
}\r
}\r
}\r
bool ConjectureGenerator::optFilterFalsification() { return true; }\r
bool ConjectureGenerator::optFilterUnknown() { return true; } //may change\r
bool ConjectureGenerator::optFilterConfirmation() { return true; }\r
-bool ConjectureGenerator::optFilterConfirmationDomain() { return true; }\r
-bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }//false; }\r
-bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }//true; }\r
+unsigned ConjectureGenerator::optFilterConfirmationDomainThreshold() { return 1; }\r
+bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }\r
+bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }\r
unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }\r
unsigned ConjectureGenerator::optFullCheckConjectures() { return options::conjectureGenPerRound(); }\r
\r
+bool ConjectureGenerator::optStatsOnly() { return false; }\r
+\r
}\r
\r
\r
projects / cvc5.git / commitdiff