From 07171c6d605118437a2273cd69bf2bc22365d9c4 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 22 Jul 2018 20:20:14 +0100
Subject: [PATCH] Optimisations

---
 drs_benchmark.sh |  4 ++--
 formrsctlk.hh    |  6 +++---
 mc.cc            | 13 +++++++++++++
 mc.hh            |  2 ++
 symrs.cc         |  3 ++-
 5 files changed, 22 insertions(+), 6 deletions(-)

diff --git a/drs_benchmark.sh b/drs_benchmark.sh
index d944121..05edb14 100755
--- a/drs_benchmark.sh
+++ b/drs_benchmark.sh
@@ -2,9 +2,9 @@
 
 TMPINPUT="tmp_$RANDOM$RANDOM.rs"
 
-CMD="./reactics -z -b -B"
+CMD="./reactics -zxbB"
 
-for i in `seq 2 20`;do
+for i in `seq 2 9`;do
 
 	echo "[i] n=$i; generating input file"
 	in/gen_drs_mutex.py $i > $TMPINPUT
diff --git a/formrsctlk.hh b/formrsctlk.hh
index b992ff6..b9b94c0 100644
--- a/formrsctlk.hh
+++ b/formrsctlk.hh
@@ -40,8 +40,8 @@
 #define RSCTLK_AF_ACT  44
 #define RSCTLK_TF      50 // true/false
 
-#define RSCTLK_UK      60 // Epistemic operators
-#define RSCTLK_NK      61
+#define RSCTLK_NK      61 // Epistemic operators
+#define RSCTLK_UK      71
 
 /* For Boolean contexts: */
 #define BCTX_PV   80
@@ -57,7 +57,7 @@
 #define RSCTLK_COND_ACT(a) ((a) > 30 && (a) < 45)
 #define RSCTLK_IS_VALID(a) (RSCTLK_COND_1ARG(a) || RSCTLK_COND_2ARG(a) || (a) == RSCTLK_PV || (a) == RSCTLK_TF)
 
-#define RSCTLK_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45))
+#define RSCTLK_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45) || ((a) > 70 && (a) < 75))
 
 #define BCTX_COND_1ARG(a) ((a) == BCTX_NOT)
 #define BCTX_COND_2ARG(a) ((a) == BCTX_AND || (a) == BCTX_OR || (a) == BCTX_XOR)
diff --git a/mc.cc b/mc.cc
index 8dcf876..4d20649 100644
--- a/mc.cc
+++ b/mc.cc
@@ -75,6 +75,7 @@ inline BDD ModelChecker::getSucc(const BDD &states)
   if (opts->part_tr_rel) {
     for (const auto &trans : *trp) {
       q *= states * trans;
+      reorder();
     }
   }
   else {
@@ -101,6 +102,7 @@ inline BDD ModelChecker::getPreE(const BDD &states)
   if (opts->part_tr_rel) {
     for (const auto &trans : *trp) {
       q *= x * trans;
+      reorder();
     }
   }
   else {
@@ -123,6 +125,7 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
   if (opts->part_tr_rel) {
     for (const auto &trans : *trp) {
       q *= x * trans;
+      reorder();
     }
     q *= *contexts;
   }
@@ -619,6 +622,16 @@ bool ModelChecker::checkRSCTLKbmc(FormRSCTLK *form)
   return result;
 }
 
+void ModelChecker::reorder(void)
+{
+  if (opts->reorder_trans) {
+    VERB_L2("Reordering START");
+    // Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 100000);
+    cuddMgr->ReduceHeap(CUDD_REORDER_GROUP_SIFT);
+    VERB_L2("Reordering DONE");
+  }
+}
+
 void ModelChecker::cleanup(void)
 {
   delete reach;
diff --git a/mc.hh b/mc.hh
index 54b87b9..663d3bd 100644
--- a/mc.hh
+++ b/mc.hh
@@ -66,6 +66,8 @@ class ModelChecker
 
     void cleanup(void);
 
+    void reorder(void);
+    
   public:
     ModelChecker(SymRS *srs, Options *opts);
 
diff --git a/symrs.cc b/symrs.cc
index 0e37d21..1258e90 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -946,7 +946,8 @@ void SymRS::reorder(void)
 {
   if (opts->reorder_trans) {
     VERB_L2("Reordering START");
-    Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
+    // Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
+    cuddMgr->ReduceHeap(CUDD_REORDER_GROUP_SIFT);
     VERB_L2("Reordering DONE");
   }
 }