GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/core/SolverTypes.h Lines: 124 131 94.7 %
Date: 2021-03-23 Branches: 62 170 36.5 %

Line Exec Source
1
/***********************************************************************************[SolverTypes.h]
2
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3
Copyright (c) 2007-2010, Niklas Sorensson
4
5
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6
associated documentation files (the "Software"), to deal in the Software without restriction,
7
including without limitation the rights to use, copy, modify, merge, publish, distribute,
8
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9
furnished to do so, subject to the following conditions:
10
11
The above copyright notice and this permission notice shall be included in all copies or
12
substantial portions of the Software.
13
14
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19
**************************************************************************************************/
20
21
#ifndef BVMinisat_SolverTypes_h
22
#define BVMinisat_SolverTypes_h
23
24
#include "base/check.h"
25
#include "prop/bvminisat/mtl/Alg.h"
26
#include "prop/bvminisat/mtl/Alloc.h"
27
#include "prop/bvminisat/mtl/IntTypes.h"
28
#include "prop/bvminisat/mtl/Map.h"
29
#include "prop/bvminisat/mtl/Vec.h"
30
31
namespace CVC4 {
32
namespace BVMinisat {
33
class Solver;
34
}
35
template <class Solver>
36
class TSatProof;
37
}
38
39
namespace CVC4 {
40
41
namespace BVMinisat {
42
43
//=================================================================================================
44
// Variables, literals, lifted booleans, clauses:
45
46
47
// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
48
// so that they can be used as array indices.
49
50
typedef int Var;
51
#define var_Undef (-1)
52
53
54
struct Lit {
55
    int     x;
56
57
    // Use this as a constructor:
58
    friend Lit mkLit(Var var, bool sign);
59
60
1796242894
    bool operator == (Lit p) const { return x == p.x; }
61
384914401
    bool operator != (Lit p) const { return x != p.x; }
62
22801835
    bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
63
};
64
65
381216488
inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
66
730939269
inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
67
inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
68
2090167718
inline  bool sign      (Lit p)              { return p.x & 1; }
69
3233081952
inline  int  var       (Lit p)              { return p.x >> 1; }
70
71
// Mapping Literals to and from compact integers suitable for array indexing:
72
105180857
inline  int  toInt     (Var v)              { return v; }
73
651467171
inline  int  toInt     (Lit p)              { return p.x; }
74
inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; }
75
76
struct LitHashFunction {
77
  size_t operator () (const Lit& l) const {
78
    return toInt(l);
79
  }
80
};
81
82
//const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.
83
//const Lit lit_Error = mkLit(var_Undef, true );  // }
84
85
const Lit lit_Undef = { -2 };  // }- Useful special constants.
86
const Lit lit_Error = { -1 };  // }
87
88
//=================================================================================================
89
// Lifted booleans:
90
//
91
// NOTE: this implementation is optimized for the case when comparisons between
92
// values are mostly
93
//       between one variable and one constant. Some care had to be taken to
94
//       make sure that gcc does enough constant propagation to produce sensible
95
//       code, and this appears to be somewhat fragile unfortunately.
96
97
#ifndef l_True
98
#define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
99
#endif
100
101
#ifndef l_False
102
#define l_False (lbool((uint8_t)1))
103
#endif
104
105
#ifndef l_Undef
106
#define l_Undef (lbool((uint8_t)2))
107
#endif
108
109
class lbool {
110
    uint8_t value;
111
112
public:
113
3542841486
    explicit lbool(uint8_t v) : value(v) { }
114
115
    lbool()       : value(0) { }
116
222650838
    explicit lbool(bool x) : value(!x) { }
117
118
1674989891
    bool  operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
119
530516347
    bool  operator != (lbool b) const { return !(*this == b); }
120
1642557289
    lbool operator ^  (bool  b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
121
122
    lbool operator&&(lbool b) const
123
    {
124
      uint8_t sel = (this->value << 1) | (b.value << 3);
125
      uint8_t v = (0xF7F755F4 >> sel) & 3;
126
      return lbool(v);
127
    }
128
129
    lbool operator || (lbool b) const {
130
        uint8_t sel = (this->value << 1) | (b.value << 3);
131
        uint8_t v   = (0xFCFCF400 >> sel) & 3;
132
        return lbool(v); }
133
134
    friend int   toInt  (lbool l);
135
    friend lbool toLbool(int   v);
136
};
137
inline int   toInt  (lbool l) { return l.value; }
138
inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }
139
140
//=================================================================================================
141
// Clause -- a simple class for representing a clause:
142
143
class Clause;
144
typedef RegionAllocator<uint32_t>::Ref CRef;
145
146
class Clause {
147
    struct {
148
        unsigned mark      : 2;
149
        unsigned learnt    : 1;
150
        unsigned has_extra : 1;
151
        unsigned reloced   : 1;
152
        unsigned size      : 27; }                            header;
153
    union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
154
155
    friend class ClauseAllocator;
156
157
    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
158
    template<class V>
159
7318202
    Clause(const V& ps, bool use_extra, bool learnt) {
160
7318202
        header.mark      = 0;
161
7318202
        header.learnt    = learnt;
162
7318202
        header.has_extra = use_extra;
163
7318202
        header.reloced   = 0;
164
7318202
        header.size      = ps.size();
165
166
7318202
        for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i];
167
168
7318202
        if (header.has_extra){
169
7318202
            if (header.learnt)
170
222584
              data[header.size].act = 0;
171
            else
172
7095618
              calcAbstraction();
173
        }
174
7318202
    }
175
176
public:
177
7252131
    void calcAbstraction() {
178
7252131
      Assert(header.has_extra);
179
7252131
      uint32_t abstraction = 0;
180
26978170
      for (int i = 0; i < size(); i++)
181
19726039
        abstraction |= 1 << (var(data[i].lit) & 31);
182
7252131
      data[header.size].abs = abstraction;
183
7252131
    }
184
185
1043598025
    int          size        ()      const   { return header.size; }
186
39653
    void shrink(int i)
187
    {
188
39653
      Assert(i <= size());
189
39653
      if (header.has_extra) data[header.size - i] = data[header.size];
190
39653
      header.size -= i;
191
39653
    }
192
39653
    void         pop         ()              { shrink(1); }
193
20080872
    bool         learnt      ()      const   { return header.learnt; }
194
180811
    bool         has_extra   ()      const   { return header.has_extra; }
195
413844635
    uint32_t     mark        ()      const   { return header.mark; }
196
27233626
    void         mark        (uint32_t m)    { header.mark = m; }
197
    const Lit&   last        ()      const   { return data[header.size-1].lit; }
198
199
688341
    bool         reloced     ()      const   { return header.reloced; }
200
558995
    CRef         relocation  ()      const   { return data[0].rel; }
201
128279
    void         relocate    (CRef c)        { header.reloced = 1; data[0].rel = c; }
202
203
    // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
204
    //       subsumption operations to behave correctly.
205
1651262824
    Lit&         operator [] (int i)         { return data[i].lit; }
206
125129062
    Lit          operator [] (int i) const   { return data[i].lit; }
207
66431634
    operator const Lit* (void) const         { return (Lit*)data; }
208
209
3101091
    float& activity()
210
    {
211
3101091
      Assert(header.has_extra);
212
3101091
      return data[header.size].act;
213
    }
214
    uint32_t abstraction() const
215
    {
216
      Assert(header.has_extra);
217
      return data[header.size].abs;
218
    }
219
220
    Lit          subsumes    (const Clause& other) const;
221
    void         strengthen  (Lit p);
222
};
223
224
225
//=================================================================================================
226
// ClauseAllocator -- a simple class for allocating memory for clauses:
227
228
229
const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
230
const CRef CRef_Lazy  = RegionAllocator<uint32_t>::Ref_Undef - 1;
231
232
9046
class ClauseAllocator : public RegionAllocator<uint32_t>
233
{
234
7388687
    static int clauseWord32Size(int size, bool has_extra){
235
7388687
        return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
236
 public:
237
    bool extra_clause_field;
238
239
72
    ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}
240
8977
    ClauseAllocator() : extra_clause_field(false){}
241
242
72
    void moveTo(ClauseAllocator& to){
243
72
        to.extra_clause_field = extra_clause_field;
244
72
        RegionAllocator<uint32_t>::moveTo(to); }
245
246
    template<class Lits>
247
7318202
    CRef alloc(const Lits& ps, bool learnt = false)
248
    {
249
7318202
      Assert(sizeof(Lit) == sizeof(uint32_t));
250
7318202
      Assert(sizeof(float) == sizeof(uint32_t));
251
7318202
      bool use_extra = learnt | extra_clause_field;
252
253
7318202
      CRef cid = RegionAllocator<uint32_t>::alloc(
254
          clauseWord32Size(ps.size(), use_extra));
255
7318202
      new (lea(cid)) Clause(ps, use_extra, learnt);
256
257
7318202
      return cid;
258
    }
259
260
    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
261
844596653
    Clause&       operator[](Ref r)       { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
262
3129698
    const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
263
7318202
    Clause*       lea       (Ref r)       { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
264
1290
    const Clause* lea       (Ref r) const { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
265
    Ref           ael       (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); }
266
267
70485
    void free(CRef cid)
268
    {
269
70485
        Clause& c = operator[](cid);
270
70485
        RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
271
70485
    }
272
273
    void reloc(CRef& cr, ClauseAllocator& to);
274
};
275
276
277
//=================================================================================================
278
// OccLists -- a class for maintaining occurence lists with lazy deletion:
279
280
template<class Idx, class Vec, class Deleted>
281
17948
class OccLists
282
{
283
    vec<Vec>  occs;
284
    vec<char> dirty;
285
    vec<Idx>  dirties;
286
    Deleted   deleted;
287
288
 public:
289
17954
    OccLists(const Deleted& d) : deleted(d) {}
290
291
5560818
    void  init      (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
292
    // Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
293
344468200
    Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
294
15262781
    Vec&  lookup    (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
295
296
    void  cleanAll  ();
297
    void  clean     (const Idx& idx);
298
297999
    void  smudge    (const Idx& idx){
299
297999
        if (dirty[toInt(idx)] == 0){
300
119004
            dirty[toInt(idx)] = 1;
301
119004
            dirties.push(idx);
302
        }
303
297999
    }
304
305
    void  clear(bool free = true){
306
        occs   .clear(free);
307
        dirty  .clear(free);
308
        dirties.clear(free);
309
    }
310
};
311
312
313
template<class Idx, class Vec, class Deleted>
314
10647387
void OccLists<Idx,Vec,Deleted>::cleanAll()
315
{
316
10766391
    for (int i = 0; i < dirties.size(); i++)
317
        // Dirties may contain duplicates so check here if a variable is already cleaned:
318
119004
        if (dirty[toInt(dirties[i])])
319
76617
            clean(dirties[i]);
320
10647387
    dirties.clear();
321
10647387
}
322
323
324
template<class Idx, class Vec, class Deleted>
325
119004
void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
326
{
327
119004
    Vec& vec = occs[toInt(idx)];
328
    int  i, j;
329
3248702
    for (i = j = 0; i < vec.size(); i++)
330
3129698
        if (!deleted(vec[i]))
331
2847979
            vec[j++] = vec[i];
332
119004
    vec.shrink(i - j);
333
119004
    dirty[toInt(idx)] = 0;
334
119004
}
335
336
337
//=================================================================================================
338
// CMap -- a class for mapping clauses to values:
339
340
341
template<class T>
342
class CMap
343
{
344
    struct CRefHash {
345
        uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
346
347
    typedef Map<CRef, T, CRefHash> HashTable;
348
    HashTable map;
349
350
 public:
351
    // Size-operations:
352
    void     clear       ()                           { map.clear(); }
353
    int      size        ()                const      { return map.elems(); }
354
355
    // Insert/Remove/Test mapping:
356
    void     insert      (CRef cr, const T& t){ map.insert(cr, t); }
357
    void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
358
    void     remove      (CRef cr)            { map.remove(cr); }
359
    bool     has         (CRef cr, T& t)      { return map.peek(cr, t); }
360
361
    // Vector interface (the clause 'c' must already exist):
362
    const T& operator [] (CRef cr) const      { return map[cr]; }
363
    T&       operator [] (CRef cr)            { return map[cr]; }
364
365
    // Iteration (not transparent at all at the moment):
366
    int  bucket_count() const { return map.bucket_count(); }
367
    const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
368
369
    // Move contents to other map:
370
    void moveTo(CMap& other){ map.moveTo(other.map); }
371
372
    // TMP debug:
373
    void debug(){
374
        printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
375
};
376
377
/*_________________________________________________________________________________________________
378
|
379
|  subsumes : (other : const Clause&)  ->  Lit
380
|
381
|  Description:
382
|       Checks if clause subsumes 'other', and at the same time, if it can be
383
used to simplify 'other' |       by subsumption resolution.
384
|
385
|    Result:
386
|       lit_Error  - No subsumption or simplification
387
|       lit_Undef  - Clause subsumes 'other'
388
|       p          - The literal p can be deleted from 'other'
389
|________________________________________________________________________________________________@*/
390
123027920
inline Lit Clause::subsumes(const Clause& other) const
391
{
392
    //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
393
    //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
394
123027920
    Assert(!header.learnt);
395
123027920
    Assert(!other.header.learnt);
396
123027920
    Assert(header.has_extra);
397
123027920
    Assert(other.header.has_extra);
398
123027920
    if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
399
89869458
        return lit_Error;
400
401
33158462
    Lit        ret = lit_Undef;
402
33158462
    const Lit* c   = (const Lit*)(*this);
403
33158462
    const Lit* d   = (const Lit*)other;
404
405
75287657
    for (unsigned i = 0; i < header.size; i++) {
406
        // search for c[i] or ~c[i]
407
471053611
        for (unsigned j = 0; j < other.header.size; j++)
408
437966134
            if (c[i] == d[j])
409
14999696
                goto ok;
410
422966438
            else if (ret == lit_Undef && c[i] == ~d[j]){
411
27129499
                ret = c[i];
412
27129499
                goto ok;
413
            }
414
415
        // did not find it
416
33087477
        return lit_Error;
417
42129195
    ok:;
418
    }
419
420
70985
    return ret;
421
}
422
423
39653
inline void Clause::strengthen(Lit p)
424
{
425
39653
    remove(*this, p);
426
39653
    calcAbstraction();
427
39653
}
428
429
430
431
//=================================================================================================
432
} /* CVC4::BVMinisat namespace */
433
} /* CVC4 namespace */
434
435
#endif