blob: a8c6b0ba42f7248d43bc1875e3e29e504eed307d (
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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
#!/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 and prints the output of the solver to stderr.
function trywith {
limit=$1; shift;
result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)"
case "$result" in
sat|unsat) echo "$result"; exit 0;;
*) echo "$result" >&2;;
esac
}
# use: finishwith [params..]
# to run cvc4 and let it output whatever it will to stdout.
function finishwith {
$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
}
case "$logic" in
QF_LRA)
trywith 400 --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 --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 600 --nl-ext-tplanes --decision=internal
trywith 60 --nl-ext-tplanes --decision=justification
trywith 60 --no-nl-ext-tplanes --decision=internal
# this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail
trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
finishwith --nl-ext-tplanes --decision=internal
;;
QF_NRA)
trywith 600 --nl-ext-tplanes --decision=internal
trywith 600 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
trywith 60 --nl-ext-tplanes --decision=internal --solve-real-as-int
finishwith --nl-ext-tplanes --decision=justification
;;
# all logics with UF + quantifiers should either fall under this or special cases below
ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA)
# the following is designed for a run time of 20 min.
# initial runs 2min
trywith 60 --simplification=none --full-saturate-quant
trywith 60 --no-e-matching --full-saturate-quant
# trigger selections 6min
trywith 60 --relevant-triggers --full-saturate-quant
trywith 60 --trigger-sel=max --full-saturate-quant
trywith 60 --multi-trigger-when-single --full-saturate-quant
trywith 60 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
trywith 60 --multi-trigger-cache --full-saturate-quant
trywith 60 --no-multi-trigger-linear --full-saturate-quant
# other 8min
trywith 60 --pre-skolem-quant --full-saturate-quant
trywith 60 --inst-when=full --full-saturate-quant
trywith 60 --no-e-matching --no-quant-cf --full-saturate-quant
trywith 60 --full-saturate-quant --quant-ind
trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
trywith 60 --decision=internal --full-saturate-quant
trywith 60 --term-db-mode=relevant --full-saturate-quant
trywith 60 --fs-interleave --full-saturate-quant
# finite model find 6min
trywith 60 --finite-model-find --mbqi=none
trywith 60 --finite-model-find --decision=internal
trywith 60 --finite-model-find --macros-quant --macros-quant-mode=all
trywith 60 --finite-model-find --uf-ss=no-minimal
trywith 120 --finite-model-find --fmf-inst-engine
# long runs 8min
trywith 480 --finite-model-find --decision=internal
finishwith --full-saturate-quant
;;
ABVFP|BVFP|FP)
finishwith --full-saturate-quant --fp-exp
;;
UFBV)
# most problems in UFBV are essentially BV
trywith 600 --full-saturate-quant --decision=internal
trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate
finishwith --finite-model-find
;;
BV)
trywith 240 --full-saturate-quant
trywith 240 --full-saturate-quant --no-cbqi-innermost
trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
trywith 60 --full-saturate-quant --no-cbqi-bv
trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack
# finish 10min
finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
;;
LIA|LRA|NIA|NRA)
trywith 60 --full-saturate-quant --nl-ext-tplanes
trywith 600 --full-saturate-quant --no-cbqi-innermost
trywith 600 --full-saturate-quant --cbqi-nested-qe
finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
;;
QF_AUFBV)
trywith 1200
finishwith --decision=justification-stoponly
;;
QF_ABV)
trywith 100 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
trywith 1000 --arrays-weak-equiv
finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
;;
QF_UFBV)
# Benchmarks with uninterpreted sorts cannot be solved with eager
# bit-blasting currently
trywith 2400 --bitblast=eager --bv-sat-solver=cadical
finishwith
;;
QF_BV)
finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
;;
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 140 --decision=justification --arrays-weak-equiv
finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
;;
QF_S|QF_SLIA)
trywith 300 --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf
finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
;;
QF_ABVFP)
finishwith --fp-exp
;;
QF_BVFP)
finishwith --fp-exp
;;
QF_FP)
finishwith --fp-exp
;;
*)
# just run the default
finishwith
;;
esac
|
