summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r--src/theory/quantifiers_engine.cpp107
1 files changed, 78 insertions, 29 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6d3b17254..d81efe1da 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -57,6 +57,7 @@ using namespace CVC4::theory::inst;
QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
d_te( te ),
+ d_conflict_c(c, false),
//d_quants(u),
d_quants_red(u),
d_lemmas_produced_c(u),
@@ -88,7 +89,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
d_tr_trie = new inst::TriggerTrie;
d_curr_effort_level = QEFFORT_NONE;
d_conflict = false;
- d_num_added_lemmas_round = 0;
d_hasAddedLemma = false;
//don't add true lemma
d_lemmas_produced_c[d_term_db->d_true] = true;
@@ -352,7 +352,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
std::vector< QuantifiersModule* > qm;
if( d_model->checkNeeded() ){
needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
- for( int i=0; i<(int)d_modules.size(); i++ ){
+ for( unsigned i=0; i<d_modules.size(); i++ ){
if( d_modules[i]->needsCheck( e ) ){
qm.push_back( d_modules[i] );
needsCheck = true;
@@ -366,7 +366,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
d_conflict = false;
- d_num_added_lemmas_round = 0;
d_hasAddedLemma = false;
bool setIncomplete = false;
if( e==Theory::EFFORT_LAST_CALL ){
@@ -380,6 +379,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
if( needsCheck ){
+ //this will fail if a set of instances is marked as a conflict, but is not
+ Assert( !d_conflict_c.get() );
//flush previous lemmas (for instance, if was interupted), or other lemmas to process
flushLemmas();
if( d_hasAddedLemma ){
@@ -393,6 +394,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
d_recorded_inst.clear();
}
+
+ double clSet = 0;
+ if( Trace.isOn("quant-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
+ }
if( Trace.isOn("quant-engine-debug") ){
Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -453,7 +460,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
flushLemmas();
if( d_hasAddedLemma ){
return;
-
}
if( e==Theory::EFFORT_LAST_CALL ){
@@ -545,6 +551,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
}
}
+ if( Trace.isOn("quant-engine") ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
+ Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
+ Trace("quant-engine") << std::endl;
+ }
+
Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
}else{
Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
@@ -564,7 +577,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
}
if( setIncomplete ){
- Trace("quant-engine-debug") << "Set incomplete flag." << std::endl;
+ Trace("quant-engine") << "Set incomplete flag." << std::endl;
getOutputChannel().setIncomplete();
}
//output debug stats
@@ -621,6 +634,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
//check whether we should apply a reduction
if( reduceQuantifier( f ) ){
+ Trace("quant") << "...reduced." << std::endl;
d_quants[f] = false;
return false;
}else{
@@ -628,6 +642,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
d_term_db->makeInstantiationConstantsFor( f );
d_term_db->computeAttributes( f );
for( unsigned i=0; i<d_modules.size(); i++ ){
+ Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
d_modules[i]->preRegisterQuantifier( f );
}
QuantifiersModule * qm = getOwner( f );
@@ -640,11 +655,11 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
}
//register with each module
for( unsigned i=0; i<d_modules.size(); i++ ){
+ Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
d_modules[i]->registerQuantifier( f );
}
+ //TODO: remove this
Node ceBody = d_term_db->getInstConstantBody( f );
- //generate the phase requirements
- //d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
//also register it with the strong solver
//if( options::finiteModelFind() ){
// ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
@@ -874,8 +889,9 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
Node body;
+ Assert( vars.size()==terms.size() );
//process partial instantiation if necessary
- if( d_term_db->d_vars[q].size()!=vars.size() ){
+ if( q[0].getNumChildren()!=vars.size() ){
body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
std::vector< Node > uninst_vars;
//doing a partial instantiation, must add quantifier for all uninstantiated variables
@@ -884,6 +900,8 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std
uninst_vars.push_back( q[0][i] );
}
}
+ Trace("partial-inst") << "Partially instantiating with " << vars.size() << " / " << q[0].getNumChildren() << " for " << q << std::endl;
+ Assert( !uninst_vars.empty() );
Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
Trace("partial-inst") << "Partial instantiation : " << q << std::endl;
@@ -922,6 +940,7 @@ Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
}
Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
+ Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() );
return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
}
@@ -956,7 +975,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
d_lemmas_produced_c[ lem ] = true;
d_lemmas_waiting.push_back( lem );
Trace("inst-add-debug") << "Added lemma" << std::endl;
- d_num_added_lemmas_round++;
return true;
}else{
Trace("inst-add-debug") << "Duplicate." << std::endl;
@@ -965,7 +983,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
}else{
//do not need to rewrite, will be rewritten after sending
d_lemmas_waiting.push_back( lem );
- d_num_added_lemmas_round++;
return true;
}
}
@@ -997,6 +1014,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
Assert( !d_conflict );
Assert( terms.size()==q[0].getNumChildren() );
Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
+ std::vector< Node > rlv_cond;
for( unsigned i=0; i<terms.size(); i++ ){
Trace("inst-add-debug") << " " << q[0][i];
Trace("inst-add-debug2") << " -> " << terms[i];
@@ -1014,20 +1032,29 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
if( terms[i].isNull() ){
Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl;
return false;
+ }else{
+ //get relevancy conditions
+ if( options::instRelevantCond() ){
+ quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond );
+ }
}
#ifdef CVC4_ASSERTIONS
bool bad_inst = false;
if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
+ Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
bad_inst = true;
}else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
+ Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
bad_inst = true;
}else if( options::cbqi() ){
Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
if( !icf.isNull() ){
if( icf==q ){
+ Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
+ bad_inst = true;
+ }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){
+ Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
bad_inst = true;
- }else{
- bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] );
}
}
}
@@ -1079,13 +1106,21 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
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
+ Node orig_body = body;
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 );
+ Node lem;
+ if( rlv_cond.empty() ){
+ lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
+ }else{
+ rlv_cond.push_back( q.negate() );
+ rlv_cond.push_back( body );
+ lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond );
+ }
lem = Rewriter::rewrite(lem);
//check for lemma duplication
@@ -1106,15 +1141,20 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
}
}
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());
+ if( doVts ){
+ //virtual term substitution/instantiation level features are incompatible
+ Assert( false );
+ }else{
+ 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( orig_body, q[1], maxInstLevel+1 );
}
- setInstantiationLevelAttr( body, q[1], maxInstLevel+1 );
}
if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){
//notify listeners
@@ -1122,6 +1162,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
Trace("inst-add-debug") << "...we are in conflict." << std::endl;
d_conflict = true;
+ d_conflict_c = true;
Assert( !d_lemmas_waiting.empty() );
break;
}
@@ -1205,9 +1246,19 @@ quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
void QuantifiersEngine::flushLemmas(){
if( !d_lemmas_waiting.empty() ){
+ //filter based on notify classes
+ if( !d_inst_notify.empty() ){
+ unsigned prev_lem_sz = d_lemmas_waiting.size();
+ for( unsigned j=0; j<d_inst_notify.size(); j++ ){
+ d_inst_notify[j]->filterInstantiations();
+ }
+ if( prev_lem_sz!=d_lemmas_waiting.size() ){
+ Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
+ }
+ }
//take default output channel if none is provided
d_hasAddedLemma = true;
- for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
+ for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
}
@@ -1403,7 +1454,7 @@ bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl;
Assert( ee->hasTerm( eq[0] ) );
Assert( ee->hasTerm( eq[1] ) );
- if( ee->areDisequal( eq[0], eq[1], false ) ){
+ if( areDisequal( eq[0], eq[1] ) ){
Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
if( Trace.isOn("term-db-lemma") ){
Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
@@ -1445,11 +1496,10 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
}else{
eq::EqualityEngine* ee = getEngine();
if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areEqual( a, b ) ){
- return true;
- }
+ return ee->areEqual( a, b );
+ }else{
+ return false;
}
- return false;
}
}
@@ -1459,11 +1509,10 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
}else{
eq::EqualityEngine* ee = getEngine();
if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areDisequal( a, b, false ) ){
- return true;
- }
+ return ee->areDisequal( a, b, false );
+ }else{
+ return a.isConst() && b.isConst();
}
- return false;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback