Add CDF script to contrib

contrib/cdf.py

+#!/usr/bin/env python3
+
+from pathlib import Path
+import re
+import math
+import matplotlib.pyplot as plt
+import matplotlib.ticker as mticker
+# import tikzplotlib
+import numpy as np
+import csv
+
+logics = ["UF"]
+
+base_path = Path('.')
+
+simulation_1_file = base_path / "simulation_1.txt"
+simulation_2_file = base_path / "simulation_2.txt"
+all_strategies_file = base_path / "contrib" / "example_data.csv"
+
+data_re = r"^([^ ]+) +([-0-9\.]+) +([^ ]+)"
+
+paper_data_dir = Path(".")
+
+# This is in inches
+textwidth = 4.8041
+
+
+def parse_gtpt(file_name, logics):
+    result = {}
+    with open(file_name) as f:
+        for line in f:
+            m = re.match(data_re, line)
+            if m:
+                r = m.group(3).strip()
+                b = m.group(1)
+                # solved (1 is sat, 0 is unsat)
+                if r == "0":
+                    time = float(m.group(2))
+                else:
+                    time = math.inf
+                # exp_logic = m.group(1).split("/")[0]
+                exp_logic = "UF"
+                if exp_logic in logics:
+                    result[b] = time
+    return result
+
+
+def num_seq(ls, v):
+    for i in range(len(ls)):
+        if ls[i] > v:
+            return i + 1
+
+
+if __name__ == "__main__":
+    simulation_1 = parse_gtpt(simulation_1_file, logics)
+    simulation_2 = parse_gtpt(simulation_2_file, logics)
+
+    base_times = []
+    with open(all_strategies_file, newline="") as csvfile:
+        reader = csv.DictReader(csvfile, skipinitialspace=True, delimiter=";")
+        for row in reader:
+            strategy = row["strategy"].strip()
+            if strategy != "base-strategy":
+                continue
+            result = row["solved"].strip().lower()
+            if result in ["1", "yes", "true"]:
+                try:
+                    time = float(row["time"].strip())
+                    base_times.append(time)
+                except ValueError:
+                    pass
+    base_times.sort()
+
+    fig, ax = plt.subplots()
+    ax.grid(True)
+    ax.grid(color='0.75')
+    ax.set_xlabel(r'CPU Time', fontsize=10)
+    ax.set_ylabel(r'Solved Benchmarks', fontsize=10)
+    ax.spines['right'].set_visible(False)
+    ax.spines['top'].set_visible(False)
+    ax.xaxis.set_major_formatter(mticker.ScalarFormatter())
+    ax.yaxis.set_major_formatter(mticker.ScalarFormatter())
+    # ax.yaxis.get_offset_text().set_visible(False)
+    ax.ticklabel_format(style='plain')
+    ax.set_xlim([0, 6])
+    ax.set_ylim([0, 40])
+    plt.xticks([0, 1, 2, 3, 4, 5, 6])
+
+    n_sample = 1.5 * 100
+    time_max = 6.0
+    dist = 6.0 / (n_sample - 1)
+    sampling_6 = np.arange(0, time_max + dist, dist)
+
+    times_simulation_1 = list(simulation_1.values())
+    times_simulation_1.sort()
+    dist_simulation_1 = [num_seq(times_simulation_1, v) for v in sampling_6]
+
+    times_simulation_2 = list(simulation_2.values())
+    times_simulation_2.sort()
+    dist_simulation_2 = [num_seq(times_simulation_2, v) for v in sampling_6]
+
+    dist_base = [num_seq(base_times, v) for v in sampling_6]
+
+    ax.plot(sampling_6, dist_base, '-' , color="darkgray", label = "base strategy")
+    ax.plot(sampling_6, dist_simulation_1, linestyle='dashed', color='k', label = "slight jitter")
+    ax.plot(sampling_6, dist_simulation_2, '-' , color='k', label = "intese jitter")
+
+    ax.legend(fontsize="x-small")
+
+    fig.tight_layout()
+    fig.set_size_inches(w=textwidth * 1.1, h=textwidth * 0.1)
+
+    # tikzplotlib.clean_figure()
+    # tikzplotlib.save("plot.tex", flavor="context")
+    plt.show()