From 304404e3709ff7e95156c87f65a3e2647d9f3441 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Oct 2012 23:40:29 +0000 Subject: more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code --- src/theory/quantifiers_engine.cpp | 219 +++++++++++++++++++------------------- 1 file changed, 108 insertions(+), 111 deletions(-) (limited to 'src/theory/quantifiers_engine.cpp') diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4e933a511..a44a3ff1f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" -#include "theory/rewriterules/rr_candidate_generator.h" using namespace std; using namespace CVC4; @@ -39,6 +38,7 @@ d_te( te ), d_quant_rel( false ){ //currently do not care about relevance d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); + d_tr_trie = new inst::TriggerTrie; d_hasAddedLemma = false; //the model object @@ -124,18 +124,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } -std::vector QuantifiersEngine::createInstVariable( std::vector & vars ){ - std::vector inst_constant; - inst_constant.reserve(vars.size()); - for( std::vector::const_iterator v = vars.begin(); - v != vars.end(); ++v ){ - //make instantiation constants - Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() ); - inst_constant.push_back( ic ); - }; - return inst_constant; -} - void QuantifiersEngine::registerQuantifier( Node f ){ if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){ d_quants.push_back( f ); @@ -227,6 +215,61 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } } +bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ + Assert( f.getKind()==FORALL ); + Assert( !f.hasAttribute(InstConstantAttribute()) ); + Assert( vars.size()==terms.size() ); + Node body = getInstantiation( f, vars, terms ); + //make the lemma + NodeBuilder<> nb(kind::OR); + nb << f.notNode() << body; + Node lem = nb; + //check for duplication + if( addLemma( lem ) ){ + Trace("inst") << "*** Instantiate " << f << " with " << std::endl; + uint64_t maxInstLevel = 0; + for( int i=0; i<(int)terms.size(); i++ ){ + if( terms[i].hasAttribute(InstConstantAttribute()) ){ + Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; + for( int i=0; i<(int)terms.size(); i++ ){ + Debug("inst") << " " << terms[i] << std::endl; + } + Unreachable("Bad instantiation"); + }else{ + Trace("inst") << " " << terms[i]; + //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); + Trace("inst") << std::endl; + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + } + }else{ + setInstantiationLevelAttr( terms[i], 0 ); + } + } + } + Trace("inst-debug") << "*** Lemma is " << lem << std::endl; + setInstantiationLevelAttr( body, maxInstLevel+1 ); + ++(d_statistics.d_instantiations); + d_statistics.d_total_inst_var += (int)terms.size(); + d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 ); + return true; + }else{ + ++(d_statistics.d_inst_duplicate); + return false; + } +} + +void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ + if( !n.hasAttribute(InstLevelAttribute()) ){ + InstLevelAttribute ila; + n.setAttribute(ila,level); + } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setInstantiationLevelAttr( n[i], level ); + } +} + Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); //process partial instantiation if necessary @@ -272,51 +315,6 @@ bool QuantifiersEngine::addLemma( Node lem ){ } } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ - Assert( f.getKind()==FORALL ); - Assert( !f.hasAttribute(InstConstantAttribute()) ); - Assert( vars.size()==terms.size() ); - Node body = getInstantiation( f, vars, terms ); - //make the lemma - NodeBuilder<> nb(kind::OR); - nb << f.notNode() << body; - Node lem = nb; - //check for duplication - if( addLemma( lem ) ){ - Trace("inst") << "*** Instantiate " << f << " with " << std::endl; - uint64_t maxInstLevel = 0; - for( int i=0; i<(int)terms.size(); i++ ){ - if( terms[i].hasAttribute(InstConstantAttribute()) ){ - Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; - for( int i=0; i<(int)terms.size(); i++ ){ - Debug("inst") << " " << terms[i] << std::endl; - } - Unreachable("Bad instantiation"); - }else{ - Trace("inst") << " " << terms[i]; - //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); - Trace("inst") << std::endl; - if( terms[i].hasAttribute(InstLevelAttribute()) ){ - if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); - } - }else{ - d_term_db->setInstantiationLevelAttr( terms[i], 0 ); - } - } - } - Trace("inst-debug") << "*** Lemma is " << lem << std::endl; - d_term_db->setInstantiationLevelAttr( body, maxInstLevel+1 ); - ++(d_statistics.d_instantiations); - d_statistics.d_total_inst_var += (int)terms.size(); - d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 ); - return true; - }else{ - ++(d_statistics.d_inst_duplicate); - return false; - } -} - bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){ //make sure there are values for each variable we are instantiating m.makeComplete( f, this ); @@ -395,10 +393,8 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ bool nodeChanged = false; if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){ bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] ); - std::vector< Node > children; - children.push_back( nodes[i] ); - children.push_back( NodeManager::currentNM()->mkConst(preq) ); - nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f ); + nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst(preq) ); + d_term_db->setInstantiationConstantAttr( nodes[i], f ); nodeChanged = true; } //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ @@ -416,6 +412,56 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ d_statistics.d_lit_phase_nreq += (int)nodes.size(); } } +/* +EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) { + // Should use skeleton (in order to have the type and the kind + // or any needed other information) instead of only the type + + // TheoryId id = Theory::theoryOf(t); + // inst::EqualityQuery* eq = d_eq_query_arr[id]; + // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; + // else return eq; + + // hack because the generic one is too slow + // TheoryId id = Theory::theoryOf(t); + // if( true || id == theory::THEORY_UF){ + // uf::InstantiatorTheoryUf* ith = static_cast( getInstantiator( theory::THEORY_UF )); + // return new uf::EqualityQueryInstantiatorTheoryUf(ith); + // } + // inst::EqualityQuery* eq = d_eq_query_arr[id]; + // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; + // else return eq; + + + //Currently we use the generic EqualityQuery + return getEqualityQuery(); +} + + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() { + return new GenericCandidateGeneratorClasses(this); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() { + return new GenericCandidateGeneratorClass(this); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) { + // TheoryId id = Theory::theoryOf(t); + // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses(); + // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses(); + // else return eq; + return getRRCanGenClasses(); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) { + // TheoryId id = Theory::theoryOf(t); + // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass(); + // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass(); + // else return eq; + return getRRCanGenClass(); +} +*/ QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), @@ -602,52 +648,3 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N eqc.push_back( a ); } } - -inst::EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) { - /** Should use skeleton (in order to have the type and the kind - or any needed other information) instead of only the type */ - - // TheoryId id = Theory::theoryOf(t); - // inst::EqualityQuery* eq = d_eq_query_arr[id]; - // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; - // else return eq; - - /** hack because the generic one is too slow */ - // TheoryId id = Theory::theoryOf(t); - // if( true || id == theory::THEORY_UF){ - // uf::InstantiatorTheoryUf* ith = static_cast( getInstantiator( theory::THEORY_UF )); - // return new uf::EqualityQueryInstantiatorTheoryUf(ith); - // } - // inst::EqualityQuery* eq = d_eq_query_arr[id]; - // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; - // else return eq; - - - //Currently we use the generic EqualityQuery - return getEqualityQuery(); -} - - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() { - return new GenericCandidateGeneratorClasses(this); -} - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() { - return new GenericCandidateGeneratorClass(this); -} - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) { - // TheoryId id = Theory::theoryOf(t); - // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses(); - // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses(); - // else return eq; - return getRRCanGenClasses(); -} - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) { - // TheoryId id = Theory::theoryOf(t); - // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass(); - // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass(); - // else return eq; - return getRRCanGenClass(); -} -- cgit v1.2.3