//--------------------model checking---------------------------------------
//do exhaustive instantiation
-bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
+int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
if (effort==0) {
FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
d_addedLemmas += lem;
Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl;
}
- return quantValid;
+ return quantValid ? 1 : 0;
+ }else{
+ return 1;
}
- return true;
}
bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {
//process build model
void processBuildModel(TheoryModel* m, bool fullModel);
//do exhaustive instantiation
- bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+ int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
};
}
}
-bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
Assert( !d_qe->inConflict() );
if( optUseModel() ){
if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){
//something went wrong, resort to exhaustive instantiation
- return false;
+ return 0;
}
}
}
}
}
- return true;
+ return 1;
}else{
- return false;
+ return 0;
}
}
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
- bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+ int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
}
}
+bool InstStrategyCbqi::checkCompleteFor( Node q ) {
+ std::map< Node, int >::iterator it = d_do_cbqi.find( q );
+ if( it!=d_do_cbqi.end() ){
+ return it->second>0;
+ }else{
+ return false;
+ }
+}
+
Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
std::map< Node, Node >::iterator it = visited.find( n );
if( it==visited.end() ){
void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
- if( !options::cbqiAll() ){
+ if( d_do_cbqi[q]==2 ){
//take full ownership of the quantified formula
d_quantEngine->setOwner( q, this );
}
bool InstStrategyCbqi::doCbqi( Node q ){
- std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
+ std::map< Node, int >::iterator it = d_do_cbqi.find( q );
if( it==d_do_cbqi.end() ){
- bool ret = true;
+ int ret = 2;
if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
//if has an instantiation pattern, don't do it
if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
if( q[2][i].getKind()==INST_PATTERN ){
- ret = false;
+ ret = 0;
}
}
}
- if( ret ){
- if( options::cbqiAll() ){
- ret = true;
- }else{
- //if quantifier has a non-handled variable, then do not use cbqi
- //if quantifier has an APPLY_UF term, then do not use cbqi
- //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
- int ncbqiv = hasNonCbqiVariable( q );
- if( ncbqiv==1 ){
- //all variables imply this will be handled regardless of body (e.g. for EPR)
- ret = true;
- }else if( ncbqiv==0 ){
- std::map< Node, bool > visited;
- ret = !hasNonCbqiOperator( q[1], visited );
- }else{
- ret = false;
+ if( ret!=0 ){
+ //if quantifier has a non-handled variable, then do not use cbqi
+ //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
+ int ncbqiv = hasNonCbqiVariable( q );
+ if( ncbqiv==0 || ncbqiv==1 ){
+ std::map< Node, bool > visited;
+ if( hasNonCbqiOperator( q[1], visited ) ){
+ if( ncbqiv==1 ){
+ //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR)
+ // so, try but not exclusively
+ ret = 1;
+ }else{
+ //cannot be handled
+ ret = 0;
+ }
}
+ }else{
+ // unhandled variable type
+ ret = 0;
+ }
+ if( ret==0 && options::cbqiAll() ){
+ //try but not exclusively
+ ret = 1;
}
}
}
Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
d_do_cbqi[q] = ret;
- return ret;
+ return ret!=0;
}else{
- return it->second;
+ return it->second!=0;
}
}
std::map< Node, bool > d_active_quant;
/** whether we have instantiated quantified formulas */
//NodeSet d_added_inst;
- /** whether to do cbqi for this quantified formula */
- std::map< Node, bool > d_do_cbqi;
+ /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */
+ std::map< Node, int > d_do_cbqi;
/** register ce lemma */
bool registerCbqiLemma( Node q );
virtual void registerCounterexampleLemma( Node q, Node lem );
void reset_round( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
bool checkComplete();
+ bool checkCompleteFor( Node q );
void preRegisterQuantifier( Node q );
void registerQuantifier( Node q );
/** get next decision request */
}
}
-bool InstantiationEngine::checkComplete() {
- if( !options::finiteModelFind() ){
- for( unsigned i=0; i<d_quants.size(); i++ ){
- if( isIncomplete( d_quants[i] ) ){
- return false;
- }
- }
- }
- return true;
-}
-
-bool InstantiationEngine::isIncomplete( Node q ) {
- return true;
+bool InstantiationEngine::checkCompleteFor( Node q ) {
+ //TODO?
+ return false;
}
void InstantiationEngine::preRegisterQuantifier( Node q ) {
bool needsCheck( Theory::Effort e );
void reset_round( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
- bool checkComplete();
+ bool checkCompleteFor( Node q );
void preRegisterQuantifier( Node q );
void registerQuantifier( Node q );
Node explain(TNode n){ return Node::null(); }
void check( Theory::Effort e, unsigned quant_e );
/* Called for new quantifiers */
void registerQuantifier( Node q ) {}
+ /* check complete */
+ bool checkComplete() { return !d_wasInvoked; }
void assertNode( Node n ) {}
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const { return "LtePartialInst"; }
//do exhaustive instantiation
-bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
if( optUseModel() ){
RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
if( riter.setQuantifier( f ) ){
}
}
//if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- d_incomplete_check = riter.isIncomplete();
- return true;
+ return riter.isIncomplete() ? -1 : 1;
}else{
- return false;
+ return 0;
}
}
virtual ~QModelBuilder() throw() {}
// is quantifier active?
virtual bool isQuantifierActive( Node f );
- //do exhaustive instantiation
- virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
+ //do exhaustive instantiation
+ // 0 : failed, but resorting to true exhaustive instantiation may work
+ // >0 : success
+ // <0 : failed
+ virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
//whether to construct model
virtual bool optUseModel();
/** number of lemmas generated while building model */
- //is the exhaustive instantiation incomplete?
- bool d_incomplete_check;
int d_addedLemmas;
int d_triedLemmas;
/** exist instantiation ? */
// is quantifier active?
bool isQuantifierActive( Node f );
//do exhaustive instantiation
- bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+ int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
//temporary stats
int d_numQuantSat;
}
if( addedLemmas==0 ){
- Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
+ Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl;
//CVC4 will answer SAT or unknown
if( Trace.isOn("fmf-consistent") ){
Trace("fmf-consistent") << std::endl;
return !d_incomplete_check;
}
+bool ModelEngine::checkCompleteFor( Node q ) {
+ return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end();
+}
+
void ModelEngine::registerQuantifier( Node f ){
if( Trace.isOn("fmf-warn") ){
bool canHandle = true;
// FMC uses two sub-effort levels
int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
for( int e=0; e<e_max; e++) {
+ d_incomplete_quants.clear();
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i, true );
- Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
+ Node q = fm->getAssertedQuantifier( i, true );
+ Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
//determine if we should check this quantifier
- if( considerQuantifiedFormula( f ) ){
- exhaustiveInstantiate( f, e );
+ if( considerQuantifiedFormula( q ) ){
+ exhaustiveInstantiate( q, e );
if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
break;
}
}else{
- Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
+ Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
}
}
if( d_addedLemmas>0 ){
quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
mb->d_triedLemmas = 0;
mb->d_addedLemmas = 0;
- mb->d_incomplete_check = false;
- if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
- Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
+ int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
+ if( retEi!=0 ){
+ if( retEi<0 ){
+ Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
+ d_incomplete_quants.push_back( f );
+ }else{
+ Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
+ }
d_triedLemmas += mb->d_triedLemmas;
d_addedLemmas += mb->d_addedLemmas;
- d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
}else{
if( Trace.isOn("fmf-exh-inst-debug") ){
Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
}
//if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- d_incomplete_check = d_incomplete_check || riter.isIncomplete();
+ if( riter.isIncomplete() ){
+ d_incomplete_quants.push_back( f );
+ }
}
}
//temporary statistics
//is the exhaustive instantiation incomplete?
bool d_incomplete_check;
+ // set of quantified formulas for which check was incomplete
+ std::vector< Node > d_incomplete_quants;
int d_addedLemmas;
int d_triedLemmas;
int d_totalLemmas;
void reset_round( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
bool checkComplete();
+ bool checkCompleteFor( Node q );
void registerQuantifier( Node f );
void assertNode( Node f );
Node explain(TNode n){ return Node::null(); }
return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
}
+bool QuantDSplit::checkCompleteFor( Node q ) {
+ // true if we split q
+ return d_added_split.find( q )!=d_added_split.end();
+}
+
/* Call during quantifier engine's check */
void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
//add lemmas ASAP (they are a reduction)
/* Called for new quantifiers */
void registerQuantifier( Node q ) {}
void assertNode( Node n ) {}
+ bool checkCompleteFor( Node q );
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const { return "QuantDSplit"; }
};
for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
TypeNode tn = n[0][i].getType();
if( d_non_epr.find( tn )==d_non_epr.end() ){
- Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested quantification." << std::endl;
+ Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested or possible existential quantification." << std::endl;
d_non_epr[tn] = true;
}
}
virtual void reset_round( Theory::Effort e ){}
/* Call during quantifier engine's check */
virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
- /* check was complete (e.g. no lemmas implies a model) */
+ /* check was complete, return false if there is no way to answer "SAT", true if maybe can answer "SAT" */
virtual bool checkComplete() { return true; }
+ /* check was complete for quantified formula q (e.g. no lemmas implies a model) */
+ virtual bool checkCompleteFor( Node q ) { return false; }
/* Called for new quantified formulas */
virtual void preRegisterQuantifier( Node q ) { }
/* Called for new quantifiers after owners are finalized */
}
+bool RewriteEngine::checkCompleteFor( Node q ) {
+ // by semantics of rewrite rules, saturation -> SAT
+ return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end();
+}
+
Node RewriteEngine::getInstConstNode( Node n, Node q ) {
std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
if( it==d_inst_const_node[q].end() ){
void check( Theory::Effort e, unsigned quant_e );
void registerQuantifier( Node f );
void assertNode( Node n );
+ bool checkCompleteFor( Node q );
/** Identify this module */
std::string identify() const { return "RewriteEngine"; }
};
d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
d_modules.push_back( d_sg_gen );
}
- //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules
if( !options::finiteModelFind() || options::fmfInstEngine() ){
d_inst_engine = new quantifiers::InstantiationEngine( this );
d_modules.push_back( d_inst_engine );
d_conflict = false;
d_hasAddedLemma = false;
bool setIncomplete = false;
- if( e==Theory::EFFORT_LAST_CALL ){
- //sources of incompleteness
- if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){
- Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl;
- setIncomplete = true;
- }
- }
bool usedModelBuilder = false;
Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
}
}else if( quant_e==QEFFORT_MODEL ){
if( e==Theory::EFFORT_LAST_CALL ){
+ //sources of incompleteness
if( !d_recorded_inst.empty() ){
+ Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl;
setIncomplete = true;
}
//if we have a chance not to set incomplete
if( !setIncomplete ){
setIncomplete = false;
//check if we should set the incomplete flag
- for( unsigned i=0; i<qm.size(); i++ ){
- if( !qm[i]->checkComplete() ){
- Trace("quant-engine-debug") << "Set incomplete because " << qm[i]->identify().c_str() << " was incomplete." << std::endl;
+ for( unsigned i=0; i<d_modules.size(); i++ ){
+ if( !d_modules[i]->checkComplete() ){
+ Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl;
setIncomplete = true;
break;
}
}
+ if( !setIncomplete ){
+ //look at individual quantified formulas, one module must claim completeness for each one
+ for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
+ bool hasCompleteM = false;
+ Node q = d_model->getAssertedQuantifier( i );
+ QuantifiersModule * qmd = getOwner( q );
+ if( qmd!=NULL ){
+ hasCompleteM = qmd->checkCompleteFor( q );
+ }else{
+ for( unsigned j=0; j<d_modules.size(); j++ ){
+ if( d_modules[j]->checkCompleteFor( q ) ){
+ qmd = d_modules[j];
+ hasCompleteM = true;
+ break;
+ }
+ }
+ }
+ if( !hasCompleteM ){
+ Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
+ setIncomplete = true;
+ break;
+ }else{
+ Assert( qmd!=NULL );
+ Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
+ }
+ }
+ }
}
//if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
if( !setIncomplete ){
projects / cvc5.git / commitdiff