contrib/run-script-smteval2013

   1 #!/bin/bash
   2
   3 cat >bench-$$.smt2
   4 trap 'rm bench-$$.smt2' EXIT
   5
   6 logic=$(expr "$(head -n 1 bench-$$.smt2)" : ' *(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 -L smt2 --no-checking --no-interactive "$@" bench-$$.smt2)"
  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 -L smt2 --no-checking --no-interactive "$@" bench-$$.smt2
  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)
  31   # 60 seconds with default decision heuristic
  32   trywith --tlimit-per=60000
  33   # try simplification for 60 seconds, default decision heuristic
  34   trywith --simplification=batch --tlimit-per=60000
  35   # switch to internal decision heuristic
  36   finishwith --decision=internal
  37   ;;
  38 QF_AUFBV)
  39   trywith --tlimit-per=600000
  40   finishwith --decision=justification-stoponly
  41   ;;
  42 QF_BV)
  43   trywith --bv-core --decision=justification --tlimit-per=10000
  44   trywith --decision=justification --tlimit-per=60000
  45   trywith --decision=internal --bitblast-eager --tlimit-per=600000
  46   finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
  47   ;;
  48 QF_AX)
  49   trywith --tlimit-per=2000
  50   finishwith --no-arrays-model-based
  51   ;;
  52 *)
  53   # just run the default
  54   finishwith
  55   ;;
  56
  57 esac
  58