contrib/run-script-casc24-fnt

   1 #!/bin/bash
   2
   3 cvc4=./cvc4
   4 bench="$1"
   5
   6 file=${bench##*/}
   7 filename=${file%.*}
   8
   9 # use: trywith [params..]
  10 # to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
  11 # which case this run script terminates immediately.  Otherwise, this
  12 # function returns normally.
  13 function trywith {
  14   result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
  15   case "$result" in
  16     sat) echo "SZS Satisfiable for $filename"; exit 0;;
  17     unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
  18     conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
  19     conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
  20   esac
  21 }
  22 function finishwith {
  23   result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
  24   case "$result" in
  25     sat) echo "SZS Satisfiable for $filename"; exit 0;;
  26     unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
  27     conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
  28     conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
  29   esac
  30 }
  31
  32 trywith 15 --finite-model-find --uf-ss-totality
  33 trywith 15 --finite-model-find --decision=justification --fmf-fmc
  34 finishwith --finite-model-find --decision=justification
  35 echo "SZS GaveUp for $filename"