}
}
-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++) {
addedLemma = true;
}
}
- if( addedLemma ){
- d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
- }
+ Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl;
}
}
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();
/********************* */\r
-/*! \file subgoal_generator.cpp\r
+/*! \file conjecture_generator.cpp\r
** \verbatim\r
** Original author: Andrew Reynolds\r
** Major contributors: none\r
Node t = pending[i];\r
TypeNode tn = t.getType();\r
Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;\r
- //get all equivalent terms from conjecture database\r
+ //get all equivalent terms based on theorem database\r
std::vector< Node > eq_terms;\r
d_thm_index.getEquivalentTerms( t, eq_terms );\r
if( !eq_terms.empty() ){\r
}else{\r
Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;\r
}\r
+ //if occurs at ground level, merge with representative of ground equality engine\r
+ /*\r
+ eq::EqualityEngine * ee = getEqualityEngine();\r
+ if( ee->hasTerm( t ) ){\r
+ TNode grt = ee->getRepresentative( t );\r
+ if( t!=grt ){\r
+ Node exp;\r
+ d_uequalityEngine.assertEquality( t.eqNode( grt ), true, exp );\r
+ }\r
+ }\r
+ */\r
}\r
}\r
}\r
return d_quantEngine->getTermDatabase();\r
}\r
\r
-bool ConjectureGenerator::needsCheck( Theory::Effort e ) {\r
- if( e==Theory::EFFORT_FULL ){\r
- //d_fullEffortCount++;\r
- return d_fullEffortCount%optFullCheckFrequency()==0;\r
- }else{\r
- return false;\r
- }\r
-}\r
-\r
-void ConjectureGenerator::reset_round( Theory::Effort e ) {\r
-\r
-}\r
-\r
Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {\r
Assert( !tn.isNull() );\r
while( d_free_var[tn].size()<=i ){\r
return std::find( d_ground_terms.begin(), d_ground_terms.end(), n )!=d_ground_terms.end();\r
}\r
\r
-void ConjectureGenerator::check( Theory::Effort e ) {\r
- if( e==Theory::EFFORT_FULL ){\r
- bool doCheck = d_fullEffortCount%optFullCheckFrequency()==0;\r
- if( d_quantEngine->hasAddedLemma() ){\r
- doCheck = false;\r
- }else{\r
- d_fullEffortCount++;\r
- }\r
- if( doCheck ){\r
- Trace("sg-engine") << "---Subgoal engine, effort = " << e << "--- " << std::endl;\r
+bool ConjectureGenerator::needsCheck( Theory::Effort e ) {\r
+ return e==Theory::EFFORT_FULL;\r
+}\r
+\r
+void ConjectureGenerator::reset_round( Theory::Effort e ) {\r
+\r
+}\r
+\r
+void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {\r
+ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){\r
+ d_fullEffortCount++;\r
+ if( d_fullEffortCount%optFullCheckFrequency()==0 ){\r
+ Trace("sg-engine") << "---Conjecture generator, effort = " << e << "--- " << std::endl;\r
eq::EqualityEngine * ee = getEqualityEngine();\r
\r
Trace("sg-proc") << "Get eq classes..." << std::endl;\r
quantifiers::FirstOrderModel* m = d_quantEngine->getModel();\r
for( int i=0; i<m->getNumAssertedQuantifiers(); i++ ){\r
Node q = m->getAssertedQuantifier( i );\r
- Trace("sg-conjecture-debug") << "Is " << q << " a relevant theorem?" << std::endl;\r
+ Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;\r
Node conjEq;\r
if( q[1].getKind()==EQUAL ){\r
bool isSubsume = false;\r
if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){\r
//check each skolem variable\r
bool disproven = true;\r
- std::vector< Node > sk;\r
- getTermDatabase()->getSkolemConstants( q, sk, true );\r
+ //std::vector< Node > sk;\r
+ //getTermDatabase()->getSkolemConstants( q, sk, true );\r
Trace("sg-conjecture") << " CONJECTURE : ";\r
std::vector< Node > ce;\r
- for( unsigned j=0; j<sk.size(); j++ ){\r
- TNode k = sk[j];\r
+ for( unsigned j=0; j<getTermDatabase()->d_skolem_constants[q].size(); j++ ){\r
+ TNode k = getTermDatabase()->d_skolem_constants[q][j];\r
TNode rk = getRepresentative( k );\r
std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );\r
//check if it is a ground term\r
Trace("sg-conjecture") << "ACTIVE : " << q;\r
if( Trace.isOn("sg-gen-eqc") ){\r
Trace("sg-conjecture") << " { ";\r
- for( unsigned k=0; k<sk.size(); k++ ){ Trace("sg-conjecture") << sk[k] << ( j==k ? "*" : "" ) << " "; }\r
+ for( unsigned k=0; k<getTermDatabase()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }\r
Trace("sg-conjecture") << "}";\r
}\r
Trace("sg-conjecture") << std::endl;\r
for( unsigned i=0; i<d_waiting_conjectures.size(); i++ ){\r
Assert( d_waiting_conjectures[i].getKind()==FORALL );\r
Node lem = NodeManager::currentNM()->mkNode( OR, d_waiting_conjectures[i].negate(), d_waiting_conjectures[i] );\r
- d_quantEngine->getOutputChannel().lemma( lem );\r
- d_quantEngine->getOutputChannel().requirePhase( d_waiting_conjectures[i], false );\r
+ d_quantEngine->addLemma( lem, false );\r
+ d_quantEngine->addRequirePhase( d_waiting_conjectures[i], false );\r
}\r
d_waiting_conjectures.clear();\r
}\r
Trace("sg-conjecture-debug") << ", ";\r
}\r
Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];\r
+ if( it->second.size()==1 ){\r
+ Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";\r
+ }\r
firstTime = false;\r
}\r
Trace("sg-conjecture-debug") << std::endl;\r
}\r
- /*\r
- if( getUniversalRepresentative( lhs )!=lhs ){\r
- std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;\r
- exit(0);\r
- }\r
- if( getUniversalRepresentative( rhs )!=rhs ){\r
- std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;\r
- exit(0);\r
- }\r
- */\r
Assert( getUniversalRepresentative( rhs )==rhs );\r
Assert( getUniversalRepresentative( lhs )==lhs );\r
//make universal quantified formula\r
Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );\r
Node conj = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );\r
conj = Rewriter::rewrite( conj );\r
- Trace("sg-conjecture-debug") << " formula is : " << conj << std::endl;\r
d_waiting_conjectures.push_back( conj );\r
}\r
}\r
}\r
}\r
if( optFilterConfirmationDomain() ){\r
+ std::vector< TNode > vars;\r
+ std::vector< TNode > subs;\r
for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){\r
Assert( d_pattern_fun_id[lhs].find( it->first )!=d_pattern_fun_id[lhs].end() );\r
unsigned req = d_pattern_fun_id[lhs][it->first];\r
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;\r
return false;\r
}\r
+ if( it->second.size()==1 ){\r
+ vars.push_back( it->first );\r
+ subs.push_back( it->second[0] );\r
+ }\r
+ }\r
+ if( optFilterConfirmationNonCanonical() && !vars.empty() ){\r
+ Node slhs = lhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ Node srhs = rhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );\r
+ TNode slhsr = getUniversalRepresentative( slhs, true );\r
+ TNode srhsr = getUniversalRepresentative( srhs, true );\r
+ if( areUniversalEqual( slhsr, srhsr ) ){\r
+ Trace("sg-cconj") << " -> all ground witnesses can be proven by other theorems." << std::endl;\r
+ return false; \r
+ }else{\r
+ Trace("sg-cconj-debug") << "Checked if " << slhsr << " and " << srhsr << " were equal." << std::endl;\r
+ }\r
}\r
}\r
}\r
Trace("sg-cconj") << " #witnesses for " << it->first << " : " << it->second.size() << std::endl;\r
}\r
}\r
-\r
- return true;\r
- }\r
-}\r
-\r
-\r
-\r
-bool ConjectureGenerator::processCandidateConjecture2( TNode rhs, TypeNode tn, unsigned depth ) {\r
- for( unsigned j=0; j<d_rel_patterns_at_depth[tn][depth].size(); j++ ){\r
- if( processCandidateConjecture2( d_rel_patterns_at_depth[tn][depth][j], rhs ) ){\r
- return true;\r
- }\r
- }\r
- return false;\r
-}\r
-\r
-bool ConjectureGenerator::processCandidateConjecture2( TNode lhs, TNode rhs ) {\r
- if( !considerCandidateConjecture( lhs, rhs ) ){\r
- return false;\r
- }else{\r
- Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;\r
- Trace("sg-conjecture-debug") << " LHS generalization depth : " << d_gen_depth[lhs] << std::endl;\r
- if( optFilterConfirmation() || optFilterFalsification() ){\r
- Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;\r
- Trace("sg-conjecture-debug") << " #witnesses for ";\r
- bool firstTime = true;\r
- for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){\r
- if( !firstTime ){\r
- Trace("sg-conjecture-debug") << ", ";\r
- }\r
- Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];\r
- firstTime = false;\r
- }\r
- Trace("sg-conjecture-debug") << std::endl;\r
- }\r
+ \r
+ /*\r
if( getUniversalRepresentative( lhs )!=lhs ){\r
- Trace("ajr-temp") << "bad universal representative : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;\r
+ std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;\r
+ exit(0);\r
}\r
- Assert( getUniversalRepresentative( rhs )==rhs );\r
- Assert( getUniversalRepresentative( lhs )==lhs );\r
- //make universal quantified formula\r
- Assert( std::find( d_eq_conjectures[lhs].begin(), d_eq_conjectures[lhs].end(), rhs )==d_eq_conjectures[lhs].end() );\r
- d_eq_conjectures[lhs].push_back( rhs );\r
- d_eq_conjectures[rhs].push_back( lhs );\r
- std::vector< Node > bvs;\r
- for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){\r
- for( unsigned i=0; i<=it->second; i++ ){\r
- bvs.push_back( getFreeVar( it->first, i ) );\r
- }\r
+ if( getUniversalRepresentative( rhs )!=rhs ){\r
+ std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;\r
+ exit(0);\r
}\r
- Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );\r
- Node conj = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );\r
- conj = Rewriter::rewrite( conj );\r
- Trace("sg-conjecture-debug") << " formula is : " << conj << std::endl;\r
- d_waiting_conjectures.push_back( conj );\r
+ */\r
+ \r
+ //check if still canonical representation (should be, but for efficiency this is not guarenteed)\r
+ if( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ){\r
+ Trace("sg-cconj") << " -> after processing, not canonical." << std::endl;\r
+ }\r
+ \r
return true;\r
}\r
}\r
\r
-\r
-\r
-\r
-\r
-\r
bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) {\r
if( Trace.isOn("sg-cconj-debug") ){\r
Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substituion: " << std::endl;\r
return Node::null();\r
}\r
\r
-/*\r
-int TermGenerator::getActiveChild( ConjectureGenerator * s ) {\r
- if( d_status==1 || d_status==2 ){\r
- return d_id;\r
- }else if( d_status==5 ){\r
- Node f = s->getTgFunc( d_typ, d_status_num );\r
- int i = d_children.size()-1;\r
- if( d_children.size()==s->d_func_args[f].size() ){\r
- if( d_children.empty() ){\r
- return d_id;\r
- }else{\r
- int cac = s->d_tg_alloc[d_children[i]].getActiveChild( s );\r
- return cac==(int)d_children[i] ? d_id : cac;\r
- }\r
- }else if( !d_children.empty() ){\r
- return s->d_tg_alloc[d_children[i]].getActiveChild( s );\r
- }\r
- }else{\r
- Assert( false );\r
- }\r
- return -1;\r
-}\r
-*/\r
-\r
void TermGenerator::debugPrint( ConjectureGenerator * s, const char * c, const char * cd ) {\r
Trace(cd) << "[*" << d_id << "," << d_status << "]:";\r
if( d_status==1 || d_status==2 ){\r
bool ConjectureGenerator::optFilterConfirmation() { return true; }\r
bool ConjectureGenerator::optFilterConfirmationDomain() { return true; }\r
bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }//false; }\r
-bool ConjectureGenerator::optWaitForFullCheck() { return true; }\r
+bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }//true; }\r
unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }\r
unsigned ConjectureGenerator::optFullCheckConjectures() { return 1; }\r
\r
-\r
}\r
\r
\r
/********************* */\r
-/*! \file subgoal_generator.h\r
+/*! \file conjecture_generator.h\r
** \verbatim\r
** Original author: Andrew Reynolds\r
** Major contributors: none\r
void addCandidateConjecture( TNode lhs, TNode rhs, unsigned depth );\r
//process candidate conjecture at depth\r
void processCandidateConjecture( unsigned cid, unsigned depth );\r
- \r
- //process candidate conjecture at depth\r
- bool processCandidateConjecture2( TNode rhs, TypeNode tn, unsigned depth );\r
- //process candidate conjecture \r
- bool processCandidateConjecture2( TNode lhs, TNode rhs );\r
- \r
//whether it should be considered\r
bool considerCandidateConjecture( TNode lhs, TNode rhs );\r
//notified of a substitution\r
/* reset at a round */\r
void reset_round( Theory::Effort e );\r
/* Call during quantifier engine's check */\r
- void check( Theory::Effort e );\r
+ void check( Theory::Effort e, unsigned quant_e );\r
/* Called for new quantifiers */\r
void registerQuantifier( Node q );\r
void assertNode( Node n );\r
bool optFilterConfirmation();\r
bool optFilterConfirmationDomain();\r
bool optFilterConfirmationOnlyGround();\r
- bool optWaitForFullCheck();\r
+ bool optFilterConfirmationNonCanonical(); //filter if all ground confirmations are non-canonical\r
unsigned optFullCheckFrequency();\r
unsigned optFullCheckConjectures();\r
};\r
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 ){
}
}
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;
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
}
}
//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++;
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;
}
}
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 ){
//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") ){
++(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
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 */
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(); }
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();
}
}else{
//otherwise, the search will continue
- d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
}
}
}
//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(); }
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
\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\
\r
//-------------------------------------------------- check function\r
\r
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
+ bool performCheck = false;\r
+ if( options::quantConflictFind() && !d_conflict ){\r
+ if( level==Theory::EFFORT_LAST_CALL ){\r
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
+ }else if( level==Theory::EFFORT_FULL ){\r
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
+ }else if( level==Theory::EFFORT_STANDARD ){\r
+ performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+ }\r
+ }\r
+ return performCheck;\r
+}\r
+\r
void QuantConflictFind::reset_round( Theory::Effort level ) {\r
d_needs_computeRelEqr = true;\r
}\r
\r
/** check */\r
-void QuantConflictFind::check( Theory::Effort level ) {\r
- Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
- if( d_conflict ){\r
- Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
- if( level>=Theory::EFFORT_FULL ){\r
- Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;\r
- //Assert( false );\r
- }\r
- }else{\r
- int addedLemmas = 0;\r
- if( d_performCheck ){\r
+void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {\r
+ if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){\r
+ Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
+ if( d_conflict ){\r
+ Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
+ if( level>=Theory::EFFORT_FULL ){\r
+ Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;\r
+ //Assert( false );\r
+ }\r
+ }else{\r
+ int addedLemmas = 0;\r
++(d_statistics.d_inst_rounds);\r
double clSet = 0;\r
int prevEt = 0;\r
}\r
}\r
if( addedLemmas>0 ){\r
- d_quantEngine->flushLemmas();\r
break;\r
}\r
}\r
Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;\r
}\r
}\r
- }\r
- Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
- }\r
-}\r
-\r
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
- d_performCheck = false;\r
- if( options::quantConflictFind() && !d_conflict ){\r
- if( level==Theory::EFFORT_LAST_CALL ){\r
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
- }else if( level==Theory::EFFORT_FULL ){\r
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
- }else if( level==Theory::EFFORT_STANDARD ){\r
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+ Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
}\r
}\r
- return d_performCheck;\r
}\r
\r
void QuantConflictFind::computeRelevantEqr() {\r
private:\r
context::Context* d_c;\r
context::CDO< bool > d_conflict;\r
- bool d_performCheck;\r
std::vector< Node > d_quant_order;\r
std::map< Kind, Node > d_zero;\r
//for storing nodes created during t-constraint solving (prevents memory leaks)\r
void merge( Node a, Node b );\r
/** assert disequal */\r
void assertDisequal( Node a, Node b );\r
+ /** needs check */\r
+ bool needsCheck( Theory::Effort level );\r
/** reset round */\r
void reset_round( Theory::Effort level );\r
/** check */\r
- void check( Theory::Effort level );\r
- /** needs check */\r
- bool needsCheck( Theory::Effort level );\r
+ void check( Theory::Effort level, unsigned quant_e );\r
private:\r
bool d_needs_computeRelEqr;\r
public:\r
//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() ){
}else{
//otherwise, the search will continue
- d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
}
}
}
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 */
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() );
}
}
}
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 );
}
}
}
}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 ) ){
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;
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() ){
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() ){
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() ){
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:
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();
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;
}
}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 ){
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 );
}
}
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++ ){
}
}
+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
}
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;
}
}
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 ){
/* 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;
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;
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;
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 );
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 */
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:
projects / cvc5.git / commitdiff