libs/minisat/SolverTypes.h

   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
  22 #ifndef Minisat_SolverTypes_h
  23 #define Minisat_SolverTypes_h
  24
  25 #include <assert.h>
  26
  27 #include "IntTypes.h"
  28 #include "Alg.h"
  29 #include "Vec.h"
  30 #include "IntMap.h"
  31 #include "Map.h"
  32 #include "Alloc.h"
  33
  34 namespace Minisat {
  35
  36 //=================================================================================================
  37 // Variables, literals, lifted booleans, clauses:
  38
  39
  40 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
  41 // so that they can be used as array indices.
  42
  43 typedef int Var;
  44 #if defined(MINISAT_CONSTANTS_AS_MACROS)
  45 #define var_Undef (-1)
  46 #else
  47   const Var var_Undef = -1;
  48 #endif
  49
  50
  51 struct Lit {
  52     int     x;
  53
  54     // Use this as a constructor:
  55     friend Lit mkLit(Var var, bool sign);
  56
  57     bool operator == (Lit p) const { return x == p.x; }
  58     bool operator != (Lit p) const { return x != p.x; }
  59     bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
  60 };
  61
  62
  63 inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
  64 inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
  65 inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
  66 inline  bool sign      (Lit p)              { return p.x & 1; }
  67 inline  int  var       (Lit p)              { return p.x >> 1; }
  68
  69 // Mapping Literals to and from compact integers suitable for array indexing:
  70 inline  int  toInt     (Var v)              { return v; }
  71 inline  int  toInt     (Lit p)              { return p.x; }
  72 inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; }
  73
  74 //const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.
  75 //const Lit lit_Error = mkLit(var_Undef, true );  // }
  76
  77 const Lit lit_Undef = { -2 };  // }- Useful special constants.
  78 const Lit lit_Error = { -1 };  // }
  79
  80 struct MkIndexLit { vec<Lit>::Size operator()(Lit l) const { return vec<Lit>::Size(l.x); } };
  81
  82 template<class T> class VMap : public IntMap<Var, T>{};
  83 template<class T> class LMap : public IntMap<Lit, T, MkIndexLit>{};
  84 class LSet : public IntSet<Lit, MkIndexLit>{};
  85
  86 //=================================================================================================
  87 // Lifted booleans:
  88 //
  89 // NOTE: this implementation is optimized for the case when comparisons between values are mostly
  90 //       between one variable and one constant. Some care had to be taken to make sure that gcc
  91 //       does enough constant propagation to produce sensible code, and this appears to be somewhat
  92 //       fragile unfortunately.
  93
  94 class lbool {
  95     uint8_t value;
  96
  97 public:
  98     explicit lbool(uint8_t v) : value(v) { }
  99
 100     lbool()       : value(0) { }
 101     explicit lbool(bool x) : value(!x) { }
 102
 103     bool  operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
 104     bool  operator != (lbool b) const { return !(*this == b); }
 105     lbool operator ^  (bool  b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
 106
 107     lbool operator && (lbool b) const {
 108         uint8_t sel = (this->value << 1) | (b.value << 3);
 109         uint8_t v   = (0xF7F755F4 >> sel) & 3;
 110         return lbool(v); }
 111
 112     lbool operator || (lbool b) const {
 113         uint8_t sel = (this->value << 1) | (b.value << 3);
 114         uint8_t v   = (0xFCFCF400 >> sel) & 3;
 115         return lbool(v); }
 116
 117     friend int   toInt  (lbool l);
 118     friend lbool toLbool(int   v);
 119 };
 120 inline int   toInt  (lbool l) { return l.value; }
 121 inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }
 122
 123 #if defined(MINISAT_CONSTANTS_AS_MACROS)
 124   #define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
 125   #define l_False (lbool((uint8_t)1))
 126   #define l_Undef (lbool((uint8_t)2))
 127 #else
 128   const lbool l_True ((uint8_t)0);
 129   const lbool l_False((uint8_t)1);
 130   const lbool l_Undef((uint8_t)2);
 131 #endif
 132
 133
 134 //=================================================================================================
 135 // Clause -- a simple class for representing a clause:
 136
 137 class Clause;
 138 typedef RegionAllocator<uint32_t>::Ref CRef;
 139
 140 class Clause {
 141     struct {
 142         unsigned mark      : 2;
 143         unsigned learnt    : 1;
 144         unsigned has_extra : 1;
 145         unsigned reloced   : 1;
 146         unsigned size      : 27; }                        header;
 147     union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
 148
 149     friend class ClauseAllocator;
 150
 151     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
 152     Clause(const vec<Lit>& ps, bool use_extra, bool learnt) {
 153         header.mark      = 0;
 154         header.learnt    = learnt;
 155         header.has_extra = use_extra;
 156         header.reloced   = 0;
 157         header.size      = ps.size();
 158
 159         for (int i = 0; i < ps.size(); i++)
 160             data[i].lit = ps[i];
 161
 162         if (header.has_extra){
 163             if (header.learnt)
 164                 data[header.size].act = 0;
 165             else
 166                 calcAbstraction();
 167     }
 168     }
 169
 170     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
 171     Clause(const Clause& from, bool use_extra){
 172         header           = from.header;
 173         header.has_extra = use_extra;   // NOTE: the copied clause may lose the extra field.
 174
 175         for (int i = 0; i < from.size(); i++)
 176             data[i].lit = from[i];
 177
 178         if (header.has_extra){
 179             if (header.learnt)
 180                 data[header.size].act = from.data[header.size].act;
 181             else
 182                 data[header.size].abs = from.data[header.size].abs;
 183     }
 184     }
 185
 186 public:
 187     void calcAbstraction() {
 188         assert(header.has_extra);
 189         uint32_t abstraction = 0;
 190         for (int i = 0; i < size(); i++)
 191             abstraction |= 1 << (var(data[i].lit) & 31);
 192         data[header.size].abs = abstraction;  }
 193
 194
 195     int          size        ()      const   { return header.size; }
 196     void         shrink      (int i)         { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
 197     void         pop         ()              { shrink(1); }
 198     bool         learnt      ()      const   { return header.learnt; }
 199     bool         has_extra   ()      const   { return header.has_extra; }
 200     uint32_t     mark        ()      const   { return header.mark; }
 201     void         mark        (uint32_t m)    { header.mark = m; }
 202     const Lit&   last        ()      const   { return data[header.size-1].lit; }
 203
 204     bool         reloced     ()      const   { return header.reloced; }
 205     CRef         relocation  ()      const   { return data[0].rel; }
 206     void         relocate    (CRef c)        { header.reloced = 1; data[0].rel = c; }
 207
 208     // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
 209     //       subsumption operations to behave correctly.
 210     Lit&         operator [] (int i)         { return data[i].lit; }
 211     Lit          operator [] (int i) const   { return data[i].lit; }
 212     operator const Lit* (void) const         { return (Lit*)data; }
 213
 214     float&       activity    ()              { assert(header.has_extra); return data[header.size].act; }
 215     uint32_t     abstraction () const        { assert(header.has_extra); return data[header.size].abs; }
 216
 217     Lit          subsumes    (const Clause& other) const;
 218     void         strengthen  (Lit p);
 219 };
 220
 221
 222 //=================================================================================================
 223 // ClauseAllocator -- a simple class for allocating memory for clauses:
 224
 225 const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
 226 class ClauseAllocator
 227 {
 228     RegionAllocator<uint32_t> ra;
 229
 230     static uint32_t clauseWord32Size(int size, bool has_extra){
 231         return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
 232
 233  public:
 234     enum { Unit_Size = RegionAllocator<uint32_t>::Unit_Size };
 235
 236     bool extra_clause_field;
 237
 238     ClauseAllocator(uint32_t start_cap) : ra(start_cap), extra_clause_field(false){}
 239     ClauseAllocator() : extra_clause_field(false){}
 240
 241     void moveTo(ClauseAllocator& to){
 242         to.extra_clause_field = extra_clause_field;
 243         ra.moveTo(to.ra); }
 244
 245     CRef alloc(const vec<Lit>& ps, bool learnt = false)
 246     {
 247         assert(sizeof(Lit)      == sizeof(uint32_t));
 248         assert(sizeof(float)    == sizeof(uint32_t));
 249         bool use_extra = learnt | extra_clause_field;
 250         CRef cid       = ra.alloc(clauseWord32Size(ps.size(), use_extra));
 251         new (lea(cid)) Clause(ps, use_extra, learnt);
 252
 253         return cid;
 254     }
 255
 256     CRef alloc(const Clause& from)
 257     {
 258         bool use_extra = from.learnt() | extra_clause_field;
 259         CRef cid       = ra.alloc(clauseWord32Size(from.size(), use_extra));
 260         new (lea(cid)) Clause(from, use_extra);
 261         return cid; }
 262
 263     uint32_t size      () const      { return ra.size(); }
 264     uint32_t wasted    () const      { return ra.wasted(); }
 265
 266     // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
 267     Clause&       operator[](CRef r)         { return (Clause&)ra[r]; }
 268     const Clause& operator[](CRef r) const   { return (Clause&)ra[r]; }
 269     Clause*       lea       (CRef r)         { return (Clause*)ra.lea(r); }
 270     const Clause* lea       (CRef r) const   { return (Clause*)ra.lea(r);; }
 271     CRef          ael       (const Clause* t){ return ra.ael((uint32_t*)t); }
 272
 273     void free(CRef cid)
 274     {
 275         Clause& c = operator[](cid);
 276         ra.free(clauseWord32Size(c.size(), c.has_extra()));
 277     }
 278
 279     void reloc(CRef& cr, ClauseAllocator& to)
 280     {
 281         Clause& c = operator[](cr);
 282
 283         if (c.reloced()) { cr = c.relocation(); return; }
 284
 285         cr = to.alloc(c);
 286         c.relocate(cr);
 287     }
 288 };
 289
 290 //=================================================================================================
 291 // Simple iterator classes (for iterating over clauses and top-level assignments):
 292
 293 class ClauseIterator {
 294     const ClauseAllocator& ca;
 295     const CRef*            crefs;
 296 public:
 297     ClauseIterator(const ClauseAllocator& _ca, const CRef* _crefs) : ca(_ca), crefs(_crefs){}
 298
 299     void operator++(){ crefs++; }
 300     const Clause& operator*() const { return ca[*crefs]; }
 301
 302     // NOTE: does not compare that references use the same clause-allocator:
 303     bool operator==(const ClauseIterator& ci) const { return crefs == ci.crefs; }
 304     bool operator!=(const ClauseIterator& ci) const { return crefs != ci.crefs; }
 305 };
 306
 307
 308 class TrailIterator {
 309     const Lit* lits;
 310 public:
 311     TrailIterator(const Lit* _lits) : lits(_lits){}
 312
 313     void operator++()   { lits++; }
 314     Lit  operator*() const { return *lits; }
 315
 316     bool operator==(const TrailIterator& ti) const { return lits == ti.lits; }
 317     bool operator!=(const TrailIterator& ti) const { return lits != ti.lits; }
 318 };
 319
 320
 321 //=================================================================================================
 322 // OccLists -- a class for maintaining occurence lists with lazy deletion:
 323
 324 template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K> >
 325 class OccLists
 326 {
 327     IntMap<K, Vec,  MkIndex> occs;
 328     IntMap<K, char, MkIndex> dirty;
 329     vec<K>                   dirties;
 330     Deleted                  deleted;
 331
 332  public:
 333     OccLists(const Deleted& d, MkIndex _index = MkIndex()) :
 334         occs(_index),
 335         dirty(_index),
 336         deleted(d){}
 337
 338     void  init      (const K& idx){ occs.reserve(idx); occs[idx].clear(); dirty.reserve(idx, 0); }
 339     Vec&  operator[](const K& idx){ return occs[idx]; }
 340     Vec&  lookup    (const K& idx){ if (dirty[idx]) clean(idx); return occs[idx]; }
 341
 342     void  cleanAll  ();
 343     void  clean     (const K& idx);
 344     void  smudge    (const K& idx){
 345         if (dirty[idx] == 0){
 346             dirty[idx] = 1;
 347             dirties.push(idx);
 348         }
 349     }
 350
 351     void  clear(bool free = true){
 352         occs   .clear(free);
 353         dirty  .clear(free);
 354         dirties.clear(free);
 355     }
 356 };
 357
 358
 359 template<class K, class Vec, class Deleted, class MkIndex>
 360 void OccLists<K,Vec,Deleted,MkIndex>::cleanAll()
 361 {
 362     for (int i = 0; i < dirties.size(); i++)
 363         // Dirties may contain duplicates so check here if a variable is already cleaned:
 364         if (dirty[dirties[i]])
 365             clean(dirties[i]);
 366     dirties.clear();
 367 }
 368
 369
 370 template<class K, class Vec, class Deleted, class MkIndex>
 371 void OccLists<K,Vec,Deleted,MkIndex>::clean(const K& idx)
 372 {
 373     Vec& vec = occs[idx];
 374     int  i, j;
 375     for (i = j = 0; i < vec.size(); i++)
 376         if (!deleted(vec[i]))
 377             vec[j++] = vec[i];
 378     vec.shrink(i - j);
 379     dirty[idx] = 0;
 380 }
 381
 382
 383 //=================================================================================================
 384 // CMap -- a class for mapping clauses to values:
 385
 386
 387 template<class T>
 388 class CMap
 389 {
 390     struct CRefHash {
 391         uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
 392
 393     typedef Map<CRef, T, CRefHash> HashTable;
 394     HashTable map;
 395
 396  public:
 397     // Size-operations:
 398     void     clear       ()                           { map.clear(); }
 399     int      size        ()                const      { return map.elems(); }
 400
 401
 402     // Insert/Remove/Test mapping:
 403     void     insert      (CRef cr, const T& t){ map.insert(cr, t); }
 404     void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
 405     void     remove      (CRef cr)            { map.remove(cr); }
 406     bool     has         (CRef cr, T& t)      { return map.peek(cr, t); }
 407
 408     // Vector interface (the clause 'c' must already exist):
 409     const T& operator [] (CRef cr) const      { return map[cr]; }
 410     T&       operator [] (CRef cr)            { return map[cr]; }
 411
 412     // Iteration (not transparent at all at the moment):
 413     int  bucket_count() const { return map.bucket_count(); }
 414     const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
 415
 416     // Move contents to other map:
 417     void moveTo(CMap& other){ map.moveTo(other.map); }
 418
 419     // TMP debug:
 420     void debug(){
 421         printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
 422 };
 423
 424
 425 /*_________________________________________________________________________________________________
 426 |
 427 |  subsumes : (other : const Clause&)  ->  Lit
 428 |
 429 |  Description:
 430 |       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
 431 |       by subsumption resolution.
 432 |
 433 |    Result:
 434 |       lit_Error  - No subsumption or simplification
 435 |       lit_Undef  - Clause subsumes 'other'
 436 |       p          - The literal p can be deleted from 'other'
 437 |________________________________________________________________________________________________@*/
 438 inline Lit Clause::subsumes(const Clause& other) const
 439 {
 440     //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
 441     //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
 442     assert(!header.learnt);   assert(!other.header.learnt);
 443     assert(header.has_extra); assert(other.header.has_extra);
 444     if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
 445         return lit_Error;
 446
 447     Lit        ret = lit_Undef;
 448     const Lit* c   = (const Lit*)(*this);
 449     const Lit* d   = (const Lit*)other;
 450
 451     for (unsigned i = 0; i < header.size; i++) {
 452         // search for c[i] or ~c[i]
 453         for (unsigned j = 0; j < other.header.size; j++)
 454             if (c[i] == d[j])
 455                 goto ok;
 456             else if (ret == lit_Undef && c[i] == ~d[j]){
 457                 ret = c[i];
 458                 goto ok;
 459             }
 460
 461         // did not find it
 462         return lit_Error;
 463     ok:;
 464     }
 465
 466     return ret;
 467 }
 468
 469 inline void Clause::strengthen(Lit p)
 470 {
 471     remove(*this, p);
 472     calcAbstraction();
 473 }
 474
 475 //=================================================================================================
 476 }
 477
 478 #endif