Permalink
Browse files

SMTLIB Benchmark: Revised Util

  • Loading branch information...
marcogario committed Aug 13, 2017
1 parent c5c4a84 commit 6782ae110ef8865892d2af1fddcb6b43f75f81eb
Showing with 29 additions and 120 deletions.
  1. +0 −53 SMT-LIB/download.py
  2. +29 −25 SMT-LIB/parse_all.py
  3. +0 −5 SMT-LIB/parse_all.sh
  4. +0 −37 SMT-LIB/smtlib.urls
View

This file was deleted.

Oops, something went wrong.
View
@@ -3,18 +3,16 @@
import sys
import random
import multiprocessing
import argparse
from itertools import islice
from pysmt.shortcuts import reset_env, get_env
from pysmt.smtlib.parser import SmtLibParser
from pysmt.solvers.noop import NoopSolver
from pysmt.shortcuts import reset_env, read_smtlib
SMTLIB_DIR = "./"
def get_all_smt_files(target_dir=None):
if target_dir == None:
target_dir = SMTLIB_DIR
target_dir = "./"
assert os.path.exists(target_dir)
for root, _, files in os.walk(target_dir):
@@ -28,46 +26,52 @@ def execute_script_fname(smtfile):
print(smtfile)
reset_env()
assert os.path.exists(smtfile)
parser = SmtLibParser()
solver = NoopSolver(get_env())
start = time.clock()
script = parser.get_script_fname(smtfile)
read_smtlib(smtfile)
end = time.clock()
script.evaluate(solver)
res = solver.get_asserted_formula()
assert res is not None
return (smtfile, (end - start))
return ( (end - start), smtfile)
def dump_stats(timings, fname):
if fname is None:
fname = "stats.out"
with open(fname, "w") as f:
f.write('filename, time\n')
for k in timings:
f.write('"%s", "%s"\n' % k)
f.write('%f, "%s"\n' % k)
def main():
if len(sys.argv) != 3:
print("usage: %s <number of files to benchmark> <statistics file>" %\
sys.argv[0])
exit(1)
parser = argparse.ArgumentParser(description='SMT-LIB Parser Benchmarking')
parser.add_argument('--base', type=str, nargs='?',
help='top-directory of the benchmarks')
parser.add_argument('--count', type=int, nargs='?',
default=-1,
help='number of files to benchmark')
parser.add_argument('--out', type=str, default="stats.out", nargs='?',
help='Where to save the statistics')
args = parser.parse_args()
random.seed(42)
p = multiprocessing.Pool()
chunks = multiprocessing.cpu_count()
file_list = list(get_all_smt_files())
file_list = list(get_all_smt_files(args.base))
random.shuffle(file_list)
files_cnt = int(sys.argv[1])
if args.count == -1:
files_cnt = len(file_list)
else:
files_cnt = args.count
print("Submitting %d jobs, %d at the time" % (files_cnt, chunks))
timings = p.map(execute_script_fname, islice(file_list, files_cnt), chunks)
mean = sum(x[1] for x in timings) / len(timings)
print("The mean execution time is:", mean, "seconds")
mean = sum(x[0] for x in timings) / len(timings)
print("The mean execution time was %0.2f seconds" % mean)
print("The max execution time was %0.2f seconds" % max(x[0] for x in timings))
outfile = sys.argv[2]
outfile = args.out
dump_stats(timings, outfile)
print("The statistics file has been generated in '%s'" % outfile)
View

This file was deleted.

Oops, something went wrong.
View

This file was deleted.

Oops, something went wrong.

0 comments on commit 6782ae1

Please sign in to comment.