From 029fb0427b59cc5251767fff902764eb4bba3771 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 1 Jun 2017 12:38:33 -0500 Subject: [PATCH] Minor optimizations related to cbqi. --- contrib/run-script-smtcomp2017 | 12 ++-- src/theory/quantifiers/inst_strategy_cbqi.cpp | 7 ++- .../quantifiers/quantifiers_rewriter.cpp | 30 ++++++---- src/theory/quantifiers/quantifiers_rewriter.h | 2 +- src/theory/quantifiers_engine.cpp | 56 ++++++++++--------- src/theory/quantifiers_engine.h | 2 +- 6 files changed, 66 insertions(+), 43 deletions(-) diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 index 1a9f2400f..6a0ef54b2 100644 --- a/contrib/run-script-smtcomp2017 +++ b/contrib/run-script-smtcomp2017 @@ -81,23 +81,27 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA) # finish 9min finishwith --full-saturate-quant ;; -BV|UFBV) +UFBV) # many problems in UFBV are essentially BV trywith 300 --full-saturate-quant - trywith 300 --finite-model-find + trywith 300 --full-saturate-quant --cbqi --decision=internal + finishwith --finite-model-find + ;; +BV) + trywith 300 --full-saturate-quant finishwith --full-saturate-quant --cbqi --decision=internal ;; LIA|LRA) trywith 30 --full-saturate-quant trywith 300 --full-saturate-quant --cbqi-midpoint trywith 300 --full-saturate-quant --cbqi-nested-qe - finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal ;; NIA|NRA) trywith 30 --full-saturate-quant trywith 300 --full-saturate-quant --nl-ext trywith 300 --full-saturate-quant --cbqi-nested-qe - finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal ;; QF_AUFBV) trywith 600 diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 1f1837740..88f8e2484 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -120,6 +120,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){ d_parent_quant[q].push_back( qi ); d_children_quant[qi].push_back( q ); + Assert( hasAddedCbqiLemma( qi ) ); Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi ); dep.push_back( qi ); dep.push_back( qicel ); @@ -594,8 +595,10 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){ std::map< Node, bool > proc; - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + //for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + for( NodeSet::const_iterator it = d_added_cbqi_lemma.begin(); it != d_added_cbqi_lemma.end(); ++it ){ + Node q = *it; Node d = getNextDecisionRequestProc( q, proc ); if( !d.isNull() ){ priority = 0; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 01352217e..4c395f59d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1134,21 +1134,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s return body; } -Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ +Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ){ + unsigned tindex = topLevel ? 0 : 1; + std::map< Node, Node >::iterator itv = visited[tindex].find( n ); + if( itv!=visited[tindex].end() ){ + return itv->second; + } if( containsQuantifiers( n ) ){ + Node ret = n; if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ std::vector< Node > children; Node nc = n.getKind()==NOT ? n[0] : n; for( unsigned i=0; imkNode( AND, children ); + ret = NodeManager::currentNM()->mkNode( AND, children ); }else if( n.getKind()==NOT ){ - return computePrenexAgg( n[0], false ).negate(); + ret = computePrenexAgg( n[0], false, visited ).negate(); }else if( n.getKind()==FORALL ){ /* Node nn = computePrenexAgg( n[1], false ); @@ -1163,10 +1169,10 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ std::vector< Node > children; if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){ for( unsigned i=0; i args; for( unsigned i=0; imkNode( OR, children ); - return mkForall( args, nb, true ); + ret = mkForall( args, nb, true ); }else{ std::vector< Node > args; std::vector< Node > nargs; Node nn = computePrenex( n, args, nargs, true, true ); if( n!=nn ){ - Node nnn = computePrenexAgg( nn, false ); + Node nnn = computePrenexAgg( nn, false, visited ); //merge prenex if( nnn.getKind()==FORALL ){ for( unsigned i=0; i > visited; + n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited ); n = Rewriter::rewrite( n ); Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; //Assert( isPrenexNormalForm( n ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index c61ca1fb0..bb1d77dfe 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -60,7 +60,7 @@ public: static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); static Node computeCondSplit( Node body, QAttributes& qa ); static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); - static Node computePrenexAgg( Node n, bool topLevel ); + static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); private: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 55b1af83c..501d77ecf 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -933,32 +933,37 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ } } -Node QuantifiersEngine::getSubstitute( 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() ); - } - bool changed = false; - for( unsigned i=0; imkNode( n.getKind(), cc ); - return ret; +Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv==visited.end() ){ + Node ret = n; + if( n.getKind()==INST_CONSTANT ){ + Debug("check-inst") << "Substitute inst constant : " << n << std::endl; + ret = terms[n.getAttribute(InstVarNumAttribute())]; }else{ - return n; + //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() ); + } + bool changed = false; + for( unsigned i=0; imkNode( n.getKind(), cc ); + } } + visited[n] = ret; + return ret; + }else{ + return itv->second; } } @@ -988,7 +993,8 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std }else{ //do optimized version Node icb = d_term_db->getInstConstantBody( q ); - body = getSubstitute( icb, terms ); + std::map< Node, Node > visited; + body = getSubstitute( icb, terms, visited ); if( Debug.isOn("check-inst") ){ Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); if( body!=body2 ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7405241b7..fff446eda 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -315,7 +315,7 @@ public: /** get instantiation */ Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false ); /** do substitution */ - Node getSubstitute( Node n, std::vector< Node >& terms ); + Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); /** remove pending lemma */ -- 2.30.2