Project

General

Profile

Statistics
| Branch: | Revision:

cool / benchmarks / aconjunctive_mu / bench_one_formula.sh @ cf05f9f8

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=5
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=10s
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 cool-noprop ./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 cool-pgsolver-noprop ./run_cool_pgsolver.sh ${FORMULA} sat ${COOL_LOGIC} --propagationRate once --verbose
83

    
84
#### cool with pgsolver and adaptive propagation
85

    
86
bench cool-pgsolver ./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 mlsolver-opt ./run_mlsolver.sh ${FORMULA} -sat ${MLSOLVER_LOGIC} -pgs stratimprloc2 -opt comp -opt litpro --verbose
95

    
96
echo ""