cprover
cvc_prop.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "cvc_prop.h"
10 
11 #include <cassert>
12 #include <set>
13 
14 explicit cvc_propt::cvc_propt(std::ostream &_out):out(_out)
15 {
16  _no_variables=0;
17 }
18 
20 {
21 }
22 
24 {
25  out << "%% land\n";
26  out << "ASSERT (" << cvc_literal(a) << " AND "
27  << cvc_literal(b) << ") <=> " << cvc_literal(o)
28  << ";\n\n";
29 }
30 
32 {
33  out << "%% lor\n";
34  out << "ASSERT (" << cvc_literal(a) << " OR "
35  << cvc_literal(b) << ") <=> " << cvc_literal(o)
36  << ";\n\n";
37 }
38 
40 {
41  out << "%% lxor\n";
42  out << "ASSERT (" << cvc_literal(a) << " XOR "
43  << cvc_literal(b) << ") <=> " << cvc_literal(o)
44  << ";\n\n";
45 }
46 
48 {
49  out << "%% lnand\n";
50  out << "ASSERT (NOT (" << cvc_literal(a) << " AND "
51  << cvc_literal(b) << ")) <=> " << cvc_literal(o)
52  << ";\n\n";
53 }
54 
56 {
57  out << "%% lnor\n";
58  out << "ASSERT (NOT (" << cvc_literal(a) << " OR "
59  << cvc_literal(b) << ")) <=> " << cvc_literal(o)
60  << ";\n\n";
61 }
62 
64 {
65  out << "%% lequal\n";
66  out << "ASSERT (" << cvc_literal(a) << " <=> "
67  << cvc_literal(b) << ") <=> " << cvc_literal(o)
68  << ";\n\n";
69 }
70 
72 {
73  out << "%% limplies\n";
74  out << "ASSERT (" << cvc_literal(a) << " => "
75  << cvc_literal(b) << ") <=> " << cvc_literal(o)
76  << ";\n\n";
77 }
78 
80 {
81  out << "%% land\n";
82 
83  literalt literal=def_cvc_literal();
84 
85  forall_literals(it, bv)
86  {
87  if(it!=bv.begin())
88  out << " AND ";
89  out << cvc_literal(*it);
90  }
91 
92  out << ";\n\n";
93 
94  return literal;
95 }
96 
98 {
99  out << "%% lor\n";
100 
101  literalt literal=def_cvc_literal();
102 
103  forall_literals(it, bv)
104  {
105  if(it!=bv.begin())
106  out << " OR ";
107  out << cvc_literal(*it);
108  }
109 
110  out << ";\n\n";
111 
112  return literal;
113 }
114 
116 {
117  if(bv.empty())
118  return const_literal(false);
119  if(bv.size()==1)
120  return bv[0];
121  if(bv.size()==2)
122  return lxor(bv[0], bv[1]);
123 
124  literalt literal=const_literal(false);
125 
126  forall_literals(it, bv)
127  literal=lxor(*it, literal);
128 
129  return literal;
130 }
131 
133 {
134  if(a==const_literal(true))
135  return b;
136  if(b==const_literal(true))
137  return a;
138  if(a==const_literal(false))
139  return const_literal(false);
140  if(b==const_literal(false))
141  return const_literal(false);
142  if(a==b)
143  return a;
144 
145  out << "%% land\n";
146 
148 
149  out << cvc_literal(a) << " AND " << cvc_literal(b) << ";\n\n";
150 
151  return o;
152 }
153 
155 {
156  if(a==const_literal(false))
157  return b;
158  if(b==const_literal(false))
159  return a;
160  if(a==const_literal(true))
161  return const_literal(true);
162  if(b==const_literal(true))
163  return const_literal(true);
164  if(a==b)
165  return a;
166 
167  out << "%% lor\n";
168 
170 
171  out << cvc_literal(a) << " OR " << cvc_literal(b) << ";\n\n";
172 
173  return o;
174 }
175 
177 {
178  if(a==const_literal(false))
179  return b;
180  if(b==const_literal(false))
181  return a;
182  if(a==const_literal(true))
183  return !b;
184  if(b==const_literal(true))
185  return !a;
186 
187  out << "%% lxor\n";
188 
190 
191  out << cvc_literal(a) << " XOR " << cvc_literal(b) << ";\n\n";
192 
193  return o;
194 }
195 
197 {
198  return !land(a, b);
199 }
200 
202 {
203  return !lor(a, b);
204 }
205 
207 {
208  return !lxor(a, b);
209 }
210 
212 {
213  return lor(!a, b);
214 }
215 
217 {
218  if(a==const_literal(true))
219  return b;
220  if(a==const_literal(false))
221  return c;
222  if(b==c)
223  return b;
224 
225  out << "%% lselect\n";
226 
228 
229  out << "IF " << cvc_literal(a) << " THEN "
230  << cvc_literal(b) << " ELSE "
231  << cvc_literal(c) << " ENDIF;\n\n";
232 
233  return o;
234 }
235 
237 {
238  out << "l" << _no_variables << ": BOOLEAN;\n";
239  literalt l;
240  l.set(_no_variables, false);
241  _no_variables++;
242  return l;
243 }
244 
246 {
247  out << "l" << _no_variables << ": BOOLEAN = ";
248  literalt l;
249  l.set(_no_variables, false);
250  _no_variables++;
251  return l;
252 }
253 
254 void cvc_propt::lcnf(const bvt &bv)
255 {
256  if(bv.empty())
257  return;
258  bvt new_bv;
259 
260  std::set<literalt> s;
261 
262  new_bv.reserve(bv.size());
263 
264  for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
265  {
266  if(s.insert(*it).second)
267  new_bv.push_back(*it);
268 
269  if(s.find(!*it)!=s.end())
270  return; // clause satisfied
271 
272  assert(it->var_no()<_no_variables);
273  }
274 
275  assert(!new_bv.empty());
276 
277  out << "%% lcnf\n";
278  out << "ASSERT ";
279 
280  for(bvt::const_iterator it=new_bv.begin(); it!=new_bv.end(); it++)
281  {
282  if(it!=new_bv.begin())
283  out << " OR ";
284  out << cvc_literal(*it);
285  }
286 
287  out << ";\n\n";
288 }
289 
291 {
292  if(l==const_literal(false))
293  return "FALSE";
294  else if(l==const_literal(true))
295  return "TRUE";
296 
297  if(l.sign())
298  return "(NOT l"+std::to_string(l.var_no())+")";
299 
300  return "l"+std::to_string(l.var_no());
301 }
302 
304 {
305  out << "QUERY FALSE;\n";
306  return P_ERROR;
307 }
unsigned _no_variables
Definition: cvc_prop.h:79
virtual void limplies(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:71
virtual void lor(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:31
#define forall_literals(it, bv)
Definition: literal.h:199
virtual void lnor(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:55
std::ostream & out
Definition: cvc_prop.h:80
virtual void lxor(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:39
virtual ~cvc_propt()
Definition: cvc_prop.cpp:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
void set(var_not _l)
Definition: literal.h:92
virtual void land(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:23
literalt const_literal(bool value)
Definition: literal.h:187
cvc_propt(std::ostream &_out)
Definition: cvc_prop.cpp:14
virtual void lcnf(const bvt &bv)
Definition: cvc_prop.cpp:254
literalt def_cvc_literal()
Definition: cvc_prop.cpp:245
std::string cvc_literal(literalt l)
Definition: cvc_prop.cpp:290
virtual void lequal(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:63
bool sign() const
Definition: literal.h:87
virtual literalt new_variable()
Definition: cvc_prop.cpp:236
virtual propt::resultt prop_solve()
Definition: cvc_prop.cpp:303
virtual void lnand(literalt a, literalt b, literalt o)
Definition: cvc_prop.cpp:47
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: cvc_prop.cpp:216
std::vector< literalt > bvt
Definition: literal.h:197