smtlib_schanda/run.py at master · florianschanda/smtlib_schanda · GitHub

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
#!/usr/bin/env python3
#
# This file is part of smtlib_schanda.
#
# smtlib_schanda is free software: you can redistribute it and/or
# modify it under the terms of the GNU General Public License as
# published by the Free Software Foundation, either version 3 of the
# License, or (at your option) any later version.
#
# smtlib_schanda is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
# General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with smtlib_schanda. If not, see
# <https://www.gnu.org/licenses/>.

import sys
import argparse
import json

from lib.solvers import (build_solver_library,
                         find_solver)
from lib.benchmarks import (survery_benchmarks,
                            load_benchmarks,
                            run_benchmarks,
                            serialise_results)
from lib.analysis import analyse_single, analyse_global


def main():
    solvers = build_solver_library()

    ap = argparse.ArgumentParser()
    subp = ap.add_subparsers(required=True,
                             dest="mode")

    # pylint: disable=unused-variable
    ap_manifest = subp.add_parser("manifest")

    ap_run = subp.add_parser("run")
    ap_run.add_argument("solver")
    ap_run.add_argument("version")
    ap_run.add_argument("--config",
                        default=None)
    ap_run.add_argument("--group",
                        default=[], action="append")
    ap_run.add_argument("--threads",
                        type=int,
                        default=16)
    ap_run.add_argument("--filter-name", default=None)

    ap_install = subp.add_parser("install_all")

    ap_analysis = subp.add_parser("analysis")
    ap_analysis.add_argument("solver")
    ap_analysis.add_argument("version")
    ap_analysis.add_argument("--config",
                             default=None)

    ap_global_analysis = subp.add_parser("global_analysis")
    # pylint: enable=unused-variable

    options = ap.parse_args()

    match options.mode:
        case "run" | "analysis":
            solver = find_solver(solvers,
                                 options.solver,
                                 options.version,
                                 options.config)
            if solver is None:
                ap.error("could not find specified solver")

    match options.mode:
        case "manifest":
            benchmarks = survery_benchmarks()
            with open("manifest.json", "w", encoding="UTF-8") as fd:
                json.dump([bench.to_json()
                           for bench in benchmarks],
                          fd,
                          sort_keys = True,
                          indent = 2)

        case "install_all":
            for solver in solvers:
                solver.install()

        case "run":
            benchmarks = load_benchmarks(options.group, options.filter_name)
            results = run_benchmarks(solver,
                                     benchmarks,
                                     options.threads)
            serialise_results(results, solver)

        case "analysis":
            benchmarks = load_benchmarks()
            analyse_single(benchmarks, solver)

        case "global_analysis":
            benchmarks = load_benchmarks()
            analyse_global(benchmarks, solvers)

    return 0


if __name__ == "__main__":
    sys.exit(main())