Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / GMLMIP-0.1 / onestep-example.cpp @ 7c4d2eb4

History | View | Annotate | Download (1.87 KB)

1
#include <iostream>
2
#include <vector>
3
#include <time.h>
4

    
5
#include "bdd.h"
6
#include "./formulas/formula.h"
7
#include "./formulas/GML_formula.h"
8
#include "./formulas/PML_formula.h"
9
#include "./formulas/rational.h"
10
#include "./formulas/satisfyingassignment.h"
11
#include "satisfyingstack.h"
12
#include "./parser/mlf-driver.h"
13
#include "onestep.h"
14

    
15
using namespace std;
16

    
17
int main (int argc, char *argv[]){
18
        clock_t total_time = clock();
19
        IFormula* f = NULL;
20
    // this turns into an endless loop
21
        //bdd b = bdd_and(f->modal(new bdd(f->variable(0)), 4, 0),
22
        //                bdd_not(f->modal(new bdd(f->variable(0)), 6, 0)));
23
        if (true) {
24
                mlf_driver driver;
25
                driver.set_formula_gml();
26
                if (!driver.parse ("-")) {
27
                        driver.extract_formula(f);
28
                }
29
        } else {
30
                f = new GML_Formula;
31
                bdd b = bdd_and(bdd_and(f->modal(new bdd(f->variable(8)), 4, 0),
32
                                           bdd_not(f->modal(new bdd(bdd_not(f->variable(7))), 3, 0))),
33
                                           bdd_not(f->modal(new bdd(bdd_not(f->variable(9))), 3, 0)));
34
                f->set_bdd(b);
35
        }
36
        // bdd_varblockall();
37
        // bdd_reorder(BDD_REORDER_WIN3ITE);
38
        // bdd_printdot((driver.formula)->bdd_rep);
39
        //bdd_printset(f->get_bdd());
40
        //cout << endl;
41
        //(driver.formula)->print_back_vars();
42
        //vector<RuleChild> res = f->onestep_rules(b);
43
        //cout << res.size() << " childs" << endl;
44
        //for (unsigned int r = 0; r < res.size(); r++) {
45
        //        RuleChild& rc = res[r];
46
        //        for (unsigned int i = 0; i < rc.size(); i++) {
47
        //                cout << "\\/ (";
48
        //                for (unsigned int j = 0; j < rc[i].size(); j++) {
49
        //                        pair<bool,int>& p = rc[i][j];
50
        //                        if (j != 0) cout << ", ";
51
        //                        if (!p.first) cout << "~";
52
        //                        cout << p.second;
53
        //                }
54
        //                cout << ")";
55
        //        }
56
        //        cout << endl;
57
        //}
58
        if (f) {
59
                RuleCollection vsa = f->onestep();
60
                printRuleCollection(vsa);
61
                f->clear_maps();
62
                delete f;
63
        }
64
        total_time = clock() - total_time;
65
        cout << "Total Time: " << static_cast<float>(total_time) / CLOCKS_PER_SEC << endl;
66
        return 0;
67
}
68