replace ckvec with map in satisfiability program
[charm.git] / examples / charm++ / satisfiability / par_Solver.h
1 #ifndef _PAR_SOLVER_H
2 #define _PAR_SOLVER_H
3
4 #include <map>
5
6 using namespace std;
7
8
9 typedef map<int, int> map_int_int;
10
11 class par_SolverState : public CMessage_par_SolverState {
12
13 private:
14
15 public:
16
17     
18     par_SolverState();
19
20     int clausesSize();
21     
22     
23     bool addClause(CkVec<par_Lit>& lits);
24
25     void attachClause(par_Clause& c);
26
27     void assignclause(CkVec<par_Clause>& );
28
29     int  unsolvedClauses();
30     
31     void printSolution();
32
33     CkVec<par_Clause>   clauses;
34     par_Lit             assigned_lit;
35     int             var_size;
36     int             unsolved_clauses;
37
38     int             var_frequency; // 1, -1, 1 freq = 3
39     CkVec<int>      unit_clause_index;
40     // -2 means true, -1 means false, 0 means anything, > 0 means occurrence
41     CkVec<int>      occurrence; 
42     CkVec<int>      positive_occurrence; 
43     //2 * N (positive, negative)
44     CkVec< map_int_int >   whichClauses;
45     int             level;
46    
47     int             lower;
48     int             higher;
49
50     //CkVec<Lit>      lit_state;
51     //vector<Lit> assigns;
52
53     /*
54     void pup(PUP::er &p) {
55     
56         p|assigns;
57         p|clauses;
58         p|assigned_lit;
59     }*/
60
61     friend par_SolverState* copy_solverstate( const par_SolverState* org)
62     {
63        par_SolverState *new_state = new (8*sizeof(int))par_SolverState;
64         
65        new_state->clauses.resize(org->clauses.size());
66        for(int _i=0; _i<org->clauses.size(); _i++)
67        {
68            new_state->clauses[_i] = par_Clause(org->clauses[_i]); 
69        }
70
71        new_state->var_size = org->var_size;
72        new_state->occurrence.resize(org->occurrence.size());
73        new_state->positive_occurrence.resize(org->occurrence.size());
74        for(int _i=0; _i<org->occurrence.size(); _i++){
75            new_state->occurrence[_i] = org->occurrence[_i];
76            new_state->positive_occurrence[_i] = org->occurrence[_i];
77        }
78        new_state->level = org->level;
79        int _size = org->whichClauses.size();
80        new_state->whichClauses.resize(_size); 
81        for(int i=0; i<_size; i++)
82        {
83            map<int, int> __cl_copy = org->whichClauses[i];
84            for(map_int_int::iterator iter=__cl_copy.begin(); iter!=__cl_copy.end(); iter++)
85            {
86                (new_state->whichClauses[i]).insert( pair<int, int>((*iter).first, (*iter).second));
87            }
88        }
89        return new_state;
90     }
91
92 };
93
94
95 class mySolver : public CBase_mySolver {
96
97 private:
98
99     bool seq_solve(par_SolverState*);
100 public:
101     mySolver(par_SolverState*);
102
103 };
104 #endif