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