glucose-syrup/core/SolverTypes.h

   1 /***************************************************************************************[SolverTypes.h]
   2  Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
   3                                 CRIL - Univ. Artois, France
   4                                 LRI  - Univ. Paris Sud, France (2009-2013)
   5                                 Labri - Univ. Bordeaux, France
   6
   7  Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
   8                                 CRIL - Univ. Artois, France
   9                                 Labri - Univ. Bordeaux, France
  10
  11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
  12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
  13 is based on. (see below).
  14
  15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
  16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
  17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
  18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
  19 furnished to do so, subject to the following conditions:
  20
  21 - The above and below copyrights notices and this permission notice shall be included in all
  22 copies or substantial portions of the Software;
  23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
  24 be used in any competitive event (sat competitions/evaluations) without the express permission of
  25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
  26 using Glucose Parallel as an embedded SAT engine (single core or not).
  27
  28
  29 --------------- Original Minisat Copyrights
  30
  31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  32 Copyright (c) 2007-2010, Niklas Sorensson
  33
  34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  35 associated documentation files (the "Software"), to deal in the Software without restriction,
  36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
  37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  38 furnished to do so, subject to the following conditions:
  39
  40 The above copyright notice and this permission notice shall be included in all copies or
  41 substantial portions of the Software.
  42
  43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  48  **************************************************************************************************/
  49
  50
  51 #ifndef Glucose_SolverTypes_h
  52 #define Glucose_SolverTypes_h
  53
  54 #include <assert.h>
  55 #include <stdint.h>
  56 #include <pthread.h>
  57
  58 #include "mtl/IntTypes.h"
  59 #include "mtl/Alg.h"
  60 #include "mtl/Vec.h"
  61 #include "mtl/Map.h"
  62 #include "mtl/Alloc.h"
  63
  64
  65 namespace Glucose {
  66
  67 //=================================================================================================
  68 // Variables, literals, lifted booleans, clauses:
  69
  70
  71 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
  72 // so that they can be used as array indices.
  73
  74 typedef int Var;
  75 #define var_Undef (-1)
  76
  77
  78 struct Lit {
  79     int     x;
  80
  81     // Use this as a constructor:
  82     friend Lit mkLit(Var var, bool sign);
  83
  84     bool operator == (Lit p) const { return x == p.x; }
  85     bool operator != (Lit p) const { return x != p.x; }
  86     bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
  87 };
  88
  89
  90 inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
  91 inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
  92 inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
  93 inline  bool sign      (Lit p)              { return p.x & 1; }
  94 inline  int  var       (Lit p)              { return p.x >> 1; }
  95
  96 // Mapping Literals to and from compact integers suitable for array indexing:
  97 inline  int  toInt     (Var v)              { return v; }
  98 inline  int  toInt     (Lit p)              { return p.x; }
  99 inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; }
 100
 101 //const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.
 102 //const Lit lit_Error = mkLit(var_Undef, true );  // }
 103
 104 const Lit lit_Undef = { -2 };  // }- Useful special constants.
 105 const Lit lit_Error = { -1 };  // }
 106
 107
 108 //=================================================================================================
 109 // Lifted booleans:
 110 //
 111 // NOTE: this implementation is optimized for the case when comparisons between values are mostly
 112 //       between one variable and one constant. Some care had to be taken to make sure that gcc
 113 //       does enough constant propagation to produce sensible code, and this appears to be somewhat
 114 //       fragile unfortunately.
 115
 116 #define l_True  (Glucose::lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
 117 #define l_False (Glucose::lbool((uint8_t)1))
 118 #define l_Undef (Glucose::lbool((uint8_t)2))
 119
 120 class lbool {
 121     uint8_t value;
 122
 123 public:
 124     explicit lbool(uint8_t v) : value(v) { }
 125
 126     lbool()       : value(0) { }
 127     explicit lbool(bool x) : value(!x) { }
 128
 129     bool  operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
 130     bool  operator != (lbool b) const { return !(*this == b); }
 131     lbool operator ^  (bool  b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
 132
 133     lbool operator && (lbool b) const {
 134         uint8_t sel = (this->value << 1) | (b.value << 3);
 135         uint8_t v   = (0xF7F755F4 >> sel) & 3;
 136         return lbool(v); }
 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 // Clause -- a simple class for representing a clause:
 151
 152 class Clause;
 153 typedef RegionAllocator<uint32_t>::Ref CRef;
 154
 155 #define BITS_LBD 13
 156 #define BITS_SIZEWITHOUTSEL 19
 157 #define BITS_REALSIZE 21
 158 class Clause {
 159     struct {
 160       unsigned mark       : 2;
 161       unsigned learnt     : 1;
 162       unsigned szWithoutSelectors : BITS_SIZEWITHOUTSEL;
 163       unsigned canbedel   : 1;
 164       unsigned extra_size : 2; // extra size (end of 32bits) 0..3
 165       unsigned size       : BITS_REALSIZE;
 166       unsigned seen       : 1;
 167       unsigned reloced    : 1;
 168       unsigned exported   : 2; // Values to keep track of the clause status for exportations
 169       unsigned oneWatched : 1;
 170       unsigned lbd : BITS_LBD;
 171     }  header;
 172
 173     union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
 174
 175     friend class ClauseAllocator;
 176
 177     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
 178     template<class V>
 179     Clause(const V& ps, int _extra_size, bool learnt) {
 180         assert(_extra_size < (1<<2));
 181         header.mark      = 0;
 182         header.learnt    = learnt;
 183         header.extra_size = _extra_size;
 184         header.reloced   = 0;
 185         header.size      = ps.size();
 186         header.lbd = 0;
 187         header.canbedel = 1;
 188         header.exported = 0;
 189         header.oneWatched = 0;
 190         header.seen = 0;
 191         for (int i = 0; i < ps.size(); i++)
 192             data[i].lit = ps[i];
 193
 194         if (header.extra_size > 0){
 195           if (header.learnt)
 196                 data[header.size].act = 0;
 197             else
 198                 calcAbstraction();
 199           if (header.extra_size > 1) {
 200               data[header.size+1].abs = 0; // learntFrom
 201           }
 202         }
 203     }
 204
 205 public:
 206     void calcAbstraction() {
 207         assert(header.extra_size > 0);
 208         uint32_t abstraction = 0;
 209         for (int i = 0; i < size(); i++)
 210             abstraction |= 1 << (var(data[i].lit) & 31);
 211         data[header.size].abs = abstraction;  }
 212
 213     int          size        ()      const   { return header.size; }
 214     void         shrink      (int i)         { assert(i <= size());
 215                                                 if (header.extra_size > 0) {
 216                                                     data[header.size-i] = data[header.size];
 217                                                     if (header.extra_size > 1) { // Special case for imported clauses
 218                                                         data[header.size-i-1] = data[header.size-1];
 219                                                     }
 220                                                 }
 221     header.size -= i; }
 222     void         pop         ()              { shrink(1); }
 223     bool         learnt      ()      const   { return header.learnt; }
 224     bool         has_extra   ()      const   { return header.extra_size > 0; }
 225     uint32_t     mark        ()      const   { return header.mark; }
 226     void         mark        (uint32_t m)    { header.mark = m; }
 227     const Lit&   last        ()      const   { return data[header.size-1].lit; }
 228
 229     bool         reloced     ()      const   { return header.reloced; }
 230     CRef         relocation  ()      const   { return data[0].rel; }
 231     void         relocate    (CRef c)        { header.reloced = 1; data[0].rel = c; }
 232
 233     // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
 234     //       subsumption operations to behave correctly.
 235     Lit&         operator [] (int i)         { return data[i].lit; }
 236     Lit          operator [] (int i) const   { return data[i].lit; }
 237     operator const Lit* (void) const         { return (Lit*)data; }
 238
 239     float&       activity    ()              { assert(header.extra_size > 0); return data[header.size].act; }
 240     uint32_t     abstraction () const        { assert(header.extra_size > 0); return data[header.size].abs; }
 241
 242     // Handle imported clauses lazy sharing
 243     bool        wasImported() const {return header.extra_size > 1;}
 244     uint32_t    importedFrom () const       { assert(header.extra_size > 1); return data[header.size + 1].abs;}
 245     void setImportedFrom(uint32_t ifrom) {assert(header.extra_size > 1); data[header.size+1].abs = ifrom;}
 246
 247     Lit          subsumes    (const Clause& other) const;
 248     void         strengthen  (Lit p);
 249     void         setLBD(int i)  {if (i < (1<<(BITS_LBD-1))) header.lbd = i; else header.lbd = (1<<(BITS_LBD-1));}
 250     // unsigned int&       lbd    ()              { return header.lbd; }
 251     unsigned int        lbd    () const        { return header.lbd; }
 252     void setCanBeDel(bool b) {header.canbedel = b;}
 253     bool canBeDel() {return header.canbedel;}
 254     void setSeen(bool b) {header.seen = b;}
 255     bool getSeen() {return header.seen;}
 256     void setExported(unsigned int b) {header.exported = b;}
 257     unsigned int getExported() {return header.exported;}
 258     void setOneWatched(bool b) {header.oneWatched = b;}
 259     bool getOneWatched() {return header.oneWatched;}
 260     void setSizeWithoutSelectors   (unsigned int n)              {header.szWithoutSelectors = n; }
 261     unsigned int        sizeWithoutSelectors   () const        { return header.szWithoutSelectors; }
 262
 263 };
 264
 265
 266 //=================================================================================================
 267 // ClauseAllocator -- a simple class for allocating memory for clauses:
 268
 269
 270 const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
 271 class ClauseAllocator : public RegionAllocator<uint32_t>
 272 {
 273     static int clauseWord32Size(int size, int extra_size){
 274         return (sizeof(Clause) + (sizeof(Lit) * (size + extra_size))) / sizeof(uint32_t); }
 275  public:
 276     bool extra_clause_field;
 277
 278     ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}
 279     ClauseAllocator() : extra_clause_field(false){}
 280
 281     void moveTo(ClauseAllocator& to){
 282         to.extra_clause_field = extra_clause_field;
 283         RegionAllocator<uint32_t>::moveTo(to); }
 284
 285     template<class Lits>
 286     CRef alloc(const Lits& ps, bool learnt = false, bool imported = false)
 287     {
 288         assert(sizeof(Lit)      == sizeof(uint32_t));
 289         assert(sizeof(float)    == sizeof(uint32_t));
 290
 291         bool use_extra = learnt | extra_clause_field;
 292         int extra_size = imported?3:(use_extra?1:0);
 293         CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), extra_size));
 294         new (lea(cid)) Clause(ps, extra_size, learnt);
 295
 296         return cid;
 297     }
 298
 299     // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
 300     Clause&       operator[](Ref r)       { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
 301     const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
 302     Clause*       lea       (Ref r)       { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
 303     const Clause* lea       (Ref r) const { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
 304     Ref           ael       (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); }
 305
 306     void free(CRef cid)
 307     {
 308         Clause& c = operator[](cid);
 309         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
 310     }
 311
 312     void reloc(CRef& cr, ClauseAllocator& to)
 313     {
 314         Clause& c = operator[](cr);
 315
 316         if (c.reloced()) { cr = c.relocation(); return; }
 317
 318         cr = to.alloc(c, c.learnt(), c.wasImported());
 319         c.relocate(cr);
 320
 321         // Copy extra data-fields:
 322         // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
 323         to[cr].mark(c.mark());
 324         if (to[cr].learnt())        {
 325           to[cr].activity() = c.activity();
 326           to[cr].setLBD(c.lbd());
 327           to[cr].setExported(c.getExported());
 328           to[cr].setOneWatched(c.getOneWatched());
 329           to[cr].setSeen(c.getSeen());
 330           to[cr].setSizeWithoutSelectors(c.sizeWithoutSelectors());
 331           to[cr].setCanBeDel(c.canBeDel());
 332           if (c.wasImported()) {
 333              to[cr].setImportedFrom(c.importedFrom());
 334           }
 335         }
 336         else if (to[cr].has_extra()) to[cr].calcAbstraction();
 337     }
 338 };
 339
 340
 341 //=================================================================================================
 342 // OccLists -- a class for maintaining occurence lists with lazy deletion:
 343
 344 template<class Idx, class Vec, class Deleted>
 345 class OccLists
 346 {
 347     vec<Vec>  occs;
 348     vec<char> dirty;
 349     vec<Idx>  dirties;
 350     Deleted   deleted;
 351
 352  public:
 353     OccLists(const Deleted& d) : deleted(d) {}
 354
 355     void  init      (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
 356     // Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
 357     Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
 358     Vec&  lookup    (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
 359
 360     void  cleanAll  ();
 361     void copyTo(OccLists &copy) const {
 362
 363         copy.occs.growTo(occs.size());
 364         for(int i = 0;i<occs.size();i++)
 365             occs[i].memCopyTo(copy.occs[i]);
 366         dirty.memCopyTo(copy.dirty);
 367         dirties.memCopyTo(copy.dirties);
 368     }
 369
 370     void  clean     (const Idx& idx);
 371     void  smudge    (const Idx& idx){
 372         if (dirty[toInt(idx)] == 0){
 373             dirty[toInt(idx)] = 1;
 374             dirties.push(idx);
 375         }
 376     }
 377
 378     void  clear(bool free = true){
 379         occs   .clear(free);
 380         dirty  .clear(free);
 381         dirties.clear(free);
 382     }
 383 };
 384
 385
 386 template<class Idx, class Vec, class Deleted>
 387 void OccLists<Idx,Vec,Deleted>::cleanAll()
 388 {
 389     for (int i = 0; i < dirties.size(); i++)
 390         // Dirties may contain duplicates so check here if a variable is already cleaned:
 391         if (dirty[toInt(dirties[i])])
 392             clean(dirties[i]);
 393     dirties.clear();
 394 }
 395
 396
 397 template<class Idx, class Vec, class Deleted>
 398 void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
 399 {
 400     Vec& vec = occs[toInt(idx)];
 401     int  i, j;
 402     for (i = j = 0; i < vec.size(); i++)
 403         if (!deleted(vec[i]))
 404             vec[j++] = vec[i];
 405     vec.shrink(i - j);
 406     dirty[toInt(idx)] = 0;
 407 }
 408
 409
 410 //=================================================================================================
 411 // CMap -- a class for mapping clauses to values:
 412
 413
 414 template<class T>
 415 class CMap
 416 {
 417     struct CRefHash {
 418         uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
 419
 420     typedef Map<CRef, T, CRefHash> HashTable;
 421     HashTable map;
 422
 423  public:
 424     // Size-operations:
 425     void     clear       ()                           { map.clear(); }
 426     int      size        ()                const      { return map.elems(); }
 427
 428
 429     // Insert/Remove/Test mapping:
 430     void     insert      (CRef cr, const T& t){ map.insert(cr, t); }
 431     void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
 432     void     remove      (CRef cr)            { map.remove(cr); }
 433     bool     has         (CRef cr, T& t)      { return map.peek(cr, t); }
 434
 435     // Vector interface (the clause 'c' must already exist):
 436     const T& operator [] (CRef cr) const      { return map[cr]; }
 437     T&       operator [] (CRef cr)            { return map[cr]; }
 438
 439     // Iteration (not transparent at all at the moment):
 440     int  bucket_count() const { return map.bucket_count(); }
 441     const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
 442
 443     // Move contents to other map:
 444     void moveTo(CMap& other){ map.moveTo(other.map); }
 445
 446     // TMP debug:
 447     void debug(){
 448         printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
 449 };
 450
 451
 452 /*_________________________________________________________________________________________________
 453 |
 454 |  subsumes : (other : const Clause&)  ->  Lit
 455 |
 456 |  Description:
 457 |       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
 458 |       by subsumption resolution.
 459 |
 460 |    Result:
 461 |       lit_Error  - No subsumption or simplification
 462 |       lit_Undef  - Clause subsumes 'other'
 463 |       p          - The literal p can be deleted from 'other'
 464 |________________________________________________________________________________________________@*/
 465 inline Lit Clause::subsumes(const Clause& other) const
 466 {
 467     //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
 468     //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
 469     assert(!header.learnt);   assert(!other.header.learnt);
 470     assert(header.extra_size > 0); assert(other.header.extra_size > 0);
 471     if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
 472         return lit_Error;
 473
 474     Lit        ret = lit_Undef;
 475     const Lit* c   = (const Lit*)(*this);
 476     const Lit* d   = (const Lit*)other;
 477
 478     for (unsigned i = 0; i < header.size; i++) {
 479         // search for c[i] or ~c[i]
 480         for (unsigned j = 0; j < other.header.size; j++)
 481             if (c[i] == d[j])
 482                 goto ok;
 483             else if (ret == lit_Undef && c[i] == ~d[j]){
 484                 ret = c[i];
 485                 goto ok;
 486             }
 487
 488         // did not find it
 489         return lit_Error;
 490     ok:;
 491     }
 492
 493     return ret;
 494 }
 495
 496 inline void Clause::strengthen(Lit p)
 497 {
 498     remove(*this, p);
 499     calcAbstraction();
 500 }
 501
 502 //=================================================================================================
 503 }
 504
 505
 506 #endif