cprover
smt1_dec.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 "smt1_dec.h"
10 
11 #include <cstdlib>
12 
13 #if defined(__linux__) || \
14  defined(__FreeBSD_kernel__) || \
15  defined(__GNU__) || \
16  defined(__unix__) || \
17  defined(__CYGWIN__) || \
18  defined(__MACH__)
19 #include <unistd.h>
20 #endif
21 
22 #include <util/std_expr.h>
23 #include <util/std_types.h>
24 #include <util/tempfile.h>
25 #include <util/arith_tools.h>
26 #include <util/string2int.h>
27 #include <util/prefix.h>
28 
30 {
31  return "SMT1 "+logic+" using "+
32  (solver==solvert::GENERIC?"Generic":
33  solver==solvert::BOOLECTOR?"Boolector":
34  solver==solvert::CVC3?"CVC3":
35  solver==solvert::CVC4?"CVC3":
36  solver==solvert::MATHSAT?"MathSAT":
37  solver==solvert::OPENSMT?"OpenSMT":
38  solver==solvert::YICES?"Yices":
39  solver==solvert::Z3?"Z3":
40  "(unknown)");
41 }
42 
44 {
45  temp_out_filename=get_temporary_file("smt1_dec_out_", "");
46 
47  temp_out.open(
48  temp_out_filename.c_str(),
49  std::ios_base::out | std::ios_base::trunc);
50 }
51 
53 {
54  temp_out.close();
55 
56  if(temp_out_filename!="")
57  unlink(temp_out_filename.c_str());
58 
59  if(temp_result_filename!="")
60  unlink(temp_result_filename.c_str());
61 }
62 
64 {
65  // SMT1 is really not incremental
66  assert(!dec_solve_was_called);
68 
69  // this closes the SMT benchmark
70  write_footer();
71  temp_out.close();
72 
74  get_temporary_file("smt1_dec_result_", "");
75 
76  std::string command;
77 
78  switch(solver)
79  {
80  case solvert::BOOLECTOR:
81  // -rwl0 disables rewriting, which makes things slower,
82  // but in return values for arrays appear
83  // command = "boolector -rwl0 --smt "
84  // Removed as not necessarily needed on newer versions
85  command = "boolector --smt "
87  + " --model --output "
89  break;
90 
91  case solvert::CVC3:
92  command = "cvc3 +model -lang smtlib -output-lang smtlib "
94  + " > "
96  break;
97 
98  case solvert::CVC4:
99  command = "cvc4 -L smt1 "
101  + " > "
103  break;
104 
105  case solvert::MATHSAT:
106  command = "mathsat -model -input=smt"
107  " < "+temp_out_filename
108  + " > "+temp_result_filename;
109  break;
110 
111  case solvert::OPENSMT:
112  command = "opensmt "
114  + " > "
116  break;
117 
118  case solvert::YICES:
119  // command = "yices -smt -e " // Calling convention for older versions
120  command = "yices-smt --full-model " // Calling for 2.2.1
122  + " > "
124  break;
125 
126  case solvert::Z3:
127  command = "z3 -smt "
129  + " > "
131  break;
132 
133  default:
134  assert(false);
135  }
136 
137  #if defined(__linux__) || defined(__APPLE__)
138  command+=" 2>&1";
139  #endif
140 
141  int res=system(command.c_str());
142  if(res<0)
143  {
144  error() << "error running SMT1 solver" << eom;
146  }
147 
148  std::ifstream in(temp_result_filename.c_str());
149 
150  switch(solver)
151  {
152  case solvert::BOOLECTOR:
153  return read_result_boolector(in);
154 
155  case solvert::CVC3:
156  return read_result_cvc3(in);
157 
158  case solvert::CVC4:
159  error() << "no support for CVC4 with SMT1, use SMT2 instead" << eom;
161 
162  case solvert::MATHSAT:
163  return read_result_mathsat(in);
164 
165  case solvert::OPENSMT:
166  return read_result_opensmt(in);
167 
168  case solvert::YICES:
169  return read_result_yices(in);
170 
171  case solvert::Z3:
172  return read_result_z3(in);
173 
174  case solvert::GENERIC:
175  default:
176  error() << "Generic solver can't solve" << eom;
178  }
179 }
180 
183 {
184  std::string line;
185 
186  std::getline(in, line);
187 
188  if(line=="sat")
189  {
190  boolean_assignment.clear();
192 
193  typedef std::unordered_map<std::string, valuet, string_hash> valuest;
194  valuest values;
195 
196  while(std::getline(in, line))
197  {
198  std::size_t pos=line.find(' ');
199  if(pos!=std::string::npos && pos!=0)
200  {
201  std::string id=std::string(line, 0, pos);
202  std::string value=std::string(line, pos+1, std::string::npos);
203 
204  // Boolector offers array values as follows:
205  //
206  // ID[INDEX] VALUE
207  //
208  // There may be more than one line per ID
209 
210  if(id!="" && id[id.size()-1]==']') // array?
211  {
212  std::size_t pos2=id.find('[');
213 
214  if(pos2!=std::string::npos)
215  {
216  std::string new_id=std::string(id, 0, pos2);
217  std::string index=std::string(id, pos2+1, id.size()-pos2-2);
218  values[new_id].index_value_map[index]=value;
219  }
220  }
221  else
222  values[id].value=value;
223  }
224  }
225 
226  // Theory variables
227 
228  for(identifier_mapt::iterator
229  it=identifier_map.begin();
230  it!=identifier_map.end();
231  it++)
232  {
233  it->second.value.make_nil();
234  std::string conv_id=convert_identifier(it->first);
235  const valuet &v=values[conv_id];
236 
237  for(valuet::index_value_mapt::const_iterator
238  i_it=v.index_value_map.begin(); i_it!=v.index_value_map.end(); i_it++)
239  set_value(it->second, i_it->first, i_it->second);
240 
241  if(v.value!="")
242  set_value(it->second, "", v.value);
243  }
244 
245  // Booleans
246 
247  for(unsigned v=0; v<no_boolean_variables; v++)
248  {
249  std::string value=values["B"+std::to_string(v)].value;
250  if(value=="")
251  continue;
252  boolean_assignment[v]=(value=="1");
253  }
254 
255  return resultt::D_SATISFIABLE;
256  }
257  else if(line=="unsat")
259  else
260  error() << "Unexpected result from SMT-Solver: " << line << eom;
261 
262  return resultt::D_ERROR;
263 }
264 
266 {
267  return resultt::D_ERROR;
268 }
269 
271 {
272  std::string line;
273 
274  while(std::getline(in, line))
275  {
276  if(line=="sat")
277  {
278  // fixme: read values
279  return resultt::D_SATISFIABLE;
280  }
281  else if(line=="unsat")
283  }
284 
285  error() << "Unexpected result from SMT-Solver" << eom;
286 
287  return resultt::D_ERROR;
288 }
289 
290 std::string smt1_dect::mathsat_value(const std::string &src)
291 {
292  std::size_t pos=src.find('[');
293 
294  if(std::string(src, 0, 2)=="bv" &&
295  pos!=std::string::npos &&
296  src[src.size()-1]==']')
297  {
298  unsigned width=
299  safe_string2unsigned(std::string(src, pos+1, src.size()-pos-2));
300  mp_integer i=string2integer(std::string(src, 2, pos-2));
301  return integer2binary(i, width);
302  }
303 
304  return "";
305 }
306 
308 {
309  std::string line;
311 
312  boolean_assignment.clear();
314 
315  typedef std::unordered_map<std::string, valuet, string_hash> valuest;
316  valuest values;
317 
318  while(std::getline(in, line))
319  {
320  if(line=="sat")
322  else if(line=="unsat")
324  else if(line.size()>=1 && line[0]=='(')
325  {
326  // (iff B0 true)
327  // (= c_h39__h39___CPROVER_malloc_size_h39_35_h39_1 bv0[64])
328  // (= (select __h64_0 bv0[32]) bv5[8])
329  std::size_t pos1=line.find(' ');
330  std::size_t pos2=line.rfind(' ');
331  if(pos1!=std::string::npos &&
332  pos2!=std::string::npos &&
333  pos1!=pos2)
334  {
335  std::string id=std::string(line, pos1+1, pos2-pos1-1);
336  std::string value=std::string(line, pos2+1, line.size()-pos2-2);
337 
338  if(has_prefix(id, "(select "))
339  {
340  #if 0
341  std::size_t pos3=id.rfind(' ');
342  std::string index=std::string(pos3+1, id.size()-pos3-1);
343  id=std::string(id, 8, pos3-8);
344  #endif
345  }
346  else
347  values[id].value=value;
348  }
349  }
350  }
351 
352  for(identifier_mapt::iterator
353  it=identifier_map.begin();
354  it!=identifier_map.end();
355  it++)
356  {
357  it->second.value.make_nil();
358  std::string conv_id=convert_identifier(it->first);
359  std::string value=mathsat_value(values[conv_id].value);
360 
361  if(value!="")
362  set_value(it->second, "", value);
363  }
364 
365  // Booleans
366  for(unsigned v=0; v<no_boolean_variables; v++)
367  {
368  std::string value=values["B"+std::to_string(v)].value;
369  if(value=="")
370  continue;
371  boolean_assignment[v]=(value=="true");
372  }
373 
374  return res;
375 }
376 
378 {
379  std::string line;
381 
382  boolean_assignment.clear();
384 
385  typedef std::unordered_map<std::string, std::string, string_hash> valuest;
386  valuest values;
387 
388  while(std::getline(in, line))
389  {
390  if(line=="sat")
392  else if(line=="unsat")
394  else
395  {
396  std::size_t pos=line.find(" -> ");
397  if(pos!=std::string::npos)
398  values[std::string(line, 0, pos)]=
399  std::string(line, pos+4, std::string::npos);
400  }
401  }
402 
403  for(identifier_mapt::iterator
404  it=identifier_map.begin();
405  it!=identifier_map.end();
406  it++)
407  {
408  it->second.value.make_nil();
409  std::string conv_id=convert_identifier(it->first);
410  std::string value=values[conv_id];
411  if(value=="")
412  continue;
413 
414  exprt e;
415  if(string_to_expr_z3(it->second.type, value, e))
416  it->second.value=e;
417  else
418  set_value(it->second, "", value);
419  }
420 
421  // Booleans
422  for(unsigned v=0; v<no_boolean_variables; v++)
423  {
424  std::string value=values["B"+std::to_string(v)];
425  if(value=="")
426  continue;
427  boolean_assignment[v]=(value=="true");
428  }
429 
430  return res;
431 }
432 
434  const typet &type,
435  const std::string &value,
436  exprt &e) const
437 {
438  if(value.substr(0, 2)=="bv")
439  {
440  std::string v=value.substr(2, value.find('[')-2);
441  size_t p = value.find('[')+1;
442  std::string w=value.substr(p, value.find(']')-p);
443 
444  std::string binary=integer2binary(string2integer(v, 10),
446 
447  if(type.id()==ID_struct)
448  {
449  e=binary2struct(to_struct_type(type), binary);
450  }
451  else if(type.id()==ID_union)
452  {
453  e=binary2union(to_union_type(type), binary);
454  }
455  else
456  {
457  constant_exprt c(type);
458  c.set_value(binary);
459  e=c;
460  }
461 
462  return true;
463  }
464  else if(value.substr(0, 6)=="(const") // const arrays
465  {
466  std::string av = value.substr(7, value.length()-8);
467 
468  exprt ae;
469  if(!string_to_expr_z3(type.subtype(), av, ae))
470  return false;
471 
472  array_of_exprt ao;
473  ao.type() = typet(ID_array);
474  ao.type().subtype()=ae.type();
475  ao.what() = ae;
476 
477  e = ao;
478 
479  return true;
480  }
481  else if(value.substr(0, 6)=="(store")
482  {
483  size_t p1=value.rfind(' ')+1;
484  size_t p2=value.rfind(' ', p1-2)+1;
485 
486  assert(p1!=std::string::npos && p2!=std::string::npos);
487 
488  std::string elem = value.substr(p1, value.size()-p1-1);
489  std::string inx = value.substr(p2, p1-p2-1);
490  std::string array = value.substr(7, p2-8);
491 
492  exprt old;
493  if(!string_to_expr_z3(type, array, old))
494  return false;
495 
496  exprt where;
497  if(!string_to_expr_z3(array_index_type(), inx, where))
498  return false;
499 
500  exprt new_val;
501  if(!string_to_expr_z3(type.subtype(), elem, new_val))
502  return false;
503 
504  e = with_exprt(old, where, new_val);
505 
506  return true;
507  }
508  else if(value=="false")
509  {
510  e = false_exprt();
511  return true;
512  }
513  else if(value=="true")
514  {
515  e = true_exprt();
516  return true;
517  }
518  else if(value.substr(0, 8)=="array_of")
519  {
520  // We assume that array_of has only concrete arguments...
521  irep_idt id(value);
522  array_of_mapt::const_iterator fit=array_of_map.begin();
523  while(fit!=array_of_map.end() && fit->second!=id) fit++;
524 
525  if(fit==array_of_map.end())
526  return false;
527 
528  e = fit->first;
529 
530  return true;
531  }
532  else if(type.id()==ID_rational)
533  {
535  result.type()=rational_typet();
536 
537  if(value.substr(0, 4)=="val!")
538  result.set_value(value.substr(4));
539  else
540  result.set_value(value);
541 
542  e = result;
543  return true;
544  }
545 
546  return false;
547 }
548 
550 {
551  std::string line;
553 
554  boolean_assignment.clear();
556 
557  typedef std::unordered_map<std::string, std::string, string_hash> valuest;
558  valuest values;
559 
560  while(std::getline(in, line))
561  {
562  if(line=="sat")
564  else if(line=="unsat")
566  else if(line.find("Current scope level")!=std::string::npos ||
567  line.find("Variable Assignment")!=std::string::npos)
568  {
569  // ignore
570  }
571  else
572  {
573  assert(line.substr(0, 13)==" :assumption");
574  std::size_t pos=line.find('(');
575 
576  if(pos!=std::string::npos)
577  {
578  std::string var;
579  std::string val;
580 
581  if(line[pos+1]=='=')
582  {
583  std::string ops = line.substr(pos+3, line.length()-pos-4);
584  std::size_t blank=ops.find(' ');
585  var = ops.substr(0, blank);
586  val = ops.substr(blank+1, ops.length()-blank);
587 
588  if((var.length()>=4 && var.substr(0, 4)=="cvc3") ||
589  (val.length()>=4 && val.substr(0, 4)=="cvc3") ||
590  var==val)
591  continue;
592  else if((var.substr(0, 9)=="array_of'") ||
593  (var.substr(0, 2)=="bv" && val.substr(0, 2)!="bv"))
594  {
595  std::string t=var; var=val; val=t;
596  }
597  }
598  else if(line.substr(pos+1, 3)=="not")
599  {
600  var = line.substr(pos+5, line.length()-pos-6);
601  val = "false";
602  }
603  else
604  {
605  var = line.substr(pos+1, line.length()-pos-2);
606  assert(var.find(' ')==std::string::npos);
607  val = "true";
608  }
609 
610  values[var]=val;
611  }
612  }
613  }
614 
615  for(identifier_mapt::iterator
616  it=identifier_map.begin();
617  it!=identifier_map.end();
618  it++)
619  {
620  it->second.value.make_nil();
621  std::string conv_id=convert_identifier(it->first);
622  std::string value=values[conv_id];
623  if(value=="")
624  continue;
625 
626  if(value.substr(0, 2)=="bv")
627  {
628  std::string v=value.substr(2, value.find('[')-2);
629  size_t p = value.find('[')+1;
630  std::string w=value.substr(p, value.find(']')-p);
631 
632  std::string binary=
634  string2integer(v, 10),
636 
637  set_value(it->second, "", binary);
638  }
639  else if(value=="false")
640  it->second.value=false_exprt();
641  else if(value=="true")
642  it->second.value=true_exprt();
643  else if(value.substr(0, 8)=="array_of")
644  {
645  // We assume that array_of has only concrete arguments...
646  irep_idt id(value);
647  array_of_mapt::const_iterator fit=array_of_map.begin();
648  while(fit!=array_of_map.end() && fit->second!=id) fit++;
649 
650  if(fit!=array_of_map.end())
651  it->second.value = fit->first;
652  }
653  else
654  set_value(it->second, "", value);
655  }
656 
657  // Booleans
658  for(unsigned v=0; v<no_boolean_variables; v++)
659  {
660  std::string value=values["B"+std::to_string(v)];
661  if(value=="")
662  continue;
663  boolean_assignment[v]=(value=="true");
664  }
665 
666  return res;
667 }
The type of an expression.
Definition: type.h:20
mstreamt & result()
Definition: message.h:233
BigInt mp_integer
Definition: mp_arith.h:19
resultt read_result_opensmt(std::istream &in)
Definition: smt1_dec.cpp:265
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
index_value_mapt index_value_map
Definition: smt1_dec.h:70
Unbounded, signed rational numbers.
Definition: std_types.h:89
literalt pos(literalt a)
Definition: literal.h:193
void write_footer()
Definition: smt1_conv.cpp:70
typet & type()
Definition: expr.h:60
void set_value(identifiert &identifier, const std::string &index, const std::string &value)
Definition: smt1_conv.h:155
A constant literal expression.
Definition: std_expr.h:3685
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
identifier_mapt identifier_map
Definition: smt1_conv.h:173
std::string value
Definition: smt1_dec.h:71
const irep_idt & id() const
Definition: irep.h:189
std::string temp_out_filename
Definition: smt1_dec.h:25
std::ofstream temp_out
Definition: smt1_dec.h:24
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
virtual resultt dec_solve()
Definition: smt1_dec.cpp:63
The boolean constant true.
Definition: std_expr.h:3742
resultt read_result_mathsat(std::istream &in)
Definition: smt1_dec.cpp:307
typet array_index_type() const
Definition: smt1_conv.cpp:232
API to expression classes.
unsigned no_boolean_variables
Definition: smt1_conv.h:210
array constructor from single element
Definition: std_expr.h:1252
std::vector< bool > boolean_assignment
Definition: smt1_conv.h:211
virtual std::string decision_procedure_text() const
Definition: smt1_dec.cpp:29
resultt read_result_z3(std::istream &in)
Definition: smt1_dec.cpp:377
resultt read_result_cvc3(std::istream &in)
Definition: smt1_dec.cpp:549
resultt read_result_boolector(std::istream &in)
read model produced by Boolector
Definition: smt1_dec.cpp:182
The boolean constant false.
Definition: std_expr.h:3753
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
array_of_mapt array_of_map
Definition: smt1_conv.h:179
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:51
API to type classes.
resultt read_result_yices(std::istream &in)
Definition: smt1_dec.cpp:270
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
Definition: tempfile.cpp:87
Base class for all expressions.
Definition: expr.h:46
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
mstreamt & error()
Definition: message.h:223
solvert solver
Definition: smt1_conv.h:80
exprt binary2struct(const struct_typet &type, const std::string &binary) const
Definition: smt1_conv.cpp:3080
exprt & what()
Definition: std_expr.h:1265
std::string logic
Definition: smt1_dec.h:50
bool string_to_expr_z3(const typet &type, const std::string &value, exprt &e) const
Definition: smt1_dec.cpp:433
const typet & subtype() const
Definition: type.h:31
exprt binary2union(const union_typet &type, const std::string &binary) const
Definition: smt1_conv.cpp:3114
std::string temp_result_filename
Definition: smt1_dec.h:25
bool dec_solve_was_called
Definition: smt1_dec.h:51
std::string mathsat_value(const std::string &src)
Definition: smt1_dec.cpp:290
std::string convert_identifier(const irep_idt &identifier)
Definition: smt1_conv.cpp:478