contrib/run-script-smtcomp2012

   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   # 3 minutes with default decision heuristic
  29   trywith --tlimit-per=180000
  30   # switch to internal decision heuristic
  31   finishwith --decision=internal
  32   ;;
  33 AUFLIA)
  34   # 60 seconds with default decision heuristic
  35   trywith --tlimit-per=60000
  36   # try simplification for 60 seconds, default decision heuristic
  37   trywith --simplification=batch --tlimit-per=60000
  38   # switch to internal decision heuristic
  39   finishwith --decision=internal
  40   ;;
  41 QF_AUFBV)
  42   trywith --tlimit-per=600000
  43   finishwith --decision=justification-stoponly
  44   ;;
  45 *)
  46   # just run the default
  47   finishwith
  48   ;;
  49
  50 esac
  51