--- /dev/null
+#!/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
+
--- /dev/null
+#!/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
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
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
#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;
}else{
Assert( d_conj->d_quant==q );
}
+ }else{
+ Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
}
}
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;
}
}
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{
}
}
+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;
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 );
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 ){
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;
}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
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...
}
}
-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 );
// 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 );
//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 );
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 ) {
projects / cvc5.git / commitdiff