aggressive split quantified formulas that lead to variable eliminations
option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
split ites with dt testers as conditions
-# Whether to CNF quantifier bodies
-# option cnfQuant --cnf-quant bool :default false
-# apply CNF conversion to quantified formulas
-option nnfQuant --nnf-quant bool :default true
- apply NNF conversion to quantified formulas
# Whether to pre-skolemize quantifier bodies.
# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
# forall x. P( x ) => f( S( x ) ) = x
*/
unsigned d_simplifyAssertionsDepth;
+ /** whether certain preprocess steps are necessary */
+ bool d_needsExpandDefs;
+ bool d_needsRewriteBoolTerms;
+ bool d_needsConstrainSubTypes;
+
public:
/**
* Map from skolem variables to index in d_assertions containing
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
d_simplifyAssertionsDepth(0),
+ d_needsExpandDefs(true),
+ d_needsRewriteBoolTerms(true),
+ d_needsConstrainSubTypes(true), //TODO
d_iteSkolemMap(),
d_iteRemover(smt.d_userContext),
d_pbsProcessor(smt.d_userContext),
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
+
dumpAssertions("pre-constrain-subtypes", d_assertions);
{
// Any variables of subtype types need to be constrained properly.
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
dumpAssertions("post-everything", d_assertions);
+
//set instantiation level of everything to zero
if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
}else{
Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
- Node ee_exp;
+ std::vector< TNode > assumptions;
//if( options::dtRExplainLemmas() ){
- ee_exp = explain( exp );
+ explain( exp, assumptions );
//}else{
// ee_exp = exp;
//}
- Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
- lem = NodeManager::currentNM()->mkNode( OR, ee_exp.negate(), fact );
- lem = Rewriter::rewrite( lem );
+ //Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
+ if( assumptions.empty() ){
+ lem = fact;
+ }else{
+ std::vector< Node > children;
+ for( unsigned i=0; i<assumptions.size(); i++ ){
+ children.push_back( assumptions[i].negate() );
+ }
+ children.push_back( fact );
+ lem = NodeManager::currentNM()->mkNode( OR, children );
+ }
}
Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
if( doSendLemma( lem ) ){
bool addLemma = false;
if( options::dtInferAsLemmas() && exp!=d_true ){
addLemma = true;
- }else if( n.getKind()==EQUAL || n.getKind()==IFF ){
- /*
- for( unsigned i=0; i<2; i++ ){
- if( !n[i].isVar() && n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
- addLemma = true;
- }
- }
- */
+ }else if( n.getKind()==EQUAL ){
TypeNode tn = n[0].getType();
if( !DatatypesRewriter::isTypeDatatype( tn ) ){
addLemma = true;
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
addLemma = dt.involvesExternalType();
}
- //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
- // if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
- // addLemma = true;
- // break;
- // }
- //}
- }else if( n.getKind()==LEQ ){
- addLemma = true;
- }else if( n.getKind()==OR ){
+ }else if( n.getKind()==LEQ || n.getKind()==IFF || n.getKind()==OR ){
addLemma = true;
}
if( addLemma ){
d_op( op ), d_qe( qe ), d_term_iter( -1 ){
Assert( !d_op.isNull() );
}
+
void CandidateGeneratorQE::resetInstantiationRound(){
d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op );
}
if( eqc.isNull() ){
d_mode = cand_term_db;
}else{
- //create an equivalence class iterator in eq class eqc
- //d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
-
- eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
- if( ee->hasTerm( eqc ) ){
- Node rep = ee->getRepresentative( eqc );
- d_eqc_iter = eq::EqClassIterator( rep, ee );
- d_mode = cand_term_eqc;
+ if( isExcludedEqc( eqc ) ){
+ d_mode = cand_term_none;
}else{
- d_n = eqc;
- d_mode = cand_term_ident;
+ 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;
+ }else{
+ d_n = eqc;
+ d_mode = cand_term_ident;
+ }
}
- //a should be in its equivalence class
- //Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
}
}
bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
Node CandidateGeneratorQE::getNextCandidate(){
if( d_mode==cand_term_db ){
+ Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
//get next candidate term in the uf term database
while( d_term_iter<d_term_iter_limit ){
Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
d_term_iter++;
if( isLegalCandidate( n ) ){
if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
- return n;
+ if( d_exclude_eqc.empty() ){
+ return n;
+ }else{
+ Node r = d_qe->getEqualityQuery()->getRepresentative( n );
+ if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
+ return n;
+ }
+ }
}
}
}
}else if( d_mode==cand_term_eqc ){
+ Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
while( !d_eqc_iter.isFinished() ){
Node n = *d_eqc_iter;
++d_eqc_iter;
}
}
}else if( d_mode==cand_term_ident ){
+ Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
if( !d_n.isNull() ){
Node n = d_n;
d_n = Node::null();
cand_term_db,
cand_term_ident,
cand_term_eqc,
+ cand_term_none,
};
short d_mode;
bool isLegalOpCandidate( Node n );
Node d_n;
+ std::map< Node, bool > d_exclude_eqc;
public:
CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
~CandidateGeneratorQE() throw() {}
void resetInstantiationRound();
void reset( Node eqc );
Node getNextCandidate();
+ void excludeEqc( Node r ) { d_exclude_eqc[r] = true; }
+ bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); }
};
class CandidateGeneratorQELitEq : public CandidateGenerator
d_match_pattern_type = pat.getType();
d_next = NULL;
d_matchPolicy = MATCH_GEN_DEFAULT;
- d_eq_class_rel = false;
}
InstMatchGenerator::InstMatchGenerator() {
void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
if( !d_pattern.isNull() ){
- Debug("inst-match-gen") << "Pattern term is " << d_pattern << std::endl;
+ Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
if( d_match_pattern.getKind()==NOT ){
//we want to add the children of the NOT
d_match_pattern = d_pattern[0];
if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
//make sure the matching portion of the equality is on the LHS of d_pattern
// and record what d_match_pattern is
- if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){
- if( d_match_pattern[1].getKind()!=INST_CONSTANT ){
- Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) );
- Node mp = d_match_pattern[1];
- //swap sides
- Node pat = d_pattern;
- if(d_match_pattern.getKind()==GEQ){
- d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] );
- d_pattern = d_pattern.negate();
- }else{
- d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
- }
- d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
- d_match_pattern = mp;
- }
- }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){
- if( d_match_pattern[0].getKind()!=INST_CONSTANT ){
- Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) );
- if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
- d_match_pattern = d_match_pattern[0];
- }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){
- d_match_pattern = d_match_pattern[0];
+ for( unsigned i=0; i<2; i++ ){
+ if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
+ Node mp = d_match_pattern[1-i];
+ Node mpo = d_match_pattern[i];
+ if( mp.getKind()!=INST_CONSTANT ){
+ if( i==0 ){
+ if( d_match_pattern.getKind()==GEQ ){
+ d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo );
+ d_pattern = d_pattern.negate();
+ }else{
+ d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo );
+ }
+ }
+ d_eq_class_rel = mpo;
+ d_match_pattern = mp;
}
+ break;
}
}
}else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT && options::purifyDtTriggers() ){
d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
//now, collect children of d_match_pattern
- //int childMatchPolicy = MATCH_GEN_DEFAULT;
for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
Node qa = quantifiers::TermDb::getInstConstAttr(d_match_pattern[i]);
if( !qa.isNull() ){
}
//create candidate generator
- if( d_match_pattern.getKind()==INST_CONSTANT ){
+ 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 );
+ //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 );
+ d_eq_class_rel = Node::null();
+ }
+ }else if( d_match_pattern.getKind()==INST_CONSTANT ){
if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
size_t selectorIndex = Datatype::cindexOf(selectorExpr);
d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
}
}else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+ Assert( d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT );
//we will be producing candidates via literal matching heuristics
if( d_pattern.getKind()!=NOT ){
//candidates will be all equalities
//candidates will be all disequalities
d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
}
- }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF ||
- d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){
- Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
- if( d_pattern.getKind()==NOT ){
- if (d_pattern[0][1].getKind()!=INST_CONSTANT) {
- Unimplemented("Disequal generator unimplemented");
- }else{
- d_eq_class = d_pattern[0][1];
- }
- }else{
- //store the equivalence class that we will call d_cg->reset( ... ) on
- d_eq_class = d_pattern[1];
- }
- d_eq_class_rel = true;
- Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
- //we are matching only in a particular equivalence class
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
- }else 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 );
}else{
d_cg = new CandidateGeneratorQueue;
Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
}
}
//for relational matching
- }else if( d_eq_class_rel && d_eq_class.getKind()==INST_CONSTANT ){
- int v = d_eq_class.getAttribute(InstVarNumAttribute());
+ }else if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()==INST_CONSTANT ){
+ int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
//also must fit match to equivalence class
bool pol = d_pattern.getKind()!=NOT;
Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
eqc = qe->getEqualityQuery()->getRepresentative( eqc );
Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
- if( !eqc.isNull() ){
+ if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
+ d_eq_class = d_eq_class_rel;
+ }else if( !eqc.isNull() ){
d_eq_class = eqc;
}
//we have a specific equivalence class in mind
//we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
//just look in equivalence class of the RHS
- d_cg->reset( d_eq_class_rel ? Node::null() : d_eq_class );
+ d_cg->reset( d_eq_class );
d_needsReset = false;
}
bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
if( d_needsReset ){
Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
- reset( d_eq_class_rel ? Node::null() : d_eq_class, qe );
+ reset( d_eq_class, qe );
}
m.d_matched = Node::null();
Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
if( !success ){
Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
//we failed, must reset
- reset( d_eq_class_rel ? Node::null() : d_eq_class, qe );
+ reset( d_eq_class, qe );
}
return success;
}
}
InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
+ if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+ d_eqc = d_match_pattern[1];
+ d_match_pattern = d_match_pattern[0];
+ Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) );
+ }
+ Assert( Trigger::isSimpleTrigger( d_match_pattern ) );
for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
if( d_match_pattern[i].getKind()==INST_CONSTANT ){
if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==q ){
InstMatch m( q );
m.add( baseMatch );
int addedLemmas = 0;
-
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_op ]) );
- return addedLemmas;
+ quantifiers::TermArgTrie* tat;
+ if( d_eqc.isNull() ){
+ tat = qe->getTermDatabase()->getTermArgTrie( d_op );
+ }else{
+ tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
+ }
+ if( tat ){
+ addInstantiations( m, qe, addedLemmas, 0, tat );
+ return addedLemmas;
+ }else{
+ return 0;
+ }
}
void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
InstMatchGenerator* d_next;
/** eq class */
Node d_eq_class;
- bool d_eq_class_rel;
+ Node d_eq_class_rel;
/** variable numbers */
std::map< int, int > d_var_num;
/** initialize pattern */
Node d_f;
/** match term */
Node d_match_pattern;
+ /** equivalence class */
+ Node d_eqc;
/** match pattern arg types */
std::vector< TypeNode > d_match_pattern_arg_types;
/** operator */
d_patTerms[1][f].clear();
bool ntrivTriggers = options::relationalTriggers();
std::vector< Node > patTermsF;
+ std::map< Node, int > reqPol;
//well-defined function: can assume LHS is only trigger
if( options::quantFunWellDefined() ){
Node hd = TermDb::getFunDefHead( f );
if( !hd.isNull() ){
hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f );
patTermsF.push_back( hd );
+ reqPol[hd] = 0;
}
}
//otherwise, use algorithm for collecting pattern terms
if( patTermsF.empty() ){
Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
- Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true );
+ Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], reqPol, true );
Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
if( ntrivTriggers ){
sortTriggers st;
std::sort( patTermsF.begin(), patTermsF.end(), st );
}
for( unsigned i=0; i<patTermsF.size(); i++ ){
- Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl;
+ Assert( reqPol.find( patTermsF[i] )!=reqPol.end() );
+ Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << " " << reqPol[patTermsF[i]] << std::endl;
}
Trace("auto-gen-trigger-debug") << std::endl;
}
- //sort into single/multi triggers
+ //sort into single/multi triggers, calculate which terms should not be considered
std::map< Node, std::vector< Node > > varContains;
std::map< Node, bool > vcMap;
std::map< Node, bool > rmPatTermsF;
}
int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
- Trace("auto-gen-trigger-debug") << "Exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
+ Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
rmPatTermsF[patTermsF[i]] = true;
}else{
last_weight = curr_w;
}
}
for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
- if( rmPatTermsF.find( it->first )==rmPatTermsF.end() ){
- if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( it->first ) ) ){
- d_patTerms[0][f].push_back( it->first );
- d_is_single_trigger[ it->first ] = true;
+ Node pat = it->first;
+ Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
+ if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
+ //process the pattern: if it has a required polarity, consider it
+ if( options::instNoEntail() ){
+ Assert( reqPol.find( pat )!=reqPol.end() );
+ int rpol = reqPol[pat];
+ Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << std::endl;
+ if( rpol!=0 ){
+ Assert( pat.getType().isBoolean() );
+ if( pat.getKind()==APPLY_UF ){
+ pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+ }
+ }
+ }
+ if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
+ d_patTerms[0][f].push_back( pat );
+ d_is_single_trigger[ pat ] = true;
}else{
- d_patTerms[1][f].push_back( it->first );
- d_is_single_trigger[ it->first ] = false;
+ d_patTerms[1][f].push_back( pat );
+ d_is_single_trigger[ pat ] = false;
}
}
}
//sort based on # occurrences (this will cause Trigger to select rarer symbols)
std::sort( patTerms.begin(), patTerms.end(), sqfs );
Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
- for( int i=0; i<(int)patTerms.size(); i++ ){
+ for( unsigned i=0; i<patTerms.size(); i++ ){
Debug("relevant-trigger") << " " << patTerms[i] << " (";
Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
}
std::map< Node, int > d_counter;
/** single, multi triggers for each quantifier */
std::map< Node, std::vector< Node > > d_patTerms[2];
+ std::map< Node, std::map< Node, bool > > d_patReqPol;
+ /** information about triggers */
std::map< Node, bool > d_is_single_trigger;
std::map< Node, bool > d_single_trigger_gen;
std::map< Node, bool > d_made_multi_trigger;
newPol = pol;
}
}
+
+void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
+ if( n.getKind()==AND || n.getKind()==OR ){
+ newHasPol = hasPol && pol==( n.getKind()==AND );
+ newPol = pol;
+ }else if( n.getKind()==IMPLIES ){
+ newHasPol = hasPol && !pol;
+ newPol = child==0 ? !pol : pol;
+ }else if( n.getKind()==NOT ){
+ newHasPol = hasPol;
+ newPol = !pol;
+ }else{
+ newHasPol = false;
+ newPol = pol;
+ }
+}
+
std::map< Node, Node > d_phase_reqs_equality_term;
static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
+ static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
};
}else if( isLiteral( body[0] ) ){
return body;
}else{
- std::vector< Node > children;
+ std::vector< Node > children;
Kind k = body[0].getKind();
if( body[0].getKind()==OR || body[0].getKind()==AND ){
}else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
return options::aggressiveMiniscopeQuant() && is_std;
}else if( computeOption==COMPUTE_NNF ){
- return options::nnfQuant();
+ return true;
}else if( computeOption==COMPUTE_PROCESS_TERMS ){
return true;
//return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
}
bool Trigger::isSimpleTrigger( Node n ){
- if( isAtomicTrigger( n ) ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){
+ Node t = n;
+ if( n.getKind()==IFF || n.getKind()==EQUAL ){
+ if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){
+ t = n[0];
+ }
+ }
+ if( isAtomicTrigger( t ) ){
+ for( unsigned i=0; i<t.getNumChildren(); i++ ){
+ if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(t[i]) ){
return false;
}
}
- if( options::purifyDtTriggers() && n.getKind()==APPLY_SELECTOR_TOTAL ){
+ if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){
return false;
}
return true;
}
}
-
-bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
- if( patMap.find( n )==patMap.end() ){
- patMap[ n ] = false;
- if( tstrt==TS_MIN_TRIGGER ){
- if( n.getKind()==FORALL ){
- return false;
- }else{
- bool retVal = false;
+//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 );
+ if( itv==visited.end() ){
+ visited[ n ] = false;
+ 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 ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
bool newHasPol, newPol;
+ bool newHasEPol, newEPol;
QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
+ QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol );
+ if( collectPatTerms2( f, n[i], visited, tstrt, exclude, reqPol, newPol, newHasPol, newEPol, newHasEPol ) ){
retVal = true;
}
}
- if( retVal ){
- return true;
- }else{
+ if( !retVal ){
Node nu;
if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
nu = getIsUsableTrigger( n, f, pol, hasPol );
}
if( !nu.isNull() ){
- patMap[ nu ] = true;
- return true;
- }else{
- return false;
+ reqPol[ nu ] = hasEPol ? ( epol==(n.getKind()!=NOT) ? 1 : -1 ) : 0;
+ visited[ nu ] = true;
+ retVal = true;
}
}
- }
- }else{
- bool retVal = false;
- Node nu;
- if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
- nu = getIsUsableTrigger( n, f, pol, hasPol );
- }
- if( !nu.isNull() ){
- patMap[ nu ] = true;
- if( tstrt==TS_MAX_TRIGGER ){
- return true;
- }else{
+ }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( n.getKind()!=FORALL ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool newHasPol, newPol;
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
- retVal = true;
+ 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;
+ }
}
}
}
- return retVal;
}
+ return retVal;
}else{
- return patMap[ n ];
+ return itv->second;
}
}
return true;
}
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
- std::map< Node, bool > patMap;
+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;
if( filterInst ){
//immediately do not consider any term t for which another term is an instance of t
std::vector< Node > patTerms2;
- collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, false );
+ std::map< Node, int > reqPol2;
+ collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, reqPol2, false );
std::vector< Node > temp;
temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
qe->getTermDatabase()->filterInstances( temp );
if( temp.size()!=patTerms2.size() ){
Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
Trace("trigger-filter-instance") << "Old: ";
- for( int i=0; i<(int)patTerms2.size(); i++ ){
+ for( unsigned i=0; i<patTerms2.size(); i++ ){
Trace("trigger-filter-instance") << patTerms2[i] << " ";
}
Trace("trigger-filter-instance") << std::endl << "New: ";
- for( int i=0; i<(int)temp.size(); i++ ){
+ for( unsigned i=0; i<temp.size(); i++ ){
Trace("trigger-filter-instance") << temp[i] << " ";
}
Trace("trigger-filter-instance") << std::endl;
}
if( tstrt==TS_ALL ){
- patTerms.insert( patTerms.begin(), temp.begin(), temp.end() );
+ for( unsigned i=0; i<temp.size(); i++ ){
+ reqPol[temp[i]] = reqPol2[temp[i]];
+ patTerms.push_back( temp[i] );
+ }
return;
}else{
//do not consider terms that have instances
- for( int i=0; i<(int)patTerms2.size(); i++ ){
+ for( unsigned i=0; i<patTerms2.size(); i++ ){
if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
- patMap[ patTerms2[i] ] = false;
+ visited[ patTerms2[i] ] = false;
}
}
}
}
- collectPatTerms2( f, n, patMap, tstrt, exclude, true, true );
- for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
- if( it->second ){
+ collectPatTerms2( f, n, visited, tstrt, exclude, reqPol, true, true, false, true );
+ for( std::map< Node, int >::iterator it = reqPol.begin(); it != reqPol.end(); ++it ){
+ if( visited[it->first] ){
patTerms.push_back( it->first );
}
}
void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) {
std::vector< Node > patTerms;
+ std::map< Node, int > reqPol;
//collect all patterns from icn
std::vector< Node > exclude;
- collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude );
+ collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude, reqPol );
//collect all variables from all patterns in patTerms, add to t_vars
for( unsigned i=0; i<patTerms.size(); i++ ){
qe->getTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars );
};
static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n,
std::vector< Node >& patTerms, int tstrt,
- std::vector< Node >& exclude,
+ std::vector< Node >& exclude, std::map< Node, int >& reqPol,
bool filterInst = false );
/** is usable trigger */
static bool isUsableTrigger( Node n, Node q );
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 >& patMap,
- int tstrt, std::vector< Node >& exclude,
- bool pol, bool hasPol );
+ static bool 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::vector< Node > d_nodes;
projects / cvc5.git / commitdiff