Update scripts

formalsec · Oct 24, 2024 · 65b1bc0 · 65b1bc0
1 parent 795b582
commit 65b1bc0
Show file tree

Hide file tree

Showing 8 changed files with 33,282 additions and 33,194 deletions.
diff --git a/bench/QF_BV_paths.list b/bench/QF_BV_paths.list
diff --git a/bench/QF_FP_paths.list b/bench/QF_FP_paths.list
diff --git a/bench/QF_LIA_paths.list b/bench/QF_LIA_paths.list
diff --git a/bench/QF_SLIA_paths.list b/bench/QF_SLIA_paths.list
diff --git a/bench/QF_S_paths.list b/bench/QF_S_paths.list
diff --git a/bench/eq2.sh b/bench/eq2.sh
@@ -39,3 +39,27 @@ python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir
 python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_colibri2 --prover smtml-colibri2
 #### QF_BV ####
 python3 single_query.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_colibri2 --prover smtml-colibri2
+
+## Concat CSVs ##
+#### QF_FP ####
+python3 plots.py --output csvs_single/QF_FP_all.csv --concat csvs_single/QF_FP_z3.csv csvs_single/QF_FP_bitwuzla.csv csvs_single/QF_FP_cvc5.csv csvs_single/QF_FP_colibri2.csv
+#### QF_LIA ####
+python3 plots.py --output csvs_single/QF_LIA_all.csv --concat csvs_single/QF_LIA_z3.csv csvs_single/QF_LIA_cvc5.csv csvs_single/QF_LIA_colibri2.csv
+#### QF_BV ####
+python3 plots.py --output csvs_single/QF_BV_all.csv --concat csvs_single/QF_BV_z3.csv csvs_single/QF_BV_bitwuzla.csv csvs_single/QF_BV_cvc5.csv csvs_single/QF_BV_colibri2.csv
+#### QF_S ####
+python3 plots.py --output csvs_single/QF_S_all.csv --concat csvs_single/QF_S_z3.csv csvs_single/QF_S_cvc5.csv
+#### QF_SLIA ####
+python3 plots.py --output csvs_single/QF_SLIA_all.csv --concat csvs_single/QF_SLIA_z3.csv csvs_single/QF_SLIA_cvc5.csv
+
+## Generate plots ##
+#### QF_FP ####
+python3 plots.py --single --QF-FP --output plot_QF_FP --files csvs_single/QF_FP_all.csv
+#### QF_LIA ####
+python3 plots.py --single --QF-LIA --output plot_QF_LIA --files csvs_single/QF_LIA_all.csv
+#### QF_BV ####
+python3 plots.py --single --QF-BV --output plot_QF_BV --files csvs_single/QF_BV_all.csv
+#### QF_S ####
+python3 plots.py --single --QF-S --output plot_QF_S --files csvs_single/QF_S_all.csv
+#### QF_SLIA ####
+python3 plots.py --single --QF-SLIA --output plot_QF_SLIA --files csvs_single/QF_SLIA_all.csv
diff --git a/bench/plots.py b/bench/plots.py
@@ -16,6 +16,14 @@ def print_success(msg):
 def print_info(msg):
   print(f"\033[94m{msg}\033[0m")
 
+def concat_dfs(files, output_file):
+  dfs = []
+  for file in files:
+    df = pd.read_csv(file)
+    dfs.append(df)
+  result = pd.concat(dfs)
+  result.to_csv(output_file, index=False)
+
 ############################################################################################################
 #                                           Single-query                                                   #
 ############################################################################################################
