backends/minisat/core/SolverTypes.h

   1 /***********************************************************************************[SolverTypes.h]
   2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
   5 associated documentation files (the "Software"), to deal in the Software without restriction,
   6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
   7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
   8 furnished to do so, subject to the following conditions:
   9
  10 The above copyright notice and this permission notice shall be included in all copies or
  11 substantial portions of the Software.
  12
  13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  18 **************************************************************************************************/
  19
  20
  21 #ifndef SolverTypes_h
  22 #define SolverTypes_h
  23
  24 #include <cassert>
  25 #include <stdint.h>
  26
  27 //=================================================================================================
  28 // Variables, literals, lifted booleans, clauses:
  29
  30
  31 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
  32 // so that they can be used as array indices.
  33
  34 typedef int Var;
  35 #define var_Undef (-1)
  36
  37
  38 class Lit {
  39     int     x;
  40  public:
  41     Lit() : x(2*var_Undef)                                              { }   // (lit_Undef)
  42     explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { }
  43
  44     // Don't use these for constructing/deconstructing literals. Use the normal constructors instead.
  45     friend int  toInt       (Lit p);  // Guarantees small, positive integers suitable for array indexing.
  46     friend Lit  toLit       (int i);  // Inverse of 'toInt()'
  47     friend Lit  operator   ~(Lit p);
  48     friend bool sign        (Lit p);
  49     friend int  var         (Lit p);
  50     friend Lit  unsign      (Lit p);
  51     friend Lit  id          (Lit p, bool sgn);
  52
  53     bool operator == (Lit p) const { return x == p.x; }
  54     bool operator != (Lit p) const { return x != p.x; }
  55     bool operator <  (Lit p) const { return x < p.x;  } // '<' guarantees that p, ~p are adjacent in the ordering.
  56 };
  57
  58 inline  int  toInt       (Lit p)           { return p.x; }
  59 inline  Lit  toLit       (int i)           { Lit p; p.x = i; return p; }
  60 inline  Lit  operator   ~(Lit p)           { Lit q; q.x = p.x ^ 1; return q; }
  61 inline  bool sign        (Lit p)           { return p.x & 1; }
  62 inline  int  var         (Lit p)           { return p.x >> 1; }
  63 inline  Lit  unsign      (Lit p)           { Lit q; q.x = p.x & ~1; return q; }
  64 inline  Lit  id          (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
  65
  66 const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
  67 const Lit lit_Error(var_Undef, true );  // }
  68
  69
  70 //=================================================================================================
  71 // Lifted booleans:
  72
  73
  74 class lbool {
  75     char     value;
  76     explicit lbool(int v) : value(v) { }
  77
  78 public:
  79     lbool()       : value(0) { }
  80     lbool(bool x) : value((int)x*2-1) { }
  81     int toInt(void) const { return value; }
  82
  83     bool  operator == (lbool b) const { return value == b.value; }
  84     bool  operator != (lbool b) const { return value != b.value; }
  85     lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); }
  86
  87     friend int   toInt  (lbool l);
  88     friend lbool toLbool(int   v);
  89 };
  90 inline int   toInt  (lbool l) { return l.toInt(); }
  91 inline lbool toLbool(int   v) { return lbool(v);  }
  92
  93 const lbool l_True  = toLbool( 1);
  94 const lbool l_False = toLbool(-1);
  95 const lbool l_Undef = toLbool( 0);
  96
  97 //=================================================================================================
  98 // Clause -- a simple class for representing a clause:
  99
 100
 101 class Clause {
 102     uint32_t size_etc;
 103     union { float act; uint32_t abst; } extra;
 104     Lit     data[0];
 105
 106 public:
 107     void calcAbstraction() {
 108         uint32_t abstraction = 0;
 109         for (int i = 0; i < size(); i++)
 110             abstraction |= 1 << (var(data[i]) & 31);
 111         extra.abst = abstraction;  }
 112
 113     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
 114     template<class V>
 115     Clause(const V& ps, bool learnt) {
 116         size_etc = (ps.size() << 3) | (uint32_t)learnt;
 117         for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
 118         if (learnt) extra.act = 0; else calcAbstraction(); }
 119
 120     // -- use this function instead:
 121     template<class V>
 122     static Clause* Clause_new(const V& ps, bool learnt = false) {
 123         assert(sizeof(Lit)      == sizeof(uint32_t));
 124         assert(sizeof(float)    == sizeof(uint32_t));
 125         void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
 126         return new (mem) Clause(ps, learnt); }
 127
 128     int          size        ()      const   { return size_etc >> 3; }
 129     void         shrink      (int i)         { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); }
 130     void         pop         ()              { shrink(1); }
 131     bool         learnt      ()      const   { return size_etc & 1; }
 132     uint32_t     mark        ()      const   { return (size_etc >> 1) & 3; }
 133     void         mark        (uint32_t m)    { size_etc = (size_etc & ~6) | ((m & 3) << 1); }
 134     const Lit&   last        ()      const   { return data[size()-1]; }
 135
 136     // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
 137     //       subsumption operations to behave correctly.
 138     Lit&         operator [] (int i)         { return data[i]; }
 139     Lit          operator [] (int i) const   { return data[i]; }
 140     operator const Lit* (void) const         { return data; }
 141
 142     float&       activity    ()              { return extra.act; }
 143     uint32_t     abstraction () const { return extra.abst; }
 144
 145     Lit          subsumes    (const Clause& other) const;
 146     void         strengthen  (Lit p);
 147 };
 148
 149
 150 /*_________________________________________________________________________________________________
 151 |
 152 |  subsumes : (other : const Clause&)  ->  Lit
 153 |
 154 |  Description:
 155 |       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
 156 |       by subsumption resolution.
 157 |
 158 |    Result:
 159 |       lit_Error  - No subsumption or simplification
 160 |       lit_Undef  - Clause subsumes 'other'
 161 |       p          - The literal p can be deleted from 'other'
 162 |________________________________________________________________________________________________@*/
 163 inline Lit Clause::subsumes(const Clause& other) const
 164 {
 165     if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
 166         return lit_Error;
 167
 168     Lit        ret = lit_Undef;
 169     const Lit* c  = (const Lit*)(*this);
 170     const Lit* d  = (const Lit*)other;
 171
 172     for (int i = 0; i < size(); i++) {
 173         // search for c[i] or ~c[i]
 174         for (int j = 0; j < other.size(); j++)
 175             if (c[i] == d[j])
 176                 goto ok;
 177             else if (ret == lit_Undef && c[i] == ~d[j]){
 178                 ret = c[i];
 179                 goto ok;
 180             }
 181
 182         // did not find it
 183         return lit_Error;
 184     ok:;
 185     }
 186
 187     return ret;
 188 }
 189
 190
 191 inline void Clause::strengthen(Lit p)
 192 {
 193     remove(*this, p);
 194     calcAbstraction();
 195 }
 196
 197 #endif