diff options
| -rw-r--r-- | contrib/run-script-smtcomp2016 | 108 | ||||
| -rw-r--r-- | contrib/run-script-smtcomp2016-application | 55 | ||||
| -rw-r--r-- | src/options/quantifiers_options | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 62 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 22 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.h | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 17 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 3 |
9 files changed, 259 insertions, 18 deletions
diff --git a/contrib/run-script-smtcomp2016 b/contrib/run-script-smtcomp2016 new file mode 100644 index 000000000..8ac8d5c1d --- /dev/null +++ b/contrib/run-script-smtcomp2016 @@ -0,0 +1,108 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat|unsat) echo "$result"; exit 0;; + esac +} + +# use: finishwith [params..] +# to run cvc4 and let it output whatever it will to stdout. +function finishwith { + $cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench +} + +case "$logic" in + +QF_LRA) + trywith 200 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi + finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp + ;; +QF_LIA) + # same as QF_LRA but add --pb-rewrites + finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + # the following is designed for a run time of 2400s (40 min). + # initial runs 1min + trywith 20 --simplification=none --full-saturate-quant + trywith 20 --no-e-matching --full-saturate-quant + trywith 20 --fs-inst --decision=internal --full-saturate-quant + # trigger selections 2min + trywith 30 --relevant-triggers --full-saturate-quant + trywith 30 --trigger-sel=max --full-saturate-quant + trywith 30 --multi-trigger-when-single --full-saturate-quant + trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant + # other 2min + trywith 30 --pre-skolem-quant --full-saturate-quant + trywith 30 --inst-when=full --full-saturate-quant + trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant + trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant + # finite model find 2min + trywith 30 --finite-model-find + trywith 30 --finite-model-find --uf-ss=no-minimal + trywith 60 --finite-model-find --decision=internal + # long runs 20min + trywith 300 --decision=internal --full-saturate-quant + trywith 300 --term-db-mode=relevant --full-saturate-quant + trywith 300 --fs-inst --full-saturate-quant + trywith 300 --finite-model-find --fmf-inst-engine + # finite model find 1min + trywith 30 --finite-model-find --fmf-bound-int + trywith 30 --finite-model-find --sort-inference + # finish 12min + finishwith --full-saturate-quant + ;; +BV) + trywith 30 --finite-model-find + finishwith --cbqi-all --full-saturate-quant + ;; +LIA|LRA|NIA|NRA) + trywith 30 --full-saturate-quant + trywith 300 --full-saturate-quant --cbqi-min-bounds + trywith 300 --full-saturate-quant --decision=internal + finishwith --full-saturate-quant --cbqi-midpoint + ;; +QF_AUFBV) + trywith 600 + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --repeat-simp + ;; +QF_BV) + exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \ + --threads 2 \ + --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \ + --no-wait-to-join \ + "$bench" + #trywith 10 --bv-eq-slicer=auto --decision=justification + #trywith 60 --decision=justification + #trywith 600 --decision=internal --bitblast-eager + #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 + ;; +QF_AUFNIA) + finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_AUFLIA|QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + finishwith + ;; + +esac + diff --git a/contrib/run-script-smtcomp2016-application b/contrib/run-script-smtcomp2016-application new file mode 100644 index 000000000..750d25187 --- /dev/null +++ b/contrib/run-script-smtcomp2016-application @@ -0,0 +1,55 @@ +#!/bin/bash + +cvc4=./cvc4-application + +read line +if [ "$line" != '(set-option :print-success true)' ]; then + echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2 + exit 1 +fi +echo success +read line +logic=$(expr "$line" : ' *(set-logic *\([A-Z_]*\) *) *$') +if [ -z "$logic" ]; then + echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 + exit 1 +fi +echo success + +function runcvc4 { + # we run in this way for line-buffered input, otherwise memory's a + # concern (plus it mimics what we'll end up getting from an + # application-track trace runner?) + $cvc4 --force-logic="$logic" -L smt2 --print-success --no-checking --no-interactive "$@" <&0- +} + +case "$logic" in + +QF_LRA) + runcvc4 --tear-down-incremental --unconstrained-simp + ;; +QF_LIA) + # same as QF_LRA but add --pb-rewrites + runcvc4 --tear-down-incremental --unconstrained-simp + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + runcvc4 --tear-down-incremental + ;; +BV) + runcvc4 --cbqi-all --tear-down-incremental + ;; +LIA|LRA|NIA|NRA) + runcvc4 --tear-down-incremental + ;; +QF_BV) + runcvc4 --tear-down-incremental --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 + ;; +QF_AUFLIA|QF_AX) + runcvc4 --tear-down-incremental --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + runcvc4 --tear-down-incremental + ;; + +esac diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 9fef0295e..5dc6071ba 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -180,6 +180,8 @@ option instPropagate --inst-prop bool :read-write :default false option qcfEagerTest --qcf-eager-test bool :default true optimization, test qcf instances eagerly +option qcfSkipRd --qcf-skip-rd bool :default false + optimization, skip instances based on possibly irrelevant portions of quantified formulas ### rewrite rules options @@ -251,6 +253,9 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode template mode for sygus invariant synthesis +option sygusEagerUnfold --sygus-eager-unfold bool :default false + eager unfold evaluation functions + # approach applied to general quantified formulas option cbqiSplx --cbqi-splx bool :read-write :default false turns on old implementation of counterexample-based quantifier instantiation diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index d9059a3e6..ad900ee82 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" +#include "prop/prop_engine.h" using namespace CVC4::kind; using namespace std; @@ -291,6 +292,8 @@ void CegInstantiation::registerQuantifier( Node q ) { }else{ Assert( d_conj->d_quant==q ); } + }else{ + Trace("cegqi-debug") << "Register quantifier : " << q << std::endl; } } @@ -317,7 +320,7 @@ Node CegInstantiation::getNextDecisionRequest() { Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl; return req_dec[i]; }else{ - Trace("cegqi-debug") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl; + Trace("cegqi-debug2") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl; } } @@ -426,6 +429,16 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { d_quantEngine->addLemma( lem ); ++(d_statistics.d_cegqi_lemmas_ce); Trace("cegqi-engine") << " ...find counterexample." << std::endl; + //optimization : eagerly unfold applications of evaluation function + if( options::sygusEagerUnfold() ){ + std::vector< Node > eager_lems; + std::map< Node, bool > visited; + getEagerUnfoldLemmas( eager_lems, lem, visited ); + for( unsigned i=0; i<eager_lems.size(); i++ ){ + Trace("cegqi-lemma") << "Cegqi::Lemma : eager unfold : " << eager_lems[i] << std::endl; + d_quantEngine->addLemma( eager_lems[i] ); + } + } } }else{ @@ -589,6 +602,53 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le } } +void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + Trace("cegqi-eager-debug") << "getEagerUnfoldLemmas " << n << std::endl; + visited[n] = true; + if( n.getKind()==APPLY_UF ){ + TypeNode tn = n[0].getType(); + Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl; + if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + Trace("cegqi-eager") << "Unfold eager : " << n << std::endl; + Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( n[0], tn ); + Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl; + std::vector< Node > vars; + std::vector< Node > subs; + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + Assert( var_list.getNumChildren()+1==n.getNumChildren() ); + for( unsigned j=0; j<var_list.getNumChildren(); j++ ){ + vars.push_back( var_list[j] ); + } + for( unsigned j=1; j<n.getNumChildren(); j++ ){ + if( var_list[j-1].getType().isBoolean() ){ + //TODO: remove this case when boolean term conversion is eliminated + Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + subs.push_back( n[j].eqNode( c ) ); + }else{ + subs.push_back( n[j] ); + } + Assert( subs[j-1].getType()==var_list[j-1].getType() ); + } + bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl; + Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl; + Assert( n.getType()==bTerm.getType() ); + Node lem = Rewriter::rewrite( NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bTerm ) ); + lems.push_back( lem ); + } + } + } + if( n.getKind()!=FORALL ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + getEagerUnfoldLemmas( lems, n[i], visited ); + } + } + } +} + void CegInstantiation::printSynthSolution( std::ostream& out ) { if( d_conj->isAssigned() ){ Trace("cegqi-debug") << "Printing synth solution..." << std::endl; diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 57dc31850..81f70d600 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -139,6 +139,8 @@ private: //for enforcing fairness std::map< Node, std::map< int, Node > > d_size_term_lemma; /** get measure lemmas */ void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems ); + /** get eager unfolding */ + void getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ); private: /** check conjecture */ void checkCegConjecture( CegConjecture * conj ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 7bc51dc50..5b5f9fc22 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -34,9 +34,10 @@ using namespace CVC4::theory::quantifiers; struct sortQuantifiersForSymbol { QuantifiersEngine* d_qe; + std::map< Node, Node > d_op_map; bool operator() (Node i, Node j) { - int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() ); - int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() ); + int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[i] ); + int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[j] ); if( nqfsi<nqfsj ){ return true; }else if( nqfsi>nqfsj ){ @@ -325,6 +326,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Node pat = patTermsF[i]; if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){ Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl; + Node mpat = pat; //process the pattern: if it has a required polarity, consider it Assert( tinfo.find( pat )!=tinfo.end() ); int rpol = tinfo[pat].d_reqPol; @@ -363,10 +365,10 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ }else{ if( Trigger::isRelationalTrigger( pat ) ){ //consider both polarities - addPatternToPool( f, pat.negate(), num_fv ); + addPatternToPool( f, pat.negate(), num_fv, mpat ); } } - addPatternToPool( f, pat, num_fv ); + addPatternToPool( f, pat, num_fv, mpat ); } } //tinfo not used below this point @@ -398,12 +400,17 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( options::relevantTriggers() ){ sortQuantifiersForSymbol sqfs; sqfs.d_qe = d_quantEngine; + for( unsigned i=0; i<patTerms.size(); i++ ){ + Assert( d_pat_to_mpat.find( patTerms[i] )!=d_pat_to_mpat.end() ); + Assert( d_pat_to_mpat[patTerms[i]].hasOperator() ); + sqfs.d_op_map[ patTerms[i] ] = d_pat_to_mpat[patTerms[i]].getOperator(); + } //sort based on # occurrences (this will cause Trigger to select rarer symbols) std::sort( patTerms.begin(), patTerms.end(), sqfs ); Debug("relevant-trigger") << "Terms based on relevance: " << std::endl; for( unsigned i=0; i<patTerms.size(); i++ ){ - Debug("relevant-trigger") << " " << patTerms[i] << " ("; - Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; + Debug("relevant-trigger") << " " << patTerms[i] << " from " << d_pat_to_mpat[patTerms[i]] << " ("; + Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_pat_to_mpat[patTerms[i]].getOperator() ) << ")" << std::endl; } } //now, generate the trigger... @@ -462,7 +469,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } -void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) { +void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) { + d_pat_to_mpat[pat] = mpat; unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren(); if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){ d_patTerms[0][q].push_back( pat ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 97d97b10a..e6d993294 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -86,13 +86,14 @@ private: // number of trigger variables per quantifier std::map< Node, unsigned > d_num_trigger_vars; std::map< Node, Node > d_vc_partition[2]; + std::map< Node, Node > d_pat_to_mpat; private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node q, Theory::Effort effort, int e ); /** generate triggers */ void generateTriggers( Node q ); - void addPatternToPool( Node q, Node pat, unsigned num_fv ); + void addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ); void addTrigger( inst::Trigger * tr, Node f ); /** has user patterns */ bool hasUserPatterns( Node q ); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 1365feda9..346807a0e 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -112,14 +112,15 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { //optimization : record variable argument positions for terms that must be matched std::vector< TNode > vars; //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137) - //if( options::qcfSkipRd() ){ - // for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){ - // vars.push_back( d_vars[j] ); - // } - //} - //get all variables that are always relevant - std::map< TNode, bool > visited; - getPropagateVars( p, vars, q[1], false, visited ); + if( options::qcfSkipRd() ){ + for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){ + vars.push_back( d_vars[j] ); + } + }else{ + //get all variables that are always relevant + std::map< TNode, bool > visited; + getPropagateVars( p, vars, q[1], false, visited ); + } for( unsigned j=0; j<vars.size(); j++ ){ Node v = vars[j]; TNode f = p->getTermDatabase()->getMatchOperator( v ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ae9426172..e3cf15c53 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1944,7 +1944,8 @@ Node TermDb::simpleNegate( Node n ){ bool TermDb::isAssoc( Kind k ) { return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || + k==STRING_CONCAT; } bool TermDb::isComm( Kind k ) { |