Tyding up

etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info_per-category.csv

@@ -0,0 +1,27 @@
+category;total;min-clauses;max-clauses;avg-clauses;AALTAF@min-UC;AALTAF@min-UC[%];AALTAF@min-timing;AALTAF@min-timing%;TRP++@min-UC;TRP++@min-UC[%];TRP++@min-timing;TRP++@min-timing%;NuSMV-S@min-UC;NuSMV-S@min-UC[%];NuSMV-S@min-timing;NuSMV-S@min-timing%;NuSMV-B@min-UC;NuSMV-B@min-UC[%];NuSMV-B@min-timing;NuSMV-B@min-timing%;None@min-UC;None@min-UC[%];None@min-timing;None@min-timing%
+;1377;1;1002;97.63;690;50.11;1260;91.50;543;39.43;0;0.00;12;0.87;8;0.58;104;7.55;81;5.88;28;2.03;28;2.03
+LTL-as-LTLf/acacia/demo-v3/demo-v3:cl;11;9;49;29.00;7;63.64;11;100.00;4;36.36;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift;17;13;29;21.00;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:b;17;12;32;22.47;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:b:f;17;12;32;22.47;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:b:f:l;17;14;50;32.47;15;88.24;16;94.12;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
+LTL-as-LTLf/alaska/lift/lift:b:l;17;14;50;32.47;14;82.35;17;100.00;3;17.65;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:f;17;13;29;21.00;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:f:l;17;15;47;31.00;15;88.24;16;94.12;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
+LTL-as-LTLf/alaska/lift/lift:l;17;15;47;31.00;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/anzu/amba/amba:c;17;75;351;213.47;15;88.24;15;88.24;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;2;11.76;2;11.76
+LTL-as-LTLf/anzu/amba/amba:cl;17;77;369;223.47;16;94.12;16;94.12;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
+LTL-as-LTLf/anzu/genbuf/genbuf;20;1;1;1.00;20;100.00;20;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/anzu/genbuf/genbuf:c;20;57;441;221.00;20;100.00;20;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/anzu/genbuf/genbuf:cl;20;58;461;231.50;18;90.00;18;90.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;2;10.00;2;10.00
+LTL-as-LTLf/forobots;38;6;6;6.00;38;100.00;38;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/rozier/counter/counter;19;6;24;15.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;14;73.68;14;73.68;5;26.32;5;26.32
+LTL-as-LTLf/rozier/counter/counterCarry;19;8;26;17.00;0;0.00;0;0.00;6;31.58;0;0.00;0;0.00;0;0.00;12;63.16;18;94.74;1;5.26;1;5.26
+LTL-as-LTLf/rozier/counter/counterCarryLinear;19;8;8;8.00;0;0.00;0;0.00;6;31.58;0;0.00;0;0.00;0;0.00;13;68.42;19;100.00;0;0.00;0;0.00
+LTL-as-LTLf/rozier/counter/counterLinear;18;6;6;6.00;0;0.00;1;5.56;0;0.00;0;0.00;0;0.00;0;0.00;18;100.00;17;94.44;0;0.00;0;0.00
+LTL-as-LTLf/rozier/formulas/n;30;1;4;1.33;12;40.00;24;80.00;0;0.00;0;0.00;8;26.67;4;13.33;10;33.33;2;6.67;0;0.00;0;0.00
+LTL-as-LTLf/schuppan/O1formula;27;4;1002;224.00;20;74.07;20;74.07;0;0.00;0;0.00;4;14.81;4;14.81;3;11.11;3;11.11;0;0.00;0;0.00
+LTL-as-LTLf/schuppan/O2formula;27;2;1000;222.00;5;18.52;5;18.52;0;0.00;0;0.00;0;0.00;0;0.00;8;29.63;8;29.63;14;51.85;14;51.85
+LTL-as-LTLf/schuppan/phltl;13;5;101;30.85;12;92.31;12;92.31;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;7.69;1;7.69
+LTLf-specific/benchmarks:ltlf/LTLfRandomConjunction/C100;500;118;154;131.50;255;51.00;500;100.00;245;49.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTLf-specific/benchmarks:ltlf/LTLfRandomConjunction/V20;425;13;146;81.54;127;29.88;425;100.00;272;64.00;0;0.00;0;0.00;0;0.00;26;6.12;0;0.00;0;0.00;0;0.00

etc/AIJ-SAT-explorer/run-AIJ-results-analysis.py

