diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-01 15:16:17 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-01 15:16:17 +0200 |
commit | 8d3446768446f16e71dca48bdf14d4ed767756aa (patch) | |
tree | ab8e01fdb9fe7e5f4f7db5aa378a424f19488f0c /src/theory | |
parent | a9f4d3e2aed0c6d8d8b218c5f5d2bc95af2d45a6 (diff) |
Minor cleanup from previous commit. Better organization for how quantifiers modules check (introduce QuantifiersEngine::QEffort).
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/bounded_integers.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 197 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 60 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 53 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 67 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 59 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 18 |
18 files changed, 247 insertions, 282 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index d6f9704b3..57799fd8e 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -243,8 +243,13 @@ void BoundedIntegers::process( Node f, Node n, bool pol, } } -void BoundedIntegers::check( Theory::Effort e ) { - if( e==Theory::EFFORT_LAST_CALL ){ +bool BoundedIntegers::needsCheck( Theory::Effort e ) { + return e==Theory::EFFORT_LAST_CALL; +} + +void BoundedIntegers::check( Theory::Effort e, unsigned quant_e ) { + if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + Trace("bint-engine") << "---Bounded Integers---" << std::endl; bool addedLemma = false; //make sure proxies are up-to-date with range for( unsigned i=0; i<d_ranges.size(); i++) { @@ -252,9 +257,7 @@ void BoundedIntegers::check( Theory::Effort e ) { addedLemma = true; } } - if( addedLemma ){ - d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); - } + Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl; } } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index ac188ca65..355360e41 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -110,7 +110,8 @@ private: public: BoundedIntegers( context::Context* c, QuantifiersEngine* qe ); - void check( Theory::Effort e ); + bool needsCheck( Theory::Effort e ); + void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node n ); Node getNextDecisionRequest(); diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 462738cf8..a7c67a5e4 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1,5 +1,5 @@ /********************* */
-/*! \file subgoal_generator.cpp
+/*! \file conjecture_generator.cpp
** \verbatim
** Original author: Andrew Reynolds
** Major contributors: none
@@ -156,7 +156,7 @@ void ConjectureGenerator::doPendingAddUniversalTerms() { Node t = pending[i];
TypeNode tn = t.getType();
Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
- //get all equivalent terms from conjecture database
+ //get all equivalent terms based on theorem database
std::vector< Node > eq_terms;
d_thm_index.getEquivalentTerms( t, eq_terms );
if( !eq_terms.empty() ){
@@ -184,6 +184,17 @@ void ConjectureGenerator::doPendingAddUniversalTerms() { }else{
Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;
}
+ //if occurs at ground level, merge with representative of ground equality engine
+ /*
+ eq::EqualityEngine * ee = getEqualityEngine();
+ if( ee->hasTerm( t ) ){
+ TNode grt = ee->getRepresentative( t );
+ if( t!=grt ){
+ Node exp;
+ d_uequalityEngine.assertEquality( t.eqNode( grt ), true, exp );
+ }
+ }
+ */
}
}
}
@@ -289,19 +300,6 @@ TermDb * ConjectureGenerator::getTermDatabase() { return d_quantEngine->getTermDatabase();
}
-bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
- if( e==Theory::EFFORT_FULL ){
- //d_fullEffortCount++;
- return d_fullEffortCount%optFullCheckFrequency()==0;
- }else{
- return false;
- }
-}
-
-void ConjectureGenerator::reset_round( Theory::Effort e ) {
-
-}
-
Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
Assert( !tn.isNull() );
while( d_free_var[tn].size()<=i ){
@@ -374,16 +372,19 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) { return std::find( d_ground_terms.begin(), d_ground_terms.end(), n )!=d_ground_terms.end();
}
-void ConjectureGenerator::check( Theory::Effort e ) {
- if( e==Theory::EFFORT_FULL ){
- bool doCheck = d_fullEffortCount%optFullCheckFrequency()==0;
- if( d_quantEngine->hasAddedLemma() ){
- doCheck = false;
- }else{
- d_fullEffortCount++;
- }
- if( doCheck ){
- Trace("sg-engine") << "---Subgoal engine, effort = " << e << "--- " << std::endl;
+bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
+ return e==Theory::EFFORT_FULL;
+}
+
+void ConjectureGenerator::reset_round( Theory::Effort e ) {
+
+}
+
+void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
+ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+ d_fullEffortCount++;
+ if( d_fullEffortCount%optFullCheckFrequency()==0 ){
+ Trace("sg-engine") << "---Conjecture generator, effort = " << e << "--- " << std::endl;
eq::EqualityEngine * ee = getEqualityEngine();
Trace("sg-proc") << "Get eq classes..." << std::endl;
@@ -559,7 +560,7 @@ void ConjectureGenerator::check( Theory::Effort e ) { quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
for( int i=0; i<m->getNumAssertedQuantifiers(); i++ ){
Node q = m->getAssertedQuantifier( i );
- Trace("sg-conjecture-debug") << "Is " << q << " a relevant theorem?" << std::endl;
+ Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
Node conjEq;
if( q[1].getKind()==EQUAL ){
bool isSubsume = false;
@@ -614,12 +615,12 @@ void ConjectureGenerator::check( Theory::Effort e ) { if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){
//check each skolem variable
bool disproven = true;
- std::vector< Node > sk;
- getTermDatabase()->getSkolemConstants( q, sk, true );
+ //std::vector< Node > sk;
+ //getTermDatabase()->getSkolemConstants( q, sk, true );
Trace("sg-conjecture") << " CONJECTURE : ";
std::vector< Node > ce;
- for( unsigned j=0; j<sk.size(); j++ ){
- TNode k = sk[j];
+ for( unsigned j=0; j<getTermDatabase()->d_skolem_constants[q].size(); j++ ){
+ TNode k = getTermDatabase()->d_skolem_constants[q][j];
TNode rk = getRepresentative( k );
std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );
//check if it is a ground term
@@ -627,7 +628,7 @@ void ConjectureGenerator::check( Theory::Effort e ) { Trace("sg-conjecture") << "ACTIVE : " << q;
if( Trace.isOn("sg-gen-eqc") ){
Trace("sg-conjecture") << " { ";
- for( unsigned k=0; k<sk.size(); k++ ){ Trace("sg-conjecture") << sk[k] << ( j==k ? "*" : "" ) << " "; }
+ for( unsigned k=0; k<getTermDatabase()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }
Trace("sg-conjecture") << "}";
}
Trace("sg-conjecture") << std::endl;
@@ -903,8 +904,8 @@ void ConjectureGenerator::check( Theory::Effort e ) { for( unsigned i=0; i<d_waiting_conjectures.size(); i++ ){
Assert( d_waiting_conjectures[i].getKind()==FORALL );
Node lem = NodeManager::currentNM()->mkNode( OR, d_waiting_conjectures[i].negate(), d_waiting_conjectures[i] );
- d_quantEngine->getOutputChannel().lemma( lem );
- d_quantEngine->getOutputChannel().requirePhase( d_waiting_conjectures[i], false );
+ d_quantEngine->addLemma( lem, false );
+ d_quantEngine->addRequirePhase( d_waiting_conjectures[i], false );
}
d_waiting_conjectures.clear();
}
@@ -1244,20 +1245,13 @@ void ConjectureGenerator::processCandidateConjecture( unsigned cid, unsigned dep Trace("sg-conjecture-debug") << ", ";
}
Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];
+ if( it->second.size()==1 ){
+ Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";
+ }
firstTime = false;
}
Trace("sg-conjecture-debug") << std::endl;
}
- /*
- if( getUniversalRepresentative( lhs )!=lhs ){
- std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;
- exit(0);
- }
- if( getUniversalRepresentative( rhs )!=rhs ){
- std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;
- exit(0);
- }
- */
Assert( getUniversalRepresentative( rhs )==rhs );
Assert( getUniversalRepresentative( lhs )==lhs );
//make universal quantified formula
@@ -1273,7 +1267,6 @@ void ConjectureGenerator::processCandidateConjecture( unsigned cid, unsigned dep Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
Node conj = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );
conj = Rewriter::rewrite( conj );
- Trace("sg-conjecture-debug") << " formula is : " << conj << std::endl;
d_waiting_conjectures.push_back( conj );
}
}
@@ -1331,6 +1324,8 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { }
}
if( optFilterConfirmationDomain() ){
+ std::vector< TNode > vars;
+ std::vector< TNode > subs;
for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
Assert( d_pattern_fun_id[lhs].find( it->first )!=d_pattern_fun_id[lhs].end() );
unsigned req = d_pattern_fun_id[lhs][it->first];
@@ -1342,6 +1337,22 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { Trace("sg-cconj") << " -> did not find at least " << d_pattern_fun_id[lhs][it->first] << " different values in ground substitutions for variable " << it->first << "." << std::endl;
return false;
}
+ if( it->second.size()==1 ){
+ vars.push_back( it->first );
+ subs.push_back( it->second[0] );
+ }
+ }
+ if( optFilterConfirmationNonCanonical() && !vars.empty() ){
+ Node slhs = lhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ Node srhs = rhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ TNode slhsr = getUniversalRepresentative( slhs, true );
+ TNode srhsr = getUniversalRepresentative( srhs, true );
+ if( areUniversalEqual( slhsr, srhsr ) ){
+ Trace("sg-cconj") << " -> all ground witnesses can be proven by other theorems." << std::endl;
+ return false;
+ }else{
+ Trace("sg-cconj-debug") << "Checked if " << slhsr << " and " << srhsr << " were equal." << std::endl;
+ }
}
}
}
@@ -1353,70 +1364,27 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { Trace("sg-cconj") << " #witnesses for " << it->first << " : " << it->second.size() << std::endl;
}
}
-
- return true;
- }
-}
-
-
-
-bool ConjectureGenerator::processCandidateConjecture2( TNode rhs, TypeNode tn, unsigned depth ) {
- for( unsigned j=0; j<d_rel_patterns_at_depth[tn][depth].size(); j++ ){
- if( processCandidateConjecture2( d_rel_patterns_at_depth[tn][depth][j], rhs ) ){
- return true;
- }
- }
- return false;
-}
-
-bool ConjectureGenerator::processCandidateConjecture2( TNode lhs, TNode rhs ) {
- if( !considerCandidateConjecture( lhs, rhs ) ){
- return false;
- }else{
- Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;
- Trace("sg-conjecture-debug") << " LHS generalization depth : " << d_gen_depth[lhs] << std::endl;
- if( optFilterConfirmation() || optFilterFalsification() ){
- Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
- Trace("sg-conjecture-debug") << " #witnesses for ";
- bool firstTime = true;
- for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
- if( !firstTime ){
- Trace("sg-conjecture-debug") << ", ";
- }
- Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];
- firstTime = false;
- }
- Trace("sg-conjecture-debug") << std::endl;
- }
+
+ /*
if( getUniversalRepresentative( lhs )!=lhs ){
- Trace("ajr-temp") << "bad universal representative : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;
+ std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;
+ exit(0);
}
- Assert( getUniversalRepresentative( rhs )==rhs );
- Assert( getUniversalRepresentative( lhs )==lhs );
- //make universal quantified formula
- Assert( std::find( d_eq_conjectures[lhs].begin(), d_eq_conjectures[lhs].end(), rhs )==d_eq_conjectures[lhs].end() );
- d_eq_conjectures[lhs].push_back( rhs );
- d_eq_conjectures[rhs].push_back( lhs );
- std::vector< Node > bvs;
- for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){
- for( unsigned i=0; i<=it->second; i++ ){
- bvs.push_back( getFreeVar( it->first, i ) );
- }
+ if( getUniversalRepresentative( rhs )!=rhs ){
+ std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;
+ exit(0);
}
- Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
- Node conj = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );
- conj = Rewriter::rewrite( conj );
- Trace("sg-conjecture-debug") << " formula is : " << conj << std::endl;
- d_waiting_conjectures.push_back( conj );
+ */
+
+ //check if still canonical representation (should be, but for efficiency this is not guarenteed)
+ if( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ){
+ Trace("sg-cconj") << " -> after processing, not canonical." << std::endl;
+ }
+
return true;
}
}
-
-
-
-
-
bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) {
if( Trace.isOn("sg-cconj-debug") ){
Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substituion: " << std::endl;
@@ -1807,30 +1775,6 @@ Node TermGenerator::getTerm( ConjectureGenerator * s ) { return Node::null();
}
-/*
-int TermGenerator::getActiveChild( ConjectureGenerator * s ) {
- if( d_status==1 || d_status==2 ){
- return d_id;
- }else if( d_status==5 ){
- Node f = s->getTgFunc( d_typ, d_status_num );
- int i = d_children.size()-1;
- if( d_children.size()==s->d_func_args[f].size() ){
- if( d_children.empty() ){
- return d_id;
- }else{
- int cac = s->d_tg_alloc[d_children[i]].getActiveChild( s );
- return cac==(int)d_children[i] ? d_id : cac;
- }
- }else if( !d_children.empty() ){
- return s->d_tg_alloc[d_children[i]].getActiveChild( s );
- }
- }else{
- Assert( false );
- }
- return -1;
-}
-*/
-
void TermGenerator::debugPrint( ConjectureGenerator * s, const char * c, const char * cd ) {
Trace(cd) << "[*" << d_id << "," << d_status << "]:";
if( d_status==1 || d_status==2 ){
@@ -1999,11 +1943,10 @@ bool ConjectureGenerator::optFilterFalsification() { return true; } bool ConjectureGenerator::optFilterConfirmation() { return true; }
bool ConjectureGenerator::optFilterConfirmationDomain() { return true; }
bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }//false; }
-bool ConjectureGenerator::optWaitForFullCheck() { return true; }
+bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }//true; }
unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
unsigned ConjectureGenerator::optFullCheckConjectures() { return 1; }
-
}
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 90c76d410..afdd9e018 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -1,5 +1,5 @@ /********************* */
-/*! \file subgoal_generator.h
+/*! \file conjecture_generator.h
** \verbatim
** Original author: Andrew Reynolds
** Major contributors: none
@@ -339,12 +339,6 @@ public: //for property enumeration void addCandidateConjecture( TNode lhs, TNode rhs, unsigned depth );
//process candidate conjecture at depth
void processCandidateConjecture( unsigned cid, unsigned depth );
-
- //process candidate conjecture at depth
- bool processCandidateConjecture2( TNode rhs, TypeNode tn, unsigned depth );
- //process candidate conjecture
- bool processCandidateConjecture2( TNode lhs, TNode rhs );
-
//whether it should be considered
bool considerCandidateConjecture( TNode lhs, TNode rhs );
//notified of a substitution
@@ -381,7 +375,7 @@ public: /* reset at a round */
void reset_round( Theory::Effort e );
/* Call during quantifier engine's check */
- void check( Theory::Effort e );
+ void check( Theory::Effort e, unsigned quant_e );
/* Called for new quantifiers */
void registerQuantifier( Node q );
void assertNode( Node n );
@@ -395,7 +389,7 @@ private: bool optFilterConfirmation();
bool optFilterConfirmationDomain();
bool optFilterConfirmationOnlyGround();
- bool optWaitForFullCheck();
+ bool optFilterConfirmationNonCanonical(); //filter if all ground confirmations are non-canonical
unsigned optFullCheckFrequency();
unsigned optFullCheckConjectures();
};
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 2167c7c7d..684831773 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ } @@ -41,18 +41,19 @@ InstantiationEngine::~InstantiationEngine() { } void InstantiationEngine::finishInit(){ - //for UF terms if( !options::finiteModelFind() || options::fmfInstEngine() ){ - //if( options::cbqi() ){ - // addInstStrategy( new InstStrategyCheckCESolved( this, d_quantEngine ) ); - //} - //these are the instantiation strategies for basic E-matching + + //these are the instantiation strategies for E-matching + + //user-provided patterns if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ d_isup = new InstStrategyUserPatterns( d_quantEngine ); addInstStrategy( d_isup ); }else{ d_isup = NULL; } + + //auto-generated patterns int tstrt = Trigger::TS_ALL; if( options::triggerSelMode()==TRIGGER_SEL_MIN ){ tstrt = Trigger::TS_MIN_TRIGGER; @@ -62,26 +63,23 @@ void InstantiationEngine::finishInit(){ d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 ); d_i_ag->setGenerateAdditional( true ); addInstStrategy( d_i_ag ); - //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) ); + + //full saturation : instantiate from relevant domain, then arbitrary terms if( !options::finiteModelFind() && options::fullSaturateQuant() ){ addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) ); } - //d_isup->setPriorityOver( d_i_ag ); - //d_isup->setPriorityOver( i_agm ); - //i_ag->setPriorityOver( i_agm ); } - //for arithmetic + + //counterexample-based quantifier instantiation if( options::cbqi() ){ addInstStrategy( new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ) ); - } - //for datatypes - //if( options::cbqi() ){ // addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) ); - //} + } } bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ + unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size(); //if counterexample-based quantifier instantiation is active if( options::cbqi() ){ //check if any cbqi lemma has not been added yet @@ -155,7 +153,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } } //do not consider another level if already added lemma at this level - if( d_quantEngine->hasAddedLemma() ){ + if( d_quantEngine->d_lemmas_waiting.size()>lastWaiting ){ d_inst_round_status = InstStrategy::STATUS_UNKNOWN; } e++; @@ -164,14 +162,11 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ 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( !d_quantEngine->hasAddedLemma() ){ - Debug("inst-engine-stuck") << "No instantiations produced at this state." << std::endl; Debug("inst-engine-ctrl") << "---Fail." << std::endl; return false; }else{ - Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; - Trace("inst-engine") << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; - //flush lemmas to output channel - d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); + Debug("inst-engine-ctrl") << "---Done. " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl; + Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl; return true; } } @@ -181,17 +176,17 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){ d_ierCounter++; } //determine if we should perform check, based on instWhenMode - d_performCheck = false; + bool performCheck = false; if( options::instWhenMode()==INST_WHEN_FULL ){ - d_performCheck = ( e >= Theory::EFFORT_FULL ); + performCheck = ( e >= Theory::EFFORT_FULL ); }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){ - d_performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck(); + performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck(); }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ - d_performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ - d_performCheck = ( e >= Theory::EFFORT_LAST_CALL ); + performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ - d_performCheck = true; + performCheck = true; } static int ierCounter2 = 0; if( e==Theory::EFFORT_LAST_CALL ){ @@ -199,15 +194,14 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){ //with bounded integers, skip every other last call, // since matching loops may occur with infinite quantification if( ierCounter2%2==0 && options::fmfBoundInt() ){ - d_performCheck = false; + performCheck = false; } } - - return d_performCheck; + return performCheck; } -void InstantiationEngine::check( Theory::Effort e ){ - if( d_performCheck && !d_quantEngine->hasAddedLemma() ){ +void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ + if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl; double clSet = 0; if( Trace.isOn("inst-engine") ){ @@ -217,7 +211,7 @@ void InstantiationEngine::check( Theory::Effort e ){ ++(d_statistics.d_instantiation_rounds); bool quantActive = false; Debug("quantifiers") << "quantifiers: check: asserted quantifiers size=" - << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; + << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 7a3528217..393f53897 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -99,7 +99,6 @@ private: bool d_setIncomplete; /** inst round counter */ int d_ierCounter; - bool d_performCheck; /** whether each quantifier is active */ std::map< Node, bool > d_quant_active; /** whether we have added cbqi lemma */ @@ -131,7 +130,7 @@ public: void finishInit(); bool needsCheck( Theory::Effort e ); - void check( Theory::Effort e ); + void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 3c2f9903e..f3d3e4bc9 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -66,8 +66,12 @@ ModelEngine::~ModelEngine() { delete d_builder; } -void ModelEngine::check( Theory::Effort e ){ - if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ +bool ModelEngine::needsCheck( Theory::Effort e ) { + return e==Theory::EFFORT_LAST_CALL; +} + +void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ + if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ int addedLemmas = 0; bool needsBuild = true; FirstOrderModel* fm = d_quantEngine->getModel(); @@ -145,7 +149,6 @@ void ModelEngine::check( Theory::Effort e ){ } }else{ //otherwise, the search will continue - d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); } } } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index caf27f691..890af1643 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -52,7 +52,8 @@ public: //get the builder QModelBuilder* getModelBuilder() { return d_builder; } public: - void check( Theory::Effort e ); + bool needsCheck( Theory::Effort e ); + void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e23e70174..71b05cec5 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -145,8 +145,8 @@ option rrOneInstPerRound --rr-one-inst-per-round bool :default false add one instance of rewrite rule per round option dtStcInduction --dt-stc-ind bool :default false - apply strengthening for existential quantification over datatypes based on structural + apply strengthening for existential quantification over datatypes based on structural induction option conjectureGen --conjecture-gen bool :default false - generate candidate conjectures for inductive strengthening + generate candidate conjectures for inductive proofs endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 86d0c27e4..97eaf4aaa 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -153,7 +153,7 @@ ignore \n\ \n\ "; static const std::string triggerSelModeHelp = "\ -User pattern modes currently supported by the --trigger-sel option:\n\ +Trigger selection modes currently supported by the --trigger-sel option:\n\ \n\ default \n\ + Default, consider all subterms of quantified formulas for trigger selection.\n\ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 4e4d92d28..504c3dcff 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1922,22 +1922,36 @@ void QuantConflictFind::assertDisequal( Node a, Node b ) { //-------------------------------------------------- check function
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {
+ bool performCheck = false;
+ if( options::quantConflictFind() && !d_conflict ){
+ if( level==Theory::EFFORT_LAST_CALL ){
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
+ }else if( level==Theory::EFFORT_FULL ){
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
+ }else if( level==Theory::EFFORT_STANDARD ){
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
+ }
+ }
+ return performCheck;
+}
+
void QuantConflictFind::reset_round( Theory::Effort level ) {
d_needs_computeRelEqr = true;
}
/** check */
-void QuantConflictFind::check( Theory::Effort level ) {
- Trace("qcf-check") << "QCF : check : " << level << std::endl;
- if( d_conflict ){
- Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
- if( level>=Theory::EFFORT_FULL ){
- Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
- //Assert( false );
- }
- }else{
- int addedLemmas = 0;
- if( d_performCheck ){
+void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
+ if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+ Trace("qcf-check") << "QCF : check : " << level << std::endl;
+ if( d_conflict ){
+ Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
+ if( level>=Theory::EFFORT_FULL ){
+ Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
+ //Assert( false );
+ }
+ }else{
+ int addedLemmas = 0;
++(d_statistics.d_inst_rounds);
double clSet = 0;
int prevEt = 0;
@@ -2048,7 +2062,6 @@ void QuantConflictFind::check( Theory::Effort level ) { }
}
if( addedLemmas>0 ){
- d_quantEngine->flushLemmas();
break;
}
}
@@ -2065,23 +2078,9 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;
}
}
- }
- Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
- }
-}
-
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {
- d_performCheck = false;
- if( options::quantConflictFind() && !d_conflict ){
- if( level==Theory::EFFORT_LAST_CALL ){
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
- }else if( level==Theory::EFFORT_FULL ){
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
- }else if( level==Theory::EFFORT_STANDARD ){
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
+ Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
}
}
- return d_performCheck;
}
void QuantConflictFind::computeRelevantEqr() {
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 1f3635e78..d8f1c8e6f 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -166,7 +166,6 @@ class QuantConflictFind : public QuantifiersModule private:
context::Context* d_c;
context::CDO< bool > d_conflict;
- bool d_performCheck;
std::vector< Node > d_quant_order;
std::map< Kind, Node > d_zero;
//for storing nodes created during t-constraint solving (prevents memory leaks)
@@ -220,12 +219,12 @@ public: void merge( Node a, Node b );
/** assert disequal */
void assertDisequal( Node a, Node b );
+ /** needs check */
+ bool needsCheck( Theory::Effort level );
/** reset round */
void reset_round( Theory::Effort level );
/** check */
- void check( Theory::Effort level );
- /** needs check */
- bool needsCheck( Theory::Effort level );
+ void check( Theory::Effort level, unsigned quant_e );
private:
bool d_needs_computeRelEqr;
public:
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 1b13d772e..7d9fa3344 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -61,8 +61,14 @@ double RewriteEngine::getPriority( Node f ) { //return deterministic ? 0.0 : 1.0; } -void RewriteEngine::check( Theory::Effort e ) { - if( e==Theory::EFFORT_FULL ){ +bool RewriteEngine::needsCheck( Theory::Effort e ){ + return e==Theory::EFFORT_FULL; + //return e>=Theory::EFFORT_LAST_CALL; +} + +void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { + if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + //if( e==Theory::EFFORT_FULL ){ Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; //if( e==Theory::EFFORT_LAST_CALL ){ // if( !d_quantEngine->getModel()->isModelSet() ){ @@ -102,7 +108,6 @@ void RewriteEngine::check( Theory::Effort e ) { }else{ //otherwise, the search will continue - d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); } } } diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index d2108bf3e..1703a9bfc 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -54,7 +54,8 @@ private: public: RewriteEngine( context::Context* c, QuantifiersEngine* qe ); - void check( Theory::Effort e ); + bool needsCheck( Theory::Effort e ); + void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node n ); /** Identify this module */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0d5103db6..60ee5d1e9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -144,8 +144,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ for( size_t i=0; i<d_op_triggers[op].size(); i++ ){ addedLemmas += d_op_triggers[op][i]->addTerm( n ); } - //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; - d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); } } } @@ -241,9 +239,9 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, Assert( ee->hasTerm( n1 ) ); Assert( ee->hasTerm( n2 ) ); if( pol ){ - return ee->areEqual( n1, n2 ); + return n1==n2 || ee->areEqual( n1, n2 ); }else{ - return ee->areDisequal( n1, n2, false ); + return n1!=n2 && ee->areDisequal( n1, n2, false ); } } } @@ -260,18 +258,19 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, }else if( n.getKind()==NOT ){ return isEntailed( n[0], subs, subsRep, !pol ); }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, pol ) ){ - if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){ + if( simPol ){ return true; } }else{ - if( ( !pol && n.getKind()==OR ) || ( pol && n.getKind()==AND ) ){ + if( !simPol ){ return false; } } } - return true; + return !simPol; }else if( n.getKind()==IFF || n.getKind()==ITE ){ for( unsigned i=0; i<2; i++ ){ if( isEntailed( n[0], subs, subsRep, i==0 ) ){ @@ -594,6 +593,7 @@ void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vecto Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs, std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) { + Assert( sk.empty() || sk.size()==f[0].getNumChildren() ); //calculate the variables and substitution std::vector< TNode > ind_vars; std::vector< unsigned > ind_var_indicies; @@ -608,19 +608,23 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes var_indicies.push_back( i ); } Node s; - //make the new function symbol - if( argTypes.empty() ){ - s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" ); + //make the new function symbol or use existing + if( i>=sk.size() ){ + if( argTypes.empty() ){ + s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" ); + }else{ + TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() ); + Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" ); + //DOTHIS: set attribute on op, marking that it should not be selected as trigger + std::vector< Node > funcArgs; + funcArgs.push_back( op ); + funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); + s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ); + } + sk.push_back( s ); }else{ - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() ); - Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" ); - //DOTHIS: set attribute on op, marking that it should not be selected as trigger - std::vector< Node > funcArgs; - funcArgs.push_back( op ); - funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); - s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ); + Assert( sk[i].getType()==f[0][i].getType() ); } - sk.push_back( s ); } Node ret; if( vars.empty() ){ @@ -688,9 +692,11 @@ Node TermDb::getSkolemizedBody( Node f ){ d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars ); //store sub quantifier information if( !sub.isNull() ){ - Assert( sub[0].getNumChildren()==sub_vars.size() ); - d_skolem_sub_quant[f] = sub; - d_skolem_sub_quant_vars[f].insert( d_skolem_sub_quant_vars[f].end(), sub_vars.begin(), sub_vars.end() ); + //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them + Assert( d_skolem_constants[sub].empty() ); + for( unsigned i=0; i<sub_vars.size(); i++ ){ + d_skolem_constants[sub].push_back( d_skolem_constants[f][sub_vars[i]] ); + } } Assert( d_skolem_constants[f].size()==f[0].getNumChildren() ); if( options::sortInference() ){ @@ -703,25 +709,6 @@ Node TermDb::getSkolemizedBody( Node f ){ return d_skolem_body[ f ]; } -void TermDb::getSkolemConstants( Node f, std::vector< Node >& sk, bool expSub ) { - std::map< Node, std::vector< Node > >::iterator it = d_skolem_constants.find( f ); - if( it!=d_skolem_constants.end() ){ - sk.insert( sk.end(), it->second.begin(), it->second.end() ); - if( expSub ){ - std::map< Node, Node >::iterator its = d_skolem_sub_quant.find( f ); - if( its!=d_skolem_sub_quant.end() && !its->second.isNull() ){ - std::vector< Node > ssk; - getSkolemConstants( its->second, ssk, true ); - Assert( ssk.size()==d_skolem_sub_quant_vars[f].size() ); - for( unsigned i=0; i<d_skolem_sub_quant_vars[f].size(); i++ ){ - sk[d_skolem_sub_quant_vars[f][i]] = ssk[i]; - } - } - } - Assert( sk.size()==f[0].getNumChildren() ); - } -} - Node TermDb::getFreeVariableForInstConstant( Node n ){ TypeNode tn = n.getType(); if( d_free_vars.find( tn )==d_free_vars.end() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index d63f61ca8..d6b336dfa 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -223,16 +223,11 @@ private: public: /** map from universal quantifiers to the list of skolem constants */ std::map< Node, std::vector< Node > > d_skolem_constants; - /** for quantified formulas whose skolemization was strengthened by induction */ - std::map< Node, Node > d_skolem_sub_quant; - std::map< Node, std::vector< unsigned > > d_skolem_sub_quant_vars; /** make the skolemized body f[e/x] */ static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs, std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ); /** get the skolemized body */ Node getSkolemizedBody( Node f); - /** get skolem constants */ - void getSkolemConstants( Node f, std::vector< Node >& sk, bool expSub = false ); //miscellaneous public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a4adf8054..f80f65723 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -167,20 +167,29 @@ void QuantifiersEngine::finishInit(){ void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); bool needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call + std::vector< QuantifiersModule* > qm; for( int i=0; i<(int)d_modules.size(); i++ ){ if( d_modules[i]->needsCheck( e ) ){ + qm.push_back( d_modules[i] ); needsCheck = true; } } if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; + Trace("quant-engine-debug") << " modules to check : "; + for( unsigned i=0; i<qm.size(); i++ ){ + Trace("quant-engine-debug") << qm[i]->identify() << " "; + } + Trace("quant-engine-debug") << std::endl; Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; + if( !getMasterEqualityEngine()->consistent() ){ Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl; return; } - Trace("quant-engine-debug") << "Resetting modules..." << std::endl; + Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; //reset relevant information + d_conflict = false; d_hasAddedLemma = false; d_term_db->reset( e ); d_eq_query->reset(); @@ -191,12 +200,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->reset_round( e ); } - Trace("quant-engine-debug") << "Done resetting modules." << std::endl; + Trace("quant-engine-debug") << "Done resetting all modules." << std::endl; if( e==Theory::EFFORT_LAST_CALL ){ //if effort is last call, try to minimize model first if( options::finiteModelFind() ){ - //first, check if we can minimize the model further + //first, check if we can minimize the model further FIXME: remove? if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ return; } @@ -205,12 +214,22 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); } - Trace("quant-engine-debug") << "Check with modules..." << std::endl; - for( int i=0; i<(int)d_modules.size(); i++ ){ - Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl; - d_modules[i]->check( e ); + + Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; + for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){ + for( int i=0; i<(int)qm.size(); i++ ){ + Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl; + qm[i]->check( e, quant_e ); + } + //flush all current lemmas + flushLemmas(); + //if we have added one, stop + if( d_hasAddedLemma ){ + break; + } } - Trace("quant-engine-debug") << "Done check with modules." << std::endl; + Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; + //build the model if not done so already // this happens if no quantifiers are currently asserted and no model-building module is enabled if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ @@ -270,7 +289,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) { for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){ std::set< Node > added; - getTermDatabase()->addTerm(*p,added); + getTermDatabase()->addTerm( *p, added ); } } @@ -323,6 +342,10 @@ Node QuantifiersEngine::getNextDecisionRequest(){ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant ); + //maybe have triggered instantiations if we are doing eager instantiation + if( options::eagerInstQuant() ){ + flushLemmas(); + } //added contains also the Node that just have been asserted in this branch if( d_quant_rel ){ for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ @@ -520,6 +543,10 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ } } +void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ + d_phase_req_waiting[lit] = req; +} + bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){ std::vector< Node > terms; //make sure there are values for each variable we are instantiating @@ -568,7 +595,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo } if( d_term_db->isEntailed( f[1], subs, false, true ) ){ Trace("inst-add-debug") << " -> Currently entailed." << std::endl; - Trace("inst-add-entail") << " -> instantiation for " << f[1] << " currently entailed." << std::endl; return false; } } @@ -628,18 +654,21 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } -void QuantifiersEngine::flushLemmas( OutputChannel* out ){ +void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ - if( !out ){ - out = &getOutputChannel(); - } //take default output channel if none is provided d_hasAddedLemma = true; for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){ - out->lemma( d_lemmas_waiting[i], false, true ); + getOutputChannel().lemma( d_lemmas_waiting[i], false, true ); } d_lemmas_waiting.clear(); } + if( !d_phase_req_waiting.empty() ){ + for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){ + getOutputChannel().requirePhase( it->first, it->second ); + } + d_phase_req_waiting.clear(); + } } void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 220fa0b1f..f74c478ae 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -52,7 +52,7 @@ public: /* reset at a round */ virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */ - virtual void check( Theory::Effort e ) = 0; + virtual void check( Theory::Effort e, unsigned quant_e ) = 0; /* Called for new quantifiers */ virtual void registerQuantifier( Node q ) = 0; virtual void assertNode( Node n ) = 0; @@ -115,6 +115,12 @@ private: quantifiers::RewriteEngine * d_rr_engine; /** subgoal generator */ quantifiers::ConjectureGenerator * d_sg_gen; +public: //effort levels + enum { + QEFFORT_CONFLICT, + QEFFORT_STANDARD, + QEFFORT_MODEL, + }; private: /** list of all quantifiers seen */ std::vector< Node > d_quants; @@ -123,8 +129,12 @@ private: BoolMap d_lemmas_produced_c; /** lemmas waiting */ std::vector< Node > d_lemmas_waiting; + /** phase requirements waiting */ + std::map< Node, bool > d_phase_req_waiting; /** has added lemma this round */ bool d_hasAddedLemma; + /** has a conflict been found */ + bool d_conflict; /** list of all instantiations produced for each quantifier */ std::map< Node, inst::InstMatchTrie > d_inst_match_trie; std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; @@ -196,6 +206,8 @@ private: bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** set instantiation level attr */ void setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms ); + /** flush lemmas */ + void flushLemmas(); public: /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); @@ -209,6 +221,8 @@ public: bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true ); + /** add require phase */ + void addRequirePhase( Node lit, bool req ); /** do instantiation specified by m */ bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false ); /** add instantiation */ @@ -219,8 +233,6 @@ public: bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); /** has added lemma */ bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } - /** flush lemmas */ - void flushLemmas( OutputChannel* out = NULL ); /** get number of waiting lemmas */ int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } public: |