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