CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 *\file minisat_types.h 00004 *\brief MiniSat internal types 00005 * 00006 * Author: Alexander Fuchs 00007 * 00008 * Created: Fri Sep 08 11:04:00 2006 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 */ 00019 /*****************************************************************************/ 00020 00021 /***********************************************************************************[SolverTypes.h] 00022 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson 00023 00024 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and 00025 associated documentation files (the "Software"), to deal in the Software without restriction, 00026 including without limitation the rights to use, copy, modify, merge, publish, distribute, 00027 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is 00028 furnished to do so, subject to the following conditions: 00029 00030 The above copyright notice and this permission notice shall be included in all copies or 00031 substantial portions of the Software. 00032 00033 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT 00034 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00035 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, 00036 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT 00037 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00038 **************************************************************************************************/ 00039 00040 #ifndef _cvc3__minisat__types_h_ 00041 #define _cvc3__minisat__types_h_ 00042 00043 //================================================================================================= 00044 // Variables, literals, clause IDs: 00045 00046 #include "minisat_global.h" 00047 #include "theorem.h" 00048 #include <vector> 00049 00050 namespace MiniSat { 00051 00052 // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, 00053 // so that they can be used as array indices. 00054 // CVC additionally requires that N >= 2. 00055 typedef int Var; 00056 const int var_Undef = -1; 00057 00058 00059 class Lit { 00060 int x; 00061 00062 explicit Lit(int index) : x(index) {} // (lit_Undef) 00063 public: 00064 Lit() : x(2*var_Undef) {} // (lit_Undef) 00065 explicit Lit(Var var, bool sgn) : x((var+var) + (int)sgn) {} 00066 Lit operator~ () const { return Lit(x ^ 1); }; 00067 00068 bool sign () const { return x & 1; }; 00069 int var () const { return x >> 1; }; 00070 int index () const { return x; }; 00071 static Lit toLit (int i) { return Lit(i); }; 00072 Lit unsign() const { return Lit(x & ~1); }; 00073 static Lit id (Lit p, bool sgn) { return Lit(p.x ^ (int)sgn); }; 00074 00075 bool operator == (const Lit q) const { return index() == q.index(); }; 00076 bool operator != (const Lit q) const { return !(operator==(q)); }; 00077 // '<' guarantees that p, ~p are adjacent in the ordering.; 00078 bool operator < (const Lit q) const { return index() < q.index(); } 00079 00080 unsigned int hash() const { return (unsigned int)x; } 00081 00082 std::string toString() const { 00083 std::ostringstream buffer; 00084 if (sign()) 00085 buffer << "+"; 00086 else 00087 buffer << "-"; 00088 buffer << var(); 00089 return buffer.str(); 00090 } 00091 00092 int toDimacs() const { return sign() ? -var() - 1 : var() + 1; } 00093 }; 00094 00095 const Lit lit_Undef(var_Undef, false); // }- Useful special constants. 00096 const Lit lit_Error(var_Undef, true ); // } 00097 00098 00099 00100 // Clause -- a simple class for representing a clause: 00101 class Clause { 00102 unsigned int d_size_learnt; 00103 int d_id; 00104 int d_pushID; 00105 float d_activity; 00106 // The derivation of this SAT clause 00107 CVC3::Theorem d_theorem; 00108 Lit d_data[1]; 00109 00110 static Clause* s_decision; 00111 static Clause* s_theoryImplication; 00112 public: 00113 // NOTE: This constructor cannot be used directly, 00114 // it doesn't allocate enough memory for d_data[]. 00115 // 00116 // using the hand-made allocator allows to allocate the data[] 00117 // like a static array within clause instead of as a pointer to the array. 00118 // this shows significant performance improvements 00119 Clause(bool learnt, const std::vector<Lit>& ps, CVC3::Theorem theorem, 00120 int id, int pushID) { 00121 d_size_learnt = (ps.size() << 1) | (int)learnt; 00122 d_id = id; 00123 d_pushID = pushID; 00124 d_activity = 0; 00125 d_theorem = theorem; 00126 for (std::vector<Lit>::size_type i = 0; i < ps.size(); i++) d_data[i] = ps[i]; 00127 } 00128 00129 // -- use this function instead: 00130 friend Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id); 00131 friend Clause* Lemma_new(const std::vector<Lit>& ps, int id, int pushID); 00132 00133 int size () const { return d_size_learnt >> 1; } 00134 bool learnt () const { return d_size_learnt & 1; } 00135 Lit operator [] (int i) const { return d_data[i]; } 00136 Lit& operator [] (int i) { return d_data[i]; } 00137 // intended to be unique id per clause, > 0, or clauseIDNull 00138 int id () const { return d_id; } 00139 00140 // used with Solver::push/pop: 00141 // this is the highest id of all clauses used in the regression / 00142 // resolution / creation of this lemma 00143 int pushID () const { return d_pushID; } 00144 float activity () const { 00145 DebugAssert(learnt(), "MiniSat::Types:activity: not a lemma"); 00146 return d_activity; 00147 } 00148 void setActivity (float activity) { 00149 DebugAssert(learnt(), "MiniSat::Types:setActivity: not a lemma"); 00150 d_activity = activity; 00151 } 00152 void toLit (std::vector<Lit>& literals) const; 00153 CVC3::Theorem getTheorem() const { return d_theorem; }; 00154 00155 static int ClauseIDNull() { return 0; } 00156 00157 // special Clause, used to mark that an implication is a decision, id = -1. 00158 static Clause* Decision(); 00159 // special Clause, used to mark that an implication is a theory implication 00160 // and that the explanation has not been retrieved yet, id = -2. 00161 static Clause* TheoryImplication(); 00162 00163 std::string toString() const { 00164 if (size() == 0) return ""; 00165 00166 std::ostringstream buffer; 00167 buffer << d_data[0].toString(); 00168 for (int j = 1; j < size(); ++j) { 00169 buffer << " " << d_data[j].toString(); 00170 } 00171 return buffer.str(); 00172 } 00173 00174 bool contains(Lit l) { 00175 for (int i = 0; i < size(); ++i) { 00176 if (d_data[i] == l) return true; 00177 } 00178 return false; 00179 } 00180 }; 00181 00182 Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id); 00183 Clause* Lemma_new(const std::vector<Lit>& ps, int id, int pushID); 00184 00185 } 00186 00187 00188 00189 //================================================================================================= 00190 #endif