b6d4fbabaa5f17fb36ba8f060da3036f1e3f555e
[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 nVars();
14
15     int clausesSize();
16     
17     int newVar (bool polarity = true, bool dvar = true);
18     
19     bool addClause(CkVec<par_Lit>& lits);
20
21     void attachClause(par_Clause& c);
22
23     void assignclause(CkVec<par_Clause>& );
24
25     int  unsolvedClauses();
26     
27     void printSolution();
28
29     CkVec<par_Clause>   clauses;
30     par_Lit             assigned_lit;
31     int             var_size;
32     int             unsolved_vars;
33     int             unsolved_clauses;
34
35     int             var_frequency; // 1, -1, 1 freq = 3
36     CkVec<int>      unit_clause_index;
37     // -2 means true, -1 means false, 0 means anything, > 0 means occurrence
38     CkVec<int>      occurrence; 
39     CkVec<int>      positive_occurrence; 
40     //2 * N (positive, negative)
41     CkVec< CkVec< int > >   whichClauses;
42     int             level;
43    
44     int             lower;
45     int             higher;
46
47     //CkVec<Lit>      lit_state;
48     //vector<Lit> assigns;
49
50     /*
51     void pup(PUP::er &p) {
52     
53         p|assigns;
54         p|clauses;
55         p|assigned_lit;
56     }*/
57
58     friend par_SolverState* copy_solverstate( const par_SolverState* org)
59     {
60        par_SolverState *new_state = new (8*sizeof(int))par_SolverState;
61         
62        new_state->clauses.resize(org->clauses.size());
63        for(int _i=0; _i<org->clauses.size(); _i++)
64        {
65            new_state->clauses[_i] = par_Clause(org->clauses[_i]); 
66        }
67
68        new_state->var_size = org->var_size;
69        new_state->unsolved_vars = org->unsolved_vars;
70        new_state->occurrence.resize(org->occurrence.size());
71        new_state->positive_occurrence.resize(org->occurrence.size());
72        for(int _i=0; _i<org->occurrence.size(); _i++){
73            new_state->occurrence[_i] = org->occurrence[_i];
74            new_state->positive_occurrence[_i] = org->occurrence[_i];
75        }
76        new_state->level = org->level;
77        int _size = org->whichClauses.size();
78        new_state->whichClauses.resize(_size); 
79        for(int i=0; i<_size; i++)
80        {
81            int _sub_size = org->whichClauses[i].size();
82            new_state->whichClauses[i].resize(_sub_size);
83
84            for(int j=0; j<_sub_size; j++)
85            {
86                new_state->whichClauses[i][j] = org->whichClauses[i][j];
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