cool / benchmarks / aconjunctive_mu / bench_one_formula.sh @ 221a3816
History  View  Annotate  Download (2.72 KB)
1 
#!/bin/bash 

2  
3 
# Usage: ./bench_one_formula.sh NAME_OF_FORMULA COOL_LOGIC MLSOLVER_LOGIC 
4 
# 
5 
# where 
6 
# NAME_OF_FORMULA: name of the formula series to be passed to gen.ml 
7 
# COOL_LOGIC: cool functor to use 
8 
# MLSOLVER_LOGIC: logic for mlsolvers val argument 
9 
# 
10 
# 
11 
# Example: ./bench_one_formula.sh linear_dpa_is_nba_neg Id ltmc 
12 
# 
13 
# 
14 
# The variables TIMEOUT, REPEATS and OUTPUT_BASE configure the behaviour of this 
15 
# script. 
16 
# 
17 
# Requirements: The 'perf' linux command, 'mlsolver' must be in the search path. 
18  
19 
# Number of times to run each programm for each formula series member. The 
20 
# mesured time will be printed as an average of all runs plus stddev. 
21 
REPEATS=3 
22  
23 
# Maximum time to spend on a single formula for each program. Formulas are 
24 
# tested until one formula exceeds this timetout. 
25 
# 
26 
# This includes _all_ repeats as specified above, so to give each program a 
27 
# maximum time of 5 minutes to solve each fomula with 3 repeats, you have to set 
28 
# this to 5*3 = 15 minutes. 
29 
TIMEOUT=6m 
30  
31 
# Directory where output files will be stored 
32 
OUTPUT_BASE="output/" 
33  
34 
###################################################################### 
35  
36 
set e 
37  
38 
if [[ $# ne 3 ]]; then 
39 
echo "Usage: ./bench_one_formula.sh NAME_OF_FORMULA COOL_LOGIC MLSOLVER_LOGIC" 
40 
exit 1 
41 
fi 
42  
43 
# Force dot as decimal seperator 
44 
export LC_ALL=C 
45  
46 
FORMULA=$1 
47 
COOL_LOGIC=$2 
48 
MLSOLVER_LOGIC=$3 
49  
50 
OUTPUT_DIR="${OUTPUT_BASE}/${FORMULA}/" 
51  
52 
mkdir p "${OUTPUT_DIR}" 
53  
54 
echo "# ${FORMULA}:" 
55  
56 
function bench { 
57 
i=1 
58  
59 
echo n "  ${FORMULA}${1}: " 
60  
61 
while timeout ${TIMEOUT} perf stat o "${OUTPUT_DIR}/tmp.time" r ${REPEATS} "$2" "$3" "$i" "${@:4}" > "${OUTPUT_DIR}/tmp.out" 2>&1; do 
62 
mv "${OUTPUT_DIR}/tmp.time" "${OUTPUT_DIR}/${FORMULA}${i}${1}.time"; 
63 
mv "${OUTPUT_DIR}/tmp.out" "${OUTPUT_DIR}/${FORMULA}${i}${1}.out"; 
64 
i=$(($i+1)) 
65 
echo n "." 
66 
done 
67 

68 
rm "${OUTPUT_DIR}/tmp."{time,out} 
69 
echo "" 
70 
} 
71  
72 
#### cool without intermediate propagation 
73  
74 
bench coolnoprop ./run_cool.sh ${FORMULA} sat ${COOL_LOGIC} propagationRate once verbose 
75  
76 
#### cool with adaptive propagation 
77  
78 
bench cool ./run_cool.sh ${FORMULA} sat ${COOL_LOGIC} propagationRate adaptive verbose 
79  
80 
#### cool with pgsolver but without intermediate propagation 
81  
82 
bench coolpgsolvernoprop ./run_cool_pgsolver.sh ${FORMULA} sat ${COOL_LOGIC} propagationRate once verbose 
83  
84 
#### cool with pgsolver and adaptive propagation 
85  
86 
bench coolpgsolver ./run_cool_pgsolver.sh ${FORMULA} sat ${COOL_LOGIC} propagationRate adaptive verbose 
87  
88 
##### mlsolver without optimization 
89  
90 
bench mlsolver ./run_mlsolver.sh ${FORMULA} sat ${MLSOLVER_LOGIC} pgs stratimprloc2 verbose 
91  
92 
##### mlsolver with optimization 
93  
94 
bench mlsolveropt ./run_mlsolver.sh ${FORMULA} sat ${MLSOLVER_LOGIC} pgs stratimprloc2 opt comp opt litpro verbose 
95  
96 
echo "" 