summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/inst_match_generator.cpp4
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp104
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.h1
-rw-r--r--src/theory/quantifiers/macros.cpp2
-rw-r--r--src/theory/quantifiers/quant_util.h2
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp26
-rw-r--r--src/theory/quantifiers/term_database.cpp90
-rw-r--r--src/theory/quantifiers/term_database.h13
-rw-r--r--src/theory/quantifiers/trigger.cpp261
-rw-r--r--src/theory/quantifiers/trigger.h33
-rw-r--r--src/theory/quantifiers_engine.cpp170
-rw-r--r--src/theory/quantifiers_engine.h14
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am3
-rw-r--r--test/regress/regress0/quantifiers/double-pattern.smt26
14 files changed, 442 insertions, 287 deletions
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 34c7949d6..cfa4190e4 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -139,8 +139,8 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
}else{
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 );
+ }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) &&
+ 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
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 491da7116..8c3154c1c 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -60,6 +60,7 @@ struct sortTriggers {
};
void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
+ Trace("inst-alg-debug") << "reset user triggers" << std::endl;
//reset triggers
for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
for( unsigned i=0; i<it->second.size(); i++ ){
@@ -67,6 +68,7 @@ void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort ef
it->second[i]->reset( Node::null() );
}
}
+ Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
}
int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
@@ -118,11 +120,13 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
bool usable = true;
std::vector< Node > nodes;
for( unsigned i=0; i<pat.getNumChildren(); i++ ){
- nodes.push_back( pat[i] );
- if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], q ) ){
+ Node pat_use = Trigger::getIsUsableTrigger( pat[i], q );
+ if( pat_use.isNull() ){
Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
usable = false;
break;
+ }else{
+ nodes.push_back( pat_use );
}
}
if( usable ){
@@ -132,7 +136,12 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
d_user_gen_wait[q].push_back( nodes );
}else{
- d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ) );
+ Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW );
+ if( t ){
+ d_user_gen[q].push_back( t );
+ }else{
+ Trace("trigger-warn") << "Failed to construct trigger : " << pat << " due to variable mismatch" << std::endl;
+ }
}
}
}
@@ -154,6 +163,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe
}
void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
+ Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl;
//reset triggers
for( unsigned r=0; r<2; r++ ){
for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger[r].begin(); it != d_auto_gen_trigger[r].end(); ++it ){
@@ -164,6 +174,7 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
}
}
d_processed_trigger.clear();
+ Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
}
int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
@@ -235,49 +246,51 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
}
void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
- Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << std::endl;
+ Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << ", #var=" << f[0].getNumChildren() << "..." << std::endl;
if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
//determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
d_patTerms[0][f].clear();
d_patTerms[1][f].clear();
bool ntrivTriggers = options::relationalTriggers();
std::vector< Node > patTermsF;
- std::map< Node, int > reqPol;
+ std::map< Node, inst::TriggerTermInfo > tinfo;
//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;
+ tinfo[hd].init( f, hd );
}
}
//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], reqPol, true );
- Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
+ Trigger::collectPatTerms( f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true );
if( ntrivTriggers ){
sortTriggers st;
std::sort( patTermsF.begin(), patTermsF.end(), st );
}
- for( unsigned i=0; i<patTermsF.size(); i++ ){
- Assert( reqPol.find( patTermsF[i] )!=reqPol.end() );
- Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << " " << reqPol[patTermsF[i]] << std::endl;
+ if( Trace.isOn("auto-gen-trigger-debug") ){
+ Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
+ for( unsigned i=0; i<patTermsF.size(); i++ ){
+ Assert( tinfo.find( patTermsF[i] )!=tinfo.end() );
+ Trace("auto-gen-trigger-debug") << " " << patTermsF[i];
+ Trace("auto-gen-trigger-debug") << " info[" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
+ }
+ Trace("auto-gen-trigger-debug") << std::endl;
}
- Trace("auto-gen-trigger-debug") << std::endl;
}
//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 last_weight = -1;
for( unsigned i=0; i<patTermsF.size(); i++ ){
- d_quantEngine->getTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] );
+ Assert( patTermsF[i].getKind()!=NOT );
bool newVar = false;
- for( unsigned j=0; j<varContains[ patTermsF[i] ].size(); j++ ){
- if( vcMap.find( varContains[ patTermsF[i] ][j] )==vcMap.end() ){
- vcMap[varContains[ patTermsF[i] ][j]] = true;
+ for( unsigned j=0; j<tinfo[ patTermsF[i] ].d_fv.size(); j++ ){
+ if( vcMap.find( tinfo[ patTermsF[i] ].d_fv[j] )==vcMap.end() ){
+ vcMap[tinfo[ patTermsF[i] ].d_fv[j]] = true;
newVar = true;
}
}
@@ -289,33 +302,46 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
last_weight = curr_w;
}
}
- for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
- Node pat = it->first;
- Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
+ for( unsigned i=0; i<patTermsF.size(); i++ ){
+ Node pat = patTermsF[i];
if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
+ Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
//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 ){
+ Assert( tinfo.find( pat )!=tinfo.end() );
+ int rpol = tinfo[pat].d_reqPol;
+ Node rpoleq = tinfo[pat].d_reqPolEq;
+ unsigned num_fv = tinfo[pat].d_fv.size();
+ Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl;
+ if( rpol!=0 ){
+ if( Trigger::isRelationalTrigger( pat ) ){
+ pat = rpol==-1 ? pat.negate() : pat;
+ }else{
+ Assert( Trigger::isAtomicTrigger( pat ) );
+ if( pat.getType().isBoolean() && rpoleq.isNull() ){
pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+ }else{
+ Assert( !rpoleq.isNull() );
+ if( rpol==-1 ){
+ //all equivalence classes except rpoleq
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
+ }else if( rpol==1 ){
+ //all equivalence classes that are not disequal to rpoleq TODO
+ }
}
}
- }
- 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;
+ Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
}else{
- d_patTerms[1][f].push_back( pat );
- d_is_single_trigger[ pat ] = false;
+ if( Trigger::isRelationalTrigger( pat ) ){
+ //consider both polarities
+ addPatternToPool( f, pat.negate(), num_fv );
+ }
}
+ addPatternToPool( f, pat, num_fv );
}
}
+ //tinfo not used below this point
d_made_multi_trigger[f] = false;
- Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
+ Trace("auto-gen-trigger") << "Single trigger pool for " << f << " : " << std::endl;
for( unsigned i=0; i<d_patTerms[0][f].size(); i++ ){
Trace("auto-gen-trigger") << " " << d_patTerms[0][f][i] << std::endl;
}
@@ -427,6 +453,16 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
}
}
+void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) {
+ if( num_fv==q[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
+ d_patTerms[0][q].push_back( pat );
+ d_is_single_trigger[ pat ] = true;
+ }else{
+ d_patTerms[1][q].push_back( pat );
+ d_is_single_trigger[ pat ] = false;
+ }
+}
+
bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
if( q.getNumChildren()==3 ){
std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index d48084514..028f24b27 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -89,6 +89,7 @@ private:
int process( Node q, Theory::Effort effort, int e );
/** generate triggers */
void generateTriggers( Node q );
+ void addPatternToPool( Node q, Node pat, unsigned num_fv );
//bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
/** has user patterns */
bool hasUserPatterns( Node q );
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 90d01ac28..582599680 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -153,7 +153,7 @@ bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
d_qe->getTermDatabase()->getVarContainsNode( f, icn, var );
Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
std::vector< Node > trigger_var;
- inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var );
+ inst::Trigger::getTriggerVariables( icn, f, trigger_var );
Trace("macros-debug2") << "Done." << std::endl;
//only if all variables are also trigger variables
return trigger_var.size()>=var.size();
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 2558dcbee..8db79db9c 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -101,6 +101,8 @@ class EqualityQuery {
public:
EqualityQuery(){}
virtual ~EqualityQuery(){};
+ /** extends engine */
+ virtual bool extendsEngine() { return false; }
/** contains term */
virtual bool hasTerm( Node a ) = 0;
/** get the representative of the equivalence class of a */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 79c300401..5aae4d640 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -244,17 +244,21 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
ret = ret.negate();
status = REWRITE_AGAIN_FULL;
}else if( in.getKind()==FORALL ){
- //compute attributes
- QAttributes qa;
- TermDb::computeQuantAttributes( in, qa );
- if( !qa.isRewriteRule() ){
- for( int op=0; op<COMPUTE_LAST; op++ ){
- if( doOperation( in, op, qa ) ){
- ret = computeOperation( in, op, qa );
- if( ret!=in ){
- rew_op = op;
- status = REWRITE_AGAIN_FULL;
- break;
+ if( in[1].isConst() ){
+ return RewriteResponse( status, in[1] );
+ }else{
+ //compute attributes
+ QAttributes qa;
+ TermDb::computeQuantAttributes( in, qa );
+ if( !qa.isRewriteRule() ){
+ for( int op=0; op<COMPUTE_LAST; op++ ){
+ if( doOperation( in, op, qa ) ){
+ ret = computeOperation( in, op, qa );
+ if( ret!=in ){
+ rew_op = op;
+ status = REWRITE_AGAIN_FULL;
+ break;
+ }
}
}
}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5d20a7048..763a80af3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -208,27 +208,26 @@ void TermDb::computeUfEqcTerms( TNode f ) {
//returns a term n' equivalent to n
// - if hasSubs = true, then n is consider under substitution subs
// - if mkNewTerms = true, then n' is either null, or a term in the master equality engine
-Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited ) {
+Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
std::map< TNode, Node >::iterator itv = visited.find( n );
if( itv != visited.end() ){
return itv->second;
}
Node ret;
Trace("term-db-eval") << "evaluate term : " << n << std::endl;
- eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
- if( ee->hasTerm( n ) ){
+ if( qy->hasTerm( n ) ){
Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
- ret = ee->getRepresentative( n );
+ ret = qy->getRepresentative( n );
}else if( n.getKind()==BOUND_VARIABLE ){
if( hasSubs ){
Assert( subs.find( n )!=subs.end() );
Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
if( subsRep ){
- Assert( ee->hasTerm( subs[n] ) );
- Assert( ee->getRepresentative( subs[n] )==subs[n] );
+ Assert( qy->hasTerm( subs[n] ) );
+ Assert( qy->getRepresentative( subs[n] )==subs[n] );
ret = subs[n];
}else{
- ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited );
+ ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited, qy );
}
}
}else if( n.getKind()==FORALL ){
@@ -239,7 +238,7 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
std::vector< TNode > args;
bool ret_set = false;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited );
+ TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited, qy );
if( c.isNull() ){
ret = TNode::null();
ret_set = true;
@@ -260,9 +259,9 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
Trace("term-db-eval") << "Get term from DB" << std::endl;
TNode nn = d_func_map_trie[f].existsTerm( args );
Trace("term-db-eval") << "Got term " << nn << std::endl;
- if( !nn.isNull() && ee->hasTerm( nn ) ){
+ if( !nn.isNull() && qy->hasTerm( nn ) ){
Trace("term-db-eval") << "return rep " << std::endl;
- ret = ee->getRepresentative( nn );
+ ret = qy->getRepresentative( nn );
ret_set = true;
}
}
@@ -283,10 +282,10 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
}
-TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs ) {
+TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
+ Assert( !qy->extendsEngine() );
Trace("term-db-eval") << "evaluate term : " << n << std::endl;
- eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
- if( ee->hasTerm( n ) ){
+ if( qy->getEngine()->hasTerm( n ) ){
Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
return n;
}else if( n.getKind()==BOUND_VARIABLE ){
@@ -294,11 +293,11 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
Assert( subs.find( n )!=subs.end() );
Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
if( subsRep ){
- Assert( ee->hasTerm( subs[n] ) );
- Assert( ee->getRepresentative( subs[n] )==subs[n] );
+ Assert( qy->getEngine()->hasTerm( subs[n] ) );
+ Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] );
return subs[n];
}else{
- return evaluateTerm2( subs[n], subs, subsRep, hasSubs );
+ return evaluateTerm2( subs[n], subs, subsRep, hasSubs, qy );
}
}
}else{
@@ -307,11 +306,11 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
if( !f.isNull() ){
std::vector< TNode > args;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs );
+ TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, qy );
if( c.isNull() ){
return TNode::null();
}
- c = ee->getRepresentative( c );
+ c = qy->getEngine()->getRepresentative( c );
Trace("term-db-eval") << "Got child : " << c << std::endl;
args.push_back( c );
}
@@ -325,53 +324,59 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
return TNode::null();
}
-Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms ) {
+Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms, EqualityQuery * qy ) {
+ if( qy==NULL ){
+ qy = d_quantEngine->getEqualityQuery();
+ }
if( mkNewTerms ){
std::map< TNode, Node > visited;
- return evaluateTerm2( n, subs, subsRep, true, visited );
+ return evaluateTerm2( n, subs, subsRep, true, visited, qy );
}else{
- return evaluateTerm2( n, subs, subsRep, true );
+ return evaluateTerm2( n, subs, subsRep, true, qy );
}
}
-Node TermDb::evaluateTerm( TNode n, bool mkNewTerms ) {
+Node TermDb::evaluateTerm( TNode n, bool mkNewTerms, EqualityQuery * qy ) {
+ if( qy==NULL ){
+ qy = d_quantEngine->getEqualityQuery();
+ }
std::map< TNode, TNode > subs;
if( mkNewTerms ){
std::map< TNode, Node > visited;
- return evaluateTerm2( n, subs, false, false, visited );
+ return evaluateTerm2( n, subs, false, false, visited, qy );
}else{
- return evaluateTerm2( n, subs, false, false );
+ return evaluateTerm2( n, subs, false, false, qy );
}
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol ) {
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
+ Assert( !qy->extendsEngine() );
Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
Assert( n.getType().isBoolean() );
if( n.getKind()==EQUAL ){
- TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs );
+ TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs, qy );
if( !n1.isNull() ){
- TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs );
+ TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs, qy );
if( !n2.isNull() ){
if( n1==n2 ){
return pol;
}else{
- eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
- Assert( ee->hasTerm( n1 ) );
- Assert( ee->hasTerm( n2 ) );
+ Assert( qy->getEngine()->hasTerm( n1 ) );
+ Assert( qy->getEngine()->hasTerm( n2 ) );
if( pol ){
- return ee->areEqual( n1, n2 );
+ return qy->getEngine()->areEqual( n1, n2 );
}else{
- return ee->areDisequal( n1, n2, false );
+ return qy->getEngine()->areDisequal( n1, n2, false );
}
}
}
}
}else if( n.getKind()==NOT ){
- return isEntailed( n[0], subs, subsRep, hasSubs, !pol );
+ return isEntailed( n[0], subs, subsRep, hasSubs, !pol, qy );
}else if( n.getKind()==OR || n.getKind()==AND ){
bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( isEntailed( n[i], subs, subsRep, hasSubs, pol ) ){
+ if( isEntailed( n[i], subs, subsRep, hasSubs, pol, qy ) ){
if( simPol ){
return true;
}
@@ -384,31 +389,34 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
return !simPol;
}else if( n.getKind()==IFF || n.getKind()==ITE ){
for( unsigned i=0; i<2; i++ ){
- if( isEntailed( n[0], subs, subsRep, hasSubs, i==0 ) ){
+ if( isEntailed( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
- return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol );
+ return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol, qy );
}
}
}else if( n.getKind()==APPLY_UF ){
- TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs );
+ TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs, qy );
if( !n1.isNull() ){
+ Assert( qy->hasTerm( n1 ) );
if( n1==d_true ){
return pol;
}else if( n1==d_false ){
return !pol;
}else{
- eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
- return ee->getRepresentative( n1 ) == ( pol ? d_true : d_false );
+ return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
}
}
}
return false;
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+ if( qy==NULL ){
+ qy = d_quantEngine->getEqualityQuery();
+ }
if( d_consistent_ee ){
- return isEntailed( n, subs, subsRep, true, pol );
+ return isEntailed( n, subs, subsRep, true, pol, qy );
}else{
//don't check entailment wrt an inconsistent ee
return false;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 4cba619a8..9177d3a1a 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -20,6 +20,7 @@
#include "expr/attribute.h"
#include "theory/theory.h"
#include "theory/type_enumerator.h"
+#include "theory/quantifiers/quant_util.h"
#include <map>
@@ -182,9 +183,9 @@ private:
/** set has term */
void setHasTerm( Node n );
/** evaluate term */
- TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs );
- Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited );
- bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol );
+ TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+ Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy );
+ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
public:
TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
~TermDb(){}
@@ -237,11 +238,11 @@ public:
/** evaluate a term under a substitution. Return representative in EE if possible.
* subsRep is whether subs contains only representatives
*/
- Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false );
+ Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false, EqualityQuery * qy = NULL );
/** same as above, but without substitution */
- Node evaluateTerm( TNode n, bool mkNewTerms = false );
+ Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL );
/** is entailed (incomplete check) */
- bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
+ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
/** has term */
bool hasTermCurrent( Node n, bool useMode = true );
/** is term eligble for instantiation? */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index b4e00386a..38635b37b 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -30,6 +30,18 @@ namespace CVC4 {
namespace theory {
namespace inst {
+void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
+ if( d_fv.empty() ){
+ quantifiers::TermDb::getVarContainsNode( q, n, d_fv );
+ }
+ if( d_reqPol==0 ){
+ d_reqPol = reqPol;
+ d_reqPolEq = reqPolEq;
+ }else{
+ //determined a ground (dis)equality must hold or else q is a tautology?
+ }
+}
+
/** trigger class constructor */
Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption )
: d_quantEngine( qe ), d_f( f )
@@ -122,7 +134,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
std::map< Node, std::vector< Node > > patterns;
size_t varCount = 0;
std::map< Node, std::vector< Node > > varContains;
- qe->getTermDatabase()->getVarContains( f, temp, varContains );
+ quantifiers::TermDb::getVarContains( f, temp, varContains );
for( unsigned i=0; i<temp.size(); i++ ){
bool foundVar = false;
for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
@@ -213,7 +225,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt
bool Trigger::isUsable( Node n, Node q ){
if( quantifiers::TermDb::getInstConstAttr(n)==q ){
if( isAtomicTrigger( n ) ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( !isUsable( n[i], q ) ){
return false;
}
@@ -238,68 +250,91 @@ bool Trigger::isUsable( Node n, Node q ){
}
}
-Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
- Trace("trigger-debug") << "Is " << n << " a usable trigger? pol/hasPol=" << pol << "/" << hasPol << std::endl;
+Node Trigger::getIsUsableEq( Node q, Node n ) {
+ Assert( isRelationalTrigger( n ) );
+ for( unsigned i=0; i<2; i++) {
+ if( isUsableEqTerms( q, n[i], n[1-i] ) ){
+ if( i==1 && ( n.getKind()==EQUAL || n.getKind()==IFF ) && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
+ return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
+ }else{
+ return n;
+ }
+ }
+ }
+ return Node::null();
+}
+
+bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
+ if( n1.getKind()==INST_CONSTANT ){
+ if( options::relationalTriggers() ){
+ if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
+ return true;
+ }else if( n2.getKind()==INST_CONSTANT ){
+ return true;
+ }
+ }
+ }else if( isAtomicTrigger( n1 ) && isUsable( n1, q ) ){
+ if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){
+ return true;
+ }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
+ return true;
+ }
+ }
+ return false;
+}
+
+Node Trigger::getIsUsableTrigger( Node n, Node q ) {
+ bool pol = true;
+ Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
if( n.getKind()==NOT ){
pol = !pol;
n = n[0];
}
- if( options::relationalTriggers() ){
- if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
- Node rtr;
- bool do_negate = hasPol && pol;
- bool is_arith = n[0].getType().isReal();
- for( unsigned i=0; i<2; i++) {
- if( n[1-i].getKind()==INST_CONSTANT ){
- if( ( ( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ) || !quantifiers::TermDb::hasInstConstAttr(n[i]) ) &&
- ( !do_negate || is_arith ) ){
- rtr = n;
- break;
- }
- if( n[i].getKind()==INST_CONSTANT && ( !hasPol || pol ) ){
- do_negate = true;
- rtr = n;
- break;
+ if( n.getKind()==INST_CONSTANT ){
+ return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+ }else if( isRelationalTrigger( n ) ){
+ Node rtr = getIsUsableEq( q, n );
+ if( rtr.isNull() && n[0].getType().isReal() ){
+ //try to solve relation
+ std::map< Node, Node > m;
+ if( QuantArith::getMonomialSumLit(n, m) ){
+ for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
+ bool trySolve = false;
+ if( !it->first.isNull() ){
+ if( it->first.getKind()==INST_CONSTANT ){
+ trySolve = options::relationalTriggers();
+ }else if( isUsableTrigger( it->first, q ) ){
+ trySolve = true;
+ }
}
- }
- }
- if( is_arith ){
- //try to rearrange?
- std::map< Node, Node > m;
- if( QuantArith::getMonomialSumLit(n, m) ){
- for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
- if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
- Node veq;
- if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
- int vti = veq[0]==it->first ? 1 : 0;
- if( ( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ) || !quantifiers::TermDb::hasInstConstAttr(veq[vti]) ){
- rtr = veq;
- }
- }
+ if( trySolve ){
+ Trace("trigger-debug") << "Try to solve for " << it->first << std::endl;
+ Node veq;
+ if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
+ rtr = getIsUsableEq( q, veq );
}
+ //either all solves will succeed or all solves will fail
+ break;
}
}
}
- if( !rtr.isNull() ){
- Trace("relational-trigger") << "Relational trigger : " << std::endl;
- Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl;
- Trace("relational-trigger") << " in quantifier " << f << std::endl;
- if( hasPol ){
- Trace("relational-trigger") << " polarity : " << pol << std::endl;
- }
- Node rtr2 = do_negate ? rtr.negate() : rtr;
- Trace("relational-trigger") << " return : " << rtr2 << std::endl;
- return rtr2;
- }
}
- }
- bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
- Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl;
- if( usable ){
- return n;
+ if( !rtr.isNull() ){
+ Trace("relational-trigger") << "Relational trigger : " << std::endl;
+ Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl;
+ Trace("relational-trigger") << " in quantifier " << q << std::endl;
+ Node rtr2 = pol ? rtr : rtr.negate();
+ Trace("relational-trigger") << " return : " << rtr2 << std::endl;
+ return rtr2;
+ }
}else{
- return Node::null();
+ bool usable = quantifiers::TermDb::getInstConstAttr(n)==q && isAtomicTrigger( n ) && isUsable( n, q );
+ Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==q) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
+ if( usable ){
+ return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+ }
}
+ return Node::null();
}
bool Trigger::isUsableTrigger( Node n, Node q ){
@@ -319,6 +354,14 @@ bool Trigger::isAtomicTriggerKind( Kind k ) {
k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON;
}
+bool Trigger::isRelationalTrigger( Node n ) {
+ return isRelationalTriggerKind( n.getKind() );
+}
+
+bool Trigger::isRelationalTriggerKind( Kind k ) {
+ return k==EQUAL || k==IFF || k==GEQ;
+}
+
bool Trigger::isCbqiKind( Kind k ) {
return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ||
k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER;
@@ -347,40 +390,63 @@ bool Trigger::isSimpleTrigger( Node n ){
}
//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, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv,
- quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude,
- std::map< Node, int >& reqPol, std::vector< Node >& added,
+bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo,
+ quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 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 ] = 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( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
bool rec = true;
Node nu;
bool nu_single = false;
if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
- nu = getIsUsableTrigger( n, f, pol, hasPol );
+ nu = getIsUsableTrigger( n, q );
if( !nu.isNull() ){
- reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0;
- visited[ nu ] = nu;
- quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] );
- nu_single = visited_fv[nu].size()==f[0].getNumChildren();
- retVal = true;
- if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
- rec = false;
+ Assert( nu.getKind()!=NOT );
+ Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
+ Node reqEq;
+ if( nu.getKind()==IFF || nu.getKind()==EQUAL ){
+ if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
+ if( hasPol ){
+ reqEq = nu[1];
+ }
+ nu = nu[0];
+ }
+ }
+ Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
+ Assert( isUsableTrigger( nu, q ) );
+ //do not add if already excluded
+ bool add = true;
+ if( n!=nu ){
+ std::map< Node, Node >::iterator itvu = visited.find( nu );
+ if( itvu!=visited.end() && itvu->second.isNull() ){
+ add = false;
+ }
+ }
+ if( add ){
+ Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
+ visited[ nu ] = nu;
+ tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
+ nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
+ retVal = true;
+ if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
+ rec = false;
+ }
}
}
}
if( rec ){
+ Node nrec = nu.isNull() ? n : nu;
std::vector< Node > added2;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ for( unsigned i=0; i<nrec.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, visited_fv, tstrt, exclude, reqPol, added2, newPol, newHasPol, newEPol, newHasEPol ) ){
+ QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
+ QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
+ if( collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ) ){
retVal = true;
}
}
@@ -388,15 +454,19 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited,
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;
+ Assert( tinfo.find( added2[i] )!=tinfo.end() );
+ if( added2[i]!=nu ){
+ if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
+ rm_nu = true;
+ }
+ added.push_back( added2[i] );
+ }else{
+ Assert( false );
}
- added.push_back( added2[i] );
}
if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
visited[nu] = Node::null();
- reqPol.erase( nu );
+ tinfo.erase( nu );
}else{
added.push_back( nu );
}
@@ -448,7 +518,7 @@ int Trigger::getTriggerWeight( Node n ) {
return 0;
}else{
if( options::relationalTriggers() ){
- if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
+ if( isRelationalTrigger( n ) ){
for( unsigned i=0; i<2; i++ ){
if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){
return 0;
@@ -492,17 +562,17 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
return true;
}
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude,
- std::map< Node, int >& reqPol, bool filterInst ){
+void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude,
+ std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
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;
- std::map< Node, int > reqPol2;
- collectPatTerms( qe, f, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol2, false );
+ std::map< Node, TriggerTermInfo > tinfo2;
+ collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
std::vector< Node > temp;
temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
- qe->getTermDatabase()->filterInstances( temp );
+ quantifiers::TermDb::filterInstances( temp );
if( temp.size()!=patTerms2.size() ){
Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
Trace("trigger-filter-instance") << "Old: ";
@@ -517,7 +587,10 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
}
if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
for( unsigned i=0; i<temp.size(); i++ ){
- reqPol[temp[i]] = reqPol2[temp[i]];
+ //copy information
+ tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
+ tinfo[temp[i]].d_reqPol = tinfo2[temp[i]].d_reqPol;
+ tinfo[temp[i]].d_reqPolEq = tinfo2[temp[i]].d_reqPolEq;
patTerms.push_back( temp[i] );
}
return;
@@ -530,10 +603,9 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
}
}
}
- 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 ){
+ collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
+ for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
if( !visited[it->first].isNull() ){
patTerms.push_back( it->first );
}
@@ -615,15 +687,15 @@ Node Trigger::getInversion( Node n, Node x ) {
return Node::null();
}
-void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) {
+void Trigger::getTriggerVariables( Node icn, Node q, std::vector< Node >& t_vars ) {
std::vector< Node > patTerms;
- std::map< Node, int > reqPol;
+ std::map< Node, TriggerTermInfo > tinfo;
//collect all patterns from icn
std::vector< Node > exclude;
- collectPatTerms( qe, f, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol );
+ collectPatTerms( q, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo );
//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 );
+ quantifiers::TermDb::getVarContainsNode( q, patTerms[i], t_vars );
}
}
@@ -655,7 +727,7 @@ InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
if( nodes.empty() ){
- return d_tr;
+ return d_tr.empty() ? NULL : d_tr[0];
}else{
Node n = nodes.back();
nodes.pop_back();
@@ -669,13 +741,7 @@ Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
if( nodes.empty() ){
- if(d_tr != NULL){
- // TODO: Andy can you look at fmf/QEpres-uf.855035.smt?
- delete d_tr;
- d_tr = NULL;
- }
- Assert(d_tr == NULL);
- d_tr = t;
+ d_tr.push_back( t );
}else{
Node n = nodes.back();
nodes.pop_back();
@@ -688,7 +754,6 @@ void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
TriggerTrie::TriggerTrie()
- : d_tr( NULL )
{}
TriggerTrie::~TriggerTrie() {
@@ -699,7 +764,9 @@ TriggerTrie::~TriggerTrie() {
}
d_children.clear();
- if(d_tr != NULL) { delete d_tr; }
+ for( unsigned i=0; i<d_tr.size(); i++ ){
+ delete d_tr[i];
+ }
}
}/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 06e9011c7..41f2a1c38 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -42,6 +42,16 @@ namespace CVC4 {
namespace theory {
namespace inst {
+class TriggerTermInfo {
+public:
+ TriggerTermInfo() : d_reqPol(0){}
+ ~TriggerTermInfo(){}
+ std::vector< Node > d_fv;
+ int d_reqPol;
+ Node d_reqPolEq;
+ void init( Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null() );
+};
+
/** A collect of nodes representing a trigger. */
class Trigger {
public:
@@ -91,14 +101,16 @@ class Trigger {
static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
int matchOption = 0, bool keepAll = true,
int trOption = TR_MAKE_NEW );
- static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n,
- std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
- std::vector< Node >& exclude, std::map< Node, int >& reqPol,
+ static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
+ std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo,
bool filterInst = false );
/** is usable trigger */
static bool isUsableTrigger( Node n, Node q );
+ static Node getIsUsableTrigger( Node n, Node q );
static bool isAtomicTrigger( Node n );
static bool isAtomicTriggerKind( Kind k );
+ static bool isRelationalTrigger( Node n );
+ static bool isRelationalTriggerKind( Kind k );
static bool isCbqiKind( Kind k );
static bool isSimpleTrigger( Node n );
static bool isBooleanTermTrigger( Node n );
@@ -111,8 +123,7 @@ class Trigger {
static Node getInversionVariable( Node n );
static Node getInversion( Node n, Node x );
/** get all variables that E-matching can possibly handle */
- static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f,
- std::vector< Node >& t_vars );
+ static void getTriggerVariables( Node icn, Node f, std::vector< Node >& t_vars );
void debugPrint( const char * c ) {
Trace(c) << "TRIGGER( ";
@@ -122,19 +133,17 @@ class Trigger {
}
Trace(c) << " )";
}
-
private:
/** trigger constructor */
Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 );
/** is subterm of trigger usable */
static bool isUsable( Node n, Node q );
- static Node getIsUsableTrigger( Node n, Node f, bool pol = true,
- bool hasPol = false );
+ static Node getIsUsableEq( Node q, Node eq );
+ static bool isUsableEqTerms( Node q, Node n1, Node n2 );
/** collect all APPLY_UF pattern terms for f in n */
- static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv,
- quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude,
- std::map< Node, int >& reqPol, std::vector< Node >& added,
+ static bool collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo,
+ quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
bool pol, bool hasPol, bool epol, bool hasEPol );
std::vector< Node > d_nodes;
@@ -169,7 +178,7 @@ private:
inst::Trigger* getTrigger2( std::vector< Node >& nodes );
void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
- inst::Trigger* d_tr;
+ std::vector< inst::Trigger* > d_tr;
std::map< TNode, TriggerTrie* > d_children;
};/* class inst::Trigger::TriggerTrie */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1a2762409..d31865f35 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -142,6 +142,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
d_rel_dom = NULL;
d_builder = NULL;
+ d_curr_effort_level = QEFFORT_NONE;
d_total_inst_count_debug = 0;
//allow theory combination to go first, once initially
d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
@@ -463,6 +464,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){
+ d_curr_effort_level = quant_e;
bool success = true;
//build the model if any module requested it
if( needsModelE==quant_e ){
@@ -522,6 +524,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
}
}
+ d_curr_effort_level = QEFFORT_NONE;
Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
if( d_hasAddedLemma ){
//debug information
@@ -756,67 +759,6 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
}
}
-bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
- Assert( f.getKind()==FORALL );
- Assert( vars.size()==terms.size() );
- Node body = getInstantiation( f, vars, terms, doVts ); //do virtual term substitution
- body = quantifiers::QuantifiersRewriter::preprocess( body, true );
- Trace("inst-debug") << "...preprocess to " << body << std::endl;
- Trace("inst-assert") << "(assert " << body << ")" << std::endl;
- //make the lemma
- Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body );
- //check for duplication
- if( addLemma( lem ) ){
- d_total_inst_debug[f]++;
- d_temp_inst_debug[f]++;
- d_total_inst_count_debug++;
- Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
- for( unsigned i=0; i<terms.size(); i++ ){
- if( Trace.isOn("inst") ){
- Trace("inst") << " " << terms[i];
- if( Trace.isOn("inst-debug") ){
- Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << f[0][i].getType();
- }
- Trace("inst") << std::endl;
- }
- if( options::cbqi() ){
- Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
- bool bad_inst = false;
- if( !icf.isNull() ){
- if( icf==f ){
- bad_inst = true;
- }else{
- bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[f] );
- }
- }
- if( bad_inst ){
- Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
- for( unsigned i=0; i<terms.size(); i++ ){
- Trace("inst") << " " << terms[i] << std::endl;
- }
- Unreachable("Bad instantiation");
- }
- }
- Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
- }
- if( options::instMaxLevel()!=-1 ){
- uint64_t maxInstLevel = 0;
- for( unsigned i=0; i<terms.size(); i++ ){
- if( terms[i].hasAttribute(InstLevelAttribute()) ){
- if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
- maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
- }
- }
- }
- setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
- }
- ++(d_statistics.d_instantiations);
- return true;
- }else{
- ++(d_statistics.d_inst_duplicate);
- return false;
- }
-}
bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) {
if( options::incrementalSolving() ){
@@ -847,7 +789,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t lev
Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
}
Assert( n.getNumChildren()==qn.getNumChildren() );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
setInstantiationLevelAttr( n[i], qn[i], level );
}
}
@@ -859,7 +801,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
n.setAttribute(ila,level);
Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
}
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
setInstantiationLevelAttr( n[i], level );
}
}
@@ -970,9 +912,11 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
}
*/
-bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
+bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
if( doCache ){
- lem = Rewriter::rewrite(lem);
+ if( doRewrite ){
+ lem = Rewriter::rewrite(lem);
+ }
Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
//d_curr_out->lemma( lem, false, true );
@@ -985,6 +929,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
return false;
}
}else{
+ //do not need to rewrite, will be rewritten after sending
d_lemmas_waiting.push_back( lem );
return true;
}
@@ -1012,7 +957,6 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
if( terms[i].isNull() ){
terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() );
}
- //make it representative, this is helpful for recognizing duplication
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
@@ -1026,7 +970,29 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
return false;
}
#ifdef CVC4_ASSERTIONS
- Assert( !quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) );
+ bool bad_inst = false;
+ if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
+ bad_inst = true;
+ }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
+ bad_inst = true;
+ }else if( options::cbqi() ){
+ Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
+ if( !icf.isNull() ){
+ if( icf==q ){
+ bad_inst = true;
+ }else{
+ bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] );
+ }
+ }
+ }
+ //this assertion is critical to soundness
+ if( bad_inst ){
+ Trace("inst")<< "***& Bad Instantiate " << q << " with " << std::endl;
+ for( unsigned j=0; j<terms.size(); j++ ){
+ Trace("inst") << " " << terms[j] << std::endl;
+ }
+ Assert( false );
+ }
#endif
}
@@ -1038,7 +1004,8 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
}
}
}
- //check for entailment
+
+ //check for positive entailment
if( options::instNoEntail() ){
std::map< TNode, TNode > subs;
for( unsigned i=0; i<terms.size(); i++ ){
@@ -1053,7 +1020,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
//Trace("ajr-temp") << " " << eval << std::endl;
}
- //check for duplication
+ //check for term vector duplication
bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst );
if( alreadyExists ){
Trace("inst-add-debug") << " -> Already exists." << std::endl;
@@ -1061,16 +1028,57 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
return false;
}
-
- //add the instantiation
+ //construct the instantiation
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
- bool addedInst = addInstantiationInternal( q, d_term_db->d_vars[q], terms, doVts );
- //report the result
- if( addedInst ){
+ Assert( d_term_db->d_vars[q].size()==terms.size() );
+ Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution
+ body = quantifiers::QuantifiersRewriter::preprocess( body, true );
+ Trace("inst-debug") << "...preprocess to " << body << std::endl;
+
+ //construct the lemma
+ Trace("inst-assert") << "(assert " << body << ")" << std::endl;
+ body = Rewriter::rewrite(body);
+ Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
+ lem = Rewriter::rewrite(lem);
+
+ //check for lemma duplication
+ if( addLemma( lem, true, false ) ){
+ d_total_inst_debug[q]++;
+ d_temp_inst_debug[q]++;
+ d_total_inst_count_debug++;
+ if( Trace.isOn("inst") ){
+ Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
+ for( unsigned i=0; i<terms.size(); i++ ){
+ if( Trace.isOn("inst") ){
+ Trace("inst") << " " << terms[i];
+ if( Trace.isOn("inst-debug") ){
+ Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << q[0][i].getType();
+ }
+ Trace("inst") << std::endl;
+ }
+ }
+ }
+ if( options::instMaxLevel()!=-1 ){
+ uint64_t maxInstLevel = 0;
+ for( unsigned i=0; i<terms.size(); i++ ){
+ if( terms[i].hasAttribute(InstLevelAttribute()) ){
+ if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+ maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+ }
+ }
+ }
+ setInstantiationLevelAttr( body, q[1], maxInstLevel+1 );
+ }
+ //notify listeners
+ for( unsigned j=0; j<d_inst_notify.size(); j++ ){
+ d_inst_notify[j]->notifyInstantiation( q, lem, terms, body );
+ }
Trace("inst-add-debug") << " -> Success." << std::endl;
+ ++(d_statistics.d_instantiations);
return true;
}else{
Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
+ ++(d_statistics.d_inst_duplicate);
return false;
}
}
@@ -1380,13 +1388,17 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
}
bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areDisequal( a, b, false ) ){
- return true;
+ if( a==b ){
+ return false;
+ }else{
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ if( ee->areDisequal( a, b, false ) ){
+ return true;
+ }
}
+ return false;
}
- return false;
}
Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 641c7624e..cdf7c3b89 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -81,6 +81,12 @@ public:
quantifiers::TermDb * getTermDatabase();
};/* class QuantifiersModule */
+class InstantiationNotify {
+public:
+ InstantiationNotify(){}
+ virtual void notifyInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+};
+
namespace quantifiers {
class FirstOrderModel;
//modules
@@ -128,6 +134,8 @@ private:
TheoryEngine* d_te;
/** vector of modules for quantifiers */
std::vector< QuantifiersModule* > d_modules;
+ /** instantiation notify */
+ std::vector< InstantiationNotify* > d_inst_notify;
/** equality query class */
EqualityQueryQuantifiersEngine* d_eq_query;
/** for computing relevance of quantifiers */
@@ -176,6 +184,8 @@ public: //effort levels
QEFFORT_NONE,
};
private:
+ /** current effort level */
+ unsigned d_curr_effort_level;
/** list of all quantifiers seen */
std::map< Node, bool > d_quants;
/** quantifiers reduced */
@@ -303,8 +313,6 @@ private:
bool reduceQuantifier( Node q );
/** compute term vector */
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
- /** instantiate f with arguments terms */
- bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
/** record instantiation, return true if it was non-duplicate */
bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false );
/** set instantiation level attr */
@@ -321,7 +329,7 @@ public:
/** do substitution */
Node getSubstitute( Node n, std::vector< Node >& terms );
/** add lemma lem */
- bool addLemma( Node lem, bool doCache = true );
+ bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
/** add require phase */
void addRequirePhase( Node lit, bool req );
/** do instantiation specified by m */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index f0c9b5a33..784eaf677 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -76,7 +76,8 @@ TESTS = \
subtype-param.smt2 \
anti-sk-simp.smt2 \
pure_dt_cbqi.smt2 \
- florian-case-ax.smt2
+ florian-case-ax.smt2 \
+ double-pattern.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/double-pattern.smt2 b/test/regress/regress0/quantifiers/double-pattern.smt2
new file mode 100644
index 000000000..4ce21d446
--- /dev/null
+++ b/test/regress/regress0/quantifiers/double-pattern.smt2
@@ -0,0 +1,6 @@
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (! (! (P x) :pattern ((P x))) :pattern ((P x)))))
+(assert (not (P 0)))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback