Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / GMLMIP-0.1 / formulas / formula.h @ 7c4d2eb4

History | View | Annotate | Download (4.85 KB)

1
#ifndef FORMULA_HH
2
#define FORMULA_HH
3

    
4
#include <iostream>
5
#include <cstdlib>
6
#include <cstring>
7
#include <iomanip>
8
#include <sstream>
9
#include <string>
10
#include <set>
11
#include <time.h>
12

    
13
#include "bdd.h"
14
#include "glpk.h"
15

    
16
#include <vector>
17
#include <utility>
18

    
19
#include "google/dense_hash_map"
20
#include <ext/hash_map>
21
/* will become #include <unordered_set> */
22

    
23
#include "rational.h"
24
#include "../rules/premise.h"
25
#include "../rules/setofconclusions.h"
26
#include "../satisfyingstack.h"
27

    
28
using namespace std;
29

    
30
using std::cout;
31
using std::endl;
32
using std::vector;
33
using google::dense_hash_map;
34
using __gnu_cxx::hash;
35

    
36
typedef set<set<set<int> > > RuleCollection;
37

    
38
// Formula interface so we can have abstract template class pointers.
39
class IFormula {
40
        public:
41
                virtual ~IFormula();
42
                virtual bdd variable(int n)=0;
43
                virtual void set_bdd(bdd &b)=0;
44
                virtual bdd get_bdd()=0;
45
                virtual bdd modal(bdd *b, int n, int m)=0;
46
                virtual bool satisfiability(int option)=0;
47
                virtual void clear_maps()=0;
48
                virtual RuleCollection onestep() = 0;
49
                virtual int get_variables_back(int bddvar) = 0;
50
};
51

    
52
template<class ModalValueType>
53
class Formula : public IFormula{
54
        protected:
55
                /* REQUIRED DEFINITIONS FOR HASH_MAPS */                
56
                class data {
57
                        public:
58
                                ModalValueType value;
59
                                bdd* argument;
60
                                data() : value(-1) {argument = NULL; };
61
                                data(ModalValueType v, bdd* arg) : value(v){ argument = arg; };
62
                                ~data(){ if(argument) delete argument; };
63
                                data& operator=(const data& other){
64
                                        if (this!=&other){
65
                                                if(argument) 
66
                                                        delete argument;
67
                                                value = other.value;
68
                                                argument = NULL;
69
                                                if(other.argument)
70
                                                        argument = new bdd(*(other.argument));
71
                                                }
72
                                        return *this;
73
                                };
74
                                data(const data& other){
75
                                        value = other.value;
76
                                        argument = NULL;
77
                                        if(other.argument)
78
                                                argument = new bdd(*(other.argument));
79
                                };
80
                };
81
        
82
                // Required for dense_hash_map - how to compare keys.
83
                struct eqkey {
84
                        bool operator()(const string s1, const string s2) const{
85
                                return s1 == s2;
86
                        }
87

    
88
                        bool operator()(const int s1, const int s2) const{
89
                                return (s1 == s2);
90
                        }
91

    
92
                        bool operator()(const data& d1, const data& d2) const{
93
                                return ((d1.value == d2.value) && ((d1.argument==d2.argument) || (d1.argument && d2.argument && (*(d1.argument) == *(d2.argument)))));
94
                        }
95
                };                
96

    
97
                // Number of variables. Set to zero by constructor and
98
                // incremented as variables and modal variables are added.
99
                // (Used for building the hash_maps).        
100
                int number_of_variables;
101

    
102
                // Map of parsed variable numbers to BDD package numbers
103
                dense_hash_map<int, int, hash<int>, eqkey> variables;
104
                // Map of BDD package numbers to input numbers
105
                dense_hash_map<int, int, hash<int>, eqkey> variables_back;        
106
                
107
                // How to hash data items.
108
                struct datahash {
109
                        hash <const char*> charhash;
110
                        hash <int> inthash;
111
                        size_t operator ()(const data& d) const {
112
                                stringstream ss;
113
                                string s;
114
                                ss << d.value << " " << *d.argument << '\0';
115
                                s = ss.str();
116
                                char buf[s.size()+1];
117
                                for(unsigned int i=0; i < s.size(); i++)
118
                                        buf[i] = s[i];
119
                                buf[s.size()]='\0';
120
                                return charhash(buf);
121
                        }        
122
                };
123
                
124
                dense_hash_map<data, int, datahash, eqkey> modal_variables;
125
                dense_hash_map<int, data, hash<int>, eqkey> modal_variables_back;
126

    
127
                dense_hash_map<Premise<ModalValueType>, SetOfConclusions, typename Premise<ModalValueType>::Premise_hash, typename Premise<ModalValueType>::Premise_equal> rule_cache;
128

    
129
                int test_counter;
130

    
131
                RuleCollection check_satisfiability(bdd b);
132
                RuleCollection apply_rules(SatisfyingAssignment& sat);
133
                RuleCollection enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae);
134
                RuleCollection enum_rules_intern(glp_prob* problem, glp_iocp* parameters, Premise<ModalValueType>& prem, bdd** underlying_formulae, vector<vector<bool> >& node_queue, vector<vector<bool> >& valid_nodes, vector<pair<vector<bool>, int> >& anti_nodes);
135
                bool run_solver(glp_prob *problem, glp_iocp* parameters, bool strict, vector<bool> current_node, int index);
136
                
137
                virtual void load_linear_program(glp_prob* problem, Premise<ModalValueType>& prem)=0;
138
        
139
        public:
140
                Formula();
141
                // The parsed formula
142
                bdd bdd_rep;
143

    
144
                // Used by the driver to set bdd_rep
145
                void set_bdd(bdd &b){ bdd_rep=b; };
146
                bdd get_bdd(){ return bdd_rep;};
147
                
148
                // Called by parser to construct variable or modal variable.
149
                // Also constructs appropriate data structures. 
150
                bdd variable(int n);
151
                bdd modal_var(bdd *b, ModalValueType &n);
152
                
153
                void print_back_vars();
154
                //virtual void print_back_modal()=0;
155
                int get_variables_back(int bddvar) { return variables_back[bddvar]; }
156
                set<set<int> > gatherRules(bdd b);
157
                
158
                bool satisfiability(int option){ assert(0=="patched GMLMIP\n"); return true;};
159
                RuleCollection onestep() { return check_satisfiability(bdd_rep); };
160

    
161
                void clear_maps(){ 
162
                        variables.clear();
163
                        variables_back.clear();
164
                        modal_variables.clear();
165
                        modal_variables_back.clear();
166
                        rule_cache.clear(); };
167
};
168
#endif