From 54c1208305a7434eb2084572a9c46b82f67fcc6b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Oct 2013 14:23:20 -0500 Subject: [PATCH] performance optimizations for quantifier instantiation --- src/theory/quantifiers_engine.cpp | 94 ++++++++++++++++++------------- src/theory/quantifiers_engine.h | 10 ++-- 2 files changed, 59 insertions(+), 45 deletions(-) diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c14ee01ce..07b0ebea3 100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -283,32 +283,32 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std d_temp_inst_debug[f]++; d_total_inst_count_debug++; Trace("inst") << "*** Instantiate " << f << " with " << std::endl; - uint64_t maxInstLevel = 0; - for( int i=0; i<(int)terms.size(); i++ ){ - if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ - 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()); + //uint64_t maxInstLevel = 0; + if( options::cbqi() ){ + for( int i=0; i<(int)terms.size(); i++ ){ + if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ + 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{ - setInstantiationLevelAttr( terms[i], 0 ); + 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 ); + //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); @@ -326,10 +326,32 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ } } +Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){ + if( n.getKind()==INST_CONSTANT ){ + Debug("check-inst") << "Substitute inst constant : " << n << std::endl; + return terms[n.getAttribute(InstVarNumAttribute())]; + }else if( !quantifiers::TermDb::hasInstConstAttr( n ) ){ + Debug("check-inst") << "No inst const attr : " << n << std::endl; + return n; + }else{ + Debug("check-inst") << "Recurse on : " << n << std::endl; + std::vector< Node > cc; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + cc.push_back( n.getOperator() ); + } + for( unsigned i=0; imkNode( n.getKind(), cc ); + } +} + + 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() ); + Node body; //process partial instantiation if necessary if( d_term_db->d_vars[f].size()!=vars.size() ){ + body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); std::vector< Node > uninst_vars; //doing a partial instantiation, must add quantifier for all uninstantiated variables for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ @@ -341,6 +363,16 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std body = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); Trace("partial-inst") << "Partial instantiation : " << f << std::endl; Trace("partial-inst") << " : " << body << std::endl; + }else{ + //do optimized version + Node icb = d_term_db->getInstConstantBody( f ); + body = doSubstitute( icb, terms ); + if( Debug.isOn("check-inst") ){ + Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( body!=body2 ){ + Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + } + } } return body; } @@ -440,11 +472,7 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ n = Rewriter::rewrite( n ); Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() ); if( addLemma( lem ) ){ - ++(d_statistics.d_splits); Debug("inst") << "*** Add split " << n<< std::endl; - //if( reqPhase ){ - // d_curr_out->requirePhase( n, reqPhasePol ); - //} return true; } return false; @@ -503,12 +531,8 @@ QuantifiersEngine::Statistics::Statistics(): d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), d_instantiations("QuantifiersEngine::Instantiations_Total", 0), - d_max_instantiation_level("QuantifiersEngine::Max_Instantiation_Level", 0), - d_splits("QuantifiersEngine::Total_Splits", 0), - d_total_inst_var("QuantifiersEngine::Vars_Inst", 0), - d_total_inst_var_unspec("QuantifiersEngine::Vars_Inst_Unspecified", 0), - d_inst_unspec("QuantifiersEngine::Unspecified_Inst", 0), d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), + d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), d_lit_phase_req("QuantifiersEngine::lit_phase_req", 0), d_lit_phase_nreq("QuantifiersEngine::lit_phase_nreq", 0), d_triggers("QuantifiersEngine::Triggers", 0), @@ -528,12 +552,8 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_instantiation_rounds); StatisticsRegistry::registerStat(&d_instantiation_rounds_lc); StatisticsRegistry::registerStat(&d_instantiations); - StatisticsRegistry::registerStat(&d_max_instantiation_level); - StatisticsRegistry::registerStat(&d_splits); - StatisticsRegistry::registerStat(&d_total_inst_var); - StatisticsRegistry::registerStat(&d_total_inst_var_unspec); - StatisticsRegistry::registerStat(&d_inst_unspec); StatisticsRegistry::registerStat(&d_inst_duplicate); + StatisticsRegistry::registerStat(&d_inst_duplicate_eq); StatisticsRegistry::registerStat(&d_lit_phase_req); StatisticsRegistry::registerStat(&d_lit_phase_nreq); StatisticsRegistry::registerStat(&d_triggers); @@ -555,12 +575,8 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_instantiation_rounds); StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc); StatisticsRegistry::unregisterStat(&d_instantiations); - StatisticsRegistry::unregisterStat(&d_max_instantiation_level); - StatisticsRegistry::unregisterStat(&d_splits); - StatisticsRegistry::unregisterStat(&d_total_inst_var); - StatisticsRegistry::unregisterStat(&d_total_inst_var_unspec); - StatisticsRegistry::unregisterStat(&d_inst_unspec); StatisticsRegistry::unregisterStat(&d_inst_duplicate); + StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq); StatisticsRegistry::unregisterStat(&d_lit_phase_req); StatisticsRegistry::unregisterStat(&d_lit_phase_nreq); StatisticsRegistry::unregisterStat(&d_triggers); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 8f645afe7..6de13ff3c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -111,7 +111,7 @@ private: /** list of all quantifiers seen */ std::vector< Node > d_quants; /** list of all lemmas produced */ - std::map< Node, bool > d_lemmas_produced; + //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; /** lemmas waiting */ std::vector< Node > d_lemmas_waiting; @@ -187,6 +187,8 @@ private: bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** set instantiation level attr */ void setInstantiationLevelAttr( Node n, uint64_t level ); + /** do substitution */ + Node doSubstitute( Node n, std::vector< Node >& terms ); public: /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); @@ -234,12 +236,8 @@ public: IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; IntStat d_instantiations; - IntStat d_max_instantiation_level; - IntStat d_splits; - IntStat d_total_inst_var; - IntStat d_total_inst_var_unspec; - IntStat d_inst_unspec; IntStat d_inst_duplicate; + IntStat d_inst_duplicate_eq; IntStat d_lit_phase_req; IntStat d_lit_phase_nreq; IntStat d_triggers; -- 2.30.2