From ca1b17c8bba3681643a1a3de19d32b038c38aceb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 12 Sep 2016 15:48:11 -0500 Subject: [PATCH] Refactor prenex modes. --- src/options/options_handler.cpp | 27 ++++++++------ src/options/quantifiers_modes.h | 14 ++++---- src/options/quantifiers_options | 6 ++-- src/smt/smt_engine.cpp | 12 +++++-- .../quantifiers/quantifiers_rewriter.cpp | 36 +++++++++---------- src/theory/quantifiers/quantifiers_rewriter.h | 2 +- 6 files changed, 54 insertions(+), 43 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 8cd651da5..1d7355d9f 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -385,15 +385,18 @@ max \n\ const std::string OptionsHandler::s_prenexQuantModeHelp = "\ Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ \n\ -default \n\ -+ Default, prenex all nested quantifiers except those with user patterns.\n\ -\n\ -all \n\ -+ Prenex all nested quantifiers.\n\ -\n\ none \n\ + Do no prenex nested quantifiers. \n\ \n\ +default | simple \n\ ++ Default, do simple prenexing of same sign quantifiers.\n\ +\n\ +dnorm \n\ ++ Prenex to disjunctive prenex normal form.\n\ +\n\ +norm \n\ ++ Prenex to prenex normal form.\n\ +\n\ "; const std::string OptionsHandler::s_cegqiFairModeHelp = "\ @@ -679,12 +682,14 @@ theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveS } theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default" ) { - return theory::quantifiers::PRENEX_NO_USER_PAT; - } else if(optarg == "all") { - return theory::quantifiers::PRENEX_ALL; + if(optarg== "default" || optarg== "simple" ) { + return theory::quantifiers::PRENEX_QUANT_SIMPLE; } else if(optarg == "none") { - return theory::quantifiers::PRENEX_NONE; + return theory::quantifiers::PRENEX_QUANT_NONE; + } else if(optarg == "dnorm") { + return theory::quantifiers::PRENEX_QUANT_DISJ_NORMAL; + } else if(optarg == "norm") { + return theory::quantifiers::PRENEX_QUANT_NORMAL; } else if(optarg == "help") { puts(s_prenexQuantModeHelp.c_str()); exit(1); diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index fe76f8798..cc6abaa8b 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -123,12 +123,14 @@ enum TriggerActiveSelMode { }; enum CVC4_PUBLIC PrenexQuantMode { - /** default : prenex quantifiers without user patterns */ - PRENEX_NO_USER_PAT, - /** prenex all */ - PRENEX_ALL, - /** prenex none */ - PRENEX_NONE, + /** do not prenex */ + PRENEX_QUANT_NONE, + /** prenex same sign quantifiers */ + PRENEX_QUANT_SIMPLE, + /** aggressive prenex, disjunctive prenex normal form */ + PRENEX_QUANT_DISJ_NORMAL, + /** prenex normal form */ + PRENEX_QUANT_NORMAL, }; enum CegqiFairMode { diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2e9aa00cc..04b918afc 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -19,10 +19,10 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write miniscope quantifiers for ground subformulas option quantSplit --quant-split bool :default true :read-write apply splitting to quantified formulas based on variable disjoint disjuncts -option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode +option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode prenex mode for quantified formulas -option prenexQuantAgg --prenex-quant-agg bool :default false :read-write - aggressive prenexing to ensure prenex normal form +option prenexQuantUser --prenex-quant-user bool :default false :read-write + prenex quantified formulas with user patterns # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to # forall y. P( c, y ) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c9f80c2aa..b7997a204 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1732,7 +1732,7 @@ void SmtEngine::setDefaults() { options::mbqiMode.set( quantifiers::MBQI_NONE ); } if( ! options::prenexQuant.wasSetByUser() ){ - options::prenexQuant.set( quantifiers::PRENEX_NONE ); + options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE ); } } if( options::ufssSymBreak() ){ @@ -1856,8 +1856,14 @@ void SmtEngine::setDefaults() { options::quantConflictFind.set( true ); } if( options::cbqiNestedQE() ){ - options::prenexQuantAgg.set( true ); - //options::prenexSkolemQuant.set( true ); + //only sound with prenex = disj_normal or normal + if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL ){ + options::prenexQuant.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL ); + } + options::prenexQuantUser.set( true ); + if( !options::preSkolemQuant.wasSetByUser() ){ + options::preSkolemQuant.set( true ); + } } //for induction techniques if( options::quantInduction() ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 672cce959..3bf7749a4 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1074,9 +1074,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } -Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ){ +Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){ if( body.getKind()==FORALL ){ - if( ( pol || options::prenexQuantAgg() ) && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ + if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers @@ -1095,16 +1095,16 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s return newBody; } //must remove structure - }else if( options::prenexQuantAgg() && body.getKind()==kind::ITE && body.getType().isBoolean() ){ + }else if( prenexAgg && body.getKind()==kind::ITE && body.getType().isBoolean() ){ Node nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) ); - return computePrenex( nn, args, nargs, pol ); - }else if( options::prenexQuantAgg() && body.getKind()==kind::IFF ){ + return computePrenex( nn, args, nargs, pol, prenexAgg ); + }else if( prenexAgg && body.getKind()==kind::IFF ){ Node nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); - return computePrenex( nn, args, nargs, pol ); + return computePrenex( nn, args, nargs, pol, prenexAgg ); }else if( body.getType().isBoolean() ){ Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; @@ -1114,7 +1114,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); if( newHasPol ){ - Node n = computePrenex( body[i], args, nargs, newPol ); + Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg ); newChildren.push_back( n ); if( n!=body[i] ){ childrenChanged = true; @@ -1136,7 +1136,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ if( containsQuantifiers( n ) ){ - if( topLevel && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ + if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ std::vector< Node > children; for( unsigned i=0; i children; - if( n[1].getKind()==OR ){ + if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){ for( unsigned i=0; i args; std::vector< Node > nargs; - Node nn = computePrenex( n, args, nargs, true ); + Node nn = computePrenex( n, args, nargs, true, true ); if( n!=nn ){ Node nnn = computePrenexAgg( nn, false ); //merge prenex @@ -1533,7 +1533,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q }else if( computeOption==COMPUTE_COND_SPLIT ){ return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger; }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; + return options::prenexQuant()!=PRENEX_QUANT_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() ) && is_std; }else{ @@ -1552,9 +1552,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut if( computeOption==COMPUTE_ELIM_SYMBOLS ){ n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ - if( options::prenexQuantAgg() ){ - //if( isPrenexNormalForm( n ) ){ + if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ if( !qa.d_qid_num.isNull() ){ + //already processed this, return self return f; } } @@ -1572,14 +1572,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut }else if( computeOption==COMPUTE_COND_SPLIT ){ n = computeCondSplit( n, qa ); }else if( computeOption==COMPUTE_PRENEX ){ - if( options::prenexQuantAgg() ){ - //Node pf = computePrenexAgg( f ); - //Assert( isPrenexNormalForm( pf ) ); - //will do it at preprocess time + if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ + //will rewrite at preprocess time return f; }else{ std::vector< Node > nargs; - n = computePrenex( n, args, nargs, true ); + n = computePrenex( n, args, nargs, true, false ); Assert( nargs.empty() ); } }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ @@ -1823,7 +1821,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } } //pull all quantifiers globally - if( options::prenexQuantAgg() ){ + 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 ); n = Rewriter::rewrite( n ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2423caaee..90a22f4b7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -59,7 +59,7 @@ public: //cache is dependent upon currCond, icache is not, new_conds are negated conditions 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 computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); 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 ); -- 2.30.2