From fafe8dbe07e346907fa38da36f9ebf9486ca91f2 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur@meski.io>
Date: Thu, 8 May 2025 19:41:27 +0100
Subject: [PATCH] Optimisations are now enabled by default

---
 reactics-bdd/options.hh  |  6 +++---
 reactics-bdd/reactics.cc | 23 +++++++++++------------
 2 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/reactics-bdd/options.hh b/reactics-bdd/options.hh
index 2c05c49..4428e9f 100644
--- a/reactics-bdd/options.hh
+++ b/reactics-bdd/options.hh
@@ -24,10 +24,10 @@ class Options
       show_progress = false;
       measure = false;
 
-      part_tr_rel = false;
+      part_tr_rel = true;
 
-      reorder_reach = false;
-      reorder_trans = false;
+      reorder_reach = true;
+      reorder_trans = true;
 
       backend_mode = false;
 
diff --git a/reactics-bdd/reactics.cc b/reactics-bdd/reactics.cc
index fddd010..c86fec5 100644
--- a/reactics-bdd/reactics.cc
+++ b/reactics-bdd/reactics.cc
@@ -32,7 +32,7 @@ int main(int argc, char **argv)
   int c;
   int option_index = 0;
 
-  while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzXhe", long_options,
+  while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheEG", long_options,
                           &option_index)) != -1) {
     switch (c) {
       case 0:
@@ -102,13 +102,13 @@ int main(int argc, char **argv)
         opts->verbose++;
         break;
 
-      case 'x':
-        opts->part_tr_rel = true;
+      case 'E':
+        opts->reorder_reach = false;
+        opts->reorder_trans = false;
         break;
 
-      case 'z':
-        opts->reorder_reach = true;
-        opts->reorder_trans = true;
+      case 'G':
+        opts->part_tr_rel = false;
         break;
 
       case 'X':
@@ -266,15 +266,14 @@ void print_help(std::string path_str)
        << endl
        << endl << " OTHER:" << endl
        << "  -b       -- disable bounded model checking (BMC) heuristic" << endl
-       << "  -x       -- use partitioned transition relation" <<
-       endl
-       << "  -z       -- use reordering of the BDD variables" << endl
-       << "  -v       -- verbose (use more than once to increase verbosity)" <<
-       endl
+       << "  -v       -- verbose (use more than once to increase verbosity)" << endl
        << "  -p       -- show progress (where possible)" << endl
-       << endl
        << "  -X       -- backend mode (makes output parsing easier)" << endl
        << endl
+       << " Optimisations:" << endl
+       << "  -E       -- disable auto-reordering optimisation of BDDs" << endl
+       << "  -G       -- disable partitioned transition relation optimisation" << endl
+       << endl
        << " Benchmarking options:" << endl
        << "  -m       -- measure and display time and memory usage" << endl
        << "  -B       -- display an easy to parse summary (enables -m)" << endl