using namespace CVC4::theory::quantifiers;\r
using namespace std;\r
\r
-\r
namespace CVC4 {\r
\r
+struct sortConjectureScore {\r
+ std::vector< int > d_scores;\r
+ bool operator() (unsigned i, unsigned j) { return d_scores[i]>d_scores[j]; }\r
+};\r
+ \r
+ \r
void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){\r
if( index==n.getNumChildren() ){\r
Assert( n.hasOperator() );\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
+ double clSet = 0;\r
+ if( Trace.isOn("sg-engine") ){\r
+ clSet = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("sg-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;\r
+ }\r
eq::EqualityEngine * ee = getEqualityEngine();\r
\r
Trace("sg-proc") << "Get eq classes..." << std::endl;\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
+ unsigned addedLemmas = 0;\r
for( unsigned depth=1; depth<=3; depth++ ){\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
while( d_tge.getNextTerm() ){\r
//construct term\r
Node nn = d_tge.getTerm();\r
- if( !options::conjectureFilterCanonical() || getUniversalRepresentative( nn )==nn ){\r
+ if( !options::conjectureFilterCanonical() || considerTermCanon( nn, true ) ){\r
rel_term_count++;\r
Trace("sg-rel-term") << "*** Relevant term : ";\r
d_tge.debugPrint( "sg-rel-term", "sg-rel-term-debug2" );\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
+ unsigned mode = 2;\r
d_tge.resetMatching( r, mode );\r
while( d_tge.getNextMatch( r, subs, rev_subs ) ){\r
//we will be building substitutions\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
+ if( considerTermCanon( rhs, false ) ){\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
- }else{\r
- conj_rhs[rt_types[i]].push_back( rhs );\r
}\r
}\r
}\r
+ flushWaitingConjectures( addedLemmas, depth, rdepth );\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
+ if( (int)addedLemmas<options::conjectureGenPerRound() ){\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
+ flushWaitingConjectures( addedLemmas, lhs_depth, depth );\r
}\r
}\r
}\r
}\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
+ if( (int)addedLemmas>=options::conjectureGenPerRound() ){\r
break;\r
}\r
}\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
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
}\r
Trace("thm-ee") << std::endl;\r
}\r
+ if( Trace.isOn("sg-engine") ){\r
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("sg-engine") << "Finished conjecture generator, time = " << (clSet2-clSet) << std::endl;\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {\r
+ if( !d_waiting_conjectures_lhs.empty() ){\r
+ Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;\r
+ if( !optStatsOnly() && (int)addedLemmas<options::conjectureGenPerRound() ){\r
+ std::vector< unsigned > indices;\r
+ for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){\r
+ indices.push_back( i );\r
+ }\r
+ bool doSort = false;\r
+ if( doSort ){\r
+ //sort them based on score\r
+ sortConjectureScore scs;\r
+ scs.d_scores.insert( scs.d_scores.begin(), d_waiting_conjectures_score.begin(), d_waiting_conjectures_score.end() );\r
+ std::sort( indices.begin(), indices.end(), scs );\r
+ }\r
+ if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){\r
+ //do splitting on demand (TODO)\r
+ \r
+ }else{\r
+ for( unsigned i=0; i<indices.size(); i++ ){\r
+ //if( d_waiting_conjectures_score[indices[i]]<optFilterScoreThreshold() ){\r
+ if( d_waiting_conjectures_score[indices[i]]>=optFilterScoreThreshold() ){\r
+ //we have determined a relevant subgoal\r
+ Node lhs = d_waiting_conjectures_lhs[indices[i]];\r
+ Node rhs = d_waiting_conjectures_rhs[indices[i]];\r
+ Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;\r
+ Trace("sg-engine-debug") << " score : " << d_waiting_conjectures_score[indices[i]] << std::endl;\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
+ 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
+ addedLemmas++;\r
+ if( (int)addedLemmas>=options::conjectureGenPerRound() ){\r
+ break;\r
+ }\r
+ }else{\r
+ if( doSort ){\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ Trace("sg-proc") << "...have now added " << addedLemmas << " conjecture lemmas." << std::endl;\r
}\r
+ d_waiting_conjectures_lhs.clear();\r
+ d_waiting_conjectures_rhs.clear();\r
+ d_waiting_conjectures_score.clear();\r
+ d_waiting_conjectures.clear();\r
}\r
+ return addedLemmas;\r
}\r
\r
void ConjectureGenerator::registerQuantifier( Node q ) {\r
\r
}\r
\r
-bool ConjectureGenerator::considerCurrentTermCanon( Node ln, bool genRelevant ){\r
+bool ConjectureGenerator::considerTermCanon( 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
}\r
\r
void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {\r
- if( considerCandidateConjecture( lhs, rhs ) ){\r
+ int score = considerCandidateConjecture( lhs, rhs ); \r
+ if( score>0 ){\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
- if( optFilterConfirmation() || optFilterFalsification() ){\r
- Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;\r
- Trace("sg-conjecture-debug") << " #witnesses for ";\r
- bool firstTime = true;\r
- for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){\r
- if( !firstTime ){\r
- Trace("sg-conjecture-debug") << ", ";\r
- }\r
- Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];\r
- //if( it->second.size()==1 ){\r
- // Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";\r
- //}\r
- Trace("sg-conjecture-debug2") << " (";\r
- for( unsigned j=0; j<it->second.size(); j++ ){\r
- if( j>0 ){ Trace("sg-conjecture-debug2") << " "; }\r
- Trace("sg-conjecture-debug2") << it->second[j];\r
- }\r
- Trace("sg-conjecture-debug2") << ")";\r
- firstTime = false;\r
+ Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;\r
+ Trace("sg-conjecture-debug") << " #witnesses for ";\r
+ bool firstTime = true;\r
+ for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){\r
+ if( !firstTime ){\r
+ Trace("sg-conjecture-debug") << ", ";\r
}\r
- Trace("sg-conjecture-debug") << std::endl;\r
- Trace("sg-conjecture-debug") << " unknown = " << d_subs_unkCount << std::endl;\r
+ Trace("sg-conjecture-debug") << it->first << " : " << it->second.size();\r
+ //if( it->second.size()==1 ){\r
+ // Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";\r
+ //}\r
+ Trace("sg-conjecture-debug2") << " (";\r
+ for( unsigned j=0; j<it->second.size(); j++ ){\r
+ if( j>0 ){ Trace("sg-conjecture-debug2") << " "; }\r
+ Trace("sg-conjecture-debug2") << d_ground_eqc_map[it->second[j]];\r
+ }\r
+ Trace("sg-conjecture-debug2") << ")";\r
+ firstTime = false;\r
}\r
+ Trace("sg-conjecture-debug") << std::endl;\r
+ Trace("sg-conjecture-debug") << " unknown = " << d_subs_unkCount << std::endl;\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_score.push_back( score );\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
+int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {\r
+ Assert( lhs.getType()==rhs.getType() );\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
+ return -1;\r
}else{\r
if( lhs.getKind()==APPLY_CONSTRUCTOR && rhs.getKind()==APPLY_CONSTRUCTOR ){\r
Trace("sg-cconj-debug") << " -> irrelevant by syntactic analysis." << std::endl;\r
- return false;\r
+ return -1;\r
}\r
//variables of LHS must subsume variables of RHS\r
for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[rhs].begin(); it != d_pattern_var_id[rhs].end(); ++it ){\r
if( itl!=d_pattern_var_id[lhs].end() ){\r
if( itl->second<it->second ){\r
Trace("sg-cconj-debug") << " -> variables of sort " << it->first << " are not subsumed." << std::endl;\r
- return false;\r
+ return -1;\r
}else{\r
Trace("sg-cconj-debug2") << " variables of sort " << it->first << " are : " << itl->second << " vs " << it->second << std::endl;\r
}\r
}else{\r
Trace("sg-cconj-debug") << " -> has no variables of sort " << it->first << "." << std::endl;\r
- return false;\r
+ return -1;\r
}\r
}\r
\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
+ return -1;\r
}\r
}\r
//current a waiting conjecture?\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
+ return -1;\r
}\r
}\r
-\r
+ //check if canonical representation (should be, but for efficiency this is not guarenteed)\r
+ //if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){\r
+ // Trace("sg-cconj") << " -> after processing, not canonical." << std::endl;\r
+ // return -1;\r
+ //}\r
+ \r
+ int score;\r
+ bool scoreSet = false;\r
\r
Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;\r
//find witness for counterexample, if possible\r
- if( options::conjectureFilterModel() && ( optFilterConfirmation() || optFilterFalsification() ) ){\r
+ if( options::conjectureFilterModel() ){\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
d_subs_unkCount = 0;\r
if( !d_rel_pattern_subs_index[lhs].notifySubstitutions( this, subs, rhs, d_rel_pattern_var_sum[lhs] ) ){\r
Trace("sg-cconj") << " -> found witness that falsifies the conjecture." << std::endl;\r
- return false;\r
+ return -1;\r
}\r
- if( optFilterConfirmation() ){\r
- if( d_subs_confirmCount==0 ){\r
- Trace("sg-cconj") << " -> not confirmed by a ground substitutions." << std::endl;\r
- return false;\r
+ //score is the minimum number of distinct substitutions for a variable\r
+ for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){\r
+ int num = (int)it->second.size();\r
+ if( !scoreSet || num<score ){\r
+ score = num;\r
+ scoreSet = true;\r
}\r
}\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 = 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
- }\r
- if( it->second.size()<req ){\r
- Trace("sg-cconj") << " -> did not find at least " << d_pattern_fun_id[lhs][it->first] << " different values in ground substitutions for variable " << it->first << "." << std::endl;\r
- return false;\r
- }\r
- if( it->second.size()==1 ){\r
- vars.push_back( it->first );\r
- subs.push_back( it->second[0] );\r
- }\r
- }\r
+ if( !scoreSet ){\r
+ score = 0;\r
}\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
+ }else{\r
+ score = 0;\r
}\r
\r
- //check if still canonical representation (should be, but for efficiency this is not guarenteed)\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
+ Trace("sg-cconj") << " -> SUCCESS." << std::endl;\r
+ Trace("sg-cconj") << " score : " << score << std::endl;\r
+ \r
+ return score;\r
}\r
}\r
\r
Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;\r
if( !grhs.isNull() ){\r
if( glhs!=grhs ){\r
- if( optFilterFalsification() ){\r
- Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs << std::endl;\r
- //check based on ground terms\r
- std::map< TNode, Node >::iterator itl = d_ground_eqc_map.find( glhs );\r
- if( itl!=d_ground_eqc_map.end() ){\r
- std::map< TNode, Node >::iterator itr = d_ground_eqc_map.find( grhs );\r
- if( itr!=d_ground_eqc_map.end() ){\r
- Trace("sg-cconj-debug") << "We have ground terms " << itl->second << " and " << itr->second << "." << std::endl;\r
- if( itl->second.isConst() && itr->second.isConst() ){\r
- Trace("sg-cconj-debug") << "...disequal constants." << std::endl;\r
- Trace("sg-cconj-witness") << " Witness of falsification : " << itl->second << " != " << itr->second << ", substutition is : " << std::endl;\r
- for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){\r
- Trace("sg-cconj-witness") << " " << it->first << " -> " << it->second << std::endl;\r
- }\r
- return false;\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
+ Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs << std::endl;\r
+ //check based on ground terms\r
+ std::map< TNode, Node >::iterator itl = d_ground_eqc_map.find( glhs );\r
+ if( itl!=d_ground_eqc_map.end() ){\r
+ std::map< TNode, Node >::iterator itr = d_ground_eqc_map.find( grhs );\r
+ if( itr!=d_ground_eqc_map.end() ){\r
+ Trace("sg-cconj-debug") << "We have ground terms " << itl->second << " and " << itr->second << "." << std::endl;\r
+ if( itl->second.isConst() && itr->second.isConst() ){\r
+ Trace("sg-cconj-debug") << "...disequal constants." << std::endl;\r
+ Trace("sg-cconj-witness") << " Witness of falsification : " << itl->second << " != " << itr->second << ", substutition is : " << std::endl;\r
+ for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){\r
+ Trace("sg-cconj-witness") << " " << it->first << " -> " << it->second << std::endl;\r
}\r
+ return false;\r
}\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
- Trace("sg-cconj-witness") << " " << it->first << " -> " << it->second << std::endl;\r
- if( std::find( d_subs_confirmWitnessDomain[it->first].begin(), d_subs_confirmWitnessDomain[it->first].end(), it->second )==d_subs_confirmWitnessDomain[it->first].end() ){\r
- d_subs_confirmWitnessDomain[it->first].push_back( it->second );\r
- }\r
+ }\r
+ Trace("sg-cconj-debug") << "RHS is identical." << std::endl;\r
+ bool isGroundSubs = true;\r
+ for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){\r
+ std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( it->second );\r
+ if( git==d_ground_eqc_map.end() ){\r
+ isGroundSubs = false;\r
+ break;\r
}\r
- d_subs_confirmCount++;\r
- if( std::find( d_subs_confirmWitnessRange.begin(), d_subs_confirmWitnessRange.end(), glhs )==d_subs_confirmWitnessRange.end() ){\r
- d_subs_confirmWitnessRange.push_back( glhs );\r
+ }\r
+ if( isGroundSubs ){\r
+ if( glhs==grhs ){\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
+ Trace("sg-cconj-witness") << " " << it->first << " -> " << it->second << std::endl;\r
+ if( std::find( d_subs_confirmWitnessDomain[it->first].begin(), d_subs_confirmWitnessDomain[it->first].end(), it->second )==d_subs_confirmWitnessDomain[it->first].end() ){\r
+ d_subs_confirmWitnessDomain[it->first].push_back( it->second );\r
+ }\r
+ }\r
+ d_subs_confirmCount++;\r
+ if( std::find( d_subs_confirmWitnessRange.begin(), d_subs_confirmWitnessRange.end(), glhs )==d_subs_confirmWitnessRange.end() ){\r
+ d_subs_confirmWitnessRange.push_back( glhs );\r
+ }\r
+ }else{\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
- Trace("sg-cconj-debug") << "RHS is identical." << std::endl;\r
}\r
}else{\r
Trace("sg-cconj-debug") << "(could not ground eqc for RHS)." << std::endl;\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
+ mode = 1 << 1;\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
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
+ if( options::conjectureFilterModel() && d_ccand_eqc[1][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 ground EQC matches it." << 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
+ return d_cg->considerTermCanon( ln, d_gen_relevant_terms );\r
}\r
return true;\r
}\r
}\r
\r
bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }\r
-bool ConjectureGenerator::optFilterFalsification() { return true; }\r
bool ConjectureGenerator::optFilterUnknown() { return true; } //may change\r
-bool ConjectureGenerator::optFilterConfirmation() { return true; }\r
-unsigned ConjectureGenerator::optFilterConfirmationDomainThreshold() { return 1; }\r
-bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }\r
-bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }\r
+int ConjectureGenerator::optFilterScoreThreshold() { return 1; }\r
unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }\r
-unsigned ConjectureGenerator::optFullCheckConjectures() { return options::conjectureGenPerRound(); }\r
\r
bool ConjectureGenerator::optStatsOnly() { return false; }\r
\r
projects / cvc5.git / commitdiff