From 3d429c1187a2ac7d3270eddbbf5228002ad2740a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 16 Jul 2021 12:04:39 -0500 Subject: [PATCH] Do not exhaustive instantiation when FMF is disabled (#6899) This makes FMF not handle quantified formulas when FMF options are disabled, apart from those marked internal. This is required for combinations of sequences + quantified formulas. --- src/theory/quantifiers/fmf/model_engine.cpp | 55 ++++++++++++++------- src/theory/quantifiers/fmf/model_engine.h | 7 +-- 2 files changed, 42 insertions(+), 20 deletions(-) diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 5eba46657..747b0621f 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -103,7 +103,9 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) } if( addedLemmas==0 ){ - Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl; + Trace("model-engine-debug") + << "No lemmas added, incomplete = " + << (d_incomplete_check || !d_incompleteQuants.empty()) << std::endl; // cvc5 will answer SAT or unknown if( Trace.isOn("fmf-consistent") ){ Trace("fmf-consistent") << std::endl; @@ -124,7 +126,7 @@ bool ModelEngine::checkComplete(IncompleteId& incId) } bool ModelEngine::checkCompleteFor( Node q ) { - return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end(); + return d_incompleteQuants.find(q) == d_incompleteQuants.end(); } void ModelEngine::registerQuantifier( Node f ){ @@ -151,10 +153,6 @@ void ModelEngine::registerQuantifier( Node f ){ } } -void ModelEngine::assertNode( Node f ){ - -} - int ModelEngine::checkModel(){ FirstOrderModel* fm = d_treg.getModel(); @@ -194,7 +192,7 @@ int ModelEngine::checkModel(){ if( Trace.isOn("model-engine") ){ for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this)) + if (fm->isQuantifierActive(f) && shouldProcess(f)) { int totalInst = 1; for( unsigned j=0; jgetNumAssertedQuantifiers(); i++ ){ 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 (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this)) + if (!fm->isQuantifierActive(q)) { - exhaustiveInstantiate( q, e ); - if (d_qstate.isInConflict()) - { - break; - } - }else{ Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl; + continue; + } + if (!shouldProcess(q)) + { + Trace("fmf-exh-inst") << "-> Not processed : " << q << std::endl; + d_incompleteQuants.insert(q); + continue; + } + exhaustiveInstantiate(q, e); + if (d_qstate.isInConflict()) + { + break; } } if( d_addedLemmas>0 ){ @@ -262,7 +266,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int 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 ); + d_incompleteQuants.insert(f); }else{ Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; } @@ -318,7 +322,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round if( riter.isIncomplete() ){ - d_incomplete_quants.push_back( f ); + d_incompleteQuants.insert(f); } } } @@ -348,6 +352,23 @@ void ModelEngine::debugPrint( const char* c ){ } } +bool ModelEngine::shouldProcess(Node q) +{ + if (!d_qreg.hasOwnership(q, this)) + { + return false; + } + // if finite model finding or fmf bound is on, we process everything + if (options::finiteModelFind() || options::fmfBound()) + { + return true; + } + // otherwise, we are only using model-based instantiation for internal + // quantified formulas + QuantAttributes& qattr = d_qreg.getQuantAttributes(); + return qattr.isInternal(q); +} + } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 89150bda4..f818a6362 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -38,8 +38,6 @@ private: //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; @@ -59,15 +57,18 @@ public: bool checkComplete(IncompleteId& incId) override; bool checkCompleteFor(Node q) override; void registerQuantifier(Node f) override; - void assertNode(Node f) override; Node explain(TNode n) { return Node::null(); } void debugPrint(const char* c); /** Identify this module */ std::string identify() const override { return "ModelEngine"; } private: + /** Should we process quantified formula q? */ + bool shouldProcess(Node q); /** Pointer to the model builder of quantifiers engine */ QModelBuilder* d_builder; + /** set of quantified formulas for which check was incomplete */ + std::unordered_set d_incompleteQuants; };/* class ModelEngine */ } // namespace quantifiers -- 2.30.2