From d4ac425963a755456855c3fe0e07ad37e15a4e44 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sat, 22 Sep 2018 20:05:19 +0100
Subject: [PATCH] state constraints

---
 stateconstr.cc |  74 +++++++++++++++++++++++++++++++++
 stateconstr.hh | 110 +++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 184 insertions(+)
 create mode 100644 stateconstr.cc
 create mode 100644 stateconstr.hh

diff --git a/stateconstr.cc b/stateconstr.cc
new file mode 100644
index 0000000..b1e47e4
--- /dev/null
+++ b/stateconstr.cc
@@ -0,0 +1,74 @@
+/*
+    Copyright (c) 2018
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#include "stateconstr.hh"
+
+std::string StateConstr::toStr(void) const
+{
+  if (oper == STC_PV) {
+    return proc_name + "." + entity_name;
+  }
+  else if (oper == STC_TF) {
+    if (tf) {
+      return "true";
+    }
+    else {
+      return "false";
+    }
+  }
+  else if (oper == STC_AND) {
+    return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_OR) {
+    return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_XOR) {
+    return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_NOT) {
+    return "~" + arg[0]->toStr();
+  }
+
+  else {
+    return "??";
+    assert(0);
+  }
+}
+
+BDD StateConstr::getBDD(const SymRS *srs) const
+{
+  if (oper == STC_PV) {
+    return srs->encActStrEntity(proc_name, entity_name);
+  }
+  else if (oper == STC_TF) {
+    if (tf) {
+      return srs->getBDDtrue();
+    }
+    else {
+      return srs->getBDDfalse();
+    }
+  }
+  else if (oper == STC_AND) {
+    return arg[0]->getBDD(srs) * arg[1]->getBDD(srs);
+  }
+  else if (oper == STC_OR) {
+    return arg[0]->getBDD(srs) + arg[1]->getBDD(srs);
+  }
+  else if (oper == STC_XOR) {
+    return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs);
+  }
+  else if (oper == STC_NOT) {
+    return !arg[0]->getBDD(srs);
+  }
+  else {
+    assert(0);
+    FERROR("Undefined operator used in Boolean context definition. This should not happen.");
+    return srs->getBDDfalse();
+  }
+}
+
diff --git a/stateconstr.hh b/stateconstr.hh
new file mode 100644
index 0000000..8fbbc59
--- /dev/null
+++ b/stateconstr.hh
@@ -0,0 +1,110 @@
+/*
+    Copyright (c) 2018
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#ifndef STATECONSTR_HH
+#define STATECONSTR_HH
+
+#include "types.hh"
+
+/* For Boolean contexts: */
+#define STC_PV   80
+#define STC_AND  81
+#define STC_OR   82
+#define STC_XOR  83
+#define STC_NOT  84
+#define STC_TF   90
+
+#define STC_COND_1ARG(a) ((a) == STC_NOT)
+#define STC_COND_2ARG(a) ((a) == STC_AND || (a) == STC_OR || (a) == STC_XOR)
+#define STC_IS_VALID(a) (STC_COND_1ARG(a) || STC_COND_2ARG(a) || (a) == STC_PV || (a) == STC_TF)
+
+class SymRS;
+
+class StateConstr
+{
+    Oper oper;
+    StateConstr *arg[2];
+    std::string entity_name;
+    std::string proc_name;
+    bool tf;
+
+  public:
+
+    StateConstr(std::string procName, std::string varName)
+    {
+      oper = STC_PV;
+      entity_name = varName;
+      proc_name = procName;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for true/false.
+     *
+     * @param   val value of the logical constant
+     */
+    StateConstr(bool val)
+    {
+      oper = STC_TF;
+      tf = val;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for one-argument formula.
+     */
+    StateConstr(Oper op, StateConstr *form1)
+    {
+      assert(op == STC_NOT);
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for two-argument formula.
+     */
+    StateConstr(Oper op, StateConstr *form1, StateConstr *form2)
+    {
+      assert(STC_COND_2ARG(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = form2;
+    }
+
+    ~StateConstr()
+    {
+      delete arg[0];
+      delete arg[1];
+    }
+
+    std::string toStr(void) const;
+
+    BDD getBDD(const SymRS *srs) const;
+
+    Oper getOper(void) const
+    {
+      assert(STC_IS_VALID(oper));
+      return oper;
+    }
+    StateConstr *getLeftSF(void) const
+    {
+      assert(arg[0] != nullptr);
+      return arg[0];
+    }
+    StateConstr *getRightSF(void) const
+    {
+      assert(STC_COND_2ARG(oper));
+      assert(arg[1] != nullptr);
+      return arg[1];
+    }
+};
+
+#endif