CVC3  2.4.1
minisat_types.h
Go to the documentation of this file.
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 
62  explicit Lit(int index) : x(index) {} // (lit_Undef)
63  public:
64  Lit() : x(2*var_Undef) {} // (lit_Undef)
65  explicit Lit(Var var, bool sgn) : x((var+var) + (int)sgn) {}
66  Lit operator~ () const { return Lit(x ^ 1); };
67 
68  bool sign () const { return x & 1; };
69  int var () const { return x >> 1; };
70  int index () const { return x; };
71  static Lit toLit (int i) { return Lit(i); };
72  Lit unsign() const { return Lit(x & ~1); };
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 
80  unsigned int hash() const { return (unsigned int)x; }
81 
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 
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
109 
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
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 
133  int size () const { return d_size_learnt >> 1; }
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
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
143  int pushID () const { return d_pushID; }
144  float activity () const {
145  DebugAssert(learnt(), "MiniSat::Types:activity: not a lemma");
146  return d_activity;
147  }
148  void setActivity (float activity) {
149  DebugAssert(learnt(), "MiniSat::Types:setActivity: not a lemma");
151  }
152  void toLit (std::vector<Lit>& literals) const;
153  CVC3::Theorem getTheorem() const { return d_theorem; };
154 
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 
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 
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
bool learnt() const
std::string toString() const
Definition: minisat_types.h:82
Lit unsign() const
Definition: minisat_types.h:72
std::string toString() const
const Lit lit_Undef(var_Undef, false)
bool operator!=(const Lit q) const
Definition: minisat_types.h:76
void toLit(std::vector< Lit > &literals) const
MiniSat global functions.
int size() const
bool contains(Lit l)
#define DebugAssert(cond, str)
Definition: debug.h:408
Clause * Lemma_new(const vector< Lit > &ps, int id, int pushID)
static Clause * s_theoryImplication
int var() const
Definition: minisat_types.h:69
friend Clause * Clause_new(const std::vector< Lit > &ps, CVC3::Theorem theorem, int id)
CVC3::Theorem getTheorem() const
const int var_Undef
Definition: minisat_types.h:56
Clause * Clause_new(const vector< Lit > &ps, CVC3::Theorem theorem, int id)
bool operator==(const Lit q) const
Definition: minisat_types.h:75
static Lit id(Lit p, bool sgn)
Definition: minisat_types.h:73
float activity() const
int index() const
Definition: minisat_types.h:70
const Lit lit_Error(var_Undef, true)
static Clause * TheoryImplication()
static Clause * s_decision
int toDimacs() const
Definition: minisat_types.h:92
unsigned int hash() const
Definition: minisat_types.h:80
int pushID() const
size_t size_type
Definition: hash_table.h:75
Clause(bool learnt, const std::vector< Lit > &ps, CVC3::Theorem theorem, int id, int pushID)
int id() const
static Clause * Decision()
Lit(Var var, bool sgn)
Definition: minisat_types.h:65
CVC3::Theorem d_theorem
friend Clause * Lemma_new(const std::vector< Lit > &ps, int id, int pushID)
Lit(int index)
Definition: minisat_types.h:62
bool operator<(const Lit q) const
Definition: minisat_types.h:78
bool sign() const
Definition: minisat_types.h:68
Lit operator[](int i) const
void setActivity(float activity)
unsigned int d_size_learnt
static Lit toLit(int i)
Definition: minisat_types.h:71
static int ClauseIDNull()
Lit operator~() const
Definition: minisat_types.h:66