cprover
literal.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_PROP_LITERAL_H
11 #define CPROVER_SOLVERS_PROP_LITERAL_H
12 
13 #include <vector>
14 #include <iosfwd>
15 
16 // a pair of a variable number and a sign, encoded as follows:
17 //
18 // sign='false' means positive
19 // sign='true' means negative
20 //
21 // The top bit is used to indicate that the literal is constant
22 // true or false.
23 
24 class literalt
25 {
26 public:
27  // We deliberately don't use size_t here to save some memory
28  // on 64-bit machines; i.e., in practice, we restrict ourselves
29  // to SAT instances with no more than 2^31 variables.
30  typedef unsigned var_not;
31 
32  // constructors
34  {
35  set(unused_var_no(), false);
36  }
37 
39  {
40  set(v, sign);
41  }
42 
43  bool operator==(const literalt other) const
44  {
45  return l==other.l;
46  }
47 
48  bool operator!=(const literalt other) const
49  {
50  return l!=other.l;
51  }
52 
53  // for sets
54  bool operator<(const literalt other) const
55  {
56  return l<other.l;
57  }
58 
59  // negates if 'b' is true
60  literalt operator^(const bool b) const
61  {
62  literalt result(*this);
63  result.l^=(var_not)b;
64  return result;
65  }
66 
67  // negates the literal
69  {
70  literalt result(*this);
71  result.invert();
72  return result;
73  }
74 
75  literalt operator^=(const bool a)
76  {
77  // we use the least significant bit to store the sign
78  l^=(var_not)a;
79  return *this;
80  }
81 
82  var_not var_no() const
83  {
84  return l>>1;
85  }
86 
87  bool sign() const
88  {
89  return l&1;
90  }
91 
92  void set(var_not _l)
93  {
94  l=_l;
95  }
96 
97  void set(var_not v, bool sign)
98  {
99  l=(v<<1)|((var_not)sign);
100  }
101 
102  var_not get() const
103  {
104  return l;
105  }
106 
107  void invert()
108  {
109  l^=(var_not)1;
110  }
111 
112  //
113  // Returns a literal in the dimacs CNF encoding.
114  // A negative integer denotes a negated literal.
115  //
116  int dimacs() const
117  {
118  int result=var_no();
119 
120  if(sign())
121  result=-result;
122 
123  return result;
124  }
125 
126  void from_dimacs(int d)
127  {
128  bool sign=d<0;
129  if(sign)
130  d=-d;
131  set(d, sign);
132  }
133 
134  void clear()
135  {
136  l=0;
137  }
138 
139  void swap(literalt &x)
140  {
141  std::swap(x.l, l);
142  }
143 
144  // constants
145  void make_true()
146  {
147  set(const_var_no(), true);
148  }
149 
150  void make_false()
151  {
152  set(const_var_no(), false);
153  }
154 
155  bool is_true() const
156  {
157  return is_constant() && sign();
158  }
159 
160  bool is_false() const
161  {
162  return is_constant() && !sign();
163  }
164 
165  bool is_constant() const
166  {
167  return var_no()==const_var_no();
168  }
169 
170  static inline var_not const_var_no()
171  {
172  return (var_not(-1)<<1)>>1;
173  }
174 
175  static inline var_not unused_var_no()
176  {
177  return (var_not(-2)<<1)>>1;
178  }
179 
180 protected:
182 };
183 
184 std::ostream &operator << (std::ostream &out, literalt l);
185 
186 // constants
187 inline literalt const_literal(bool value)
188 {
189  return literalt(literalt::const_var_no(), value);
190 }
191 
192 inline literalt neg(literalt a) { return !a; }
193 inline literalt pos(literalt a) { return a; }
194 
195 
196 inline bool is_false (const literalt &l) { return (l.is_false()); }
197 inline bool is_true (const literalt &l) { return (l.is_true()); }
198 
199 // bit-vectors
200 typedef std::vector<literalt> bvt;
201 
202 #define forall_literals(it, bv) \
203  for(bvt::const_iterator it=(bv).begin(), it_end=(bv).end(); \
204  it!=it_end; ++it)
205 
206 #define Forall_literals(it, bv) \
207  for(bvt::iterator it=(bv).begin(); \
208  it!=(bv).end(); ++it)
209 
210 #endif // CPROVER_SOLVERS_PROP_LITERAL_H
literalt::operator<
bool operator<(const literalt other) const
Definition: literal.h:54
literalt::var_not
unsigned var_not
Definition: literal.h:30
literalt::literalt
literalt(var_not v, bool sign)
Definition: literal.h:38
literalt::operator==
bool operator==(const literalt other) const
Definition: literal.h:43
operator<<
std::ostream & operator<<(std::ostream &out, literalt l)
Definition: literal.cpp:16
pos
literalt pos(literalt a)
Definition: literal.h:193
bvt
std::vector< literalt > bvt
Definition: literal.h:200
literalt::const_var_no
static var_not const_var_no()
Definition: literal.h:170
literalt::dimacs
int dimacs() const
Definition: literal.h:116
literalt::make_false
void make_false()
Definition: literal.h:150
literalt::var_no
var_not var_no() const
Definition: literal.h:82
literalt::swap
void swap(literalt &x)
Definition: literal.h:139
literalt::unused_var_no
static var_not unused_var_no()
Definition: literal.h:175
literalt::invert
void invert()
Definition: literal.h:107
is_false
bool is_false(const literalt &l)
Definition: literal.h:196
literalt::is_true
bool is_true() const
Definition: literal.h:155
literalt::make_true
void make_true()
Definition: literal.h:145
literalt::is_false
bool is_false() const
Definition: literal.h:160
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
literalt::get
var_not get() const
Definition: literal.h:102
literalt::operator^
literalt operator^(const bool b) const
Definition: literal.h:60
literalt::sign
bool sign() const
Definition: literal.h:87
literalt::set
void set(var_not v, bool sign)
Definition: literal.h:97
literalt::operator!=
bool operator!=(const literalt other) const
Definition: literal.h:48
literalt::set
void set(var_not _l)
Definition: literal.h:92
literalt
Definition: literal.h:24
literalt::operator!
literalt operator!() const
Definition: literal.h:68
literalt::from_dimacs
void from_dimacs(int d)
Definition: literal.h:126
literalt::is_constant
bool is_constant() const
Definition: literal.h:165
is_true
bool is_true(const literalt &l)
Definition: literal.h:197
neg
literalt neg(literalt a)
Definition: literal.h:192
literalt::clear
void clear()
Definition: literal.h:134
literalt::l
var_not l
Definition: literal.h:181
literalt::operator^=
literalt operator^=(const bool a)
Definition: literal.h:75
literalt::literalt
literalt()
Definition: literal.h:33