cool / src / lib / GMLMIP0.1 / onestep.c @ 7c4d2eb4
History  View  Annotate  Download (2.69 KB)
1 
#include <iostream> 

2 
#include <vector> 
3 
#include <time.h> 
4 
#include "onestep.h" 
5  
6 
#include "bdd.h" 
7 
#include "./formulas/formula.h" 
8 
#include "./formulas/GML_formula.h" 
9 
#include "./formulas/PML_formula.h" 
10 
#include "./formulas/rational.h" 
11 
#include "./formulas/satisfyingassignment.h" 
12 
#include "./rules/setofconclusions.h" 
13 
#include "satisfyingstack.h" 
14  
15 
using namespace std; 
16  
17 
vector<SatisfyingAssignment> sat_ass_stack; 
18  
19 
/* Error handler for running out of BDD nodes */

20 
static void error_handler(int errorcode){ 
21 
if(errorcode==BDD_VAR)

22 
bdd_extvarnum(1000);

23 
else

24 
cerr << "BDD package error number " << errorcode << endl;

25 
} 
26  
27 
// use C++Magic to initialize and destroy bdd library

28 
class BDDInitializer { public:

29 
BDDInitializer() { 
30 
bdd_init(100000, 10000); 
31 
bdd_setvarnum(100); // Minimum is two. 
32 
bdd_error_hook(error_handler); 
33 
}; 
34 
~BDDInitializer() { 
35 
bdd_done(); 
36 
}; 
37 
}; 
38  
39 
BDDInitializer initializeBddLibrary; 
40  
41 
// some utils

42 
static bdd tupleModality2Bdd(IFormula* f, const pair<pair<bool,int>,int>& t) { 
43 
if (t.first.first) {

44 
/* diamond */

45 
bdd* b = new bdd(f>variable(t.second)); 
46 
return f>modal(b, t.first.second, 0); 
47 
} else {

48 
/* box */

49 
bdd* b = new bdd(bdd_not(f>variable(t.second))); 
50 
return bdd_not(f>modal(b, t.first.second, 0)); 
51 
} 
52 
} 
53  
54  
55 
GMLConclusion gmlmip_onestep_gml(GMLPremise modvec) { 
56 
IFormula* f = NULL;

57 
if (modvec.size() <= 0) { 
58 
// Nothing to do > no rules

59 
GMLConclusion rulevec; 
60 
return rulevec;

61 
} else {

62 
f = new GML_Formula; 
63 
bdd b = tupleModality2Bdd(f, modvec[0]);

64 
for (unsigned int i = 1; i < modvec.size(); i++) { 
65 
b = bdd_and(b, tupleModality2Bdd(f, modvec[i])); 
66 
} 
67 
f>set_bdd(b); 
68 
RuleCollection vsa = f>onestep(); 
69 
f>clear_maps(); 
70 
delete f; 
71 
return vsa;

72 
} 
73 
} 
74  
75 
void printRuleCollection(const RuleCollection& rc) { 
76 
cout << rc.size() << " rules\n";

77 
for (RuleCollection::iterator it = rc.begin(); it != rc.end(); ++it) {

78 
const set<set<int> > &r = *it; 
79 
bool first = true; 
80 
cout << "(\\/ ";

81 
for (set<set<int> >::iterator jt = r.begin(); jt != r.end(); ++jt) { 
82 
const set<int>& clause = *jt; 
83 
if (first) first = false; else cout << "\n "; 
84 
cout << "(/\\";

85 
for (set<int>::iterator kt = clause.begin(); kt != clause.end(); ++kt) { 
86 
int v = *kt;

87 
if (v > 0) { 
88 
cout << " p" << v;

89 
} else {

90 
cout << " ¬p" << (v);

91 
} 
92 
} 
93 
cout << " )";

94 
} 
95 
cout << ")";

96 
cout << endl << endl; 
97 
} 
98 
} 
99 