summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/instantiation_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp156
1 files changed, 75 insertions, 81 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index c1476acb8..fae54c151 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -18,6 +18,8 @@
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
using namespace std;
using namespace CVC4;
@@ -26,15 +28,9 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-//#define IE_PRINT_PROCESS_TIMES
+InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
+QuantifiersModule( qe ), d_setIncomplete( setIncomplete ){
-InstantiationEngine::InstantiationEngine( TheoryQuantifiers* th ) :
-d_th( th ){
-
-}
-
-QuantifiersEngine* InstantiationEngine::getQuantifiersEngine(){
- return d_th->getQuantifiersEngine();
}
bool InstantiationEngine::hasAddedCbqiLemma( Node f ) {
@@ -46,25 +42,25 @@ void InstantiationEngine::addCbqiLemma( Node f ){
//code for counterexample-based quantifier instantiation
Debug("cbqi") << "Do cbqi for " << f << std::endl;
//make the counterexample body
- //Node ceBody = f[1].substitute( getQuantifiersEngine()->d_vars[f].begin(), getQuantifiersEngine()->d_vars[f].end(),
- // getQuantifiersEngine()->d_inst_constants[f].begin(),
- // getQuantifiersEngine()->d_inst_constants[f].end() );
+ //Node ceBody = f[1].substitute( d_quantEngine->d_vars[f].begin(), d_quantEngine->d_vars[f].end(),
+ // d_quantEngine->d_inst_constants[f].begin(),
+ // d_quantEngine->d_inst_constants[f].end() );
//get the counterexample literal
- Node ceBody = getQuantifiersEngine()->getCounterexampleBody( f );
- Node ceLit = d_th->getValuation().ensureLiteral( ceBody.notNode() );
+ Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
+ Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
d_ce_lit[ f ] = ceLit;
- getQuantifiersEngine()->setInstantiationConstantAttr( ceLit, f );
+ d_quantEngine->getTermDatabase()->setInstantiationConstantAttr( ceLit, f );
// set attributes, mark all literals in the body of n as dependent on cel
//registerLiterals( ceLit, f );
//require any decision on cel to be phase=true
- d_th->getOutputChannel().requirePhase( ceLit, true );
+ d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
//add counterexample lemma
NodeBuilder<> nb(kind::OR);
nb << f << ceLit;
Node lem = nb;
Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
- d_th->getOutputChannel().lemma( lem );
+ d_quantEngine->getOutputChannel().lemma( lem );
}
bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
@@ -72,8 +68,8 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
if( Options::current()->cbqi ){
//check if any cbqi lemma has not been added yet
bool addedLemma = false;
- for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
- Node f = getQuantifiersEngine()->getAssertedQuantifier( i );
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
//add cbqi lemma
addCbqiLemma( f );
@@ -87,14 +83,9 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
//if not, proceed to instantiation round
Debug("inst-engine") << "IE: Instantiation Round." << std::endl;
Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl;
- //reset instantiators
+ //reset the quantifiers engine
Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
- for( int i=0; i<theory::THEORY_LAST; i++ ){
- if( getQuantifiersEngine()->getInstantiator( i ) ){
- getQuantifiersEngine()->getInstantiator( i )->resetInstantiationRound( effort );
- }
- }
- getQuantifiersEngine()->getTermDatabase()->reset( effort );
+ d_quantEngine->resetInstantiationRound( effort );
//iterate over an internal effort level e
int e = 0;
int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
@@ -104,20 +95,19 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
d_inst_round_status = InstStrategy::STATUS_SAT;
//instantiate each quantifier
- for( int q=0; q<getQuantifiersEngine()->getNumAssertedQuantifiers(); q++ ){
- Node f = getQuantifiersEngine()->getAssertedQuantifier( q );
+ for( int q=0; q<d_quantEngine->getModel()->getNumAssertedQuantifiers(); q++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( q );
Debug("inst-engine-debug") << "IE: Instantiate " << f << "..." << std::endl;
//if this quantifier is active
- if( getQuantifiersEngine()->getActive( f ) ){
- //int e_use = getQuantifiersEngine()->getRelevance( f )==-1 ? e - 1 : e;
+ if( d_quantEngine->getActive( f ) ){
+ //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
int e_use = e;
if( e_use>=0 ){
//use each theory instantiator to instantiate f
for( int i=0; i<theory::THEORY_LAST; i++ ){
- if( getQuantifiersEngine()->getInstantiator( i ) ){
- Debug("inst-engine-debug") << "Do " << getQuantifiersEngine()->getInstantiator( i )->identify() << " " << e_use << std::endl;
- int limitInst = 0;
- int quantStatus = getQuantifiersEngine()->getInstantiator( i )->doInstantiation( f, effort, e_use, limitInst );
+ if( d_quantEngine->getInstantiator( i ) ){
+ Debug("inst-engine-debug") << "Do " << d_quantEngine->getInstantiator( i )->identify() << " " << e_use << std::endl;
+ int quantStatus = d_quantEngine->getInstantiator( i )->doInstantiation( f, effort, e_use );
Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
InstStrategy::updateStatus( d_inst_round_status, quantStatus );
}
@@ -126,31 +116,31 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
}
}
//do not consider another level if already added lemma at this level
- if( getQuantifiersEngine()->hasAddedLemma() ){
+ if( d_quantEngine->hasAddedLemma() ){
d_inst_round_status = InstStrategy::STATUS_UNKNOWN;
}
e++;
}
Debug("inst-engine") << "All instantiators finished, # added lemmas = ";
- Debug("inst-engine") << (int)getQuantifiersEngine()->d_lemmas_waiting.size() << std::endl;
+ Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
//Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
- if( !getQuantifiersEngine()->hasAddedLemma() ){
+ if( !d_quantEngine->hasAddedLemma() ){
Debug("inst-engine-stuck") << "No instantiations produced at this state: " << std::endl;
for( int i=0; i<theory::THEORY_LAST; i++ ){
- if( getQuantifiersEngine()->getInstantiator( i ) ){
- getQuantifiersEngine()->getInstantiator( i )->debugPrint("inst-engine-stuck");
+ if( d_quantEngine->getInstantiator( i ) ){
+ d_quantEngine->getInstantiator( i )->debugPrint("inst-engine-stuck");
Debug("inst-engine-stuck") << std::endl;
}
}
Debug("inst-engine-ctrl") << "---Fail." << std::endl;
return false;
}else{
- Debug("inst-engine-ctrl") << "---Done. " << (int)getQuantifiersEngine()->d_lemmas_waiting.size() << std::endl;
-#ifdef IE_PRINT_PROCESS_TIMES
- Notice() << "lemmas = " << (int)getQuantifiersEngine()->d_lemmas_waiting.size() << std::endl;
-#endif
+ Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
+ if( Options::current()->printInstEngine ){
+ Message() << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
+ }
//flush lemmas to output channel
- getQuantifiersEngine()->flushLemmas( &d_th->getOutputChannel() );
+ d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
return true;
}
}
@@ -174,42 +164,43 @@ void InstantiationEngine::check( Theory::Effort e ){
}
if( performCheck ){
Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl;
-#ifdef IE_PRINT_PROCESS_TIMES
- double clSet = double(clock())/double(CLOCKS_PER_SEC);
- Notice() << "Run instantiation round " << e << " " << ierCounter << std::endl;
-#endif
+ double clSet = 0;
+ if( Options::current()->printInstEngine ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Message() << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
+ }
bool quantActive = false;
//for each quantifier currently asserted,
// such that the counterexample literal is not in positive in d_counterexample_asserts
// for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
// if( (*i).second ) {
- Debug("quantifiers") << "quantifiers: check: asserted quantifiers size"
- << getQuantifiersEngine()->getNumAssertedQuantifiers() << std::endl;
- for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
- Node n = getQuantifiersEngine()->getAssertedQuantifier( i );
+ Debug("quantifiers") << "quantifiers: check: asserted quantifiers size"
+ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){
Node cel = d_ce_lit[ n ];
bool active, value;
bool ceValue = false;
- if( d_th->getValuation().hasSatValue( cel, value ) ){
+ if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
active = value;
ceValue = true;
}else{
active = true;
}
- getQuantifiersEngine()->setActive( n, active );
+ d_quantEngine->setActive( n, active );
if( active ){
Debug("quantifiers") << " Active : " << n;
quantActive = true;
}else{
Debug("quantifiers") << " NOT active : " << n;
- if( d_th->getValuation().isDecision( cel ) ){
+ if( d_quantEngine->getValuation().isDecision( cel ) ){
Debug("quant-req-phase") << "Bad decision : " << cel << std::endl;
}
//note that the counterexample literal must not be a decision
- Assert( !d_th->getValuation().isDecision( cel ) );
+ Assert( !d_quantEngine->getValuation().isDecision( cel ) );
}
- if( d_th->getValuation().hasSatValue( n, value ) ){
+ if( d_quantEngine->getValuation().hasSatValue( n, value ) ){
Debug("quantifiers") << ", value = " << value;
}
if( ceValue ){
@@ -217,18 +208,18 @@ void InstantiationEngine::check( Theory::Effort e ){
}
Debug("quantifiers") << std::endl;
}else{
- getQuantifiersEngine()->setActive( n, true );
+ d_quantEngine->setActive( n, true );
quantActive = true;
Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl;
}
Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl;
- Debug("quantifiers-relevance") << " Relevance : " << getQuantifiersEngine()->getRelevance( n ) << std::endl;
- Debug("quantifiers") << " Relevance : " << getQuantifiersEngine()->getRelevance( n ) << std::endl;
+ Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl;
+ Debug("quantifiers") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl;
}
//}
if( quantActive ){
bool addedLemmas = doInstantiationRound( e );
- //Debug("quantifiers-dec") << "Do instantiation, level = " << d_th->getValuation().getDecisionLevel() << std::endl;
+ //Debug("quantifiers-dec") << "Do instantiation, level = " << d_quantEngine->getValuation().getDecisionLevel() << std::endl;
//for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
// Debug("quantifiers-dec") << " " << d_valuation.getDecision( i ) << std::endl;
//}
@@ -237,9 +228,12 @@ void InstantiationEngine::check( Theory::Effort e ){
if( d_inst_round_status==InstStrategy::STATUS_SAT ){
Debug("inst-engine") << "No instantiation given, returning SAT..." << std::endl;
debugSat( SAT_INST_STRATEGY );
- }else{
+ }else if( d_setIncomplete ){
Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl;
- d_th->getOutputChannel().setIncomplete();
+ d_quantEngine->getOutputChannel().setIncomplete();
+ }else{
+ Assert( Options::current()->finiteModelFind );
+ Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl;
}
}
}
@@ -250,30 +244,30 @@ void InstantiationEngine::check( Theory::Effort e ){
}
}
}
-#ifdef IE_PRINT_PROCESS_TIMES
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Notice() << "Done Run instantiation round " << (clSet2-clSet) << std::endl;
-#endif
+ if( Options::current()->printInstEngine ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Message() << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+ }
}
}
void InstantiationEngine::registerQuantifier( Node f ){
//Notice() << "do cbqi " << f << " ? " << std::endl;
- Node ceBody = getQuantifiersEngine()->getCounterexampleBody( f );
+ Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
if( !doCbqi( f ) ){
- getQuantifiersEngine()->addTermToDatabase( ceBody, true );
+ d_quantEngine->addTermToDatabase( ceBody, true );
//need to tell which instantiators will be responsible
//by default, just chose the UF instantiator
- getQuantifiersEngine()->getInstantiator( theory::THEORY_UF )->setHasConstraintsFrom( f );
+ d_quantEngine->getInstantiator( theory::THEORY_UF )->setHasConstraintsFrom( f );
}
//take into account user patterns
if( f.getNumChildren()==3 ){
- Node subsPat = getQuantifiersEngine()->getSubstitutedNode( f[2], f );
+ Node subsPat = d_quantEngine->getTermDatabase()->getSubstitutedNode( f[2], f );
//add patterns
for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
//Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
- ((uf::InstantiatorTheoryUf*)getQuantifiersEngine()->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
+ ((uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
}
}
}
@@ -337,11 +331,11 @@ bool InstantiationEngine::doCbqi( Node f ){
// registerLiterals( n[i], f );
// }
// if( !d_ce_lit[ f ].isNull() ){
-// if( getQuantifiersEngine()->d_te->getPropEngine()->isSatLiteral( n ) && n.getKind()!=NOT ){
+// if( d_quantEngine->d_te->getPropEngine()->isSatLiteral( n ) && n.getKind()!=NOT ){
// if( n!=d_ce_lit[ f ] && n.notNode()!=d_ce_lit[ f ] ){
// Debug("quant-dep-dec") << "Make " << n << " dependent on ";
// Debug("quant-dep-dec") << d_ce_lit[ f ] << std::endl;
-// d_th->getOutputChannel().dependentDecision( d_ce_lit[ f ], n );
+// d_quantEngine->getOutputChannel().dependentDecision( d_ce_lit[ f ], n );
// }
// }
// }
@@ -351,19 +345,19 @@ bool InstantiationEngine::doCbqi( Node f ){
void InstantiationEngine::debugSat( int reason ){
if( reason==SAT_CBQI ){
//Debug("quantifiers-sat") << "Decisions:" << std::endl;
- //for( int i=1; i<=(int)d_th->getValuation().getDecisionLevel(); i++ ){
- // Debug("quantifiers-sat") << " " << i << ": " << d_th->getValuation().getDecision( i ) << std::endl;
+ //for( int i=1; i<=(int)d_quantEngine->getValuation().getDecisionLevel(); i++ ){
+ // Debug("quantifiers-sat") << " " << i << ": " << d_quantEngine->getValuation().getDecision( i ) << std::endl;
//}
//for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
// if( (*i).second ) {
- for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
- Node f = getQuantifiersEngine()->getAssertedQuantifier( i );
+ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
Node cel = d_ce_lit[ f ];
Assert( !cel.isNull() );
bool value;
- if( d_th->getValuation().hasSatValue( cel, value ) ){
+ if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
if( !value ){
- AlwaysAssert(! d_th->getValuation().isDecision( cel ),
+ AlwaysAssert(! d_quantEngine->getValuation().isDecision( cel ),
"bad decision on counterexample literal");
}
}
@@ -386,9 +380,9 @@ void InstantiationEngine::propagate( Theory::Effort level ){
//propagate as decision all counterexample literals that are not asserted
for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){
bool value;
- if( !d_th->getValuation().hasSatValue( it->second, value ) ){
+ if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){
//if not already set, propagate as decision
- d_th->getOutputChannel().propagateAsDecision( it->second );
+ d_quantEngine->getOutputChannel().propagateAsDecision( it->second );
Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback