contrib/run-script-syguscomp2015

   1 #!/bin/bash
   2
   3 cvc4=./cvc4
   4 bench="$1"
   5
   6 function trywith {
   7   ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
   8   (read result w1;
   9   case "$result" in
  10   unsat) echo "$w1";cat;exit 0;;
  11   esac; exit 1)
  12   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
  13 }
  14
  15 trywith --cegqi --cegqi-si-multi-inst-abort --cegqi-si-abort --decision=internal
  16 trywith --cegqi --no-cegqi-si
  17