From 79ad2d6ec3ebd5c45dce4e13e895d0bed0a6f525 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 24 Jan 2015 19:42:21 +0100 Subject: [PATCH] Variable patterns only look at eligible terms. Minor refactoring of quantifiers check for sat. --- .../quantifiers/candidate_generator.cpp | 2 +- src/theory/quantifiers/quant_util.cpp | 11 +-- src/theory/quantifiers/quant_util.h | 9 +- src/theory/quantifiers/term_database.cpp | 73 +++++++++++----- src/theory/quantifiers/term_database.h | 6 +- src/theory/quantifiers_engine.cpp | 83 ++++++------------- src/theory/quantifiers_engine.h | 2 - 7 files changed, 93 insertions(+), 93 deletions(-) diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 9e3fed20a..7d2544b6f 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -200,7 +200,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { TNode n = (*d_eq); ++d_eq; if( n.getType().isSubtypeOf( d_match_pattern_type ) ){ - TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n ); + TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 ){ nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index ); diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 2a9a764b9..088ba093f 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -257,8 +257,8 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& } -QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_lte_asserts( c ){ - +QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){ + } /** add quantifier */ @@ -278,7 +278,7 @@ bool QuantLtePartialInst::addQuantifier( Node q ) { vars[q[0][i]] = true; } getEligibleInstVars( q[1], vars ); - + //TODO : instantiate only if we would force ground instances? bool doInst = true; for( unsigned i=0; i& lemmas ) { getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, 0 ); Assert( !conj.empty() ); lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); + d_wasInvoked = true; } } } -void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, +void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){ if( index==vars.size() ){ Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index c1c39fa0f..116211bfb 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { class QuantifiersEngine; - + class QuantArith { public: @@ -112,6 +112,9 @@ public: class QuantLtePartialInst { private: + // was this module invoked + bool d_wasInvoked; + //representatives per type std::map< TypeNode, std::vector< Node > > d_reps; // should we instantiate quantifier std::map< Node, bool > d_do_inst; @@ -125,7 +128,7 @@ private: /** reset */ void reset(); /** get instantiations */ - void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, + void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index ); /** get eligible inst variables */ void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); @@ -135,6 +138,8 @@ public: bool addQuantifier( Node q ); /** get instantiations */ void getInstantiations( std::vector< Node >& lemmas ); + /** was invoked */ + bool wasInvoked() { return d_wasInvoked; } }; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index fb28974a9..0f0329a93 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -338,33 +338,60 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { } } -Node TermDb::getHasTermEqc( Node r ) { - if( hasTermCurrent( r ) ){ +bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) { + if( options::lteRestrictInstClosure() ){ + //has to be both in inst closure and in ground assertions + if( !isInstClosure( n ) ){ + Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl; + return false; + } + // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this + if( !hasTermCurrent( n, false ) ){ + Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl; + return false; + } + } + if( options::instMaxLevel()!=-1 ){ + if( n.hasAttribute(InstLevelAttribute()) ){ + int fml = f.isNull() ? -1 : getQAttrQuantInstLevel( f ); + unsigned ml = fml>=0 ? fml : options::instMaxLevel(); + + if( n.getAttribute(InstLevelAttribute())>ml ){ + Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; + return false; + } + }else{ + if( options::instLevelInputOnly() ){ + Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; + return false; + } + } + } + return true; +} + +Node TermDb::getEligibleTermInEqc( TNode r ) { + if( isTermEligibleForInstantiation( r, TNode::null() ) ){ return r; }else{ - /* - if( options::termDbInstClosure() ){ - std::map< Node, Node >::iterator it = d_has_eqc.find( r ); - if( it==d_has_eqc.end() ){ - Node h; - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( h.isNull() && !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - ++eqc_i; - if( hasTermCurrent( n ) ){ - h = n; - } + std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r ); + if( it==d_term_elig_eqc.end() ){ + Node h; + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( h.isNull() && !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + ++eqc_i; + if( hasTermCurrent( n ) ){ + h = n; } - d_has_eqc[r] = h; - return h; - }else{ - return it->second; } + d_term_elig_eqc[r] = h; + return h; + }else{ + return it->second; } - */ - //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc - return Node::null(); } } @@ -404,7 +431,7 @@ void TermDb::reset( Theory::Effort effort ){ //compute has map if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){ d_has_map.clear(); - d_has_eqc.clear(); + d_term_elig_eqc.clear(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 8a20d6b41..eb491d036 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -151,7 +151,7 @@ public: /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ - std::map< Node, Node > d_has_eqc; + std::map< Node, Node > d_term_elig_eqc; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; @@ -184,8 +184,10 @@ public: bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); /** has term */ bool hasTermCurrent( Node n, bool useMode = true ); + /** is term eligble for instantiation? */ + bool isTermEligibleForInstantiation( TNode n, TNode f, bool print = false ); /** get has term eqc */ - Node getHasTermEqc( Node r ); + Node getEligibleTermInEqc( TNode r ); /** is inst closure */ bool isInstClosure( Node r ); //for model basis diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 13822eb98..2cf6002cd 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -286,7 +286,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } - bool defaultBuildModel = false; if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; Trace("quant-engine-debug") << " modules to check : "; @@ -371,19 +370,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } 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 ){ - if( options::produceModels() && !d_model->isModelSet() ){ - defaultBuildModel = true; - } - if( Trace.isOn("inst-per-quant") ){ - for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){ - Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl; - } - } - }else{ + if( d_hasAddedLemma ){ + //debug information if( Trace.isOn("inst-per-quant-round") ){ for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){ Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl; @@ -392,16 +380,29 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; - }else{ - if( e==Theory::EFFORT_LAST_CALL && options::produceModels() ){ - defaultBuildModel = true; - } } - - if( defaultBuildModel ){ - Trace("quant-engine-debug") << "Build the model..." << std::endl; - d_te->getModelBuilder()->buildModel( d_model, true ); - Trace("quant-engine-debug") << "Done building the model." << std::endl; + //SAT case + if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ + if( options::produceModels() && !d_model->isModelSet() ){ + //use default model builder when no module built the model + Trace("quant-engine-debug") << "Build the model..." << std::endl; + d_te->getModelBuilder()->buildModel( d_model, true ); + Trace("quant-engine-debug") << "Done building the model." << std::endl; + } + //check other sources of incompleteness + bool setInc = false; + if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){ + setInc = true; + } + if( setInc ){ + getOutputChannel().setIncomplete(); + } + //output debug stats + if( Trace.isOn("inst-per-quant") ){ + for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){ + Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl; + } + } } } @@ -603,40 +604,6 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ } } -bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) { - if( options::lteRestrictInstClosure() ){ - //has to be both in inst closure and in ground assertions - if( !d_term_db->isInstClosure( n ) ){ - Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl; - return false; - } - // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this - if( !d_term_db->hasTermCurrent( n, false ) ){ - Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl; - return false; - } - } - if( options::instMaxLevel()!=-1 ){ - if( n.hasAttribute(InstLevelAttribute()) ){ - int fml = d_term_db->getQAttrQuantInstLevel( f ); - unsigned ml = fml>=0 ? fml : options::instMaxLevel(); - - if( n.getAttribute(InstLevelAttribute())>ml ){ - Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); - Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; - return false; - } - }else{ - if( options::instLevelInputOnly() ){ - Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; - return false; - } - } - } - return true; -} - - Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){ if( n.getKind()==INST_CONSTANT ){ Debug("check-inst") << "Substitute inst constant : " << n << std::endl; @@ -791,7 +758,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //check based on instantiation level if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ for( unsigned i=0; iisTermEligibleForInstantiation( terms[i], f, true ) ){ return false; } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 14e26f2b6..c533f4cbb 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -282,8 +282,6 @@ public: bool getInstWhenNeedsCheck( Theory::Effort e ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); - /** is term eligble for instantiation? */ - bool isTermEligibleForInstantiation( Node n, Node f, bool print = false ); public: /** get number of quantifiers */ int getNumQuantifiers() { return (int)d_quants.size(); } -- 2.30.2