diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-05 19:56:42 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-05 19:56:42 +0200 |
commit | ba56661b4a49d4b470c6298d3531324b3bf15005 (patch) | |
tree | 6dee0cde13ab4e86a6bde22bf130e1d3f70c2a6f /src/theory | |
parent | 69769dae4886621f82c2905b82db727bf2e8cf3f (diff) |
Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching. Avoid unecessary delta lemmas. Update casc scripts.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 28 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 25 |
9 files changed, 76 insertions, 18 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 8e7e3d69c..0a434e4ca 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -538,6 +538,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< d_qe->getOutputChannel().lemma( delta_lem ); } subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); + d_used_delta = true; } } //check if we have already added this instantiation diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index eb99fc4f6..eb33c479e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -71,6 +71,7 @@ public: std::vector< Node > d_vars; //delta Node d_n_delta; + bool d_used_delta; //check : add instantiations based on valuation of d_vars bool check(); // get delta lemmas : on-demand force minimality of d_n_delta diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 941eaf89b..f7dc709d9 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -463,13 +463,17 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE s = Rewriter::rewrite( s ); Trace("var-trigger-matching") << "...got " << s << std::endl; d_eq_class = Node::null(); - d_rm_prev = m.get( d_var_num[0] ).isNull(); - if( !m.set( qe, d_var_num[0], s ) ){ - return false; - }else{ - if( continueNextMatch( f, m, qe ) ){ - return true; + if( s.getType().isSubtypeOf( d_var.getType() ) ){ + d_rm_prev = m.get( d_var_num[0] ).isNull(); + if( !m.set( qe, d_var_num[0], s ) ){ + return false; + }else{ + if( continueNextMatch( f, m, qe ) ){ + return true; + } } + }else{ + Trace("var-trigger-matching") << "Violates type requirement." << std::endl; } } if( d_rm_prev ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index de80146f9..dab32af71 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -126,9 +126,9 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder< } int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ - if( e<2 ){ + if( e<1 ){ return STATUS_UNFINISHED; - }else if( e==2 ){ + }else if( e==1 ){ if( d_quantActive.find( f )!=d_quantActive.end() ){ //the point instantiation InstMatch m_point( f ); @@ -373,9 +373,9 @@ void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { - if( e<2 ){ + if( e<1 ){ return STATUS_UNFINISHED; - }else if( e==2 ){ + }else if( e==1 ){ CegInstantiator * cinst; std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f ); if( it==d_cinst.end() ){ @@ -417,10 +417,11 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; bool addedLemma = cinst->check(); + d_used_delta = d_used_delta || cinst->d_used_delta; d_curr_quant = Node::null(); return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; - }else if( e==3 ){ - if( d_check_delta_lemma_lc ){ + }else if( e==2 ){ + if( d_check_delta_lemma_lc && d_used_delta ){ d_check_delta_lemma_lc = false; d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub ); d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub ); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 13e8cf54b..d59690c84 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -104,6 +104,7 @@ private: Node d_curr_quant; bool d_check_delta_lemma; bool d_check_delta_lemma_lc; + bool d_used_delta; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 231392a9a..ce7f01328 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -57,6 +57,9 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions +# Whether to CNF quantifier bodies +option elimTautQuant --elim-taut-quant bool :default true + eliminate tautological disjuncts of quantified formulas #### E-matching options @@ -83,6 +86,8 @@ option purifyDtTriggers --purify-dt-triggers bool :default false :read-write purify dt triggers, match all constructors of correct form instead of selectors option pureThTriggers --pure-th-triggers bool :default false :read-write use pure theory terms as single triggers +option partialTriggers --partial-triggers bool :default false :read-write + use triggers that do not contain all free variables option multiTriggerWhenSingle --multi-trigger-when-single bool :default false select multi triggers when single triggers exist option multiTriggerPriority --multi-trigger-priority bool :default false @@ -250,7 +255,7 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false ### reduction options -option quantAlphaEquiv --quant-alpha-equiv bool :default false +option quantAlphaEquiv --quant-alpha-equiv bool :default true infer alpha equivalence between quantified formulas endmodule diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 07aa89ece..0198e014f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -774,6 +774,30 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } } +Node QuantifiersRewriter::computeElimTaut( Node body ) { + if( body.getKind()==OR ){ + std::vector< Node > children; + std::map< Node, bool > lit_pol; + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node lit = body[i].getKind()==NOT ? body[i][0] : body[i]; + bool pol = body[i].getKind()!=NOT; + std::map< Node, bool >::iterator it = lit_pol.find( lit ); + if( it==lit_pol.end() ){ + lit_pol[lit] = pol; + children.push_back( body[i] ); + }else{ + if( it->second!=pol ){ + return NodeManager::currentNM()->mkConst( true ); + } + } + } + if( children.size()!=body.getNumChildren() ){ + return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + } + } + return body; +} + Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) { if( body.getKind()==OR ){ size_t var_found_count = 0; @@ -1104,6 +1128,8 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption return options::iteDtTesterSplitQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + return options::elimTautQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant() || options::dtVarExpandQuant(); }else if( computeOption==COMPUTE_CNF ){ @@ -1144,6 +1170,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp n = computeProcessIte2( n ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + n = computeElimTaut( n ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ Node prev; do{ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 201a03737..d01677171 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -51,6 +51,7 @@ private: static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); + static Node computeElimTaut( Node body ); static Node computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ @@ -61,6 +62,7 @@ private: COMPUTE_PROCESS_ITE, COMPUTE_PROCESS_ITE_2, COMPUTE_PRENEX, + COMPUTE_ELIM_TAUT, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, COMPUTE_CNF, diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c55ed27ea..e4d9a2730 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -145,7 +145,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& break; } } - if( varCount<f[0].getNumChildren() ){ + if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){ Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; for( unsigned i=0; i<nodes.size(); i++) { Trace("trigger-debug") << nodes[i] << " "; @@ -226,6 +226,12 @@ bool Trigger::isUsable( Node n, Node f ){ if( isBooleanTermTrigger( n ) ){ return true; } + if( options::purifyTriggers() ){ + Node x = getInversionVariable( n ); + if( !x.isNull() ){ + return true; + } + } } return false; }else{ @@ -247,6 +253,7 @@ bool nodeContainsVar( Node n, Node v ){ } Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { + Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl; if( options::relationalTriggers() ){ if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ Node rtr; @@ -287,7 +294,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { } } bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); - Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; + Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; if( usable ){ return n; }else{ @@ -512,13 +519,16 @@ Node Trigger::getInversionVariable( Node n ) { if( !n[i].isConst() ){ Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl; return Node::null(); - }else if( n.getType().isInteger() ){ + } + /* + else if( n.getType().isInteger() ){ Rational r = n[i].getConst<Rational>(); if( r!=Rational(-1) && r!=Rational(1) ){ Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl; return Node::null(); } } + */ } } return ret; @@ -539,8 +549,13 @@ Node Trigger::getInversion( Node n, Node x ) { x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] ); }else if( n.getKind()==MULT ){ Assert( n[i].isConst() ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() ); - x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + if( x.getType().isInteger() ){ + Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() ); + x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() ); + x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + } } }else{ Assert( cindex==-1 ); |