diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-01 12:38:33 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-01 12:38:33 -0500 |
commit | 029fb0427b59cc5251767fff902764eb4bba3771 (patch) | |
tree | 97ef5e9f00bd2734f242a2b0855a0b52036eded0 /src/theory | |
parent | 73a60e60a6036f635e8819c672c227156b351964 (diff) |
Minor optimizations related to cbqi.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 30 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 56 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
5 files changed, 58 insertions, 39 deletions
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; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + //for( unsigned i=0; i<d_quantEngine->getModel()->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; i<nc.getNumChildren(); i++ ){ - Node ncc = computePrenexAgg( nc[i], true ); + Node ncc = computePrenexAgg( nc[i], true, visited ); if( n.getKind()==NOT ){ ncc = ncc.negate(); } children.push_back( ncc ); } - return NodeManager::currentNM()->mkNode( 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<n[1].getNumChildren(); i++ ){ - children.push_back( computePrenexAgg( n[1][i], false ) ); + children.push_back( computePrenexAgg( n[1][i], false, visited ) ); } }else{ - children.push_back( computePrenexAgg( n[1], false ) ); + children.push_back( computePrenexAgg( n[1], false, visited ) ); } std::vector< Node > args; for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ @@ -1182,14 +1188,15 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ children[i] = children[i][1]; } } + // TODO : keep the pattern Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( 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<nnn[0].getNumChildren(); i++ ){ @@ -1213,12 +1220,14 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ if( !args.empty() ){ nnn = mkForall( args, nnn, true ); } - return nnn; + ret = nnn; }else{ Assert( args.empty() ); Assert( nargs.empty() ); } } + visited[tindex][n] = ret; + return ret; } return n; } @@ -1822,7 +1831,8 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { //pull all quantifiers globally if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; - n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true ); + std::map< unsigned, std::map< Node, Node > > 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; i<n.getNumChildren(); i++ ){ - Node c = getSubstitute( n[i], terms ); - cc.push_back( c ); - changed = changed || c!=n[i]; - } - if( changed ){ - Node ret = NodeManager::currentNM()->mkNode( 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; i<n.getNumChildren(); i++ ){ + Node c = getSubstitute( n[i], terms, visited ); + cc.push_back( c ); + changed = changed || c!=n[i]; + } + if( changed ){ + ret = NodeManager::currentNM()->mkNode( 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 */ |