From 3d82de01011931ee352715ac4f45c7bbc66f2201 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 27 Jan 2015 18:17:27 +0100 Subject: [PATCH] Always miniscope nested quantifiers. Disable miniscoping when cegqi enabled. Simplify option names. --- src/smt/smt_engine.cpp | 7 + .../quantifiers/ce_guided_instantiation.cpp | 8 +- src/theory/quantifiers/options | 16 +- .../quantifiers/quantifiers_rewriter.cpp | 226 ++++++++---------- src/theory/quantifiers/quantifiers_rewriter.h | 11 +- 5 files changed, 117 insertions(+), 151 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 94efd8a75..0be445f57 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1354,6 +1354,13 @@ void SmtEngine::setDefaults() { if( !options::bitvectorDivByZeroConst.wasSetByUser() ){ options::bitvectorDivByZeroConst.set( true ); } + //do not miniscope + if( !options::miniscopeQuant.wasSetByUser() ){ + options::miniscopeQuant.set( false ); + } + if( !options::miniscopeQuantFreeVar.wasSetByUser() ){ + options::miniscopeQuantFreeVar.set( false ); + } } //implied options... diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 71bfcd42b..089fd973e 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -589,7 +589,7 @@ void CegInstantiation::analyzeSygusConjecture( Node q ) { d_single_inv_app_map[q][prog] = sinv; } //construct the single invocation version of the property - Trace("cegqi-analyze") << "Single invocation formula is : " << std::endl; + Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl; std::vector< Node > si_conj; for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ std::vector< Node > tmp; @@ -626,14 +626,14 @@ void CegInstantiation::analyzeSygusConjecture( Node q ) { disj.push_back( cr ); } Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); - Trace("cegqi-analyze-debug") << " " << curr; + Trace("cegqi-analyze") << " " << curr; if( it->first.isNull() ){ si_conj.push_back( curr.negate() ); }else{ tmp.push_back( curr ); Trace("cegqi-analyze-debug") << " under " << it->first; } - Trace("cegqi-analyze-debug") << std::endl; + Trace("cegqi-analyze") << std::endl; } if( !it->first.isNull() ){ Assert( !tmp.empty() ); @@ -644,7 +644,7 @@ void CegInstantiation::analyzeSygusConjecture( Node q ) { } } Node si = si_conj.size()==1 ? si_conj[0] : NodeManager::currentNM()->mkNode( OR, si_conj ); - Trace("cegqi-analyze") << " " << si << std::endl; + Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl; d_single_inv[q] = si; }else{ Trace("cegqi-analyze") << "Property is not single invocation." << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index b47c98aa3..6fc13498c 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -11,13 +11,13 @@ option eMatching --e-matching bool :read-write :default true # Whether to mini-scope quantifiers. # For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to # ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) -option miniscopeQuant /--disable-miniscope-quant bool :default true +option miniscopeQuant --miniscope-quant bool :default true :read-write disable miniscope quantifiers # Whether to mini-scope quantifiers based on formulas with no free variables. # For example, forall x. ( P( x ) V Q ) will be rewritten to # ( forall x. P( x ) ) V Q -option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true +option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write disable miniscope quantifiers for ground subformulas # Whether to prenex (nested universal) quantifiers @@ -27,14 +27,14 @@ option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMod # 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 ) -option varElimQuant /--disable-var-elim-quant bool :default true +option varElimQuant --var-elim-quant bool :default true disable simple variable elimination for quantified formulas option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true split variables occurring as conditions of ITE in quantifiers -option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true +option simpleIteLiftQuant --ite-lift-quant bool :default true disable simple ite lifting for quantified formulas # Whether to CNF quantifier bodies @@ -65,7 +65,7 @@ option foPropQuant --fo-prop-quant bool :default false option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h" which ground terms to consider for instantiation # Whether to use smart triggers -option smartTriggers /--disable-smart-triggers bool :default true +option smartTriggers --smart-triggers bool :default true disable smart triggers # Whether to use relevent triggers option relevantTriggers --relevant-triggers bool :default false @@ -123,7 +123,7 @@ option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode option flipDecision --flip-decision/ bool :default false turns on flip decision heuristic -option internalReps /--disable-quant-internal-reps bool :default true +option internalReps --quant-internal-reps bool :default true disables instantiating with representatives chosen by quantifiers engine option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write @@ -138,13 +138,13 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding -option fmfInstGen /--disable-fmf-inst-gen bool :default true +option fmfInstGen --fmf-inst-gen bool :default true disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques -option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true +option fmfFmcSimple --fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write finite model finding on bounded integer quantification diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 1e6ec3a02..1f15bb797 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -153,31 +153,9 @@ bool QuantifiersRewriter::hasArg1( Node a, Node n ) { } } -void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){ - std::vector< Node > processed; - setNestedQuantifiers2( n, q, processed ); -} - -void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ) { - if( std::find( processed.begin(), processed.end(), n )==processed.end() ){ - processed.push_back( n ); - if( n.getKind()==FORALL || n.getKind()==EXISTS ){ - Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl; - NestedQuantAttribute nqai; - n[0].setAttribute(nqai,q); - } - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - setNestedQuantifiers2( n[i], q, processed ); - } - } -} - RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ - Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl; - if( !in.hasAttribute(NestedQuantAttribute()) ){ - setNestedQuantifiers( in[ 1 ], in ); - } + Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl; std::vector< Node > args; for( int i=0; i<(int)in[0].getNumChildren(); i++ ){ args.push_back( in[0][i] ); @@ -211,7 +189,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { } Node n = NodeManager::currentNM()->mkNode( in.getKind(), children ); if( in!=n ){ - setAttributes( in, n ); Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl; Trace("quantifiers-pre-rewrite") << " to " << std::endl; Trace("quantifiers-pre-rewrite") << n << std::endl; @@ -224,7 +201,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; - Trace("quantifiers-rewrite-debug") << "Attributes : " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl; + Trace("quantifiers-rewrite-debug") << "Attributes : " << std::endl; if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){ RewriteStatus status = REWRITE_DONE; Node ret = in; @@ -250,8 +227,9 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { ret = ret.negate(); status = REWRITE_AGAIN_FULL; }else{ - bool isNested = in[0].hasAttribute(NestedQuantAttribute()); for( int op=0; op& args, NodeBuilder<>& defs, bool forcePred ){ if( isLiteral( n ) ){ return n; @@ -830,7 +798,7 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i } } -Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested ){ +Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){ //Notice() << "rewrite quant " << body << std::endl; if( body.getKind()==FORALL ){ //combine arguments @@ -840,7 +808,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, } newArgs.insert( newArgs.end(), args.begin(), args.end() ); return mkForAll( newArgs, body[ 1 ], ipl ); - }else if( !isNested ){ + }else{ if( body.getKind()==NOT ){ //push not downwards if( body[0].getKind()==NOT ){ @@ -903,108 +871,106 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, //} } -Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){ - if( !isNested ){ - std::map< Node, std::vector< Node > > varLits; - std::map< Node, std::vector< Node > > litVars; - if( body.getKind()==OR ){ - Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl; - for( size_t i=0; i activeArgs; - computeArgVec( args, activeArgs, body[i] ); - for (unsigned j=0; j& args, Node body ){ + std::map< Node, std::vector< Node > > varLits; + std::map< Node, std::vector< Node > > litVars; + if( body.getKind()==OR ){ + Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl; + for( size_t i=0; i activeArgs; + computeArgVec( args, activeArgs, body[i] ); + for (unsigned j=0; j >::iterator it = varLits.begin(); it != varLits.end(); ++it ){ - if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){ - bestVar = it->first; - } + litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() ); + } + //find the variable in the least number of literals + Node bestVar; + for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){ + if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){ + bestVar = it->first; } - Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl; - if( !bestVar.isNull() && varLits[bestVar].size() qlit1; - qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() ); - std::vector< Node > qlitt; - //for all literals not containing bestVar - for( size_t i=0; i qlit1; + qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() ); + std::vector< Node > qlitt; + //for all literals not containing bestVar + for( size_t i=0; i qvl1; - std::vector< Node > qvl2; - std::vector< Node > qvsh; - for( unsigned i=0; i qvl1; + std::vector< Node > qvl2; + std::vector< Node > qvsh; + for( unsigned i=0; i qlitsh; - std::vector< Node > qlit2; - for( size_t i=0; imkNode( OR, qlit1 ); - n1 = computeAggressiveMiniscoping( qvl1, n1 ); - qlitsh.push_back( n1 ); - if( !qlit2.empty() ){ - Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 ); - n2 = computeAggressiveMiniscoping( qvl2, n2 ); - qlitsh.push_back( n2 ); + } + Assert( !qvl1.empty() ); + Assert( !qvl2.empty() || !qvsh.empty() ); + //check for literals that only contain shared variables + std::vector< Node > qlitsh; + std::vector< Node > qlit2; + for( size_t i=0; imkNode( OR, qlitsh ); - if( !qvsh.empty() ){ - Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh); - n = NodeManager::currentNM()->mkNode( FORALL, bvl, n ); + if( hasVar2 ){ + qlit2.push_back( qlitt[i] ); + }else{ + qlitsh.push_back( qlitt[i] ); } - Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl; - return n; } + varLits.clear(); + litVars.clear(); + Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size(); + Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl; + Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 ); + n1 = computeAggressiveMiniscoping( qvl1, n1 ); + qlitsh.push_back( n1 ); + if( !qlit2.empty() ){ + Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 ); + n2 = computeAggressiveMiniscoping( qvl2, n2 ); + qlitsh.push_back( n2 ); + } + Node n = NodeManager::currentNM()->mkNode( OR, qlitsh ); + if( !qvsh.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh); + n = NodeManager::currentNM()->mkNode( FORALL, bvl, n ); + } + Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl; + return n; } } return mkForAll( args, body, Node::null() ); @@ -1068,9 +1034,9 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ //return directly - return computeMiniscoping( f, args, n, ipl, isNested ); + return computeMiniscoping( f, args, n, ipl ); }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ - return computeAggressiveMiniscoping( args, n, isNested ); + return computeAggressiveMiniscoping( args, n ); }else if( computeOption==COMPUTE_NNF ){ n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_ITE ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index badf97c46..7c57c6d60 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -26,10 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// attribute for "contains instantiation constants from" -struct NestedQuantAttributeId {}; -typedef expr::Attribute NestedQuantAttribute; - class QuantifiersRewriter { public: static bool isClause( Node n ); @@ -43,14 +39,11 @@ private: static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); static bool hasArg( std::vector< Node >& args, Node n ); static bool hasArg1( Node a, Node n ); - static void setNestedQuantifiers( Node n, Node q ); - static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ); static Node computeClause( Node n ); - static void setAttributes( Node in, Node n ); private: static Node computeElimSymbols( Node body ); - static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); - static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false ); + static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); + static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); static Node computeProcessIte( Node body, bool hasPol, bool pol ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); -- 2.30.2