From ba56661b4a49d4b470c6298d3531324b3bf15005 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 5 Jul 2015 19:56:42 +0200 Subject: [PATCH] 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. --- contrib/run-script-casc25-fof | 4 +-- contrib/run-script-casc25-tfa | 5 ++-- src/smt/smt_engine.cpp | 2 +- .../quantifiers/ce_guided_single_inv.cpp | 1 + src/theory/quantifiers/ce_guided_single_inv.h | 1 + .../quantifiers/inst_match_generator.cpp | 16 +++++++---- src/theory/quantifiers/inst_strategy_cbqi.cpp | 13 +++++---- src/theory/quantifiers/inst_strategy_cbqi.h | 1 + src/theory/quantifiers/options | 7 ++++- .../quantifiers/quantifiers_rewriter.cpp | 28 +++++++++++++++++++ src/theory/quantifiers/quantifiers_rewriter.h | 2 ++ src/theory/quantifiers/trigger.cpp | 25 +++++++++++++---- 12 files changed, 82 insertions(+), 23 deletions(-) diff --git a/contrib/run-script-casc25-fof b/contrib/run-script-casc25-fof index 7717abe47..26c544062 100755 --- a/contrib/run-script-casc25-fof +++ b/contrib/run-script-casc25-fof @@ -15,7 +15,7 @@ echo "------- cvc4-fof casc 25 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump --quant-alpha-equiv "$@" $bench) 2>/dev/null | + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump --quant-alpha-equiv "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench } # designed for 300 seconds diff --git a/contrib/run-script-casc25-tfa b/contrib/run-script-casc25-tfa index 463b5396e..40ed76df5 100644 --- a/contrib/run-script-casc25-tfa +++ b/contrib/run-script-casc25-tfa @@ -29,11 +29,12 @@ function finishwith { } trywith 10 --cbqi2 --decision=internal --full-saturate-quant -trywith 10 --relevant-triggers --full-saturate-quant +trywith 10 --relevant-triggers --full-saturate-quant --partial-triggers --purify-triggers trywith 10 --cbqi --full-saturate-quant +trywith 10 --cbqi2 --e-matching --partial-triggers --purify-triggers trywith 30 --qcf-tconstraint --full-saturate-quant trywith 60 --cbqi --cbqi-recurse --full-saturate-quant -trywith 10 --full-saturate-quant +trywith 10 --full-saturate-quant --partial-triggers --purify-triggers trywith 10 --no-e-matching --full-saturate-quant trywith 10 --fmf-bound-int finishwith --cbqi2 --cbqi-recurse --full-saturate-quant diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 54c97750a..921583ed2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -771,7 +771,7 @@ void SmtEngine::finishInit() { // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); LogicInfo everything; everything.lock(); - Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, \"all-supported\" logic (below), as some internals might require the use of a logic more general than the input.") + Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.") << SetBenchmarkLogicCommand(everything.getLogicString()); } 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::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(); 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() ); - x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + if( x.getType().isInteger() ){ + Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst() ); + x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst() ); + x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + } } }else{ Assert( cindex==-1 ); -- 2.30.2