@@ -647,48 +655,93 @@ def plot_multi_testcomp_eca(file_multi, file_single_solver, file_single_smtml, o
   parser.add_argument('--multi', action='store_true', help='Generate plots for single-query results')
   parser.add_argument('--single', action='store_true', help='Generate plots for single-query results')
   parser.add_argument('--testcomp', action='store_true', help='Generate plots for Test-Comp 2023 benchmarks')
+  parser.add_argument('--QF-FP', action='store_true', help='Run QF_FP benchmarks')
+  parser.add_argument('--QF-LIA', action='store_true', help='Run QF_LIA benchmarks')
+  parser.add_argument('--QF-BV', action='store_true', help='Run QF_BV benchmarks')
+  parser.add_argument('--QF-S', action='store_true', help='Run QF_S benchmarks')
+  parser.add_argument('--QF-SLIA', action='store_true', help='Run QF_SLIA benchmarks')
+  parser.add_argument('--array-examples', action='store_true', help='Run array-examples benchmarks')
+  parser.add_argument('--array-industry-pattern', action='store_true', help='Run array-industry-pattern benchmarks')
+  parser.add_argument('--eca-rers20218', action='store_true', help='Run eca-rers20218 benchmarks')
+  parser.add_argument('--concat', action='store_true', help='Concatenate the results')
+  parser.add_argument('--files', nargs='+', help='List of input files')
   args = parser.parse_args()
 
   if not args.output:
     print_error("Output file name not provided.")
     print("Use --output to specify the output file name.")
     sys.exit(1)
-
+
+  if args.concat:
+    print_info("Concatenating the results")
+    concat_dfs(args.files, args.output)
+    print_success("Results concatenated successfully.")
+    sys.exit(0)
+
   if args.single:
-    print_info("Generating plots for single-query results")
-    print_info("Generating plots for QF_FP")
-    plot_QF_FP_single('benchmarks/QF_FP.csv', f'{args.output}_QF_FP')
-    print_info("Generating plots for QF_LIA")
-    plot_QF_LIA_single('benchmarks/QF_LIA.csv', f'{args.output}_QF_LIA')
-    print_info("Generating plots for QF_BV")
-    plot_QF_BV_single('benchmarks/QF_BV.csv', f'{args.output}_QF_BV')
-    print_info("Generating plots for QF_S")
-    plot_QF_S_single('benchmarks/QF_S.csv', f'{args.output}_QF_S')
-    print_info("Generating plots for QF_SLIA")
-    plot_QF_SLIA_single('benchmarks/QF_SLIA.csv', f'{args.output}_QF_SLIA')
-    print_success("All plots generated successfully")
+    if args.QF_FP:
+      print_info("Generating plots for QF_FP")
+      plot_QF_FP_single(args.files[0], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_LIA:
+      print_info("Generating plots for QF_LIA")
+      plot_QF_LIA_single(args.files[0], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_BV:
+      print_info("Generating plots for QF_BV")
+      plot_QF_BV_single(args.files[0], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_S:
+      print_info("Generating plots for QF_S")
+      plot_QF_S_single(args.files[0], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_SLIA:
+      print_info("Generating plots for QF_SLIA")
+      plot_QF_SLIA_single(args.files[0], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    else:
+      print_error("No benchmark selected.")
+      sys.exit(1)
   elif args.multi:
-    print_info("Generating plots for multi-query results")
-    print_info("Generating plots for QF_FP")
-    plot_QF_FP_multi('benchmarks/QF_FP_multi.csv', 'benchmarks/QF_FP.csv', 'benchmarks/QF_FP_bitwuzla.csv', 'benchmarks/bitwuzla_QF_FP.csv', f'{args.output}_QF_FP')
-    print_info("Generating plots for QF_LIA")
-    plot_QF_LIA_multi('benchmarks/QF_LIA_multi.csv', 'benchmarks/QF_LIA.csv', f'{args.output}_QF_LIA')
-    print_info("Generating plots for QF_BV")
-    plot_QF_BV_multi('benchmarks/QF_BV_multi.csv', 'benchmarks/QF_BV.csv', f'{args.output}_QF_BV')
-    print_info("Generating plots for QF_S")
-    plot_QF_S_multi('benchmarks/QF_S_multi.csv', 'benchmarks/QF_S.csv', f'{args.output}_QF_S')
-    print_info("Generating plots for QF_SLIA")
-    plot_QF_SLIA_multi('benchmarks/QF_SLIA_multi.csv', 'benchmarks/QF_SLIA.csv', f'{args.output}_QF_SLIA')
-    print_success("All plots generated successfully")
+    if args.QF_FP:
+      print_info("Generating plots for QF_FP")
+      plot_QF_FP_multi(args.files[0], args.files[1], args.files[2], args.files[3], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_LIA:
+      print_info("Generating plots for QF_LIA")
+      plot_QF_LIA_multi(args.files[0], args.files[1], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_BV:
+      print_info("Generating plots for QF_BV")
+      plot_QF_BV_multi(args.files[0], args.files[1], args.files[2], args.files[3], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_S:
+      print_info("Generating plots for QF_S")
+      plot_QF_S_multi(args.files[0], args.files[1], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.QF_SLIA:
+      print_info("Generating plots for QF_SLIA")
+      plot_QF_SLIA_multi(args.files[0], args.files[1], args.output)
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    else:
+      print_error("No benchmark selected.")
+      sys.exit(1)
   elif args.testcomp:
-    print_info("Generating plots for Test-Comp 2023 benchmarks")
-    print_info("Generating plots for array-examples category")
-    plot_multi_testcomp_array('benchmarks/testcomp2023_array.csv', 'benchmarks/array-examples.csv', 'benchmarks/array-examples_smtml.csv', f'{args.output}_array')
-    print_info("Generating plots for array-industry-pattern category")
-    plot_multi_testcomp_array_industry('benchmarks/testcomp2023_array_industry.csv', 'benchmarks/array-industry-pattern.csv', 'benchmarks/array-industry-pattern_smtml.csv', f'{args.output}_array_industry')
-    print_info("Generating plots for eca-rers20218 category")
-    plot_multi_testcomp_eca('benchmarks/testcomp2023_eca.csv', 'benchmarks/eca-rers20218.csv', 'benchmarks/eca-rers20218_smtml.csv', f'{args.output}_eca')
-    print_success("All plots generated successfully")
+    if args.array_examples:
+      print_info("Generating plots for array-examples category")
+      plot_multi_testcomp_array('benchmarks/testcomp2023_array.csv', 'benchmarks/array-examples.csv', 'benchmarks/array-examples_smtml.csv', f'{args.output}_array')
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.array_industry_pattern:
+      print_info("Generating plots for array-industry-pattern category")
+      plot_multi_testcomp_array_industry('benchmarks/testcomp2023_array_industry.csv', 'benchmarks/array-industry-pattern.csv', 'benchmarks/array-industry-pattern_smtml.csv', f'{args.output}_array_industry')
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    elif args.eca_rers20218:
+      print_info("Generating plots for eca-rers20218 category")
+      plot_multi_testcomp_eca('benchmarks/testcomp2023_eca.csv', 'benchmarks/eca-rers20218.csv', 'benchmarks/eca-rers20218_smtml.csv', f'{args.output}_eca')
+      print_success(f"Plot generated successfully. Saved to {args.output}.pdf")
+    else:
+      print_error("No category selected.")
+      sys.exit(1)
   else:
     print_error("No option selected.")
     print("Use --single to generate plots for single-query results")

diff --git a/bench/single_query.py → bench/run_benchmarks.py b/bench/single_query.py → bench/run_benchmarks.py
@@ -50,7 +50,7 @@ def to_csv(sqlite_file, output_csv_dir, output_csv_name, table_name="prover_res"
       writer.writerows(rows)
   conn.close()
 
-def automate_benchpress(directory_to_benchmark, output_csv_dir, output_csv_name, config, prover):
+def automate_benchpress_single(directory_to_benchmark, output_csv_dir, output_csv_name, config, prover):
   benchpress_data_dir = "/home/smtml/.local/share/benchpress"
   if run_benchpress(directory_to_benchmark, config, prover):
     try:
@@ -62,14 +62,25 @@ def automate_benchpress(directory_to_benchmark, output_csv_dir, output_csv_name,
     except Exception as e:
       print_error(f"Error during SQLite to CSV process: {e}")
 
+def automate_multi_query():
+  pass
+
 if __name__ == "__main__":
   parser = argparse.ArgumentParser(description="Automate benchpress and convert the output to CSV.")
   parser.add_argument("--dir", type=str, help="The directory to benchmark.")
   parser.add_argument("--output-dir", type=str, help="The directory to store the CSV files.")
   parser.add_argument("--output-filename", type=str, default="benchpress_output", help="The name of the CSV file.")
   parser.add_argument("--config", type=str, default="/home/smtml/smtml/bench/benchpress.sexp", help="The name of the CSV file.")
   parser.add_argument("--prover", type=str, help="The solver to be used.")
+  parser.add_argument("--single", action="store_true", help="Run single-query mode.")
+  parser.add_argument("--multi", action="store_true", help="Run multi-query mode.")
   parser.add_argument("-j", type=int, help="Number of threads to use.")
   parser.add_argument("-t", type=int, help="Timeout (in seconds).")
   args = parser.parse_args()
-  automate_benchpress(args.dir, args.output_dir, args.output_filename, args.config, args.prover)
+
+  if args.single:
+    automate_benchpress_single(args.dir, args.output_dir, args.output_filename, args.config, args.prover)
+  elif args.multi:
+    automate_multi_query()
+  else:
+    print_error("Please specify --single or --multi.")