1#!/bin/bash
2
3cvc4=./cvc4
4bench="$1"
5
6logic=$(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.
12function 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.
21function finishwith {
22  $cvc4 --stats -L smt2 --no-checking --no-interactive "$@" $bench
23}
24
25case "$logic" in
26
27QF_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  ;;
30AUFLIA|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  ;;
38LRA)
39  finishwith --enable-cbqi
40  ;;
41QF_AUFBV)
42  trywith --tlimit-per=600000
43  finishwith --decision=justification-stoponly
44  ;;
45QF_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  ;;
51QF_AX)
52  trywith --tlimit-per=2000
53  finishwith --no-arrays-model-based
54  ;;
55*)
56  # just run the default
57  finishwith
58  ;;
59
60esac
61
62