Reset setofconclusions again

GMLMIP-0.1/rules/setofconclusions.cpp

 #include "setofconclusions.h"
-#include <set>
-#include "../formulas/formula.h"
 
 SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
 	no_of_literals=n;
@@ -19,17 +17,19 @@ SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
 	}
 }
 
-set<set<int> > SetOfConclusions::get_jth_conclusion(IFormula* f, bdd** underlying, int j){
-	set< set<int> > disj;
+bdd SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
+	bdd b = bdd_false();
 	for(unsigned int i=0; i < rules[j].size(); i++){
-		set<int> conj;
+		bdd clause = bdd_true();
 		for(int k=0; k < no_of_literals; k++){
 			if(rules[j][i].get_p_i(k)==1)
-				conj.insert(f->get_variables_back(bdd_var(*(underlying[k]))));
+				clause = bdd_and(clause, *(underlying[k]));
 			if(rules[j][i].get_p_i(k)==0)
-				conj.insert(-f->get_variables_back(bdd_var(bdd_not(*(underlying[k])))));
+				clause = bdd_and(clause, bdd_not(*(underlying[k])));
 		}
-		disj.insert(conj);
+		b = bdd_or(clause, b);
+   		
 	}
-	return disj;
+	return b;
 }
+	

GMLMIP-0.1/rules/setofconclusions.h

@@ -3,7 +3,6 @@
 
 
 #include <vector>
-#include <set>
 
 #include <stdio.h>
 #include <cmath>
@@ -19,8 +18,6 @@ using namespace std;
 
 typedef vector<TruthAssignment> Conclusion;
 
-class IFormula;
-
 class SetOfConclusions{
 	private:
 		int no_of_literals;
@@ -31,7 +28,10 @@ class SetOfConclusions{
 		SetOfConclusions(int n, const vector<vector<bool> >& set);
 		
 		int number_of_conclusions(){return rules.size();};		
-		set<set<int> > get_jth_conclusion(IFormula* f, bdd** underlying, int j);
+		bdd get_jth_conclusion(bdd** underlying, int j);
+		
+		
+		
 		
 		//bdd get_ith_conclusion(int i, bdd* bddarray);
 };