contrib/run-script-smteval2013

   1 #!/bin/bash
   2
   3 cvc4=./cvc4
   4 bench="$1"
   5
   6 logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
   7
   8 # use: trywith [params..]
   9 # to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
  10 # which case this run script terminates immediately.  Otherwise, this
  11 # function returns normally.
  12 function trywith {
  13   result="$($cvc4 --stats -L smt2 --no-checking --no-interactive "$@" $bench)"
  14   case "$result" in
  15     sat|unsat) echo "$result"; exit 0;;
  16   esac
  17 }
  18
  19 # use: finishwith [params..]
  20 # to run cvc4 and let it output whatever it will to stdout.
  21 function finishwith {
  22   $cvc4 --stats -L smt2 --no-checking --no-interactive "$@" $bench
  23 }
  24
  25 case "$logic" in
  26
  27 QF_LRA)
  28   finishwith --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --use-soi --new-prop --dio-decomps --unconstrained-simp --fancy-final
  29   ;;
  30 AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA)
  31   # 60 seconds with default decision heuristic
  32   trywith --simplification=none --tlimit-per=60000
  33   # try simplification for 60 seconds, default decision heuristic
  34   trywith --tlimit-per=60000
  35   # switch to internal decision heuristic
  36   finishwith --simplification=none --decision=internal
  37   ;;
  38 LRA)
  39   finishwith --enable-cbqi
  40   ;;
  41 QF_AUFBV)
  42   trywith --tlimit-per=600000
  43   finishwith --decision=justification-stoponly
  44   ;;
  45 QF_BV)
  46   trywith --bv-core --decision=justification --tlimit-per=10000
  47   trywith --decision=justification --tlimit-per=60000
  48   trywith --decision=internal --bitblast-eager --tlimit-per=600000
  49   finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
  50   ;;
  51 QF_AX)
  52   trywith --tlimit-per=2000
  53   finishwith --no-arrays-model-based
  54   ;;
  55 *)
  56   # just run the default
  57   finishwith
  58   ;;
  59
  60 esac
  61