}
theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) {
- if(optarg == "default" || optarg == "all" ) {
+ if(optarg == "default") {
return theory::quantifiers::TRIGGER_SEL_DEFAULT;
} else if(optarg == "min") {
return theory::quantifiers::TRIGGER_SEL_MIN;
} else if(optarg == "max") {
return theory::quantifiers::TRIGGER_SEL_MAX;
+ } else if(optarg == "all") {
+ return theory::quantifiers::TRIGGER_SEL_ALL;
} else if(optarg == "help") {
puts(s_triggerSelModeHelp.c_str());
exit(1);
TRIGGER_SEL_MIN,
/** only consider maximal terms for triggers */
TRIGGER_SEL_MAX,
+ /** consider all terms for triggers */
+ TRIGGER_SEL_ALL,
};
enum CVC4_PUBLIC PrenexQuantMode {
}
}
-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
- d_op( op ), d_qe( qe ), d_term_iter( -1 ){
+CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
+ d_qe( qe ), d_term_iter( -1 ){
+ d_op = qe->getTermDatabase()->getMatchOperator( pat );
Assert( !d_op.isNull() );
+ d_op_arity = pat.getNumChildren();
}
void CandidateGeneratorQE::resetInstantiationRound(){
}else{
eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
if( ee->hasTerm( eqc ) ){
- //create an equivalence class iterator in eq class eqc
- Node rep = ee->getRepresentative( eqc );
- d_eqc_iter = eq::EqClassIterator( rep, ee );
- d_mode = cand_term_eqc;
+ quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op );
+ if( tat ){
+#if 1
+ //create an equivalence class iterator in eq class eqc
+ Node rep = ee->getRepresentative( eqc );
+ d_eqc_iter = eq::EqClassIterator( rep, ee );
+ d_mode = cand_term_eqc;
+#else
+ d_tindex.push_back( tat );
+ d_tindex_iter.push_back( tat->d_data.begin() );
+ d_mode = cand_term_tindex;
+#endif
+ }else{
+ d_mode = cand_term_none;
+ }
}else{
+ //the only match is this term itself
d_n = eqc;
d_mode = cand_term_ident;
}
}else{
Node r = d_qe->getEqualityQuery()->getRepresentative( n );
if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
+ Debug("cand-gen-qe") << "...returning " << n << std::endl;
return n;
}
}
Node n = *d_eqc_iter;
++d_eqc_iter;
if( isLegalOpCandidate( n ) ){
+ Debug("cand-gen-qe") << "...returning " << n << std::endl;
return n;
}
}
+ }else if( d_mode==cand_term_tindex ){
+ Debug("cand-gen-qe") << "...get next candidate in tindex " << d_op << " " << d_op_arity << std::endl;
+ //increment the term index iterator
+ if( !d_tindex.empty() ){
+ //populate the vector
+ while( d_tindex_iter.size()<=d_op_arity ){
+ Assert( !d_tindex_iter.empty() );
+ Assert( !d_tindex_iter.back()->second.d_data.empty() );
+ d_tindex.push_back( &(d_tindex_iter.back()->second) );
+ d_tindex_iter.push_back( d_tindex_iter.back()->second.d_data.begin() );
+ }
+ //get the current node
+ Assert( d_tindex_iter.back()->second.hasNodeData() );
+ Node n = d_tindex_iter.back()->second.getNodeData();
+ Debug("cand-gen-qe") << "...returning " << n << std::endl;
+ Assert( !n.isNull() );
+ Assert( isLegalOpCandidate( n ) );
+ //increment
+ bool success = false;
+ do{
+ ++d_tindex_iter.back();
+ if( d_tindex_iter.back()==d_tindex.back()->d_data.end() ){
+ d_tindex.pop_back();
+ d_tindex_iter.pop_back();
+ }else{
+ success = true;
+ }
+ }while( !success && !d_tindex.empty() );
+ return n;
+ }
}else if( d_mode==cand_term_ident ){
Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
if( !d_n.isNull() ){
namespace CVC4 {
namespace theory {
+namespace quantifiers {
+ class TermArgTrie;
+}
+
class QuantifiersEngine;
namespace inst {
//instantiator pointer
QuantifiersEngine* d_qe;
//the equality class iterator
+ unsigned d_op_arity;
+ std::vector< quantifiers::TermArgTrie* > d_tindex;
+ std::vector< std::map< TNode, quantifiers::TermArgTrie >::iterator > d_tindex_iter;
eq::EqClassIterator d_eqc_iter;
//std::vector< Node > d_eqc;
int d_term_iter;
cand_term_db,
cand_term_ident,
cand_term_eqc,
+ cand_term_tindex,
cand_term_none,
};
short d_mode;
Node d_n;
std::map< Node, bool > d_exclude_eqc;
public:
- CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
+ CandidateGeneratorQE( QuantifiersEngine* qe, Node pat );
~CandidateGeneratorQE() throw() {}
void resetInstantiationRound();
namespace CVC4 {
-EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ) {
+EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_rep_exp(c) {
}
-EqualityInference::EqualityInference( context::Context* c ) : d_c( c ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ){
+EqualityInference::EqualityInference( context::Context* c, bool trackExp ) :
+d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
}
Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl;
Trace("eq-infer") << " since they both normalize to : " << r << std::endl;
d_pending_merges.push_back( t.eqNode( t2 ) );
+ if( d_trackExplain ){
+ //TODO
+ d_pending_merge_exp.push_back( t.eqNode( t2 ) );
+ }
}
}
}
}
}
+Node EqualityInference::getPendingMergeExplanation( unsigned i ) {
+ Assert( d_trackExplain );
+ return d_pending_merge_exp[i];
+}
+
}
~EqcInfo(){}
context::CDO< Node > d_rep;
context::CDO< bool > d_valid;
+ //explanation for why d_rep is how it is
+ NodeList d_rep_exp;
};
+ /** track explanations */
+ bool d_trackExplain;
/** information necessary for equivalence classes */
NodeMap d_elim_vars;
std::map< Node, EqcInfo * > d_eqci;
void addToUseList( Node used, Node eqc );
/** pending merges */
NodeList d_pending_merges;
+ NodeList d_pending_merge_exp;
public:
- EqualityInference(context::Context* c);
+ //second argument is whether explanations should be tracked
+ EqualityInference(context::Context* c, bool trackExp = false);
virtual ~EqualityInference();
/** input : notification when equality engine is updated */
void eqNotifyNewClass(TNode t);
/** output : inferred equalities */
unsigned getNumPendingMerges() { return d_pending_merges.size(); }
Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; }
+ Node getPendingMergeExplanation( unsigned i );
};
}
//create candidate generator
if( Trigger::isAtomicTrigger( d_match_pattern ) ){
//we will be scanning lists trying to find d_match_pattern.getOperator()
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
+ d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern );
//if matching on disequality, inform the candidate generator not to match on eqc
if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){
((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
}
InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
+ if( d_match_pattern.getKind()==NOT ){
+ d_match_pattern = d_match_pattern[0];
+ d_pol = false;
+ }else{
+ d_pol = true;
+ }
if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
d_eqc = d_match_pattern[1];
d_match_pattern = d_match_pattern[0];
}
int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
- InstMatch m( q );
- m.add( baseMatch );
int addedLemmas = 0;
quantifiers::TermArgTrie* tat;
if( d_eqc.isNull() ){
tat = qe->getTermDatabase()->getTermArgTrie( d_op );
}else{
- tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
+ if( d_pol ){
+ tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
+ }else{
+ Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
+ //iterate over all classes except r
+ tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
+ for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+ if( it->first!=r ){
+ InstMatch m( q );
+ m.add( baseMatch );
+ addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+ }
+ }
+ tat = NULL;
+ }
}
if( tat ){
+ InstMatch m( q );
+ m.add( baseMatch );
addInstantiations( m, qe, addedLemmas, 0, tat );
return addedLemmas;
}else{
Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
if( argIndex==(int)d_match_pattern.getNumChildren() ){
Assert( !tat->d_data.empty() );
- Node t = tat->d_data.begin()->first;
+ TNode t = tat->getNodeData();
Debug("simple-trigger") << "Actual term is " << t << std::endl;
//convert to actual used terms
for( std::map< int, int >::iterator it = d_var_num.begin(); it != d_var_num.end(); ++it ){
/** match term */
Node d_match_pattern;
/** equivalence class */
+ bool d_pol;
Node d_eqc;
/** match pattern arg types */
std::vector< TypeNode > d_match_pattern_arg_types;
InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
//how to select trigger terms
- if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
+ if( options::triggerSelMode()==TRIGGER_SEL_MIN || options::triggerSelMode()==TRIGGER_SEL_DEFAULT ){
d_tr_strategy = Trigger::TS_MIN_TRIGGER;
}else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
d_tr_strategy = Trigger::TS_MAX_TRIGGER;
/** the data */
std::map< TNode, TermArgTrie > d_data;
public:
+ bool hasNodeData() { return !d_data.empty(); }
+ TNode getNodeData() { return d_data.begin()->first; }
TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 );
TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
//for triggers
private:
/** helper function for compute var contains */
- void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited );
+ static void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited );
/** triggers for each operator */
std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
/** helper for is instance of */
- bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
+ static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
/** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
- int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
+ static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
public:
/** compute var contains */
- void computeVarContains( Node n, std::vector< Node >& varContains );
+ static void computeVarContains( Node n, std::vector< Node >& varContains );
/** get var contains for each of the patterns in pats */
- void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
+ static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
/** get var contains for node n */
- void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
- /** register trigger (for eager quantifier instantiation) */
- void registerTrigger( inst::Trigger* tr, Node op );
+ static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
/** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
- int isInstanceOf( Node n1, Node n2 );
+ static int isInstanceOf( Node n1, Node n2 );
/** filter all nodes that have instances */
- void filterInstances( std::vector< Node >& nodes );
+ static void filterInstances( std::vector< Node >& nodes );
+ /** register trigger (for eager quantifier instantiation) */
+ void registerTrigger( inst::Trigger* tr, Node op );
//for term ordering
private:
}
bool Trigger::isSimpleTrigger( Node n ){
- Node t = n;
+ Node t = n.getKind()==NOT ? n[0] : n;
if( n.getKind()==IFF || n.getKind()==EQUAL ){
if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){
t = n[0];
}
//store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
-bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited, int tstrt, std::vector< Node >& exclude,
- std::map< Node, int >& reqPol, bool pol, bool hasPol, bool epol, bool hasEPol ){
- std::map< Node, bool >::iterator itv = visited.find( n );
+bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv,
+ int tstrt, std::vector< Node >& exclude,
+ std::map< Node, int >& reqPol, std::vector< Node >& added,
+ bool pol, bool hasPol, bool epol, bool hasEPol ){
+ std::map< Node, Node >::iterator itv = visited.find( n );
if( itv==visited.end() ){
- visited[ n ] = false;
+ visited[ n ] = Node::null();
Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
bool retVal = false;
if( n.getKind()!=FORALL ){
- if( tstrt==TS_MIN_TRIGGER ){
+ bool rec = true;
+ Node nu;
+ if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+ nu = getIsUsableTrigger( n, f, pol, hasPol );
+ if( !nu.isNull() ){
+ reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0;
+ visited[ nu ] = nu;
+ quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] );
+ retVal = true;
+ if( tstrt==TS_MAX_TRIGGER ){
+ rec = false;
+ }
+ }
+ }
+ if( rec ){
+ std::vector< Node > added2;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
bool newHasPol, newPol;
bool newHasEPol, newEPol;
QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol );
- if( collectPatTerms2( f, n[i], visited, tstrt, exclude, reqPol, newPol, newHasPol, newEPol, newHasEPol ) ){
+ if( collectPatTerms2( f, n[i], visited, visited_fv, tstrt, exclude, reqPol, added2, newPol, newHasPol, newEPol, newHasEPol ) ){
retVal = true;
}
}
- if( !retVal ){
- Node nu;
- if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
- nu = getIsUsableTrigger( n, f, pol, hasPol );
- }
- if( !nu.isNull() ){
- reqPol[ nu ] = hasEPol ? ( epol==(n.getKind()!=NOT) ? 1 : -1 ) : 0;
- visited[ nu ] = true;
- retVal = true;
- }
- }
- }else{
- Node nu;
- if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
- nu = getIsUsableTrigger( n, f, pol, hasPol );
- }
- bool rec = true;
if( !nu.isNull() ){
- reqPol[ nu ] = hasEPol ? ( epol==(n.getKind()!=NOT) ? 1 : -1 ) : 0;
- visited[ nu ] = true;
- retVal = true;
- if( tstrt==TS_MAX_TRIGGER ){
- rec = false;
- }
- }
- if( rec ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool newHasPol, newPol;
- bool newHasEPol, newEPol;
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol );
- if( collectPatTerms2( f, n[i], visited, tstrt, exclude, reqPol, newPol, newHasPol, newEPol, newHasEPol ) ){
- retVal = true;
+ bool rm_nu = false;
+ //discard if we added a subterm as a trigger with all variables that nu has
+ for( unsigned i=0; i<added2.size(); i++ ){
+ Assert( visited_fv.find( added2[i] )!=visited_fv.end() );
+ if( visited_fv[ nu ].size()==visited_fv[added2[i]].size() ){
+ rm_nu = true;
}
+ added.push_back( added2[i] );
+ }
+ if( rm_nu && tstrt==TS_MIN_TRIGGER ){
+ visited[nu] = Node::null();
+ reqPol.erase( nu );
+ }else{
+ added.push_back( nu );
}
}
}
}
return retVal;
}else{
- return itv->second;
+ if( itv->second.isNull() ){
+ return false;
+ }else{
+ added.push_back( itv->second );
+ return true;
+ }
}
}
-
-
bool Trigger::isBooleanTermTrigger( Node n ) {
if( n.getKind()==ITE ){
//check for boolean term converted to ITE
void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude,
std::map< Node, int >& reqPol, bool filterInst ){
- std::map< Node, bool > visited;
+ std::map< Node, Node > visited;
if( filterInst ){
//immediately do not consider any term t for which another term is an instance of t
std::vector< Node > patTerms2;
//do not consider terms that have instances
for( unsigned i=0; i<patTerms2.size(); i++ ){
if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
- visited[ patTerms2[i] ] = false;
+ visited[ patTerms2[i] ] = Node::null();
}
}
}
}
- collectPatTerms2( f, n, visited, tstrt, exclude, reqPol, true, true, false, true );
+ std::map< Node, std::vector< Node > > visited_fv;
+ std::vector< Node > added;
+ collectPatTerms2( f, n, visited, visited_fv, tstrt, exclude, reqPol, added, true, true, false, true );
for( std::map< Node, int >::iterator it = reqPol.begin(); it != reqPol.end(); ++it ){
- if( visited[it->first] ){
+ if( !visited[it->first].isNull() ){
patTerms.push_back( it->first );
}
}
static Node getIsUsableTrigger( Node n, Node f, bool pol = true,
bool hasPol = false );
/** collect all APPLY_UF pattern terms for f in n */
- static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited,
- int tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol,
+ static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv,
+ int tstrt, std::vector< Node >& exclude,
+ std::map< Node, int >& reqPol, std::vector< Node >& added,
bool pol, bool hasPol, bool epol, bool hasEPol );
std::vector< Node > d_nodes;
projects / cvc5.git / commitdiff