Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (1.79 KB)

1 e034e268 Thorsten Wißmann
#include <iostream>
2
#include <vector>
3
#include <time.h>
4
5
#include "./parser/mlf-driver.h"
6
#include "./formulas/formula.h"
7
#include "./formulas/satisfyingassignment.h"
8
#include "satisfyingstack.h"
9
10
#include "bdd.h"
11
12
using namespace std;
13
14
vector<SatisfyingAssignment> sat_ass_stack;
15
16
/* Error handler for running out of BDD nodes */
17
void error_handler(int errorcode){
18
        if(errorcode==BDD_VAR)
19
                bdd_extvarnum(1000); 
20
        else
21
                cout << "BDD package error number " << errorcode << endl;
22
}
23
24
void parse(IFormula* &formula, int argc, char *argv[], int& verbose);
25
26
int main (int argc, char *argv[]){
27
        clock_t total_time = clock();
28
        IFormula* f = NULL;
29
        int verbose = 0;        
30
        //initalize buddy
31
        bdd_init(100000, 10000);
32
        bdd_setvarnum(100); // Minimum is two.
33
        bdd_error_hook(error_handler);
34
        parse(f, argc, argv, verbose);
35
        if(f){
36 aaa43ff5 Thorsten Wißmann
                // 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 7c405625 Thorsten Wißmann
                fprintf(stderr,"Cannot check satisfiability due to patched GMLMIP\n");
43
                //if(f->satisfiability(verbose))
44
                //        cout << "Satisfiable" << endl;
45
                //else
46
                //        cout << "Unsatisfiable" << endl;
47 aaa43ff5 Thorsten Wißmann
                f->clear_maps();
48
                delete f;
49 e034e268 Thorsten Wißmann
        }
50
        bdd_done();
51
        total_time = clock() - total_time;
52
        cout << "Total Time: " << static_cast<float>(total_time) / CLOCKS_PER_SEC << endl;
53
        return 0;
54
}
55
56
void parse(IFormula* &formula, int argc, char *argv[], int& option){
57
        mlf_driver driver;
58
        for (++argv; argv[0]; ++argv)
59
                if (*argv == std::string ("-p"))
60
                        driver.trace_parsing = true;
61
                else if (*argv == std::string ("-v"))
62
                        option = 1;
63
                else if (*argv == std::string ("-t"))
64
                        option = 2;
65
                else if (*argv == std::string ("-s"))
66
                        driver.trace_scanning = true;
67
                else if (!driver.parse (*argv))
68
                        driver.extract_formula(formula);
69
}