| /***********************************************************************************[SolverTypes.h] |
| MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson |
| |
| Permission is hereby granted, free of charge, to any person obtaining a copy of this software and |
| associated documentation files (the "Software"), to deal in the Software without restriction, |
| including without limitation the rights to use, copy, modify, merge, publish, distribute, |
| sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is |
| furnished to do so, subject to the following conditions: |
| |
| The above copyright notice and this permission notice shall be included in all copies or |
| substantial portions of the Software. |
| |
| THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT |
| NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND |
| NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, |
| DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT |
| OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
| **************************************************************************************************/ |
| |
| |
| #ifndef SolverTypes_h |
| #define SolverTypes_h |
| |
| #include <cassert> |
| #include <stdint.h> |
| |
| //================================================================================================= |
| // Variables, literals, lifted booleans, clauses: |
| |
| |
| // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, |
| // so that they can be used as array indices. |
| |
| typedef int Var; |
| #define var_Undef (-1) |
| |
| |
| class Lit { |
| int x; |
| public: |
| Lit() : x(2*var_Undef) { } // (lit_Undef) |
| explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { } |
| |
| // Don't use these for constructing/deconstructing literals. Use the normal constructors instead. |
| friend int toInt (Lit p); // Guarantees small, positive integers suitable for array indexing. |
| friend Lit toLit (int i); // Inverse of 'toInt()' |
| friend Lit operator ~(Lit p); |
| friend bool sign (Lit p); |
| friend int var (Lit p); |
| friend Lit unsign (Lit p); |
| friend Lit id (Lit p, bool sgn); |
| |
| bool operator == (Lit p) const { return x == p.x; } |
| bool operator != (Lit p) const { return x != p.x; } |
| bool operator < (Lit p) const { return x < p.x; } // '<' guarantees that p, ~p are adjacent in the ordering. |
| }; |
| |
| inline int toInt (Lit p) { return p.x; } |
| inline Lit toLit (int i) { Lit p; p.x = i; return p; } |
| inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } |
| inline bool sign (Lit p) { return p.x & 1; } |
| inline int var (Lit p) { return p.x >> 1; } |
| inline Lit unsign (Lit p) { Lit q; q.x = p.x & ~1; return q; } |
| inline Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; } |
| |
| const Lit lit_Undef(var_Undef, false); // }- Useful special constants. |
| const Lit lit_Error(var_Undef, true ); // } |
| |
| |
| //================================================================================================= |
| // Lifted booleans: |
| |
| |
| class lbool { |
| char value; |
| explicit lbool(int v) : value(v) { } |
| |
| public: |
| lbool() : value(0) { } |
| lbool(bool x) : value((int)x*2-1) { } |
| int toInt(void) const { return value; } |
| |
| bool operator == (lbool b) const { return value == b.value; } |
| bool operator != (lbool b) const { return value != b.value; } |
| lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); } |
| |
| friend int toInt (lbool l); |
| friend lbool toLbool(int v); |
| }; |
| inline int toInt (lbool l) { return l.toInt(); } |
| inline lbool toLbool(int v) { return lbool(v); } |
| |
| const lbool l_True = toLbool( 1); |
| const lbool l_False = toLbool(-1); |
| const lbool l_Undef = toLbool( 0); |
| |
| //================================================================================================= |
| // Clause -- a simple class for representing a clause: |
| |
| |
| class Clause { |
| uint32_t size_etc; |
| union { float act; uint32_t abst; } extra; |
| Lit data[0]; |
| |
| public: |
| void calcAbstraction() { |
| uint32_t abstraction = 0; |
| for (int i = 0; i < size(); i++) |
| abstraction |= 1 << (var(data[i]) & 31); |
| extra.abst = abstraction; } |
| |
| // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). |
| template<class V> |
| Clause(const V& ps, bool learnt) { |
| size_etc = (ps.size() << 3) | (uint32_t)learnt; |
| for (int i = 0; i < ps.size(); i++) data[i] = ps[i]; |
| if (learnt) extra.act = 0; else calcAbstraction(); } |
| |
| int size () const { return size_etc >> 3; } |
| void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); } |
| void pop () { shrink(1); } |
| bool learnt () const { return size_etc & 1; } |
| uint32_t mark () const { return (size_etc >> 1) & 3; } |
| void mark (uint32_t m) { size_etc = (size_etc & ~6) | ((m & 3) << 1); } |
| const Lit& last () const { return data[size()-1]; } |
| |
| // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for |
| // subsumption operations to behave correctly. |
| Lit& operator [] (int i) { return data[i]; } |
| Lit operator [] (int i) const { return data[i]; } |
| operator const Lit* (void) const { return data; } |
| |
| float& activity () { return extra.act; } |
| uint32_t abstraction () const { return extra.abst; } |
| |
| Lit subsumes (const Clause& other) const; |
| void strengthen (Lit p); |
| }; |
| |
| // -- use this function instead: |
| template<class V> |
| Clause* Clause_new(const V& ps, bool learnt = false) { |
| assert(sizeof(Lit) == sizeof(uint32_t)); |
| assert(sizeof(float) == sizeof(uint32_t)); |
| void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size())); |
| return new (mem) Clause(ps, learnt); |
| } |
| |
| /*_________________________________________________________________________________________________ |
| | |
| | subsumes : (other : const Clause&) -> Lit |
| | |
| | Description: |
| | Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other' |
| | by subsumption resolution. |
| | |
| | Result: |
| | lit_Error - No subsumption or simplification |
| | lit_Undef - Clause subsumes 'other' |
| | p - The literal p can be deleted from 'other' |
| |________________________________________________________________________________________________@*/ |
| inline Lit Clause::subsumes(const Clause& other) const |
| { |
| if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) |
| return lit_Error; |
| |
| Lit ret = lit_Undef; |
| const Lit* c = (const Lit*)(*this); |
| const Lit* d = (const Lit*)other; |
| |
| for (int i = 0; i < size(); i++) { |
| // search for c[i] or ~c[i] |
| for (int j = 0; j < other.size(); j++) |
| if (c[i] == d[j]) |
| goto ok; |
| else if (ret == lit_Undef && c[i] == ~d[j]){ |
| ret = c[i]; |
| goto ok; |
| } |
| |
| // did not find it |
| return lit_Error; |
| ok:; |
| } |
| |
| return ret; |
| } |
| |
| |
| inline void Clause::strengthen(Lit p) |
| { |
| remove(*this, p); |
| calcAbstraction(); |
| } |
| |
| #endif |