From: ajreynol Date: Thu, 12 May 2016 15:13:17 +0000 (-0500) Subject: Add casc scripts. Improvements to qcf related to nested quantifiers and variable... X-Git-Tag: cvc5-1.0.0~6049^2~48 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=411ced2c475e5ccb4c114ce2c77a39bf93d139f4;p=cvc5.git Add casc scripts. Improvements to qcf related to nested quantifiers and variable ordering. --- diff --git a/contrib/run-script-cascj8-fnt b/contrib/run-script-cascj8-fnt new file mode 100644 index 000000000..bc37180a6 --- /dev/null +++ b/contrib/run-script-cascj8-fnt @@ -0,0 +1,37 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fnt casc j8 : $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 --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $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;; + CounterSatisfiable) 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 --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench +} + +# designed for 300 seconds +trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair +trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair +trywith 60 --finite-model-find --decision=internal --sort-inference --uf-ss-fair +finishwith --finite-model-find --mbqi=abs --sort-inference --uf-ss-fair +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj8-fof b/contrib/run-script-cascj8-fof new file mode 100644 index 000000000..f8d79b1de --- /dev/null +++ b/contrib/run-script-cascj8-fof @@ -0,0 +1,47 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fof casc j8 : $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 --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 --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench +} + +# designed for 300 seconds +trywith 20 --relevant-triggers --full-saturate-quant +trywith 20 --no-e-matching --full-saturate-quant +trywith 20 --finite-model-find --mbqi=abs +trywith 5 --multi-trigger-when-single --full-saturate-quant +trywith 5 --trigger-sel=max --full-saturate-quant +trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant +trywith 5 --relational-triggers --full-saturate-quant +trywith 15 --term-db-mode=relevant --full-saturate-quant +trywith 15 --pre-quant=none --full-saturate-quant +trywith 15 --finite-model-find --uf-ss=no-minimal +trywith 30 --decision=internal --full-saturate-quant +trywith 30 --fs-inst --full-saturate-quant +trywith 30 --no-quant-cf --full-saturate-quant +finishwith --relational-triggers --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj8-tfa b/contrib/run-script-cascj8-tfa new file mode 100644 index 000000000..a7a97a44d --- /dev/null +++ b/contrib/run-script-cascj8-tfa @@ -0,0 +1,40 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfa casc j8 : $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 --decision=internal --full-saturate-quant +trywith 10 --finite-model-find --decision=internal +trywith 10 ---purify-quant --full-saturate-quant +trywith 10 ---partial-triggers --full-saturate-quant +trywith 10 ---no-e-matching --full-saturate-quant +trywith 30 --cbqi-all --purify-triggers --full-saturate-quant +trywith 60 --cbqi-all ---fs-inst --full-saturate-quant +finishwith --full-saturate-quant +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj8-tfn b/contrib/run-script-cascj8-tfn new file mode 100644 index 000000000..a6fe1e23c --- /dev/null +++ b/contrib/run-script-cascj8-tfn @@ -0,0 +1,37 @@ +#!/bin/bash + +here=`dirname $0` +cvc4=$here/cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-fnt casc j8 : $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 --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $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;; + CounterSatisfiable) 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 --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench +} + +# designed for 300 seconds +trywith 60 --finite-model-find --sort-inference --uf-ss-fair +trywith 30 --full-saturate-quant +trywith 30 --finite-model-find --fmf-bound-int --macros-quant +finishwith --finite-model-find --decision=internal --sort-inference --uf-ss-fair +# echo "% SZS status" "GaveUp for $filename" diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 5dc6071ba..19d6885b7 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -171,6 +171,12 @@ option qcfTConstraint --qcf-tconstraint bool :read-write :default false enable entailment checks for t-constraints in qcf algorithm option qcfAllConflict --qcf-all-conflict bool :read-write :default false add all available conflicting instances during conflict-based instantiation +option qcfNestedConflict --qcf-nested-conflict bool :default false + consider conflicts for nested quantifiers +option qcfVoExp --qcf-vo-exp bool :default false + qcf experimental variable ordering + + option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -182,7 +188,6 @@ 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 quantRewriteRules --rewrite-rules bool :default false diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 346807a0e..9450c5daa 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -49,7 +49,7 @@ QuantInfo::~QuantInfo() { void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { d_q = q; - d_extra_var = 0; + d_extra_var.clear(); for( unsigned i=0; i& v } bool QuantInfo::isBaseMatchComplete() { - return d_vars_set.size()==(d_q[0].getNumChildren()+d_extra_var); + return d_vars_set.size()==(d_q[0].getNumChildren()+d_extra_var.size()); } void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) { @@ -230,7 +230,7 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) { if( n.getKind()==ITE ){ registerNode( n, false, false ); }else if( n.getKind()==BOUND_VARIABLE ){ - d_extra_var++; + d_extra_var.push_back( n ); }else{ for( unsigned i=0; i " << n << std::endl; + subs[d_extra_var[i]] = n; + } if( !p->getTermDatabase()->isEntailed( d_q[1], subs, false, false ) ){ Trace("qcf-instance-check") << "...not entailed to be false." << std::endl; return true; @@ -616,6 +621,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) { if( n.getKind()==FORALL ){ + //TODO? return true; }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || n.getKind()==IFF ){ for( unsigned i=0; i& cbvars ) { - int v = qi->getVarNum( n ); - if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){ - cbvars.push_back( v ); - } - for( unsigned i=0; i& cbvars, std::map< Node, bool >& visited, bool& hasNested ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==FORALL ){ + hasNested = true; + } + int v = qi->getVarNum( n ); + if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){ + cbvars.push_back( v ); + } + for( unsigned i=0; i& bvars ) { - Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl; - bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ); - std::map< int, std::vector< int > > c_to_vars; - std::map< int, std::vector< int > > vars_to_c; - std::map< int, int > vb_count; - std::map< int, int > vu_count; - std::vector< bool > assigned; - Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl; - for( unsigned i=0; i visited; + has_nested[i] = false; + collectBoundVar( qi, d_children[i].d_n, c_to_vars[i], visited, has_nested[i] ); + assigned.push_back( false ); + vb_count[i] = 0; + vu_count[i] = 0; + for( unsigned j=0; jd_vars.size()*( qi->d_vars.size() - vb_count[i] ) + ( qi->d_vars.size() - vu_count[i] ) ); + } + if( min_score==-1 || score0& bvars for( unsigned i=0; i visited; + std::vector< int > cvars; + bool has_nested = false; + collectBoundVar( qi, d_children[i].d_n, cvars, visited, has_nested ); + for( unsigned j=0; j conflict, since equality may be a propagation if( vn[1]!=-1 && vn[0]==-1 ){ //swap Node t = nn[1]; @@ -1384,7 +1419,9 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { d_qn.push_back( NULL ); }else{ if( d_tgt && d_n.getKind()==FORALL ){ - //do nothing + //fail + }else if( d_n.getKind()==FORALL && p->d_effort==QuantConflictFind::effort_conflict && !options::qcfNestedConflict() ){ + //fail }else{ //reset the first child to d_tgt d_child_counter = 0; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 974495269..47a66b1b1 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -62,7 +62,7 @@ private: std::map< int, Node > d_ground_eval; //determine variable order void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ); - void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ); + void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars, std::map< Node, bool >& visited, bool& hasNested ); public: //type of the match generator enum { @@ -121,7 +121,7 @@ private: //for completing match //optimization: number of variables set, to track when we can stop std::map< int, bool > d_vars_set; std::map< Node, bool > d_ground_terms; - unsigned d_extra_var; + std::vector< Node > d_extra_var; public: void setGroundSubterm( Node t ) { d_ground_terms[t] = true; } bool isGroundSubterm( Node t ) { return d_ground_terms.find( t )!=d_ground_terms.end(); } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e3cf15c53..7b4719878 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -415,14 +415,16 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su return n; }else if( n.getKind()==BOUND_VARIABLE ){ if( hasSubs ){ - Assert( subs.find( n )!=subs.end() ); - Trace("term-db-entail") << "...substitution is : " << subs[n] << std::endl; - if( subsRep ){ - Assert( qy->getEngine()->hasTerm( subs[n] ) ); - Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] ); - return subs[n]; - }else{ - return getEntailedTerm2( subs[n], subs, subsRep, hasSubs, qy ); + std::map< TNode, TNode >::iterator it = subs.find( n ); + if( it!=subs.end() ){ + Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; + if( subsRep ){ + Assert( qy->getEngine()->hasTerm( it->second ) ); + Assert( qy->getEngine()->getRepresentative( it->second )==it->second ); + return it->second; + }else{ + return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy ); + } } } }else if( n.getKind()==ITE ){ @@ -535,6 +537,8 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false ); } } + }else if( n.getKind()==FORALL ){ + return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy ); } return false; }