blob: 58b281b4c4d45ba25d899f86dd699f6f9e3e1770 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
#!/bin/bash
cvc4=./cvc4
bench="$1"
logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$')
# use: trywith [params..]
# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in
# which case this run script terminates immediately. Otherwise, this
# function returns normally.
function trywith {
limit=$1; shift;
result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench)"
case "$result" in
sat|unsat) echo "$result"; exit 0;;
esac
}
# use: finishwith [params..]
# to run cvc4 and let it output whatever it will to stdout.
function finishwith {
$cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench
}
case "$logic" in
QF_LRA)
trywith 200 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
;;
QF_LIA)
# same as QF_LRA but add --pb-rewrites
finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
;;
QF_NIA)
trywith 20
trywith 1800 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cryptominisat
trywith 1800 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat
trywith 1800 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cryptominisat
trywith 1800 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cryptominisat
finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
;;
ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA)
# the following is designed for a run time of 2400s (40 min).
# initial runs 1min
trywith 20 --simplification=none --full-saturate-quant
trywith 20 --no-e-matching --full-saturate-quant
trywith 20 --fs-inst --decision=internal --full-saturate-quant
# trigger selections 2min
trywith 30 --relevant-triggers --full-saturate-quant
trywith 30 --trigger-sel=max --full-saturate-quant
trywith 30 --multi-trigger-when-single --full-saturate-quant
trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
# other 2min
trywith 30 --pre-skolem-quant --full-saturate-quant
trywith 30 --inst-when=full --full-saturate-quant
trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
# finite model find 2min
trywith 30 --finite-model-find
trywith 30 --finite-model-find --uf-ss=no-minimal
trywith 60 --finite-model-find --decision=internal
# long runs 20min
trywith 300 --decision=internal --full-saturate-quant
trywith 300 --term-db-mode=relevant --full-saturate-quant
trywith 300 --fs-inst --full-saturate-quant
trywith 300 --finite-model-find --fmf-inst-engine
# finite model find 1min
trywith 30 --finite-model-find --fmf-bound-int
trywith 30 --finite-model-find --sort-inference
# finish 12min
finishwith --full-saturate-quant
;;
UFBV)
# many problems in UFBV are essentially BV
trywith 300 --full-saturate-quant
trywith 300 --finite-model-find
finishwith --cbqi-all --full-saturate-quant
;;
BV)
trywith 300 --finite-model-find
finishwith --cbqi-all --full-saturate-quant
;;
LIA|LRA|NIA|NRA)
trywith 30 --full-saturate-quant
trywith 300 --full-saturate-quant --cbqi-min-bounds
trywith 300 --full-saturate-quant --decision=internal
finishwith --full-saturate-quant --cbqi-midpoint
;;
QF_AUFBV)
trywith 600
finishwith --decision=justification-stoponly
;;
QF_ABV)
trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
trywith 500 --arrays-weak-equiv
finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
;;
QF_UFBV)
finishwith --bitblast=eager --bv-sat-solver=cryptominisat
;;
QF_BV)
exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \
--threads 2 \
--thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-abstraction' \
--thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \
--no-wait-to-join \
"$bench"
#trywith 10 --bv-eq-slicer=auto --decision=justification
#trywith 60 --decision=justification
#trywith 600 --decision=internal --bitblast-eager
#finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
;;
QF_AUFLIA)
finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
;;
QF_AX)
finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
;;
QF_AUFNIA)
finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
;;
QF_ALIA)
trywith 70 --decision=justification --arrays-weak-equiv
finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
;;
*)
# just run the default
finishwith
;;
esac
|
