From 639f698548bb29c7fa7f5b491b5c8e734b764e88 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:24:42 +0100
Subject: [PATCH] Resolve bdd variable numbers
---
GMLMIP-0.1/formulas/formula.cpp | 4 ++--
GMLMIP-0.1/formulas/formula.h | 2 ++
GMLMIP-0.1/onestep.cpp | 1 +
GMLMIP-0.1/rules/setofconclusions.cpp | 8 ++++----
GMLMIP-0.1/rules/setofconclusions.h | 7 +++----
5 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index 09a9e6a..ec2beb4 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -109,7 +109,7 @@ RuleCollection Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
if(rule_cache.count(premise)){ // if in cache
SetOfConclusions concs = rule_cache[premise];
for(int i = 0; i < concs.number_of_conclusions(); i++){
- result.insert(concs.get_jth_conclusion(underlying_formulae, i));
+ result.insert(concs.get_jth_conclusion((IFormula*)this, underlying_formulae, i));
}
} else {
result = enumerate_rules(premise, underlying_formulae);
@@ -221,7 +221,7 @@ RuleCollection Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp
vector<vector<bool> > singleton;
singleton.push_back(new_node);
SetOfConclusions temp = SetOfConclusions(prem.get_n() + prem.get_m(), singleton);
- result.insert(temp.get_jth_conclusion(underlying_formulae, 0));
+ result.insert(temp.get_jth_conclusion(this, underlying_formulae, 0));
} else {
new_node_queue.push_back(new_node);
}
diff --git a/GMLMIP-0.1/formulas/formula.h b/GMLMIP-0.1/formulas/formula.h
index 6226bbf..e263210 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -46,6 +46,7 @@ class IFormula {
virtual bool satisfiability(int option)=0;
virtual void clear_maps()=0;
virtual RuleCollection onestep() = 0;
+ virtual int get_variables_back(int bddvar) = 0;
};
template<class ModalValueType>
@@ -151,6 +152,7 @@ class Formula : public IFormula{
void print_back_vars();
//virtual void print_back_modal()=0;
+ int get_variables_back(int bddvar) { return variables_back[bddvar]; }
bool satisfiability(int option){ assert(0=="patched GMLMIP\n"); return true;};
RuleCollection onestep() { return check_satisfiability(bdd_rep); };
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
index 99bf6b7..94182a0 100644
--- a/GMLMIP-0.1/onestep.cpp
+++ b/GMLMIP-0.1/onestep.cpp
@@ -9,6 +9,7 @@
#include "./formulas/PML_formula.h"
#include "./formulas/rational.h"
#include "./formulas/satisfyingassignment.h"
+#include "./rules/setofconclusions.h"
#include "satisfyingstack.h"
using namespace std;
diff --git a/GMLMIP-0.1/rules/setofconclusions.cpp b/GMLMIP-0.1/rules/setofconclusions.cpp
index 98b25f1..8af62cc 100644
--- a/GMLMIP-0.1/rules/setofconclusions.cpp
+++ b/GMLMIP-0.1/rules/setofconclusions.cpp
@@ -1,5 +1,6 @@
#include "setofconclusions.h"
#include <set>
+#include "../formulas/formula.h"
SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
no_of_literals=n;
@@ -18,18 +19,17 @@ SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
}
}
-set<set<int> > SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
+set<set<int> > SetOfConclusions::get_jth_conclusion(IFormula* f, bdd** underlying, int j){
set< set<int> > disj;
for(unsigned int i=0; i < rules[j].size(); i++){
set<int> conj;
for(int k=0; k < no_of_literals; k++){
if(rules[j][i].get_p_i(k)==1)
- conj.insert(bdd_var(*(underlying[k])));
+ conj.insert(f->get_variables_back(bdd_var(*(underlying[k]))));
if(rules[j][i].get_p_i(k)==0)
- conj.insert(-bdd_var(bdd_not(*(underlying[k]))));
+ conj.insert(-f->get_variables_back(bdd_var(bdd_not(*(underlying[k])))));
}
disj.insert(conj);
}
return disj;
}
-
diff --git a/GMLMIP-0.1/rules/setofconclusions.h b/GMLMIP-0.1/rules/setofconclusions.h
index c0e1142..54e1451 100644
--- a/GMLMIP-0.1/rules/setofconclusions.h
+++ b/GMLMIP-0.1/rules/setofconclusions.h
@@ -19,6 +19,8 @@ using namespace std;
typedef vector<TruthAssignment> Conclusion;
+class IFormula;
+
class SetOfConclusions{
private:
int no_of_literals;
@@ -29,10 +31,7 @@ class SetOfConclusions{
SetOfConclusions(int n, const vector<vector<bool> >& set);
int number_of_conclusions(){return rules.size();};
- set<set<int> > get_jth_conclusion(bdd** underlying, int j);
-
-
-
+ set<set<int> > get_jth_conclusion(IFormula* f, bdd** underlying, int j);
//bdd get_ith_conclusion(int i, bdd* bddarray);
};
--
GitLab