Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / GMLMIP-0.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