From d475d255f3c61380524517cd9b97725dcb0c9c22 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 1 Jul 2015 18:42:43 +0200 Subject: Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-quant. Minor bug fixes for internalReps, alpha equivalence. Update casc 25 FOF script. --- contrib/run-script-casc25-fof | 8 ++++---- contrib/run-script-casc25-tfa | 40 ++++++++++++++++++++++++++++++++++++++++ contrib/run-script-casc25-tff | 40 ---------------------------------------- 3 files changed, 44 insertions(+), 44 deletions(-) create mode 100644 contrib/run-script-casc25-tfa delete mode 100644 contrib/run-script-casc25-tff (limited to 'contrib') diff --git a/contrib/run-script-casc25-fof b/contrib/run-script-casc25-fof index b6bea37dd..7717abe47 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 "$@" $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 --quant-alpha-equiv "$@" $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,13 +25,13 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump --quant-alpha-equiv "$@" $bench } # designed for 300 seconds trywith 15 --relevant-triggers --clause-split --full-saturate-quant trywith 15 --clause-split --no-e-matching --full-saturate-quant -trywith 15 --finite-model-find --quant-cf --sort-inference --uf-ss-fair +trywith 15 --finite-model-find --quant-cf --qcf-all-conflict --sort-inference --uf-ss-fair trywith 5 --trigger-sel=max --full-saturate-quant trywith 5 --relevant-triggers --clause-split --multi-trigger-when-single --full-saturate-quant trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant @@ -39,7 +39,7 @@ trywith 5 --pre-skolem-quant --no-pre-skolem-quant-nested --full-saturate-quant trywith 15 --relevant-triggers --decision=internal --full-saturate-quant trywith 15 --clause-split --no-quant-cf --full-saturate-quant trywith 15 --clause-split --trigger-sel=min --full-saturate-quant -trywith 30 --relevant-triggers --prenex-quant=none --full-saturate-quant +trywith 30 --prenex-quant=none --full-saturate-quant trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev finishwith --term-db-mode=relevant --full-saturate-quant diff --git a/contrib/run-script-casc25-tfa b/contrib/run-script-casc25-tfa new file mode 100644 index 000000000..463b5396e --- /dev/null +++ b/contrib/run-script-casc25-tfa @@ -0,0 +1,40 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc 25 : $bench at $2..." + +# use: trywith [params..] +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --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;; + Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} +function finishwith { + echo "--- Run $@..."; + $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench +} + +trywith 10 --cbqi2 --decision=internal --full-saturate-quant +trywith 10 --relevant-triggers --full-saturate-quant +trywith 10 --cbqi --full-saturate-quant +trywith 30 --qcf-tconstraint --full-saturate-quant +trywith 60 --cbqi --cbqi-recurse --full-saturate-quant +trywith 10 --full-saturate-quant +trywith 10 --no-e-matching --full-saturate-quant +trywith 10 --fmf-bound-int +finishwith --cbqi2 --cbqi-recurse --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc25-tff b/contrib/run-script-casc25-tff deleted file mode 100644 index 9313b7886..000000000 --- a/contrib/run-script-casc25-tff +++ /dev/null @@ -1,40 +0,0 @@ -#!/bin/bash - -cvc4=./cvc4 -bench="$1" - -file=${bench##*/} -filename=${file%.*} - -echo "------- cvc4-tff casc 25 : $bench at $2..." - -# use: trywith [params..] -# to attempt a run. If an SZS ontology result is printed, then -# the run script terminates immediately. Otherwise, this -# function returns normally. -function trywith { - limit=$1; shift; - echo "--- Run $@ at $limit..."; - (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --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;; - Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; - esac; exit 1) - if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi -} -function finishwith { - echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench -} - -trywith 10 --cbqi2 --decision=internal --full-saturate-quant -trywith 10 --relevant-triggers --full-saturate-quant -trywith 10 --cbqi --full-saturate-quant -trywith 30 --qcf-tconstraint --full-saturate-quant -trywith 60 --cbqi --cbqi-recurse --full-saturate-quant -trywith 10 --full-saturate-quant -trywith 10 --no-e-matching --full-saturate-quant -trywith 10 --fmf-bound-int -finishwith --cbqi2 --cbqi-recurse --full-saturate-quant -# echo "% SZS status" "GaveUp for $filename" -- cgit v1.2.3 From 69769dae4886621f82c2905b82db727bf2e8cf3f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 2 Jul 2015 16:54:10 +0200 Subject: On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros-quant in incremental. Update casc TFN script. --- contrib/run-script-casc25-tfn | 5 ++--- src/smt/smt_engine.cpp | 2 +- src/theory/quantifiers/ce_guided_single_inv.cpp | 5 +++-- src/theory/quantifiers/ce_guided_single_inv.h | 2 +- src/theory/quantifiers/conjecture_generator.cpp | 4 ++++ src/theory/quantifiers/inst_strategy_cbqi.cpp | 16 +++++++++++++++- src/theory/quantifiers/inst_strategy_cbqi.h | 2 ++ src/theory/quantifiers/term_database.cpp | 1 + 8 files changed, 29 insertions(+), 8 deletions(-) (limited to 'contrib') diff --git a/contrib/run-script-casc25-tfn b/contrib/run-script-casc25-tfn index d3c5d0344..6888d7b49 100644 --- a/contrib/run-script-casc25-tfn +++ b/contrib/run-script-casc25-tfn @@ -15,7 +15,7 @@ echo "------- cvc4-tfn casc 25 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,11 +25,10 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench } trywith 30 --cbqi2 --decision=internal --full-saturate-quant -trywith 60 --finite-model-find --sort-inference --uf-ss-fair trywith 30 --cbqi --full-saturate-quant trywith 60 --cbqi --cbqi-recurse --full-saturate-quant trywith 60 --fmf-bound-int --macros-quant diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6fdfadbd3..54c97750a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3272,7 +3272,7 @@ void SmtEnginePrivate::processAssertions() { } } dumpAssertions("post-skolem-quant", d_assertions); - if( options::macrosQuant() ){ + if( options::macrosQuant() && !options::incrementalSolving() ){ //quantifiers macro expansion bool success; do{ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 22ffcd278..8e7e3d69c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -706,7 +706,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { */ } -void CegInstantiator::check() { +bool CegInstantiator::check() { for( unsigned r=0; r<2; r++ ){ std::vector< Node > subs; @@ -716,10 +716,11 @@ void CegInstantiator::check() { std::vector< int > subs_typ; //try to add an instantiation if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ - return; + return true; } } Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + return false; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 54f762720..eb99fc4f6 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -72,7 +72,7 @@ public: //delta Node d_n_delta; //check : add instantiations based on valuation of d_vars - void check(); + bool check(); // get delta lemmas : on-demand force minimality of d_n_delta void getDeltaLemmas( std::vector< Node >& lems ); }; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index fdb64f6b0..da3c0cce0 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1717,15 +1717,18 @@ void TermGenEnv::collectSignatureInformation() { for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){ if( !getTermDatabase()->d_op_map[it->first].empty() ){ Node nn = getTermDatabase()->d_op_map[it->first][0]; + Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ bool do_enum = true; //check if we have enumerated ground terms if( nn.getKind()==APPLY_UF ){ + Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl; if( !d_cg->hasEnumeratedUf( nn ) ){ do_enum = false; } } if( do_enum ){ + Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl; d_funcs.push_back( it->first ); for( unsigned i=0; ifirst].push_back( nn[i].getType() ); @@ -1738,6 +1741,7 @@ void TermGenEnv::collectSignatureInformation() { getTermDatabase()->computeUfEqcTerms( it->first ); } } + Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl; } } //shuffle functions diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index cbf0dbbd9..de80146f9 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -369,6 +369,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( q void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { d_check_delta_lemma = true; + d_check_delta_lemma_lc = true; } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { @@ -383,6 +384,9 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" ); Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); d_quantEngine->getOutputChannel().lemma( delta_lem ); + d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); } cinst->d_n_delta = d_n_delta; for( int i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ @@ -412,8 +416,18 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { } Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; - cinst->check(); + bool addedLemma = cinst->check(); d_curr_quant = Node::null(); + return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; + }else if( e==3 ){ + if( d_check_delta_lemma_lc ){ + 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 ); + Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } } return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 586cd492c..13e8cf54b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -100,8 +100,10 @@ private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; Node d_n_delta; + Node d_n_delta_ub; Node d_curr_quant; bool d_check_delta_lemma; + bool d_check_delta_lemma_lc; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 8c99881d6..189866494 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -945,6 +945,7 @@ Node TermDb::getSkolemizedBody( Node f ){ } Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { + Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl; std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); unsigned teIndex; if( it==d_typ_enum_map.end() ){ -- cgit v1.2.3 From ba56661b4a49d4b470c6298d3531324b3bf15005 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 5 Jul 2015 19:56:42 +0200 Subject: 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 +- src/theory/quantifiers/ce_guided_single_inv.cpp | 1 + src/theory/quantifiers/ce_guided_single_inv.h | 1 + src/theory/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 ++++++- src/theory/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(-) (limited to 'contrib') 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 ); -- cgit v1.2.3