GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/core/SolverTypes.h Lines: 140 160 87.5 %
Date: 2021-03-22 Branches: 67 190 35.3 %

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
#include "cvc4_private.h"
22
23
#ifndef Minisat_SolverTypes_h
24
#define Minisat_SolverTypes_h
25
26
#include "base/check.h"
27
#include "base/output.h"
28
#include "prop/minisat/mtl/Alg.h"
29
#include "prop/minisat/mtl/Alloc.h"
30
#include "prop/minisat/mtl/IntTypes.h"
31
#include "prop/minisat/mtl/Map.h"
32
#include "prop/minisat/mtl/Vec.h"
33
34
namespace CVC4 {
35
namespace Minisat {
36
class Solver;
37
}
38
template <class Solver>
39
class TSatProof;
40
}  // namespace CVC4
41
42
namespace CVC4 {
43
namespace Minisat {
44
45
//=================================================================================================
46
// Variables, literals, lifted booleans, clauses:
47
48
49
// NOTE! Variables 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
typedef int Var;
53
#define var_Undef (-1)
54
55
56
57
struct Lit {
58
    int     x;
59
60
    // Use this as a constructor:
61
    friend Lit mkLit(Var var, bool sign);
62
63
3878193927
    bool operator == (Lit p) const { return x == p.x; }
64
242903372
    bool operator != (Lit p) const { return x != p.x; }
65
81649409
    bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
66
};
67
68
69
100365813
inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
70
1322805651
inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
71
inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
72
1502804777
inline  bool sign      (Lit p)              { return p.x & 1; }
73
3522872056
inline  int  var       (Lit p)              { return p.x >> 1; }
74
75
// Mapping Literals to and from compact integers suitable for array indexing:
76
15073386
inline int toInt(Var v) { return v; }
77
232289007
inline int toInt(Lit p) { return p.x; }
78
72549
inline Lit toLit(int i)
79
{
80
  Lit p;
81
72549
  p.x = i;
82
72549
  return p;
83
}
84
85
//const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.
86
//const Lit lit_Error = mkLit(var_Undef, true );  // }
87
88
const Lit lit_Undef = { -2 };  // }- Useful special constants.
89
const Lit lit_Error = { -1 };  // }
90
91
//=================================================================================================
92
// Lifted booleans:
93
//
94
// NOTE: this implementation is optimized for the case when comparisons between
95
// values are mostly
96
//       between one variable and one constant. Some care had to be taken to
97
//       make sure that gcc does enough constant propagation to produce sensible
98
//       code, and this appears to be somewhat fragile unfortunately.
99
100
/*
101
  This is to avoid multiple definitions of l_True, l_False and l_Undef if using
102
  multiple copies of Minisat. IMPORTANT: if we you change the value of the
103
  constants so that it is not the same in all copies of Minisat this breaks!
104
 */
105
106
#ifndef l_True
107
#define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
108
#endif
109
110
#ifndef l_False
111
#define l_False (lbool((uint8_t)1))
112
#endif
113
114
#ifndef l_Undef
115
#define l_Undef (lbool((uint8_t)2))
116
#endif
117
118
class lbool {
119
    uint8_t value;
120
121
public:
122
2848354972
    explicit lbool(uint8_t v) : value(v) { }
123
124
516498
    lbool()       : value(0) { }
125
51753406
    explicit lbool(bool x) : value(!x) { }
126
127
1436408202
    bool  operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
128
590836428
    bool  operator != (lbool b) const { return !(*this == b); }
129
1367886716
    lbool operator ^  (bool  b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
130
131
    lbool operator&&(lbool b) const
132
    {
133
      uint8_t sel = (this->value << 1) | (b.value << 3);
134
      uint8_t v = (0xF7F755F4 >> sel) & 3;
135
      return lbool(v);
136
    }
137
138
    lbool operator || (lbool b) const {
139
        uint8_t sel = (this->value << 1) | (b.value << 3);
140
        uint8_t v   = (0xFCFCF400 >> sel) & 3;
141
        return lbool(v); }
142
143
    friend int   toInt  (lbool l);
144
    friend lbool toLbool(int   v);
145
};
146
inline int   toInt  (lbool l) { return l.value; }
147
inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }
148
149
150
class Clause;
151
typedef RegionAllocator<uint32_t>::Ref CRef;
152
153
/* convenience printing functions */
154
155
156
inline std::ostream& operator <<(std::ostream& out, Minisat::Lit lit) {
157
  const char * s = (Minisat::sign(lit)) ? "~" : " ";
158
  out << s << Minisat::var(lit);
159
  return out;
160
}
161
162
inline std::ostream& operator <<(std::ostream& out, Minisat::vec<Minisat::Lit>& clause) {
163
  out << "clause:";
164
  for(int i = 0; i < clause.size(); ++i) {
165
    out << " " << clause[i];
166
  }
167
  out << ";";
168
  return out;
169
}
170
171
inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
172
  std::string val_str;
173
  if( val == l_False ) {
174
    val_str = "0";
175
  } else if (val == l_True ) {
176
    val_str = "1";
177
  } else { // unknown
178
    val_str = "_";
179
  }
180
181
  out << val_str;
182
  return out;
183
}
184
185
} /* namespace CVC4::Minisat */
186
} /* namespace CVC4 */
187
188
189
namespace CVC4 {
190
namespace Minisat{
191
192
//=================================================================================================
193
// Clause -- a simple class for representing a clause:
194
195
class Clause {
196
    struct {
197
        unsigned mark      : 2;
198
        unsigned removable : 1;
199
        unsigned has_extra : 1;
200
        unsigned reloced   : 1;
201
        unsigned size      : 27;
202
        unsigned level     : 32; }                            header;
203
    union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
204
205
    friend class ClauseAllocator;
206
207
    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
208
    template<class V>
209
3206685
    Clause(const V& ps, bool use_extra, bool removable, int level) {
210
3206685
        header.mark      = 0;
211
3206685
        header.removable = removable;
212
3206685
        header.has_extra = use_extra;
213
3206685
        header.reloced   = 0;
214
3206685
        header.size      = ps.size();
215
3206685
        header.level     = level;
216
217
3206685
        for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i];
218
219
3206685
        if (header.has_extra){
220
3206685
            if (header.removable)
221
733005
              data[header.size].act = 0;
222
            else
223
2473680
              calcAbstraction();
224
        }
225
3206685
    }
226
227
public:
228
3499387
    void calcAbstraction() {
229
3499387
      Assert(header.has_extra);
230
3499387
      uint32_t abstraction = 0;
231
16395093
      for (int i = 0; i < size(); i++)
232
12895706
        abstraction |= 1 << (var(data[i].lit) & 31);
233
3499387
      data[header.size].abs = abstraction;
234
3499387
    }
235
236
63589588
    int          level       ()      const   { return header.level; }
237
986026545
    int          size        ()      const   { return header.size; }
238
98365
    void shrink(int i)
239
    {
240
98365
      Assert(i <= size());
241
98365
      if (header.has_extra) data[header.size - i] = data[header.size];
242
98365
      header.size -= i;
243
98365
    }
244
98365
    void         pop         ()              { shrink(1); }
245
12518085
    bool         removable   ()      const   { return header.removable; }
246
1622475
    bool         has_extra   ()      const   { return header.has_extra; }
247
79560070
    uint32_t     mark        ()      const   { return header.mark; }
248
3159156
    void         mark        (uint32_t m)    { header.mark = m; }
249
    const Lit&   last        ()      const   { return data[header.size-1].lit; }
250
251
4135686
    bool         reloced     ()      const   { return header.reloced; }
252
2965402
    CRef         relocation  ()      const   { return data[0].rel; }
253
1124195
    void         relocate    (CRef c)        { header.reloced = 1; data[0].rel = c; }
254
255
    // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
256
    //       subsumption operations to behave correctly.
257
2036668738
    Lit&         operator [] (int i)         { return data[i].lit; }
258
54425834
    Lit          operator [] (int i) const   { return data[i].lit; }
259
8803306
    operator const Lit* (void) const         { return (Lit*)data; }
260
261
12503652
    float& activity()
262
    {
263
12503652
      Assert(header.has_extra);
264
12503652
      return data[header.size].act;
265
    }
266
    uint32_t abstraction() const
267
    {
268
      Assert(header.has_extra);
269
      return data[header.size].abs;
270
    }
271
272
    Lit          subsumes    (const Clause& other) const;
273
    void         strengthen  (Lit p);
274
};
275
276
277
//=================================================================================================
278
// ClauseAllocator -- a simple class for allocating memory for clauses:
279
280
281
const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
282
const CRef CRef_Lazy  = RegionAllocator<uint32_t>::Ref_Undef - 1;
283
12126
class ClauseAllocator : public RegionAllocator<uint32_t>
284
{
285
3926704
    static int clauseWord32Size(int size, bool has_extra){
286
3926704
        return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
287
 public:
288
    bool extra_clause_field;
289
290
3102
    ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}
291
9027
    ClauseAllocator() : extra_clause_field(false){}
292
293
3102
    void moveTo(ClauseAllocator& to){
294
3102
        to.extra_clause_field = extra_clause_field;
295
3102
        RegionAllocator<uint32_t>::moveTo(to); }
296
297
    template<class Lits>
298
3206685
    CRef alloc(int level, const Lits& ps, bool removable = false)
299
    {
300
3206685
      Assert(sizeof(Lit) == sizeof(uint32_t));
301
3206685
      Assert(sizeof(float) == sizeof(uint32_t));
302
3206685
      bool use_extra = removable | extra_clause_field;
303
304
3206685
      CRef cid = RegionAllocator<uint32_t>::alloc(
305
          clauseWord32Size(ps.size(), use_extra));
306
3206685
      new (lea(cid)) Clause(ps, use_extra, removable, level);
307
308
3206685
      return cid;
309
    }
310
311
    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
312
453776135
    Clause&       operator[](Ref r)       { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
313
16863295
    const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
314
3206685
    Clause*       lea       (Ref r)       { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
315
303574
    const Clause* lea       (Ref r) const { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
316
    Ref           ael       (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); }
317
318
720019
    void free(CRef cid)
319
    {
320
720019
        Clause& c = operator[](cid);
321
720019
        RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
322
720019
    }
323
324
    void reloc(CRef& cr,
325
               ClauseAllocator& to,
326
               CVC4::TSatProof<Solver>* proof = NULL);
327
    // Implementation moved to Solver.cc.
328
};
329
330
331
//=================================================================================================
332
// OccLists -- a class for maintaining occurence lists with lazy deletion:
333
334
template<class Idx, class Vec, class Deleted>
335
18048
class OccLists
336
{
337
    vec<Vec>  occs;
338
    vec<char> dirty;
339
    vec<Idx>  dirties;
340
    Deleted   deleted;
341
342
 public:
343
18054
    OccLists(const Deleted& d) : deleted(d) {}
344
345
1800607
    void  init      (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
346
    void  resizeTo  (const Idx& idx);
347
    // Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
348
205465128
    Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
349
1006318
    Vec&  lookup    (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
350
351
    void  cleanAll  ();
352
    void  clean     (const Idx& idx);
353
2162665
    void  smudge    (const Idx& idx){
354
2162665
        if (dirty[toInt(idx)] == 0){
355
659129
            dirty[toInt(idx)] = 1;
356
659129
            dirties.push(idx);
357
        }
358
2162665
    }
359
360
    void  clear(bool free = true){
361
        occs   .clear(free);
362
        dirty  .clear(free);
363
        dirties.clear(free);
364
    }
365
};
366
367
368
template<class Idx, class Vec, class Deleted>
369
3939388
void OccLists<Idx,Vec,Deleted>::cleanAll()
370
{
371
4482341
    for (int i = 0; i < dirties.size(); i++)
372
        // Dirties may contain duplicates so check here if a variable is already cleaned:
373
542953
        if (dirty[toInt(dirties[i])])
374
456370
            clean(dirties[i]);
375
3939388
    dirties.clear();
376
3939388
}
377
378
template<class Idx, class Vec, class Deleted>
379
1893
void OccLists<Idx,Vec,Deleted>::resizeTo(const Idx& idx)
380
{
381
1893
    int shrinkSize = occs.size() - (toInt(idx) + 1);
382
1893
    occs.shrink(shrinkSize);
383
1893
    dirty.shrink(shrinkSize);
384
    // Remove out-of-bound indices from dirties
385
    int  i, j;
386
129009
    for (i = j = 0; i < dirties.size(); i++)
387
127116
        if (toInt(dirties[i]) < occs.size())
388
12112
            dirties[j++] = dirties[i];
389
1893
    dirties.shrink(i - j);
390
1893
}
391
392
template<class Idx, class Vec, class Deleted>
393
542953
void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
394
{
395
542953
    Vec& vec = occs[toInt(idx)];
396
    int  i, j;
397
17406248
    for (i = j = 0; i < vec.size(); i++)
398
16863295
        if (!deleted(vec[i]))
399
15125720
            vec[j++] = vec[i];
400
542953
    vec.shrink(i - j);
401
542953
    dirty[toInt(idx)] = 0;
402
542953
}
403
404
405
//=================================================================================================
406
// CMap -- a class for mapping clauses to values:
407
408
409
template<class T>
410
class CMap
411
{
412
    struct CRefHash {
413
        uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
414
415
    typedef Map<CRef, T, CRefHash> HashTable;
416
    HashTable map;
417
418
 public:
419
    // Size-operations:
420
    void     clear       ()                           { map.clear(); }
421
    int      size        ()                const      { return map.elems(); }
422
423
    // Insert/Remove/Test mapping:
424
    void     insert      (CRef cr, const T& t){ map.insert(cr, t); }
425
    void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
426
    void     remove      (CRef cr)            { map.remove(cr); }
427
    bool     has         (CRef cr, T& t)      { return map.peek(cr, t); }
428
429
    // Vector interface (the clause 'c' must already exist):
430
    const T& operator [] (CRef cr) const      { return map[cr]; }
431
    T&       operator [] (CRef cr)            { return map[cr]; }
432
433
    // Iteration (not transparent at all at the moment):
434
    int  bucket_count() const { return map.bucket_count(); }
435
    const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
436
437
    // Move contents to other map:
438
    void moveTo(CMap& other){ map.moveTo(other.map); }
439
440
    // TMP debug:
441
    void debug(){
442
        printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
443
};
444
445
/*_________________________________________________________________________________________________
446
|
447
|  subsumes : (other : const Clause&)  ->  Lit
448
|
449
|  Description:
450
|       Checks if clause subsumes 'other', and at the same time, if it can be
451
used to simplify 'other' |       by subsumption resolution.
452
|
453
|    Result:
454
|       lit_Error  - No subsumption or simplification
455
|       lit_Undef  - Clause subsumes 'other'
456
|       p          - The literal p can be deleted from 'other'
457
|________________________________________________________________________________________________@*/
458
27363516
inline Lit Clause::subsumes(const Clause& other) const
459
{
460
    // We restrict subsumtion to clauses at higher levels (if !enable_incremantal this should always be false)
461
27363516
    if (level() > other.level()) {
462
      return lit_Error;
463
    }
464
465
    //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
466
    //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
467
27363516
    Assert(!header.removable);
468
27363516
    Assert(!other.header.removable);
469
27363516
    Assert(header.has_extra);
470
27363516
    Assert(other.header.has_extra);
471
27363516
    if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
472
23963740
        return lit_Error;
473
474
3399776
    Lit        ret = lit_Undef;
475
3399776
    const Lit* c   = (const Lit*)(*this);
476
3399776
    const Lit* d   = (const Lit*)other;
477
478
13470720
    for (unsigned i = 0; i < header.size; i++) {
479
        // search for c[i] or ~c[i]
480
1225493736
        for (unsigned j = 0; j < other.header.size; j++)
481
1222334183
            if (c[i] == d[j])
482
8293481
                goto ok;
483
1214040702
            else if (ret == lit_Undef && c[i] == ~d[j]){
484
1777463
                ret = c[i];
485
1777463
                goto ok;
486
            }
487
488
        // did not find it
489
3159553
        return lit_Error;
490
10070944
    ok:;
491
    }
492
493
240223
    return ret;
494
}
495
496
98365
inline void Clause::strengthen(Lit p)
497
{
498
98365
    remove(*this, p);
499
98365
    calcAbstraction();
500
98365
}
501
502
//=================================================================================================
503
}
504
}
505
506
#endif