contrib/run-script-sygusComp2017-GENERAL

   1 #!/bin/bash
   2
   3 cvc4=./cvc4
   4 bench="$1"
   5
   6 function runl {
   7   limit=$1; shift;
   8   ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench
   9 }
  10
  11 function trywith {
  12   sol=$(runl $@)
  13   status=$?
  14   if [ $status -ne 134 ]; then
  15     echo $sol |
  16     (read result w1;
  17     case "$result" in
  18     unsat) echo "$w1";cat;exit 0;;
  19     esac; exit 1)
  20     if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
  21   fi
  22 }
  23
  24 function finishwith {
  25   $cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench 2>/dev/null |
  26   (read result w1;
  27   case "$result" in
  28   unsat) echo "$w1";cat;exit 0;;
  29   esac)
  30 }
  31
  32 trywith 120 --cegqi-si=all-abort --cegqi-si-abort --decision=internal --cbqi-prereg-inst
  33 finishwith --cegqi-si=none