From aaf9d965ea259109e56d7d1b619addc51658bc81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Wed, 29 Jan 2014 17:00:55 +0100
Subject: [PATCH] Make things cleaner
---
GMLMIP-0.1/makefile | 4 +--
GMLMIP-0.1/onestep-example.cpp | 39 ++-------------------------
GMLMIP-0.1/onestep.cpp | 30 +++++++++++++++++++--
GMLMIP-0.1/onestep.h | 3 +++
GMLMIP-0.1/rules/setofconclusions.cpp | 2 +-
5 files changed, 36 insertions(+), 42 deletions(-)
diff --git a/GMLMIP-0.1/makefile b/GMLMIP-0.1/makefile
index dfdfdd2..934e0e7 100644
--- a/GMLMIP-0.1/makefile
+++ b/GMLMIP-0.1/makefile
@@ -34,8 +34,8 @@ rules/%: phony
main: main.o $(POBJS) $(FOBJS) $(ROBJS)
$(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) -lbdd -lm -lglpk $< -o $@
-onestep-example: onestep-example.o $(POBJS) $(FOBJS) $(ROBJS)
- $(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) -lbdd -lm -lglpk $< -o $@
+onestep-example: onestep-example.o $(POBJS) $(FOBJS) $(ROBJS) onestep.o
+ $(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) onestep.o -lbdd -lm -lglpk $< -o $@
main.o: main.cpp $(HEADERS)
diff --git a/GMLMIP-0.1/onestep-example.cpp b/GMLMIP-0.1/onestep-example.cpp
index 3c66fac..3283733 100644
--- a/GMLMIP-0.1/onestep-example.cpp
+++ b/GMLMIP-0.1/onestep-example.cpp
@@ -10,26 +10,13 @@
#include "./formulas/satisfyingassignment.h"
#include "satisfyingstack.h"
#include "./parser/mlf-driver.h"
+#include "onestep.h"
using namespace std;
-vector<SatisfyingAssignment> sat_ass_stack;
-
-/* Error handler for running out of BDD nodes */
-void error_handler(int errorcode){
- if(errorcode==BDD_VAR)
- bdd_extvarnum(1000);
- else
- cout << "BDD package error number " << errorcode << endl;
-}
-
int main (int argc, char *argv[]){
clock_t total_time = clock();
IFormula* f = NULL;
- //initalize buddy
- bdd_init(100000, 10000);
- bdd_setvarnum(100); // Minimum is two.
- bdd_error_hook(error_handler);
// this turns into an endless loop
//bdd b = bdd_and(f->modal(new bdd(f->variable(0)), 4, 0),
// bdd_not(f->modal(new bdd(f->variable(0)), 6, 0)));
@@ -70,31 +57,9 @@ int main (int argc, char *argv[]){
//}
if (f) {
RuleCollection vsa = f->onestep();
- cout << vsa.size() << " rules\n";
- for (RuleCollection::iterator it = vsa.begin(); it != vsa.end(); ++it) {
- const set<set<int> > &r = *it;
- bool first = true;
- cout << "(\\/ ";
- for (set<set<int> >::iterator jt = r.begin(); jt != r.end(); ++jt) {
- const set<int>& clause = *jt;
- if (first) first = false; else cout << "\n ";
- cout << "(/\\";
- for (set<int>::iterator kt = clause.begin(); kt != clause.end(); ++kt) {
- int v = *kt;
- if (v > 0) {
- cout << " p" << v;
- } else {
- cout << " ¬p" << (-v);
- }
- }
- cout << " )";
- }
- cout << ")";
- cout << endl << endl;
- }
+ printRuleCollection(vsa);
f->clear_maps();
delete f;
- bdd_done();
}
total_time = clock() - total_time;
cout << "Total Time: " << static_cast<float>(total_time) / CLOCKS_PER_SEC << endl;
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
index a61f8cb..99bf6b7 100644
--- a/GMLMIP-0.1/onestep.cpp
+++ b/GMLMIP-0.1/onestep.cpp
@@ -16,7 +16,7 @@ using namespace std;
vector<SatisfyingAssignment> sat_ass_stack;
/* Error handler for running out of BDD nodes */
-void error_handler(int errorcode){
+static void error_handler(int errorcode){
if(errorcode==BDD_VAR)
bdd_extvarnum(1000);
else
@@ -35,7 +35,7 @@ class BDDInitializer { public:
};
};
-//BDDInitializer initializeBddLibrary;
+BDDInitializer initializeBddLibrary;
// some utils
static bdd tupleModality2Bdd(IFormula* f, const pair<pair<bool,int>,int>& t) {
@@ -70,3 +70,29 @@ GMLConclusion gmlmip_onestep_gml(GMLPremise modvec) {
return vsa;
}
}
+
+void printRuleCollection(const RuleCollection& rc) {
+ cout << rc.size() << " rules\n";
+ for (RuleCollection::iterator it = rc.begin(); it != rc.end(); ++it) {
+ const set<set<int> > &r = *it;
+ bool first = true;
+ cout << "(\\/ ";
+ for (set<set<int> >::iterator jt = r.begin(); jt != r.end(); ++jt) {
+ const set<int>& clause = *jt;
+ if (first) first = false; else cout << "\n ";
+ cout << "(/\\";
+ for (set<int>::iterator kt = clause.begin(); kt != clause.end(); ++kt) {
+ int v = *kt;
+ if (v > 0) {
+ cout << " p" << v;
+ } else {
+ cout << " ¬p" << (-v);
+ }
+ }
+ cout << " )";
+ }
+ cout << ")";
+ cout << endl << endl;
+ }
+}
+
diff --git a/GMLMIP-0.1/onestep.h b/GMLMIP-0.1/onestep.h
index 233f52c..525affe 100644
--- a/GMLMIP-0.1/onestep.h
+++ b/GMLMIP-0.1/onestep.h
@@ -4,6 +4,7 @@
#include <vector>
#include <set>
#include <utility> // for pair
+#include "formulas/formula.h"
/* transforms list of gml formulas (diamond?,number,formula)
@@ -16,4 +17,6 @@ typedef std::set<std::set<std::set<int> > > GMLConclusion;
GMLConclusion gmlmip_onestep_gml(GMLPremise modvec);
+void printRuleCollection(const RuleCollection& rc);
+
#endif
diff --git a/GMLMIP-0.1/rules/setofconclusions.cpp b/GMLMIP-0.1/rules/setofconclusions.cpp
index 5969e40..98b25f1 100644
--- a/GMLMIP-0.1/rules/setofconclusions.cpp
+++ b/GMLMIP-0.1/rules/setofconclusions.cpp
@@ -26,7 +26,7 @@ set<set<int> > SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
if(rules[j][i].get_p_i(k)==1)
conj.insert(bdd_var(*(underlying[k])));
if(rules[j][i].get_p_i(k)==0)
- conj.insert(-bdd_var(*(underlying[k])));
+ conj.insert(-bdd_var(bdd_not(*(underlying[k]))));
}
disj.insert(conj);
}
--
GitLab