Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add competition scripts (in progress).

4 files changed, 194 insertions, 36 deletions

diff --git a/contrib/run-script-casc25-fof b/contrib/run-script-casc25-fof
new file mode 100755
index 000000000..3986b42f6
--- /dev/null
+++ b/contrib/run-script-casc25-fof
@@ -0,0 +1,46 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof 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 --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 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 5 --trigger-sel=max --full-saturate-quant
+trywith 5 --multi-trigger-when-single --full-saturate-quant 
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant 
+trywith 5 --pre-skolem-quant --no-pre-skolem-quant-nested --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 15 --no-quant-cf --full-saturate-quant
+trywith 15 --trigger-sel=min --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
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015
new file mode 100644
index 000000000..831c892be
--- /dev/null
+++ b/contrib/run-script-smtcomp2015
@@ -0,0 +1,106 @@
+#!/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|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
+  # the following is designed for a run time of 1800s.
+  # initial runs 1min
+  trywith 20 --simplification=none --full-saturate-quant
+  trywith 20 --finite-model-find
+  trywith 20 --no-e-matching --full-saturate-quant
+  # trigger selections/special 1min
+  trywith 10 --multi-trigger-when-single --full-saturate-quant
+  trywith 10 --trigger-sel=max --full-saturate-quant
+  trywith 10 --relevant-triggers --full-saturate-quant
+  trywith 10 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+  trywith 10 --trigger-sel=min --full-saturate-quant
+  trywith 10 --qcf-tconstraint --full-saturate-quant
+  # medium runs 5min
+  trywith 30 --no-quant-cf --full-saturate-quant
+  trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
+  trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
+  trywith 30 --pre-skolem-quant --full-saturate-quant
+  trywith 30 --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality
+  trywith 30 --inst-when=full --full-saturate-quant
+  trywith 30 --fmf-bound-int --macros-quant
+  trywith 30 --no-inst-no-entail --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 30 --decision=justification-stoponly --full-saturate-quant
+  # large runs 3min
+  trywith 60 --term-db-mode=relevant --full-saturate-quant
+  trywith 60 --finite-model-find --mbqi=none
+  trywith 60 --decision=internal --full-saturate-quant
+  # last call runs 20min
+  trywith 300 --finite-model-find --fmf-inst-engine --quant-cf --sort-inference --uf-ss-fair 
+  trywith 300 --no-inst-no-entail --full-saturate-quant
+  finishwith --full-saturate-quant
+  ;;
+LIA|LRA|NIA|NRA)
+  trywith 20 --enable-cbqi --full-saturate-quant
+  trywith 20 --full-saturate-quant
+  trywith 20 --cbqi-recurse --full-saturate-quant
+  trywith 30 --quant-cf --full-saturate-quant
+  trywith 60 --quant-cf --qcf-tconstraint --full-saturate-quant
+  trywith 120 --cbqi-recurse --disable-prenex-quant --full-saturate-quant
+  finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant
+  ;;
+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 \
+         --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_AUFLIA|QF_AX)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 0c8d0fb62..371f27c95 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1205,9 +1205,11 @@ void TheoryDatatypes::computeCareGraph(){
     unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size();
     for( unsigned i=0; i<functionTerms; i++ ){
       TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i];
+      Assert(d_equalityEngine.hasTerm(f1));
       for( unsigned j=i+1; j<functionTerms; j++ ){
         TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
-        Trace("dt-cg-debug") << "dt-cg: " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
+        Trace("dt-cg-debug") << "dt-cg(" << r << "): " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
+        Assert(d_equalityEngine.hasTerm(f2));
         if( f1.getOperator()==f2.getOperator() &&
             ( ( f1.getKind()!=DT_SIZE && f1.getKind()!=DT_HEIGHT_BOUND ) || f1[0].getType()==f2[0].getType() ) &&
             !areEqual( f1, f2 ) ){
@@ -1477,7 +1479,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
     return a;
   }else{
     return it->second;
-  } 
+  }
 }
 
 void TheoryDatatypes::collectTerms( Node n ) {
@@ -1583,6 +1585,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
     //Assert( n_ic==Rewriter::rewrite( n_ic ) );
     n_ic = Rewriter::rewrite( n_ic );
     collectTerms( n_ic );
+    d_equalityEngine.addTerm(n_ic);
     Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
     d_inst_map[n][index] = n_ic;
     return n_ic;
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index a46aca3c8..32097d3eb 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -47,44 +47,47 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
       
       Node bd = TermDb::getFunDefBody( assertions[i] );
       Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
-      Assert( !bd.isNull() );
-      bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
+      if( !bd.isNull() ){
+        bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
 
-      //create a sort S that represents the inputs of the function
-      std::stringstream ss;
-      ss << "I_" << f;
-      TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
-      d_sorts[f] = iType;
-
-      //create functions f1...fn mapping from this sort to concrete elements
-      for( unsigned j=0; j<n.getNumChildren(); j++ ){
-        TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
+        //create a sort S that represents the inputs of the function
         std::stringstream ss;
-        ss << f << "_arg_" << j;
-        d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
-      }
+        ss << "I_" << f;
+        TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
+        d_sorts[f] = iType;
 
-      //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
-      std::vector< Node > children;
-      Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
-      Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
-      std::vector< Node > subs;
-      std::vector< Node > vars;
-      for( unsigned j=0; j<n.getNumChildren(); j++ ){
-        vars.push_back( n[j] );
-        subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
-      }
-      bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-      subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+        //create functions f1...fn mapping from this sort to concrete elements
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){
+          TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
+          std::stringstream ss;
+          ss << f << "_arg_" << j;
+          d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
+        }
 
-      Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
-      Trace("fmf-fun-def") << "  to " << std::endl;
-      Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
-      new_q = Rewriter::rewrite( new_q );
-      PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); );
-      assertions[i] = new_q;
-      Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
-      fd_assertions.push_back( i );
+        //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
+        std::vector< Node > children;
+        Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
+        Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
+        std::vector< Node > subs;
+        std::vector< Node > vars;
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){
+          vars.push_back( n[j] );
+          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
+        }
+        bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+        subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+
+        Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
+        Trace("fmf-fun-def") << "  to " << std::endl;
+        Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
+        new_q = Rewriter::rewrite( new_q );
+        PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); );
+        assertions[i] = new_q;
+        Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
+        fd_assertions.push_back( i );
+      }else{
+        //can be, e.g. in corner cases forall x. f(x)=f(x), forall x. f(x)=f(x)+1
+      }
     }
   }
   //second pass : rewrite assertions