GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/core/SolverTypes.h Lines: 140 160 87.5 %
Date: 2021-03-23 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
3878196191
    bool operator == (Lit p) const { return x == p.x; }
64
242903747
    bool operator != (Lit p) const { return x != p.x; }
65
81650060
    bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
66
};
67
68
69
100369621
inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
70
1322806947
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
1502812112
inline  bool sign      (Lit p)              { return p.x & 1; }
73
3522889239
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
232290843
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
2848370053
    explicit lbool(uint8_t v) : value(v) { }
123
124
516648
    lbool()       : value(0) { }
125
51753821
    explicit lbool(bool x) : value(!x) { }
126
127
1436416612
    bool  operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
128
590836758
    bool  operator != (lbool b) const { return !(*this == b); }
129
1367892933
    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
3206886
    Clause(const V& ps, bool use_extra, bool removable, int level) {
210
3206886
        header.mark      = 0;
211
3206886
        header.removable = removable;
212
3206886
        header.has_extra = use_extra;
213
3206886
        header.reloced   = 0;
214
3206886
        header.size      = ps.size();
215
3206886
        header.level     = level;
216
217
3206886
        for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i];
218
219
3206886
        if (header.has_extra){
220
3206886
            if (header.removable)
221
733028
              data[header.size].act = 0;
222
            else
223
2473858
              calcAbstraction();
224
        }
225
3206886
    }
226
227
public:
228
3499569
    void calcAbstraction() {
229
3499569
      Assert(header.has_extra);
230
3499569
      uint32_t abstraction = 0;
231
16395678
      for (int i = 0; i < size(); i++)
232
12896109
        abstraction |= 1 << (var(data[i].lit) & 31);
233
3499569
      data[header.size].abs = abstraction;
234
3499569
    }
235
236
63589608
    int          level       ()      const   { return header.level; }
237
986028210
    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
12518307
    bool         removable   ()      const   { return header.removable; }
246
1622486
    bool         has_extra   ()      const   { return header.has_extra; }
247
79560084
    uint32_t     mark        ()      const   { return header.mark; }
248
3159167
    void         mark        (uint32_t m)    { header.mark = m; }
249
    const Lit&   last        ()      const   { return data[header.size-1].lit; }
250
251
4135698
    bool         reloced     ()      const   { return header.reloced; }
252
2965410
    CRef         relocation  ()      const   { return data[0].rel; }
253
1124199
    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
2036670076
    Lit&         operator [] (int i)         { return data[i].lit; }
258
54426765
    Lit          operator [] (int i) const   { return data[i].lit; }
259
8803306
    operator const Lit* (void) const         { return (Lit*)data; }
260
261
12503664
    float& activity()
262
    {
263
12503664
      Assert(header.has_extra);
264
12503664
      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
12128
class ClauseAllocator : public RegionAllocator<uint32_t>
284
{
285
3926912
    static int clauseWord32Size(int size, bool has_extra){
286
3926912
        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
9029
    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
3206886
    CRef alloc(int level, const Lits& ps, bool removable = false)
299
    {
300
3206886
      Assert(sizeof(Lit) == sizeof(uint32_t));
301
3206886
      Assert(sizeof(float) == sizeof(uint32_t));
302
3206886
      bool use_extra = removable | extra_clause_field;
303
304
3206886
      CRef cid = RegionAllocator<uint32_t>::alloc(
305
          clauseWord32Size(ps.size(), use_extra));
306
3206886
      new (lea(cid)) Clause(ps, use_extra, removable, level);
307
308
3206886
      return cid;
309
    }
310
311
    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
312
453776740
    Clause&       operator[](Ref r)       { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
313
16863301
    const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
314
3206886
    Clause*       lea       (Ref r)       { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
315
303579
    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
720026
    void free(CRef cid)
319
    {
320
720026
        Clause& c = operator[](cid);
321
720026
        RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
322
720026
    }
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
18052
class OccLists
336
{
337
    vec<Vec>  occs;
338
    vec<char> dirty;
339
    vec<Idx>  dirties;
340
    Deleted   deleted;
341
342
 public:
343
18058
    OccLists(const Deleted& d) : deleted(d) {}
344
345
1801031
    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
205465972
    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
2162679
    void  smudge    (const Idx& idx){
354
2162679
        if (dirty[toInt(idx)] == 0){
355
659143
            dirty[toInt(idx)] = 1;
356
659143
            dirties.push(idx);
357
        }
358
2162679
    }
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
3939556
void OccLists<Idx,Vec,Deleted>::cleanAll()
370
{
371
4482515
    for (int i = 0; i < dirties.size(); i++)
372
        // Dirties may contain duplicates so check here if a variable is already cleaned:
373
542959
        if (dirty[toInt(dirties[i])])
374
456376
            clean(dirties[i]);
375
3939556
    dirties.clear();
376
3939556
}
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
129017
    for (i = j = 0; i < dirties.size(); i++)
387
127124
        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
542959
void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
394
{
395
542959
    Vec& vec = occs[toInt(idx)];
396
    int  i, j;
397
17406260
    for (i = j = 0; i < vec.size(); i++)
398
16863301
        if (!deleted(vec[i]))
399
15125720
            vec[j++] = vec[i];
400
542959
    vec.shrink(i - j);
401
542959
    dirty[toInt(idx)] = 0;
402
542959
}
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