@@ -301,7 +301,7 @@ def compute_stats(results={}, tool='aaltafuc',
     return (results, pre_parsing_solutions, timeouts, unknowns)
 
 
-def compute_virtual_best(results, vbest_tool_name=V_BEST_TOOL.tool_codename, csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results-virtual_best_info.csv'):
+def compute_virtual_best(results, vbest_tool_name=V_BEST_TOOL.tool_codename, csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results_virtual-best_info.csv'):
     csv_f = open(csv_outfile, 'w')
     csv_f.write('Test;Clauses;BestTime;BestPerformer;MinUnSATCore;MinUnSATFinder\n')
     absolute_minimum_timing = TIMEOUT
@@ -496,11 +496,13 @@ def create_csv(results, output_file):
         csv_f.write("\n")
 
 
-def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbest_tool_name=V_BEST_TOOL.tool_codename, criteria=['best_performer', 'min_unsat_core_finder'], csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results-virtual_best_info.csv'):
+def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbest_tool_name=V_BEST_TOOL.tool_codename, criteria=['best_performer', 'min_unsat_core_finder'], csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results_virtual-best_info_per-category.csv'):
     all_tools = [x for x in TOOLS.keys()] + [NO_TOOL.tool_codename]  # Including the “None” tool
+    min_cl = max_cl = avg_cl = 0
 
     test_filename_prefixes = [''] + test_filename_prefixes  # Including the “catch-all” category
     total_tests_counter = {x: 0 for x in test_filename_prefixes}
+    clauses_stats = {x: {'min': 0, 'max': 0, 'avg': 0} for x in test_filename_prefixes}
 
     tool_best_counters = {x: {} for x in test_filename_prefixes}
     for test_filename_prefix in test_filename_prefixes:
@@ -510,17 +512,22 @@ def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbe
                 tool_best_counters[test_filename_prefix][tool][criterion] = 0
                 tool_best_counters[test_filename_prefix][tool][criterion] = 0
 
+    retrieve_stats = True
     for criterion in criteria:
         for test_filename_prefix in test_filename_prefixes:  # Computational complexity is definitely improvable. I know
-            (best_performances_per_tool, total) = \
-                get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
+            (best_performances_per_tool, total, min_cl, max_cl, avg_cl) = \
+                get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name, retrieve_stats)
             for tool in best_performances_per_tool:  # Write
                 tool_best_counters[test_filename_prefix][tool][criterion] = best_performances_per_tool[tool]
             total_tests_counter[test_filename_prefix] = total
-
+            if retrieve_stats:
+                clauses_stats[test_filename_prefix]['min'] = min_cl
+                clauses_stats[test_filename_prefix]['max'] = max_cl
+                clauses_stats[test_filename_prefix]['avg'] = avg_cl
+        retrieve_stats = False
 
     csv_f = open(csv_outfile, 'w')
-    csv_f.write("category;total")
+    csv_f.write("category;total;min-clauses;max-clauses;avg-clauses")
     # Write the header
     for tool in all_tools:
         tool_label = NO_TOOL.tool_label if tool not in TOOLS else TOOLS[tool].tool_label
@@ -533,6 +540,12 @@ def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbe
         csv_f.write(build_category_label_from_path_prefix(test_filename_prefix))
         csv_f.write(';')
         csv_f.write(str(total_tests_counter[test_filename_prefix]))
+        csv_f.write(';')
+        csv_f.write(str(clauses_stats[test_filename_prefix]['min']))
+        csv_f.write(';')
+        csv_f.write(str(clauses_stats[test_filename_prefix]['max']))
+        csv_f.write(';')
+        csv_f.write("%0.2f" % clauses_stats[test_filename_prefix]['avg'])
         for tool in all_tools:
             csv_f.write(";" + str(tool_best_counters[test_filename_prefix][tool]['min_unsat_core_finder']) +
                         ";%0.2f" % (tool_best_counters[test_filename_prefix][tool]['min_unsat_core_finder'] / total_tests_counter[test_filename_prefix] * 100.0) +
@@ -872,7 +885,7 @@ def plot_unsat_core_cardinality_scatter(figure_seq_num, results, tool_0, tool_1,
 def plot_best_piechart(figure_seq_num, results, best_piechart_filename_template, test_filename_prefix='',
                        vbest_tool_name=V_BEST_TOOL.tool_codename, criterion='best_performer'):
     plt.figure(figure_seq_num)
-    (best_performances_per_tool, total) = get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
+    (best_performances_per_tool, total, _, _, _) = get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
 
     labels = [TOOLS[tool].tool_label for tool in best_performances_per_tool.keys() if tool != NO_TOOL.tool_codename]
     labels.append(NO_TOOL.tool_label)
@@ -893,9 +906,12 @@ def show_total_in_place_of_percentage(p):
     plt.close(figure_seq_num)
 
 
-def get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name):
+def get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name, retrieve_stats=False):
     best_performances_per_tool = {}
     total = 0
+    min_cl = -1
+    max_cl = avg_cl = tot_clauses = 0
+
     for test in results.keys():
         if test.startswith(test_filename_prefix):
             total += 1
@@ -906,7 +922,15 @@ def get_best_performers(criterion, results, test_filename_prefix, vbest_tool_nam
                 best_performances_per_tool[best_tool] = 1
             else:
                 best_performances_per_tool[best_tool] += 1
-    return (best_performances_per_tool, total)
+            if retrieve_stats:
+                clauses = results[test][vbest_tool_name]['clauses']
+                tot_clauses += clauses
+                if min_cl < 0 or clauses < min_cl:
+                    min_cl = clauses
+                if max_cl < clauses:
+                    max_cl = clauses
+    avg_cl = tot_clauses * 1.0 / total
+    return (best_performances_per_tool, total, min_cl, max_cl, avg_cl)
 
 
 def plot_best_stacked_bar_per_category(figure_seq_num, results, best_stacked_bar_per_category_filename_template, test_filename_prefixes=[''],
@@ -918,7 +942,7 @@ def plot_best_stacked_bar_per_category(figure_seq_num, results, best_stacked_bar
     tool_best_counters[NO_TOOL.tool_codename] = []
     i = 0
     for test_filename_prefix in test_filename_prefixes:  # Computational complexity is definitely improvable. I know
-        (best_performances_per_tool, total) = \
+        (best_performances_per_tool, total, _, _, _) = \
             get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
         for tool in tool_best_counters:  # Init
             tool_best_counters[tool].append(0)