From: ajreynol Date: Sat, 3 Sep 2016 18:03:31 +0000 (-0500) Subject: Option for prenex normal form X-Git-Tag: cvc5-1.0.0~6028^2~62 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9aaa7ca741199f73e70149f8309cd7cd9a12e69f;p=cvc5.git Option for prenex normal form --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index f99333de2..462995bec 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -17,10 +17,12 @@ option miniscopeQuant --miniscope-quant bool :default true :read-write # ( forall x. P( x ) ) V Q option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write miniscope quantifiers for ground subformulas -option quantSplit --quant-split bool :default true +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 prenex mode for quantified formulas +option prenexQuantAgg --prenex-quant-agg bool :default false :read-write + aggressive prenexing to ensure prenex normal form # 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 76a1e72c3..8a636c85e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1858,6 +1858,9 @@ void SmtEngine::setDefaults() { if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } + if( options::cbqiNestedQE() ){ + options::prenexQuantAgg.set( true ); + } //for induction techniques if( options::quantInduction() ){ if( !options::dtStcInduction.wasSetByUser() ){ @@ -3951,7 +3954,7 @@ void SmtEnginePrivate::processAssertions() { } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; - + dumpAssertions("pre-skolem-quant", d_assertions); //remove rewrite rules, apply pre-skolemization to existential quantifiers for (unsigned i = 0; i < d_assertions.size(); ++ i) { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 2c0e0a32f..814b276d3 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -143,7 +143,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { //record these as counterexample quantifiers QAttributes qa; TermDb::computeQuantAttributes( quants[i], qa ); - if( qa.d_qid_num!=-1 ){ + if( !qa.d_qid_num.isNull() ){ d_id_to_ce_quant[ qa.d_qid_num ] = quants[i]; d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num; Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl; @@ -292,7 +292,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis if( n.getKind()==FORALL ){ QAttributes qa; TermDb::computeQuantAttributes( n, qa ); - if( qa.d_qid_num==-1 ){ + if( qa.d_qid_num.isNull() ){ std::vector< Node > rc; rc.push_back( n[0] ); rc.push_back( getIdMarkedQuantNode( n[1], visited ) ); @@ -403,9 +403,9 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi if( n.getKind()==FORALL ){ QAttributes qa; TermDb::computeQuantAttributes( n, qa ); - if( qa.d_qid_num!=-1 ){ + if( !qa.d_qid_num.isNull() ){ //if it has an id, check whether we have done quantifier elimination for this id - std::map< int, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); + std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); if( it!=d_id_to_ce_quant.end() ){ Node ceq = it->second; bool doNestedQe = d_elim_quants.contains( ceq ); @@ -998,7 +998,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { return true; }else{ //this should never happen for monotonic selection strategies - Trace("cbqi-warn") << "Existing instantiation" << std::endl; + Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl; Assert( !options::cbqiNestedQE() || options::cbqiAll() ); return false; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index eb80de3ce..e88842822 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -71,8 +71,8 @@ protected: //mark ids on quantifiers Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ); // id to ce quant - std::map< int, Node > d_id_to_ce_quant; - std::map< Node, int > d_ce_quant_to_id; + std::map< Node, Node > d_id_to_ce_quant; + std::map< Node, Node > d_ce_quant_to_id; //do nested quantifier elimination recursive Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ); Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index b0718699e..24a6b78b0 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, bool pol ){ +Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ){ if( body.getKind()==FORALL ){ - if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ + if( ( pol || options::prenexQuantAgg() ) && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers @@ -1085,14 +1085,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b terms.push_back( body[0][i] ); subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); } - args.insert( args.end(), subs.begin(), subs.end() ); + if( pol ){ + args.insert( args.end(), subs.begin(), subs.end() ); + }else{ + nargs.insert( nargs.end(), subs.begin(), subs.end() ); + } Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); return newBody; - }else{ - return body; } - }else{ + //must remove structure + }else if( options::prenexQuantAgg() && 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 ){ + 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 ); + }else if( body.getType().isBoolean() ){ Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; std::vector< Node > newChildren; @@ -1101,7 +1114,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); if( newHasPol ){ - Node n = computePrenex( body[i], args, newPol ); + Node n = computePrenex( body[i], args, nargs, newPol ); newChildren.push_back( n ); if( n!=body[i] ){ childrenChanged = true; @@ -1116,10 +1129,61 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b }else{ return NodeManager::currentNM()->mkNode( body.getKind(), newChildren ); } + } + } + return body; +} + +Node QuantifiersRewriter::computePrenexAgg( Node n ){ + if( containsQuantifiers( n ) ){ + if( n.getKind()==NOT ){ + return computePrenexAgg( n[0] ).negate(); + }else if( n.getKind()==FORALL ){ + Node nn = computePrenexAgg( n[1] ); + if( nn!=n[1] ){ + if( n.getNumChildren()==2 ){ + return NodeManager::currentNM()->mkNode( FORALL, n[0], nn ); + }else{ + return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] ); + } + } }else{ - return body; + std::vector< Node > args; + std::vector< Node > nargs; + Node nn = computePrenex( n, args, nargs, true ); + if( n!=nn ){ + Node nnn = computePrenexAgg( nn ); + //merge prenex + if( nnn.getKind()==FORALL ){ + for( unsigned i=0; i& args, Node body, QAttributes& qa ) { @@ -1237,6 +1301,26 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri return NodeManager::currentNM()->mkNode( kind::FORALL, children ); } } +Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, bool marked ) { + if( args.empty() ){ + return body; + }else{ + std::vector< Node > children; + children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); + children.push_back( body ); + std::vector< Node > iplc; + if( marked ){ + Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); + QuantIdNumAttribute ida; + avar.setAttribute(ida,0); + iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); + } + if( !iplc.empty() ){ + children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) ); + } + return NodeManager::currentNM()->mkNode( FORALL, children ); + } +} //computes miniscoping, also eliminates variables that do not occur free in body Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){ @@ -1423,7 +1507,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q //general method for computing various rewrites Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){ - Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl; + Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl; std::vector< Node > args; for( unsigned i=0; i nargs; + n = computePrenex( n, args, nargs, true ); + Assert( nargs.empty() ); + } }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ n = computeVarElimination( n, args, qa ); } @@ -1592,6 +1691,15 @@ bool QuantifiersRewriter::containsQuantifiers( Node n ){ return cq; } } +bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { + if( n.getKind()==FORALL ){ + return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] ); + }else if( n.getKind()==NOT ){ + return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] ); + }else{ + return !containsQuantifiers( n ); + } +} Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){ Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; @@ -1677,6 +1785,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } } } + //pull all quantifiers globally + if( options::prenexQuantAgg() ){ + n = quantifiers::QuantifiersRewriter::computePrenexAgg( n ); + Assert( isPrenexNormalForm( n ) ); + } if( n!=prev ){ Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; Trace("quantifiers-preprocess") << "..returned " << n << std::endl; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 60dc8ab10..bb352f65c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -38,7 +38,6 @@ public: private: static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); - static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); @@ -53,14 +52,15 @@ private: static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ); static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ); -private: +public: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); //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, bool pol ); + static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ); + static Node computePrenexAgg( Node n ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); private: @@ -89,8 +89,11 @@ private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector& fvs); public: static Node rewriteRewriteRule( Node r ); - static bool containsQuantifiers(Node n); + static bool containsQuantifiers( Node n ); + static bool isPrenexNormalForm( Node n ); static Node preprocess( Node n, bool isInst = false ); + static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); + static Node mkForall( std::vector< Node >& args, Node body, bool marked = false ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index f253d655b..e7b7268b5 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -2170,8 +2170,8 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ //don't set owner, should happen naturally } if( avar.hasAttribute(QuantIdNumAttribute()) ){ - qa.d_qid_num = avar.getAttribute(QuantIdNumAttribute()); - Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num << " : " << q << std::endl; + qa.d_qid_num = avar; + Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl; } if( avar.getKind()==REWRITE_RULE ){ Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; @@ -2265,9 +2265,19 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) { } int TermDb::getQAttrQuantIdNum( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it!=d_qattr.end() ){ + if( !it->second.d_qid_num.isNull() ){ + return it->second.d_qid_num.getAttribute(QuantIdNumAttribute()); + } + } + return -1; +} + +Node TermDb::getQAttrQuantIdNumNode( Node q ) { std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); if( it==d_qattr.end() ){ - return -1; + return Node::null(); }else{ return it->second.d_qid_num; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 29b7b93c6..dd91cde33 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -136,7 +136,7 @@ public: class QAttributes{ public: QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false), - d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false), d_qid_num(-1){} + d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){} ~QAttributes(){} bool d_hasPattern; Node d_rr; @@ -150,7 +150,7 @@ public: bool d_quant_elim; bool d_quant_elim_partial; Node d_ipl; - int d_qid_num; + Node d_qid_num; bool isRewriteRule() { return !d_rr.isNull(); } bool isFunDef() { return !d_fundef_f.isNull(); } }; @@ -551,6 +551,8 @@ public: bool isQAttrQuantElimPartial( Node q ); /** get quant id num */ int getQAttrQuantIdNum( Node q ); + /** get quant id num */ + Node getQAttrQuantIdNumNode( Node q ); /** compute quantifier attributes */ static void computeQuantAttributes( Node q, QAttributes& qa ); };/* class TermDb */