1 /*****************************************************************************/ 2 /*! 3 *\file minisat_types.h 4 *\brief MiniSat internal types 5 * 6 * Author: Alexander Fuchs 7 * 8 * Created: Fri Sep 08 11:04:00 2006 9 * 10 * <hr> 11 * 12 * License to use, copy, modify, sell and/or distribute this software 13 * and its documentation for any purpose is hereby granted without 14 * royalty, subject to the terms and conditions defined in the \ref 15 * LICENSE file provided with this distribution. 16 * 17 * <hr> 18 */ 19 /*****************************************************************************/ 20 21 /***********************************************************************************[SolverTypes.h] 22 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson 23 24 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and 25 associated documentation files (the "Software"), to deal in the Software without restriction, 26 including without limitation the rights to use, copy, modify, merge, publish, distribute, 27 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is 28 furnished to do so, subject to the following conditions: 29 30 The above copyright notice and this permission notice shall be included in all copies or 31 substantial portions of the Software. 32 33 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT 34 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 35 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, 36 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT 37 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 38 **************************************************************************************************/ 39 40 #ifndef _cvc3__minisat__types_h_ 41 #define _cvc3__minisat__types_h_ 42 43 //================================================================================================= 44 // Variables, literals, clause IDs: 45 46 #include "minisat_global.h" 47 #include "theorem.h" 48 #include <vector> 49 50 namespace MiniSat { 51 52 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, 53 // so that they can be used as array indices. 54 // CVC additionally requires that N >= 2. 55 typedef int Var; 56 const int var_Undef = -1; 57 58 59 class Lit { 60 int x; 61 Lit(int index)62 explicit Lit(int index) : x(index) {} // (lit_Undef) 63 public: Lit()64 Lit() : x(2*var_Undef) {} // (lit_Undef) Lit(Var var,bool sgn)65 explicit Lit(Var var, bool sgn) : x((var+var) + (int)sgn) {} 66 Lit operator~ () const { return Lit(x ^ 1); }; 67 sign()68 bool sign () const { return x & 1; }; var()69 int var () const { return x >> 1; }; index()70 int index () const { return x; }; toLit(int i)71 static Lit toLit (int i) { return Lit(i); }; unsign()72 Lit unsign() const { return Lit(x & ~1); }; id(Lit p,bool sgn)73 static Lit id (Lit p, bool sgn) { return Lit(p.x ^ (int)sgn); }; 74 75 bool operator == (const Lit q) const { return index() == q.index(); }; 76 bool operator != (const Lit q) const { return !(operator==(q)); }; 77 // '<' guarantees that p, ~p are adjacent in the ordering.; 78 bool operator < (const Lit q) const { return index() < q.index(); } 79 hash()80 unsigned int hash() const { return (unsigned int)x; } 81 toString()82 std::string toString() const { 83 std::ostringstream buffer; 84 if (sign()) 85 buffer << "+"; 86 else 87 buffer << "-"; 88 buffer << var(); 89 return buffer.str(); 90 } 91 toDimacs()92 int toDimacs() const { return sign() ? -var() - 1 : var() + 1; } 93 }; 94 95 const Lit lit_Undef(var_Undef, false); // }- Useful special constants. 96 const Lit lit_Error(var_Undef, true ); // } 97 98 99 100 // Clause -- a simple class for representing a clause: 101 class Clause { 102 unsigned int d_size_learnt; 103 int d_id; 104 int d_pushID; 105 float d_activity; 106 // The derivation of this SAT clause 107 CVC3::Theorem d_theorem; 108 Lit d_data[1]; 109 110 static Clause* s_decision; 111 static Clause* s_theoryImplication; 112 public: 113 // NOTE: This constructor cannot be used directly, 114 // it doesn't allocate enough memory for d_data[]. 115 // 116 // using the hand-made allocator allows to allocate the data[] 117 // like a static array within clause instead of as a pointer to the array. 118 // this shows significant performance improvements Clause(bool learnt,const std::vector<Lit> & ps,CVC3::Theorem theorem,int id,int pushID)119 Clause(bool learnt, const std::vector<Lit>& ps, CVC3::Theorem theorem, 120 int id, int pushID) { 121 d_size_learnt = (ps.size() << 1) | (int)learnt; 122 d_id = id; 123 d_pushID = pushID; 124 d_activity = 0; 125 d_theorem = theorem; 126 for (std::vector<Lit>::size_type i = 0; i < ps.size(); i++) d_data[i] = ps[i]; 127 } 128 129 // -- use this function instead: 130 friend Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id); 131 friend Clause* Lemma_new(const std::vector<Lit>& ps, int id, int pushID); 132 size()133 int size () const { return d_size_learnt >> 1; } learnt()134 bool learnt () const { return d_size_learnt & 1; } 135 Lit operator [] (int i) const { return d_data[i]; } 136 Lit& operator [] (int i) { return d_data[i]; } 137 // intended to be unique id per clause, > 0, or clauseIDNull id()138 int id () const { return d_id; } 139 140 // used with Solver::push/pop: 141 // this is the highest id of all clauses used in the regression / 142 // resolution / creation of this lemma pushID()143 int pushID () const { return d_pushID; } activity()144 float activity () const { 145 DebugAssert(learnt(), "MiniSat::Types:activity: not a lemma"); 146 return d_activity; 147 } setActivity(float activity)148 void setActivity (float activity) { 149 DebugAssert(learnt(), "MiniSat::Types:setActivity: not a lemma"); 150 d_activity = activity; 151 } 152 void toLit (std::vector<Lit>& literals) const; getTheorem()153 CVC3::Theorem getTheorem() const { return d_theorem; }; 154 ClauseIDNull()155 static int ClauseIDNull() { return 0; } 156 157 // special Clause, used to mark that an implication is a decision, id = -1. 158 static Clause* Decision(); 159 // special Clause, used to mark that an implication is a theory implication 160 // and that the explanation has not been retrieved yet, id = -2. 161 static Clause* TheoryImplication(); 162 toString()163 std::string toString() const { 164 if (size() == 0) return ""; 165 166 std::ostringstream buffer; 167 buffer << d_data[0].toString(); 168 for (int j = 1; j < size(); ++j) { 169 buffer << " " << d_data[j].toString(); 170 } 171 return buffer.str(); 172 } 173 contains(Lit l)174 bool contains(Lit l) { 175 for (int i = 0; i < size(); ++i) { 176 if (d_data[i] == l) return true; 177 } 178 return false; 179 } 180 }; 181 182 Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id); 183 Clause* Lemma_new(const std::vector<Lit>& ps, int id, int pushID); 184 185 } 186 187 188 189 //================================================================================================= 190 #endif 191