blob: 914d970458427f43d48f4f9274f0e1f1173a4029 (
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
|
#!/bin/bash
cvc4=./cvc4-assertions
# Attempt to run each benchmark 1-5 min depending on numconfigs
# quanitifers get 5 min / benchmark
# quantifier free uf, arith, arrays get 1 min / benchmark
# qf_bv gets 1 min wall (2 min user) / benchmark
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 30 --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
;;
AUFLIA)
finishwith --no-e-matching --full-saturate-quant
;;
ALIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
# the following is designed for a run time of 1800s.
# initial runs 1min (30)
trywith 10 --simplification=none --full-saturate-quant
trywith 10 --finite-model-find
trywith 10 --no-e-matching --full-saturate-quant
# trigger selections/special 1min (60)
trywith 10 --multi-trigger-when-single --full-saturate-quant
trywith 10 --trigger-sel=max --full-saturate-quant
trywith 10 --relevant-triggers --full-saturate-quant
trywith 10 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
trywith 10 --trigger-sel=min --full-saturate-quant
trywith 10 --qcf-tconstraint --full-saturate-quant
# medium runs 5min (20*10 = 200)
trywith 10 --no-quant-cf --full-saturate-quant
trywith 10 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
trywith 10 --no-e-matching --no-quant-cf --full-saturate-quant
trywith 10 --pre-skolem-quant --full-saturate-quant
trywith 10 --no-inst-no-entail --no-quant-cf --full-saturate-quant
trywith 10 --finite-model-find --mbqi=gen-ev --uf-ss-totality
trywith 10 --inst-when=full --full-saturate-quant
trywith 10 --fmf-bound-int --macros-quant
trywith 10 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
trywith 10 --decision=justification-stoponly --full-saturate-quant
# large runs 3min
trywith 10 --term-db-mode=relevant --full-saturate-quant
trywith 10 --finite-model-find --mbqi=none
trywith 10 --decision=internal --full-saturate-quant
# last call runs 20min
trywith 20 --finite-model-find --fmf-inst-engine --quant-cf --sort-inference --uf-ss-fair
trywith 20 --no-inst-no-entail --full-saturate-quant
finishwith --full-saturate-quant
;;
LIA|LRA|NIA|NRA)
trywith 30 --cbqi2 --full-saturate-quant
trywith 30 --full-saturate-quant
trywith 30 --cbqi --cbqi-recurse --full-saturate-quant
trywith 30 --cbqi2 --decision=internal --full-saturate-quant
trywith 30 --qcf-tconstraint --full-saturate-quant
trywith 30 --cbqi --decision=internal --full-saturate-quant
trywith 30 --cbqi --full-saturate-quant
finishwith --cbqi2 --cbqi-recurse --full-saturate-quant
;;
QF_AUFBV)
trywith 30
finishwith --decision=justification-stoponly
;;
QF_ABV)
trywith 20 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
trywith 20 --arrays-weak-equiv
finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
;;
QF_UFBV)
finishwith --bitblast=eager --bv-sat-solver=cryptominisat --no-bv-native-xor
;;
QF_BV)
exec ./pcvc4-assertions -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-native-xor' \
--thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \
--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 30 --decision=justification --arrays-weak-equiv
finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
;;
*)
# just run the default
finishwith
;;
esac
|
