while( d_tge.getNextTerm() ){
//construct term
Node nn = d_tge.getTerm();
- if (!options().quantifiers.conjectureFilterCanonical
- || considerTermCanon(nn, true))
+ if (considerTermCanon(nn, true))
{
rel_term_count++;
Trace("sg-rel-term") << "*** Relevant term : ";
//we have determined a relevant subgoal
Node lhs = d_waiting_conjectures_lhs[i];
Node rhs = d_waiting_conjectures_rhs[i];
- if (options().quantifiers.conjectureFilterCanonical
- && (getUniversalRepresentative(lhs) != lhs
- || getUniversalRepresentative(rhs) != rhs))
+ if (getUniversalRepresentative(lhs) != lhs
+ || getUniversalRepresentative(rhs) != rhs)
{
//skip
}
if( lhs==rhs ){
Trace("sg-cconj-debug") << " -> trivial." << std::endl;
return -1;
- }else{
- if( lhs.getKind()==APPLY_CONSTRUCTOR && rhs.getKind()==APPLY_CONSTRUCTOR ){
- Trace("sg-cconj-debug") << " -> irrelevant by syntactic analysis." << std::endl;
+ }
+ if (lhs.getKind() == APPLY_CONSTRUCTOR && rhs.getKind() == APPLY_CONSTRUCTOR)
+ {
+ Trace("sg-cconj-debug")
+ << " -> irrelevant by syntactic analysis." << std::endl;
+ return -1;
+ }
+ // variables of LHS must subsume variables of RHS
+ for (std::pair<const TypeNode, unsigned>& p : d_pattern_var_id[rhs])
+ {
+ std::map<TypeNode, unsigned>::iterator itl =
+ d_pattern_var_id[lhs].find(p.first);
+ if (itl == d_pattern_var_id[lhs].end())
+ {
+ Trace("sg-cconj-debug")
+ << " -> has no variables of sort " << p.first << "." << std::endl;
return -1;
}
- //variables of LHS must subsume variables of RHS
- for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[rhs].begin(); it != d_pattern_var_id[rhs].end(); ++it ){
- std::map< TypeNode, unsigned >::iterator itl = d_pattern_var_id[lhs].find( it->first );
- if( itl!=d_pattern_var_id[lhs].end() ){
- if( itl->second<it->second ){
- Trace("sg-cconj-debug") << " -> variables of sort " << it->first << " are not subsumed." << std::endl;
- return -1;
- }else{
- Trace("sg-cconj-debug2") << " variables of sort " << it->first << " are : " << itl->second << " vs " << it->second << std::endl;
- }
- }else{
- Trace("sg-cconj-debug") << " -> has no variables of sort " << it->first << "." << std::endl;
- return -1;
- }
+ if (itl->second < p.second)
+ {
+ Trace("sg-cconj-debug") << " -> variables of sort " << p.first
+ << " are not subsumed." << std::endl;
+ return -1;
}
+ Trace("sg-cconj-debug2")
+ << " variables of sort " << p.first << " are : " << itl->second
+ << " vs " << p.second << std::endl;
+ }
- //currently active conjecture?
- std::map< Node, std::vector< Node > >::iterator iteq = d_eq_conjectures.find( lhs );
- if( iteq!=d_eq_conjectures.end() ){
- if( std::find( iteq->second.begin(), iteq->second.end(), rhs )!=iteq->second.end() ){
- Trace("sg-cconj-debug") << " -> this conjecture is already active." << std::endl;
- return -1;
- }
+ // currently active conjecture?
+ std::map<Node, std::vector<Node> >::iterator iteq =
+ d_eq_conjectures.find(lhs);
+ if (iteq != d_eq_conjectures.end())
+ {
+ if (std::find(iteq->second.begin(), iteq->second.end(), rhs)
+ != iteq->second.end())
+ {
+ Trace("sg-cconj-debug")
+ << " -> this conjecture is already active." << std::endl;
+ return -1;
}
- //current a waiting conjecture?
- std::map< Node, std::vector< Node > >::iterator itw = d_waiting_conjectures.find( lhs );
- if( itw!=d_waiting_conjectures.end() ){
- if( std::find( itw->second.begin(), itw->second.end(), rhs )!=itw->second.end() ){
- Trace("sg-cconj-debug") << " -> already are considering this conjecture." << std::endl;
- return -1;
- }
+ }
+ // current a waiting conjecture?
+ std::map<Node, std::vector<Node> >::iterator itw =
+ d_waiting_conjectures.find(lhs);
+ if (itw != d_waiting_conjectures.end())
+ {
+ if (std::find(itw->second.begin(), itw->second.end(), rhs)
+ != itw->second.end())
+ {
+ Trace("sg-cconj-debug")
+ << " -> already are considering this conjecture." << std::endl;
+ return -1;
}
- // check if canonical representation (should be, but for efficiency this is
- // not guarenteed) if( options().quantifiers.conjectureFilterCanonical && (
- // getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs
- // )!=rhs ) ){
- // Trace("sg-cconj") << " -> after processing, not canonical." <<
- // std::endl; return -1;
- //}
-
- int score;
- bool scoreSet = false;
+ }
- Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
- //find witness for counterexample, if possible
- if (options().quantifiers.conjectureFilterModel)
+ size_t score;
+ bool scoreSet = false;
+
+ Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs
+ << " == " << rhs << "?" << std::endl;
+ // find witness for counterexample, if possible
+ Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end());
+ Trace("sg-cconj-debug") << "Notify substitutions over "
+ << d_rel_pattern_var_sum[lhs] << " variables."
+ << std::endl;
+ std::map<TNode, TNode> subs;
+ d_subs_confirmCount = 0;
+ d_subs_confirmWitnessRange.clear();
+ d_subs_confirmWitnessDomain.clear();
+ d_subs_unkCount = 0;
+ if (!d_rel_pattern_subs_index[lhs].notifySubstitutions(
+ this, subs, rhs, d_rel_pattern_var_sum[lhs]))
+ {
+ Trace("sg-cconj") << " -> found witness that falsifies the conjecture."
+ << std::endl;
+ return -1;
+ }
+ // score is the minimum number of distinct substitutions for a variable
+ for (std::pair<const TNode, std::vector<TNode> >& w :
+ d_subs_confirmWitnessDomain)
+ {
+ size_t num = w.second.size();
+ if (!scoreSet || num < score)
{
- Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end());
- Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl;
- std::map< TNode, TNode > subs;
- d_subs_confirmCount = 0;
- d_subs_confirmWitnessRange.clear();
- d_subs_confirmWitnessDomain.clear();
- d_subs_unkCount = 0;
- if( !d_rel_pattern_subs_index[lhs].notifySubstitutions( this, subs, rhs, d_rel_pattern_var_sum[lhs] ) ){
- Trace("sg-cconj") << " -> found witness that falsifies the conjecture." << std::endl;
- return -1;
- }
- //score is the minimum number of distinct substitutions for a variable
- for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
- int num = (int)it->second.size();
- if( !scoreSet || num<score ){
- score = num;
- scoreSet = true;
- }
- }
- if( !scoreSet ){
- score = 0;
- }
- Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
- for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
- Trace("sg-cconj") << " #witnesses for " << it->first << " : " << it->second.size() << std::endl;
- }
+ score = num;
+ scoreSet = true;
}
- else
+ }
+ if (!scoreSet)
+ {
+ score = 0;
+ }
+ if (TraceIsOn("sg-cconj"))
+ {
+ Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount
+ << ", #witnesses range = "
+ << d_subs_confirmWitnessRange.size() << "." << std::endl;
+ for (std::pair<const TNode, std::vector<TNode> >& w :
+ d_subs_confirmWitnessDomain)
{
- score = 1;
+ Trace("sg-cconj") << " #witnesses for " << w.first << " : "
+ << w.second.size() << std::endl;
}
-
Trace("sg-cconj") << " -> SUCCESS." << std::endl;
Trace("sg-cconj") << " score : " << score << std::endl;
-
- return score;
}
+ return static_cast<int>(score);
}
bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) {
}
Trace("sg-gen-tg-debug") << std::endl;
}
- if( options::conjectureFilterActiveTerms() && d_ccand_eqc[0][i].empty() ){
+ // filter based active terms
+ if (d_ccand_eqc[0][i].empty())
+ {
Trace("sg-gen-consider-term") << "Do not consider term of form ";
d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl;
return false;
}
- if( options::conjectureFilterModel() && d_ccand_eqc[1][i].empty() ){
+ // filter based on model
+ if (d_ccand_eqc[1][i].empty())
+ {
Trace("sg-gen-consider-term") << "Do not consider term of form ";
d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl;
bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){
Assert(tg_id < d_tg_alloc.size());
- if( options::conjectureFilterCanonical() ){
- //check based on a canonicity of the term (if there is one)
- Trace("sg-gen-tg-debug") << "Consider term canon ";
- d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
- Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl;
-
- Node ln = d_tg_alloc[tg_id].getTerm( this );
- Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl;
- return d_cg->considerTermCanon( ln, d_gen_relevant_terms );
- }
- return true;
+ // filter based on canonical
+ // check based on a canonicity of the term (if there is one)
+ Trace("sg-gen-tg-debug") << "Consider term canon ";
+ d_tg_alloc[0].debugPrint(this, "sg-gen-tg-debug", "sg-gen-tg-debug");
+ Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl;
+
+ Node ln = d_tg_alloc[tg_id].getTerm(this);
+ Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl;
+ return d_cg->considerTermCanon(ln, d_gen_relevant_terms);
}
bool TermGenEnv::isRelevantFunc( Node f ) {
projects / cvc5.git / commitdiff