sat-solver/SolverTypes.h
00001 /***********************************************************************************[SolverTypes.h]
00002 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
00003 
00004 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
00005 associated documentation files (the "Software"), to deal in the Software without restriction,
00006 including without limitation the rights to use, copy, modify, merge, publish, distribute,
00007 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
00008 furnished to do so, subject to the following conditions:
00009 
00010 The above copyright notice and this permission notice shall be included in all copies or
00011 substantial portions of the Software.
00012 
00013 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
00014 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00015 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
00016 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
00017 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00018 **************************************************************************************************/
00019 
00020 
00021 #ifndef SolverTypes_h
00022 #define SolverTypes_h
00023 
00024 #include <cassert>
00025 #include <stdint.h>
00026 
00027 namespace minisat
00028 {
00029 
00030 //=================================================================================================
00031 // Variables, literals, lifted booleans, clauses:
00032 
00033 
00034 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
00035 // so that they can be used as array indices.
00036 
00037 typedef int Var;
00038 #define var_Undef (-1)
00039 
00040 
00041 class Lit {
00042     int     x;
00043  public:
00044     Lit() : x(2*var_Undef)                                              { }   // (lit_Undef)
00045     explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { }
00046 
00047     // Don't use these for constructing/deconstructing literals. Use the normal constructors instead.
00048     friend int  toInt       (Lit p);  // Guarantees small, positive integers suitable for array indexing.
00049     friend Lit  toLit       (int i);  // Inverse of 'toInt()'
00050     friend Lit  operator   ~(Lit p);
00051     friend bool sign        (Lit p);
00052     friend int  var         (Lit p);
00053     friend Lit  unsign      (Lit p);
00054     friend Lit  id          (Lit p, bool sgn);
00055 
00056     bool operator == (Lit p) const { return x == p.x; }
00057     bool operator != (Lit p) const { return x != p.x; }
00058     bool operator <  (Lit p) const { return x < p.x;  } // '<' guarantees that p, ~p are adjacent in the ordering.
00059 };
00060 
00061 inline  int  toInt       (Lit p)           { return p.x; }
00062 inline  Lit  toLit       (int i)           { Lit p; p.x = i; return p; }
00063 inline  Lit  operator   ~(Lit p)           { Lit q; q.x = p.x ^ 1; return q; }
00064 inline  bool sign        (Lit p)           { return p.x & 1; }
00065 inline  int  var         (Lit p)           { return p.x >> 1; }
00066 inline  Lit  unsign      (Lit p)           { Lit q; q.x = p.x & ~1; return q; }
00067 inline  Lit  id          (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
00068 
00069 const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
00070 const Lit lit_Error(var_Undef, true );  // }
00071 
00072 
00073 //=================================================================================================
00074 // Lifted booleans:
00075 
00076 
00077 class lbool {
00078     char     value;
00079     explicit lbool(int v) : value(v) { }
00080 
00081 public:
00082     lbool()       : value(0) { }
00083     lbool(bool x) : value((int)x*2-1) { }
00084     int toInt(void) const { return value; }
00085 
00086     bool  operator == (lbool b) const { return value == b.value; }
00087     bool  operator != (lbool b) const { return value != b.value; }
00088     lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); }
00089 
00090     friend int   toInt  (lbool l);
00091     friend lbool toLbool(int   v);
00092 };
00093 inline int   toInt  (lbool l) { return l.toInt(); }
00094 inline lbool toLbool(int   v) { return lbool(v);  }
00095 
00096 const lbool l_True  = toLbool( 1);
00097 const lbool l_False = toLbool(-1);
00098 const lbool l_Undef = toLbool( 0);
00099 
00100 //=================================================================================================
00101 // Clause -- a simple class for representing a clause:
00102 
00103 
00104 class Clause {
00105 public:
00106     uint32_t size_etc;
00107     union { float act; uint32_t abst; } extra;
00108     Lit     data[0];
00109 
00110 
00111     void calcAbstraction() {
00112         uint32_t abstraction = 0;
00113         for (int i = 0; i < size(); i++)
00114             abstraction |= 1 << (var(data[i]) & 31);
00115         extra.abst = abstraction;  }
00116 
00117     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
00118     template<class V>
00119     Clause(const V& ps, bool learnt) {
00120         size_etc = (ps.size() << 3) | (uint32_t)learnt;
00121         for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
00122         if (learnt) extra.act = 0; else calcAbstraction(); }
00123 
00124     // -- use this function instead:
00125     template<class V>
00126     friend Clause* Clause_new(const V& ps, bool learnt = false) {
00127         assert(sizeof(Lit)      == sizeof(uint32_t));
00128         assert(sizeof(float)    == sizeof(uint32_t));
00129         void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
00130         return new (mem) Clause(ps, learnt); }
00131 
00132     int          size        ()      const   { return size_etc >> 3; }
00133     void         shrink      (int i)         { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); }
00134     void         pop         ()              { shrink(1); }
00135     bool         learnt      ()      const   { return size_etc & 1; }
00136     uint32_t     mark        ()      const   { return (size_etc >> 1) & 3; }
00137     void         mark        (uint32_t m)    { size_etc = (size_etc & ~6) | ((m & 3) << 1); }
00138     const Lit&   last        ()      const   { return data[size()-1]; }
00139 
00140     // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
00141     //       subsumption operations to behave correctly.
00142     Lit&         operator [] (int i)         { return data[i]; }
00143     Lit          operator [] (int i) const   { return data[i]; }
00144     operator const Lit* (void) const         { return data; }
00145 
00146     float&       activity    ()              { return extra.act; }
00147     uint32_t     abstraction () const { return extra.abst; }
00148 
00149     Lit          subsumes    (const Clause& other) const;
00150     void         strengthen  (Lit p);
00151 };
00152 
00153 
00154 /*_________________________________________________________________________________________________
00155 |
00156 |  subsumes : (other : const Clause&)  ->  Lit
00157 |
00158 |  Description:
00159 |       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
00160 |       by subsumption resolution.
00161 |
00162 |    Result:
00163 |       lit_Error  - No subsumption or simplification
00164 |       lit_Undef  - Clause subsumes 'other'
00165 |       p          - The literal p can be deleted from 'other'
00166 |________________________________________________________________________________________________@*/
00167 inline Lit Clause::subsumes(const Clause& other) const
00168 {
00169     if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
00170         return lit_Error;
00171 
00172     Lit        ret = lit_Undef;
00173     const Lit* c  = (const Lit*)(*this);
00174     const Lit* d  = (const Lit*)other;
00175 
00176     for (int i = 0; i < size(); i++) {
00177         // search for c[i] or ~c[i]
00178         for (int j = 0; j < other.size(); j++)
00179             if (c[i] == d[j])
00180                 goto ok;
00181             else if (ret == lit_Undef && c[i] == ~d[j]){
00182                 ret = c[i];
00183                 goto ok;
00184             }
00185 
00186         // did not find it
00187         return lit_Error;
00188     ok:;
00189     }
00190 
00191     return ret;
00192 }
00193 
00194 
00195 inline void Clause::strengthen(Lit p)
00196 {
00197     remove(*this, p);
00198     calcAbstraction();
00199 }
00200 }
00201 
00202 #endif