cprover
smt2_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 "smt2_prop.h"
10 
11 #include <cassert>
12 
14  const std::string &benchmark,
15  const std::string &source,
16  const std::string &logic,
17  bool _core_enabled,
18  std::ostream &_out):
19  out(_out),
20  core_enabled(_core_enabled)
21 {
22  out << "; SMT 2" << "\n";
23 
24  out << "(set-info :source \"" << source << "\")" << "\n";
25  out << "(set-option :produce-models true)" << "\n";
26 
27  if(core_enabled)
28  {
29  out << "(set-option :produce-unsat-cores true)" << "\n";
30  }
31 
32  out << "(set-logic " << logic << ")" << "\n";
33 
34  _no_variables=0;
35 }
36 
38 {
39 }
40 
42 {
43  out << "\n";
44  out << "(check-sat)" << "\n";
45  out << "\n";
46 
47  for(smt2_identifierst::const_iterator
48  it=smt2_identifiers.begin();
49  it!=smt2_identifiers.end();
50  it++)
51  out << "(get-value (" << *it << "))" << "\n";
52 
53  out << "\n";
54 
55  if(core_enabled)
56  out << "(get-unsat-core)" << "\n";
57 
58  out << "; end of SMT2 file" << "\n";
59 }
60 
62 {
63  out << "\n";
64 
66 
67  out << "; land" << "\n";
68  out << " (and";
69 
70  forall_literals(it, bv)
71  out << " " << smt2_literal(*it);
72 
73  out << "))" << "\n";
74 
75  return l;
76 }
77 
79 {
80  out << "\n";
81 
83 
84  out << "; lor" << "\n";
85  out << " (or";
86 
87  forall_literals(it, bv)
88  out << " " << smt2_literal(*it);
89 
90  out << "))" << "\n";
91 
92  return l;
93 }
94 
96 {
97  if(bv.empty())
98  return const_literal(false);
99  if(bv.size()==1)
100  return bv[0];
101 
102  out << "\n";
103 
105 
106  out << "; lxor" << "\n";
107  out << " (xor";
108 
109  forall_literals(it, bv)
110  out << " " << smt2_literal(*it);
111 
112  out << "))" << "\n";
113 
114  return l;
115 }
116 
118 {
119  if(a==const_literal(true))
120  return b;
121  if(b==const_literal(true))
122  return a;
123  if(a==const_literal(false))
124  return const_literal(false);
125  if(b==const_literal(false))
126  return const_literal(false);
127  if(a==b)
128  return a;
129 
130  out << "\n";
131 
133 
134  out << "; land" << "\n";
135  out << " (and";
136  out << " " << smt2_literal(a);
137  out << " " << smt2_literal(b);
138  out << "))" << "\n";
139 
140  return l;
141 }
142 
144 {
145  if(a==const_literal(false))
146  return b;
147  if(b==const_literal(false))
148  return a;
149  if(a==const_literal(true))
150  return const_literal(true);
151  if(b==const_literal(true))
152  return const_literal(true);
153  if(a==b)
154  return a;
155 
156  out << "\n";
157 
159 
160  out << "; lor" << "\n";
161  out << " (or";
162  out << " " << smt2_literal(a);
163  out << " " << smt2_literal(b);
164  out << "))" << "\n";
165 
166  return l;
167 }
168 
170 {
171  if(a==const_literal(false))
172  return b;
173  if(b==const_literal(false))
174  return a;
175  if(a==const_literal(true))
176  return !b;
177  if(b==const_literal(true))
178  return !a;
179 
180  out << "\n";
181 
183 
184  out << "; lxor" << "\n";
185  out << " (xor";
186  out << " " << smt2_literal(a);
187  out << " " << smt2_literal(b);
188  out << "))" << "\n";
189 
190  return l;
191 }
192 
194 {
195  return !land(a, b);
196 }
197 
199 {
200  return !lor(a, b);
201 }
202 
204 {
205  return !lxor(a, b);
206 }
207 
209 {
210  return lor(!a, b);
211 }
212 
214 {
215  if(a==const_literal(true))
216  return b;
217  if(a==const_literal(false))
218  return c;
219  if(b==c)
220  return b;
221 
222  if(a==const_literal(false))
223  return b;
224  if(b==const_literal(false))
225  return a;
226  if(a==const_literal(true))
227  return !b;
228  if(b==const_literal(true))
229  return !a;
230 
231  out << "\n";
232 
234 
235  out << "; lselect" << "\n";
236  out << " (if_then_else "
237  << smt2_literal(a) << " " << smt2_literal(b) << " "
238  << smt2_literal(c) << "))" << "\n";
239 
240  return l;
241 }
242 
244 {
245  literalt l;
246  l.set(_no_variables, false);
247  _no_variables++;
248 
249  out << "(declare-fun " << smt2_literal(l) << " () Bool)" << "\n";
250 
251  return l;
252 }
253 
255 {
256  literalt l;
257  l.set(_no_variables, false);
258  _no_variables++;
259 
260  out << "(define-fun " << smt2_literal(l) << " () Bool ";
261  // The command is continued elsewhere, and the
262  // closing parenthesis is missing!
263 
264  return l;
265 }
266 
267 void smt2_propt::lcnf(const bvt &bv)
268 {
269  out << "\n";
270  out << "(assert ; lcnf" << "\n";
271  out << " ";
272 
273  if(bv.empty())
274  out << "false";
275  else if(bv.size()==1)
276  out << smt2_literal(bv.front());
277  else
278  {
279  out << "(or";
280 
281  for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
282  out << " " << smt2_literal(*it);
283 
284  out << ")";
285  }
286 
287  out << ")" << "\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  std::string v="B"+std::to_string(l.var_no());
298 
299  smt2_identifiers.insert(v);
300 
301  if(l.sign())
302  return "(not "+v+")";
303 
304  return v;
305 }
306 
308 {
309  if(literal.is_true())
310  return tvt(true);
311  if(literal.is_false())
312  return tvt(false);
313 
314  unsigned v=literal.var_no();
315  if(v>=assignment.size())
317  tvt r=assignment[v];
318  return literal.sign()?!r:r;
319 }
320 
321 void smt2_propt::set_assignment(literalt literal, bool value)
322 {
323  if(literal.is_true() || literal.is_false())
324  return;
325 
326  unsigned v=literal.var_no();
327  assert(v<assignment.size());
328  assignment[v]=tvt(value);
329 }
330 
332 {
333  return P_ERROR;
334 }
virtual ~smt2_propt()
Definition: smt2_prop.cpp:37
virtual literalt lselect(literalt a, literalt b, literalt c)
Definition: smt2_prop.cpp:213
static int8_t r
Definition: irep_hash.h:59
virtual literalt lxor(const bvt &bv)
Definition: smt2_prop.cpp:95
virtual literalt land(literalt a, literalt b)
Definition: smt2_prop.cpp:117
virtual void lcnf(const bvt &bv)
Definition: smt2_prop.cpp:267
virtual literalt limplies(literalt a, literalt b)
Definition: smt2_prop.cpp:208
virtual literalt lequal(literalt a, literalt b)
Definition: smt2_prop.cpp:203
virtual propt::resultt prop_solve()
Definition: smt2_prop.cpp:331
smt2_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, bool _core_enabled, std::ostream &_out)
Definition: smt2_prop.cpp:13
#define forall_literals(it, bv)
Definition: literal.h:199
smt2_identifierst smt2_identifiers
Definition: smt2_prop.h:85
std::string smt2_literal(literalt l)
Definition: smt2_prop.cpp:290
void finalize()
Definition: smt2_prop.cpp:41
virtual tvt l_get(literalt literal) const
Definition: smt2_prop.cpp:307
bool is_true() const
Definition: literal.h:155
virtual literalt lor(literalt a, literalt b)
Definition: smt2_prop.cpp:143
virtual literalt lnand(literalt a, literalt b)
Definition: smt2_prop.cpp:193
Definition: threeval.h: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 literalt lnor(literalt a, literalt b)
Definition: smt2_prop.cpp:198
size_t _no_variables
Definition: smt2_prop.h:74
literalt define_new_variable()
Definition: smt2_prop.cpp:254
literalt const_literal(bool value)
Definition: literal.h:187
virtual void set_assignment(literalt a, bool value)
Definition: smt2_prop.cpp:321
bool sign() const
Definition: literal.h:87
bool core_enabled
Definition: smt2_prop.h:87
std::vector< tvt > assignment
Definition: smt2_prop.h:80
virtual literalt new_variable()
Definition: smt2_prop.cpp:243
std::vector< literalt > bvt
Definition: literal.h:197
std::ostream & out
Definition: smt2_prop.h:75
bool is_false() const
Definition: literal.h:160