--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
--- /dev/null
+#!/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"
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
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
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<q[0].getNumChildren(); i++ ){
d_match.push_back( TNode::null() );
d_match_term.push_back( TNode::null() );
}
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 ) {
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.getNumChildren(); i++ ){
flatten( n[i], beneathQuant );
Trace("qcf-instance-check") << " " << terms[i] << std::endl;
subs[d_q[0][i]] = terms[i];
}
+ for( unsigned i=0; i<d_extra_var.size(); i++ ){
+ Node n = getCurrentExpValue( d_extra_var[i] );
+ Trace("qcf-instance-check") << " " << d_extra_var[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;
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<n.getNumChildren(); i++ ){
}
-void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& 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<n.getNumChildren(); i++ ){
- collectBoundVar( qi, n[i], cbvars );
+void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& 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<n.getNumChildren(); i++ ){
+ collectBoundVar( qi, n[i], cbvars, visited, hasNested );
+ }
}
}
void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& 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<d_children.size(); i++ ){
- collectBoundVar( qi, d_children[i].d_n, c_to_vars[i] );
- assigned.push_back( false );
- vb_count[i] = 0;
- vu_count[i] = 0;
- for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
- int v = c_to_vars[i][j];
- vars_to_c[v].push_back( i );
- if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
- vu_count[i]++;
- if( !isCom ){
- bvars.push_back( v );
+ Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl;
+ bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );
+ if( isComm ){
+ 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::map< int, bool > has_nested;
+ std::vector< bool > assigned;
+ Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
+ for( unsigned i=0; i<d_children.size(); i++ ){
+ std::map< Node, bool > 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; j<c_to_vars[i].size(); j++ ){
+ int v = c_to_vars[i][j];
+ vars_to_c[v].push_back( i );
+ if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
+ vu_count[i]++;
+ }else{
+ vb_count[i]++;
}
- }else{
- vb_count[i]++;
}
}
- }
- if( isCom ){
- //children that bind the least number of unbound variables go first
+ //children that bind no unbound variable, then the most number of bound, unbound variables go first
+ Trace("qcf-qregister-vo") << "Variable order for " << d_n << " : " << std::endl;
do {
+ int min_score0 = -1;
int min_score = -1;
int min_score_index = -1;
for( unsigned i=0; i<d_children.size(); i++ ){
if( !assigned[i] ){
- int score = vu_count[i];
- if( min_score==-1 || score<min_score ){
+ Trace("qcf-qregister-debug2") << "Child " << i << " has b/ub : " << vb_count[i] << "/" << vu_count[i] << std::endl;
+ int score0 = 0;//has_nested[i] ? 0 : 1;
+ int score;
+ if( !options::qcfVoExp() ){
+ score = vu_count[i];
+ }else{
+ score = vu_count[i]==0 ? 0 : ( 1 + qi->d_vars.size()*( qi->d_vars.size() - vb_count[i] ) + ( qi->d_vars.size() - vu_count[i] ) );
+ }
+ if( min_score==-1 || score0<min_score0 || ( score0==min_score0 && score<min_score ) ){
+ min_score0 = score0;
min_score = score;
min_score_index = i;
}
}
}
- Trace("qcf-qregister-debug") << "...assign child " << min_score_index << "/" << d_children.size() << std::endl;
+ Trace("qcf-qregister-vo") << " " << d_children_order.size()+1 << ": " << d_children[min_score_index].d_n << " : ";
+ Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl;
+ Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl;
+ Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
Assert( min_score_index!=-1 );
//add to children order
d_children_order.push_back( min_score_index );
for( unsigned i=0; i<d_children.size(); i++ ){
d_children_order.push_back( i );
d_children[i].determineVariableOrder( qi, bvars );
+ //now add to bvars
+ std::map< Node, bool > 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<cvars.size(); j++ ){
+ if( std::find( bvars.begin(), bvars.end(), cvars[j] )==bvars.end() ){
+ bvars.push_back( cvars[j] );
+ }
+ }
}
}
}
}
}
}else{
- //otherwise, add a constraint to a variable
+ //otherwise, add a constraint to a variable TODO: this may be over-eager at effort > conflict, since equality may be a propagation
if( vn[1]!=-1 && vn[0]==-1 ){
//swap
Node t = nn[1];
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;
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 {
//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(); }
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 ){
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;
}
projects / cvc5.git / commitdiff