## cool / src / lib / GMLMIP-0.1 / onestep.c @ 7c4d2eb4

History | View | Annotate | Download (2.69 KB)

1 | d4135ed7 | Thorsten Wißmann | #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 | 639f6985 | Thorsten Wißmann | #include "./rules/setofconclusions.h" |

13 | d4135ed7 | Thorsten Wißmann | #include "satisfyingstack.h" |

14 | |||

15 | using namespace std; |
||

16 | |||

17 | bd573393 | Thorsten Wißmann | vector<SatisfyingAssignment> sat_ass_stack; |

18 | d4135ed7 | Thorsten Wißmann | |

19 | ```
/* Error handler for running out of BDD nodes */
``` |
||

20 | aaf9d965 | Thorsten Wißmann | static void error_handler(int errorcode){ |

21 | d4135ed7 | Thorsten Wißmann | ```
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 | aaf9d965 | Thorsten Wißmann | BDDInitializer initializeBddLibrary; |

40 | d4135ed7 | Thorsten Wißmann | |

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 | 7c405625 | Thorsten Wißmann | GMLConclusion rulevec; |

60 | ```
return rulevec;
``` |
||

61 | d4135ed7 | Thorsten Wißmann | ```
} 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 | 7c405625 | Thorsten Wißmann | RuleCollection vsa = f->onestep(); |

69 | d4135ed7 | Thorsten Wißmann | f->clear_maps(); |

70 | delete f; |
||

71 | 7c405625 | Thorsten Wißmann | ```
return vsa;
``` |

72 | d4135ed7 | Thorsten Wißmann | } |

73 | } |
||

74 | aaf9d965 | Thorsten Wißmann | |

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 | } |