cprover
smt1_prop.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 Revisions: Roberto Bruttomesso, roberto.bruttomesso@unisi.ch
8 
9 \*******************************************************************/
10 
11 #include "smt1_prop.h"
12 
13 #include <cassert>
14 
16  const std::string &benchmark,
17  const std::string &source,
18  const std::string &logic,
19  std::ostream &_out):out(_out)
20 {
21  out << "(benchmark " << benchmark << "\n";
22  out << ":source { " << source << " }" << "\n";
23  out << ":status unknown" << "\n";
24  out << ":logic " << logic << " ; SMT1" << "\n";
25  _no_variables=0;
26 }
27 
29 {
30 }
31 
33 {
34  out << "\n";
35  out << ":formula true" << "\n";
36  out << ") ; benchmark" << "\n";
37 }
38 
40 {
41  out << "\n";
42 
44 
45  out << ":assumption ; land" << "\n";
46  out << " (iff " << smt1_literal(l) << " (and";
47 
48  forall_literals(it, bv)
49  out << " " << smt1_literal(*it);
50 
51  out << "))" << "\n";
52 
53  return l;
54 }
55 
57 {
58  out << "\n";
59 
61 
62  out << ":assumption ; lor" << "\n";
63  out << " (iff " << smt1_literal(l) << " (or";
64 
65  forall_literals(it, bv)
66  out << " " << smt1_literal(*it);
67 
68  out << "))" << "\n";
69 
70  return l;
71 }
72 
74 {
75  if(bv.empty())
76  return const_literal(false);
77  if(bv.size()==1)
78  return bv[0];
79 
80  out << "\n";
81 
83 
84  out << ":assumption ; lxor" << "\n";
85  out << " (iff " << smt1_literal(l) << " (xor";
86 
87  forall_literals(it, bv)
88  out << " " << smt1_literal(*it);
89 
90  out << "))" << "\n";
91 
92  return l;
93 }
94 
96 {
97  if(a==const_literal(true))
98  return b;
99  if(b==const_literal(true))
100  return a;
101  if(a==const_literal(false))
102  return const_literal(false);
103  if(b==const_literal(false))
104  return const_literal(false);
105  if(a==b)
106  return a;
107 
108  out << "\n";
109 
111 
112  out << ":assumption ; land" << "\n";
113  out << " (iff " << smt1_literal(l) << " (and";
114  out << " " << smt1_literal(a);
115  out << " " << smt1_literal(b);
116  out << "))" << "\n";
117 
118  return l;
119 }
120 
122 {
123  if(a==const_literal(false))
124  return b;
125  if(b==const_literal(false))
126  return a;
127  if(a==const_literal(true))
128  return const_literal(true);
129  if(b==const_literal(true))
130  return const_literal(true);
131  if(a==b)
132  return a;
133 
134  out << "\n";
135 
137 
138  out << ":assumption ; lor" << "\n";
139  out << " (iff " << smt1_literal(l) << " (or";
140  out << " " << smt1_literal(a);
141  out << " " << smt1_literal(b);
142  out << "))" << "\n";
143 
144  return l;
145 }
146 
148 {
149  if(a==const_literal(false))
150  return b;
151  if(b==const_literal(false))
152  return a;
153  if(a==const_literal(true))
154  return !b;
155  if(b==const_literal(true))
156  return !a;
157 
158  out << "\n";
159 
161 
162  out << ":assumption ; lxor" << "\n";
163  out << " (iff " << smt1_literal(l) << " (xor";
164  out << " " << smt1_literal(a);
165  out << " " << smt1_literal(b);
166  out << "))" << "\n";
167 
168  return l;
169 }
170 
172 {
173  return !land(a, b);
174 }
175 
177 {
178  return !lor(a, b);
179 }
180 
182 {
183  return !lxor(a, b);
184 }
185 
187 {
188  return lor(!a, b);
189 }
190 
192 {
193  if(a==const_literal(true))
194  return b;
195  if(a==const_literal(false))
196  return c;
197  if(b==c)
198  return b;
199 
200  if(a==const_literal(false))
201  return b;
202  if(b==const_literal(false))
203  return a;
204  if(a==const_literal(true))
205  return !b;
206  if(b==const_literal(true))
207  return !a;
208 
209  out << "\n";
210 
212 
213  out << ":assumption ; lselect" << "\n";
214  out << " (iff " << smt1_literal(l) << "(if_then_else "
215  << smt1_literal(a) << " " << smt1_literal(b) << " "
216  << smt1_literal(c) << ")" << "\n";
217 
218  return l;
219 }
220 
222 {
223  literalt l;
224  l.set(_no_variables, false);
225  _no_variables++;
226 
227  out << ":extrapreds((" << smt1_literal(l) << "))" << "\n";
228 
229  return l;
230 }
231 
232 void smt1_propt::lcnf(const bvt &bv)
233 {
234  out << "\n";
235  out << ":assumption ; lcnf" << "\n";
236  out << " ";
237 
238  if(bv.empty())
239  out << "false ; the empty clause";
240  else if(bv.size()==1)
241  out << smt1_literal(bv.front());
242  else
243  {
244  out << "(or";
245 
246  for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
247  out << " " << smt1_literal(*it);
248 
249  out << ")";
250  }
251 
252  out << "\n";
253 }
254 
256 {
257  if(l==const_literal(false))
258  return "false";
259  else if(l==const_literal(true))
260  return "true";
261 
262  std::string v="B"+std::to_string(l.var_no());
263 
264  if(l.sign())
265  return "(not "+v+")";
266 
267  return v;
268 }
269 
271 {
272  if(literal.is_true())
273  return tvt(true);
274  if(literal.is_false())
275  return tvt(false);
276 
277  unsigned v=literal.var_no();
278  if(v>=assignment.size())
280  tvt r=assignment[v];
281  return literal.sign()?!r:r;
282 }
283 
284 void smt1_propt::set_assignment(literalt literal, bool value)
285 {
286  if(literal.is_true() || literal.is_false())
287  return;
288 
289  unsigned v=literal.var_no();
290  assert(v<assignment.size());
291  assignment[v]=tvt(value);
292 }
293 
295 {
296  return P_ERROR;
297 }
static int8_t r
Definition: irep_hash.h:59
std::vector< tvt > assignment
Definition: smt1_prop.h:78
virtual literalt lnor(literalt a, literalt b)
Definition: smt1_prop.cpp:176
void finalize()
Definition: smt1_prop.cpp:32
virtual void lcnf(const bvt &bv)
Definition: smt1_prop.cpp:232
virtual literalt land(literalt a, literalt b)
Definition: smt1_prop.cpp:95
#define forall_literals(it, bv)
Definition: literal.h:199
virtual literalt lxor(const bvt &bv)
Definition: smt1_prop.cpp:73
virtual literalt new_variable()
Definition: smt1_prop.cpp:221
virtual ~smt1_propt()
Definition: smt1_prop.cpp:28
std::string smt1_literal(literalt l)
Definition: smt1_prop.cpp:255
virtual literalt lor(literalt a, literalt b)
Definition: smt1_prop.cpp:121
virtual literalt limplies(literalt a, literalt b)
Definition: smt1_prop.cpp:186
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: smt1_prop.cpp:191
resultt
Definition: prop.h:94
void set(var_not _l)
Definition: literal.h:92
literalt const_literal(bool value)
Definition: literal.h:187
virtual void set_assignment(literalt a, bool value)
Definition: smt1_prop.cpp:284
virtual literalt lequal(literalt a, literalt b)
Definition: smt1_prop.cpp:181
bool sign() const
Definition: literal.h:87
virtual literalt lnand(literalt a, literalt b)
Definition: smt1_prop.cpp:171
size_t _no_variables
Definition: smt1_prop.h:72
virtual propt::resultt prop_solve()
Definition: smt1_prop.cpp:294
smt1_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, std::ostream &_out)
Definition: smt1_prop.cpp:15
std::vector< literalt > bvt
Definition: literal.h:197
std::ostream & out
Definition: smt1_prop.h:73
virtual tvt l_get(literalt literal) const
Definition: smt1_prop.cpp:270
bool is_false() const
Definition: literal.h:160