diff options
Diffstat (limited to 'src/theory/quantifiers')
-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 |
16 files changed, 188 insertions, 264 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: |