examples: add example program demonstrating sync entry methods
[charm.git] / examples / charm++ / satisfiability / par_SolverTypes.h
1 /***********************************************************************************[SolverTypes.h]
2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
5 associated documentation files (the "Software"), to deal in the Software without restriction,
6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
8 furnished to do so, subject to the following conditions:
9
10 The above copyright notice and this permission notice shall be included in all copies or
11 substantial portions of the Software.
12
13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
18 **************************************************************************************************/
19
20
21 #ifndef _PAR_SolverTypes_h
22 #define _PAR_SolverTypes_h
23
24 #include <cassert>
25 #include <stdint.h>
26
27
28 template<class V> 
29 int get_max_element(const V& ps) {
30
31     int max_index = -1;
32     int max = -1;
33     for(int __i=0; __i<ps.size(); __i++)
34     {
35         if(ps[__i] > max)
36         {
37             max = ps[__i];
38             max_index = __i;
39         }
40     }
41     return max_index;
42 }
43
44
45 //=================================================================================================
46 // intiables, literals, lifted booleans, clauses:
47
48
49 // NOTE! intiables are just integers. No abstraction here. They should be chosen from 0..N,
50 // so that they can be used as array indices.
51
52 #define var_Undef (-1)
53
54
55 class par_Lit {
56     int     x;
57 public:
58     par_Lit() : x(var_Undef)                                              { }   // (lit_Undef)
59     par_Lit(int var) {x = var;};
60     //par_Lit(int var, bool sign)   {x=sign?var:-var; }
61
62     // Don't use these for constructing/deconstructing literals. Use the normal constructors instead.
63     friend int  toInt       (par_Lit p);  // Guarantees small, positive integers suitable for array indexing.
64     friend par_Lit  par_toLit       (int i);  // Inverse of 'toInt()'
65     friend par_Lit  operator   ~(par_Lit p);
66     //friend bool sign        (Lit p);
67     friend int  var         (par_Lit p);
68     //friend Lit  unsign      (Lit p);
69     //friend Lit  id          (Lit p, bool sgn);
70
71     bool operator == (par_Lit p) const { return x == p.x; }
72     bool operator != (par_Lit p) const { return x != p.x; }
73     bool operator <  (par_Lit p) const { return x < p.x;  } // '<' guarantees that p, ~p are adjacent in the ordering.
74
75     void pup(PUP::er &p) {
76         p|x;
77     }
78 };
79
80 inline  int  toInt       (par_Lit p)           { return p.x; }
81 inline  par_Lit  par_toLit       (int i)           { par_Lit p; p.x = i; return p; }
82 inline  par_Lit  operator   ~(par_Lit p)           { par_Lit q; q.x = -p.x; return q; }
83 //inline  bool sign        (Lit p)           { return p.x >1?true:false; }
84 inline  int  var         (par_Lit p)           { return p.x >> 1; }
85 //inline  Lit  unsign      (Lit p)           { Lit q; q.x = p.x & ~1; return q; }
86 //inline  Lit  id          (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
87
88 //const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
89 //const Lit lit_Error(var_Undef, true );  // }
90
91
92 //=================================================================================================
93 // Lifted booleans:
94
95 /*
96 class lbool {
97     char     value;
98     explicit lbool(int v) : value(v) { }
99
100 public:
101     lbool()       : value(0) { }
102     lbool(bool x) : value((int)x*2-1) { }
103     int toInt(void) const { return value; }
104
105     bool  operator == (lbool b) const { return value == b.value; }
106     bool  operator != (lbool b) const { return value != b.value; }
107     lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); }
108
109     friend int   toInt  (lbool l);
110     friend lbool toLbool(int   v);
111 };
112 inline int   toInt  (lbool l) { return l.toInt(); }
113 inline lbool toLbool(int   v) { return lbool(v);  }
114
115 const lbool l_True  = toLbool( 1);
116 const lbool l_False = toLbool(-1);
117 const lbool l_Undef = toLbool( 0);
118 */
119 //=================================================================================================
120 // Clause -- a simple class for representing a clause:
121
122
123 class par_Clause {
124     CkVec<par_Lit>  data;
125
126 public:
127    
128      par_Clause(){data.removeAll();}
129    
130      par_Clause(const par_Clause& corg)
131      {
132          data.resize(corg.size());
133         for(int _i=0; _i<data.size(); _i++)
134         {
135             data[_i] = corg[_i];
136         }
137      }
138
139     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
140     template<class V>
141     par_Clause(const V& ps, bool learnt) {
142         data.resize(ps.size());
143         for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
144     }
145     
146     template<class V>
147     void attachdata(const V& ps, bool learnt)
148     {
149         data.resize(ps.size());
150         for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
151     }
152
153     void remove(int v){
154         for(int i=0; i<data.size(); i++)
155         {
156             if(toInt(data[i]) == v)
157             {
158                 data.remove(i);
159                 return;
160             }
161         }
162     }
163     // -- use this function instead:
164     int          size        ()      const   { return data.size(); }
165     //void         shrink      (int i)         { }
166     //void         pop         ()              { shrink(1); }
167     //bool         learnt      ()      const   {  }
168     //uint32_t     mark        ()      const   { return 1; }
169     //void         mark        (uint32_t m)    {  }
170     //const Lit&   last        ()      const   { return data[size()-1]; }
171
172     // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
173     //       subsumption operations to behave correctly.
174     par_Lit&         operator [] (int i)         { return data[i]; }
175     par_Lit          operator [] (int i) const   { return data[i]; }
176     //operator const Lit* (void) const         { return data; }
177
178     //float       activity    ()              { return 1; }
179     //uint32_t     abstraction () const { return 1; }
180
181     //Lit          subsumes    (const Clause& other) const;
182     //void         strengthen  (Lit p);
183
184
185     void        resize  (int __size)  {data.resize(__size); }
186     void pup(PUP::er &p) {
187         for(int i=0; i<size(); i++)
188             p|data[i];
189     }
190 };
191
192
193 /*_________________________________________________________________________________________________
194 |
195 |  subsumes : (other : const Clause&)  ->  Lit
196 |  
197 |  Description:
198 |       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
199 |       by subsumption resolution.
200 |  
201 |    Result:
202 |       lit_Error  - No subsumption or simplification
203 |       lit_Undef  - Clause subsumes 'other'
204 |       p          - The literal p can be deleted from 'other'
205 |________________________________________________________________________________________________@*/
206 /*inline Lit Clause::subsumes(const Clause& other) const
207 {
208         return lit_Error;
209 }
210 */
211 /*
212 inline void Clause::strengthen(Lit p)
213 {
214     //remove(*this, p);
215     //calcAbstraction();
216 }
217 */
218 #endif