From d4135ed766304dfdd2864a4b3f5b975ab6b0d5bc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Sun, 26 Jan 2014 15:59:05 +0100
Subject: [PATCH] Add onestep.h onestep.cpp
---
GMLMIP-0.1/makefile | 5 ++-
GMLMIP-0.1/onestep.cpp | 81 ++++++++++++++++++++++++++++++++++++++++++
GMLMIP-0.1/onestep.h | 17 +++++++++
3 files changed, 102 insertions(+), 1 deletion(-)
create mode 100644 GMLMIP-0.1/onestep.cpp
create mode 100644 GMLMIP-0.1/onestep.h
diff --git a/GMLMIP-0.1/makefile b/GMLMIP-0.1/makefile
index 93b4228..dfdfdd2 100644
--- a/GMLMIP-0.1/makefile
+++ b/GMLMIP-0.1/makefile
@@ -13,7 +13,7 @@ parser/lex.yy.h
.PHONY: all clean parser/% formulas/% rules/%
-all: main onestep-example
+all: main onestep-example onestep.o
.PHONY: phony
# don't do anything here
@@ -44,5 +44,8 @@ main.o: main.cpp $(HEADERS)
onestep-example.o: onestep-example.cpp $(HEADERS)
$(GCC) $(GCCFLAGS) -c $<
+onestep.o: onestep.cpp $(HEADERS)
+ $(GCC) $(GCCFLAGS) -c $<
+
clean: parser/clean formulas/clean rules/clean
rm -rf *.o main
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
new file mode 100644
index 0000000..21f59af
--- /dev/null
+++ b/GMLMIP-0.1/onestep.cpp
@@ -0,0 +1,81 @@
+#include <iostream>
+#include <vector>
+#include <time.h>
+#include "onestep.h"
+
+#include "bdd.h"
+#include "./formulas/formula.h"
+#include "./formulas/GML_formula.h"
+#include "./formulas/PML_formula.h"
+#include "./formulas/rational.h"
+#include "./formulas/satisfyingassignment.h"
+#include "satisfyingstack.h"
+
+using namespace std;
+
+
+/* Error handler for running out of BDD nodes */
+void error_handler(int errorcode){
+ if(errorcode==BDD_VAR)
+ bdd_extvarnum(1000);
+ else
+ cerr << "BDD package error number " << errorcode << endl;
+}
+
+// use C++-Magic to initialize and destroy bdd library
+class BDDInitializer { public:
+ BDDInitializer() {
+ bdd_init(100000, 10000);
+ bdd_setvarnum(100); // Minimum is two.
+ bdd_error_hook(error_handler);
+ };
+ ~BDDInitializer() {
+ bdd_done();
+ };
+};
+
+//BDDInitializer initializeBddLibrary;
+
+// some utils
+static bdd tupleModality2Bdd(IFormula* f, const pair<pair<bool,int>,int>& t) {
+ if (t.first.first) {
+ /* diamond */
+ bdd* b = new bdd(f->variable(t.second));
+ return f->modal(b, t.first.second, 0);
+ } else {
+ /* box */
+ bdd* b = new bdd(bdd_not(f->variable(t.second)));
+ return bdd_not(f->modal(b, t.first.second, 0));
+ }
+}
+
+
+GMLConclusion gmlmip_onestep_gml(GMLPremise modvec) {
+ IFormula* f = NULL;
+ vector<vector<pair<int,bool> > > rulevec;
+ if (modvec.size() <= 0) {
+ // Nothing to do -> no rules
+ } else {
+ f = new GML_Formula;
+ bdd b = tupleModality2Bdd(f, modvec[0]);
+ for (unsigned int i = 1; i < modvec.size(); i++) {
+ b = bdd_and(b, tupleModality2Bdd(f, modvec[i]));
+ }
+ f->set_bdd(b);
+ vector<SatisfyingAssignment> vsa = f->onestep();
+ for (unsigned int i = 0; i < vsa.size(); i++) {
+ SatisfyingAssignment& sat = vsa[i];
+ vector<pair<int,bool> > rule;
+ for (int v=0; v < sat.get_size(); v++) {
+ if (f->has_variable_back(v)) {
+ bool val = sat.get_array_i(v) == 1;
+ rule.push_back(make_pair(v, val));
+ }
+ }
+ rulevec.push_back(rule);
+ }
+ f->clear_maps();
+ delete f;
+ }
+ return rulevec;
+}
diff --git a/GMLMIP-0.1/onestep.h b/GMLMIP-0.1/onestep.h
new file mode 100644
index 0000000..e6c43be
--- /dev/null
+++ b/GMLMIP-0.1/onestep.h
@@ -0,0 +1,17 @@
+#ifndef __GMLMIP_ONESTEP_H_
+#define __GMLMIP_ONESTEP_H_
+
+#include <vector>
+#include <utility> // for pair
+
+
+/* transforms list of gml formulas (diamond?,number,formula)
+ to list of consequences (formula,positive?),
+ here positive? means that the formula must be true in order to make the
+ given conjunct of modalities true
+*/
+typedef std::vector<std::pair<std::pair<bool,int>,int> > GMLPremise;
+typedef std::vector<std::vector<std::pair<int,bool> > > GMLConclusion;
+GMLConclusion gmlmip_onestep_gml(GMLPremise modvec);
+
+#endif
--
GitLab