diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 17:40:18 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 17:40:18 -0500 |
commit | ce883ca9296c872affb47547304a9ecc0ec5224d (patch) | |
tree | 2e797668f07fa045bde9f1b690e8402fb8238f97 | |
parent | 9aaa7ca741199f73e70149f8309cd7cd9a12e69f (diff) |
Miniscope top level conjunctions for prenex normal form, allow one level miniscoping in prenex normal form.
-rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 54 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 |
4 files changed, 50 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8a636c85e..9c8838113 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1860,6 +1860,7 @@ void SmtEngine::setDefaults() { } if( options::cbqiNestedQE() ){ options::prenexQuantAgg.set( true ); + //options::prenexSkolemQuant.set( true ); } //for induction techniques if( options::quantInduction() ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 814b276d3..3d4b6a333 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -252,7 +252,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ Node q = it->first; - Trace("cbqi") << "CBQI : Process " << q << " at effort " << ee << std::endl; + Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; if( d_nested_qe.find( q )==d_nested_qe.end() ){ process( q, e, ee ); if( d_quantEngine->inConflict() ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 24a6b78b0..672cce959 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1134,12 +1134,23 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s return body; } -Node QuantifiersRewriter::computePrenexAgg( Node n ){ +Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ if( containsQuantifiers( n ) ){ - if( n.getKind()==NOT ){ - return computePrenexAgg( n[0] ).negate(); + if( topLevel && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = computePrenexAgg( n[i], true ); + if( n.getKind()==NOT ){ + nc = nc.negate(); + } + children.push_back( nc ); + } + return NodeManager::currentNM()->mkNode( AND, children ); + }else if( n.getKind()==NOT ){ + return computePrenexAgg( n[0], false ).negate(); }else if( n.getKind()==FORALL ){ - Node nn = computePrenexAgg( n[1] ); + /* + Node nn = computePrenexAgg( n[1], false ); if( nn!=n[1] ){ if( n.getNumChildren()==2 ){ return NodeManager::currentNM()->mkNode( FORALL, n[0], nn ); @@ -1147,12 +1158,37 @@ Node QuantifiersRewriter::computePrenexAgg( Node n ){ return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] ); } } + */ + std::vector< Node > children; + if( n[1].getKind()==OR ){ + for( unsigned i=0; i<n[1].getNumChildren(); i++ ){ + children.push_back( computePrenexAgg( n[1][i], false ) ); + } + }else{ + children.push_back( computePrenexAgg( n[1], false ) ); + } + std::vector< Node > args; + for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ + args.push_back( n[0][i] ); + } + std::vector< Node > nargs; + //for each child, strip top level quant + for( unsigned i=0; i<children.size(); i++ ){ + if( children[i].getKind()==FORALL ){ + for( unsigned j=0; j<children[i][0].getNumChildren(); j++ ){ + args.push_back( children[i][0][j] ); + } + children[i] = children[i][1]; + } + } + Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + return mkForall( args, nb, true ); }else{ std::vector< Node > args; std::vector< Node > nargs; Node nn = computePrenex( n, args, nargs, true ); if( n!=nn ){ - Node nnn = computePrenexAgg( nn ); + Node nnn = computePrenexAgg( nn, false ); //merge prenex if( nnn.getKind()==FORALL ){ for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){ @@ -1770,6 +1806,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return n; } + Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { Node prev = n; if( n.getKind() == kind::REWRITE_RULE ){ @@ -1787,8 +1824,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } //pull all quantifiers globally if( options::prenexQuantAgg() ){ - n = quantifiers::QuantifiersRewriter::computePrenexAgg( n ); - Assert( isPrenexNormalForm( n ) ); + Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; + n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true ); + n = Rewriter::rewrite( n ); + Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; + //Assert( isPrenexNormalForm( n ) ); } if( n!=prev ){ Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index bb352f65c..2423caaee 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 ); - static Node computePrenexAgg( Node n ); + static Node computePrenexAgg( Node n, bool topLevel ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); private: |