CVC3

minisat_types.h

Go to the documentation of this file.
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