cprover
smt2_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 "smt2_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/ieee_float.h>
27 
28 #include "smt2irep.h"
29 
31 {
32  return "SMT2 "+logic+
33  (use_FPA_theory?" (with FPA)":"")+
34  " using "+
35  (solver==solvert::GENERIC?"Generic":
36  solver==solvert::BOOLECTOR?"Boolector":
37  solver==solvert::CVC3?"CVC3":
38  solver==solvert::CVC4?"CVC4":
39  solver==solvert::MATHSAT?"MathSAT":
40  solver==solvert::YICES?"Yices":
41  solver==solvert::Z3?"Z3":
42  "(unknown)");
43 }
44 
46 {
47  temp_out_filename=get_temporary_file("smt2_dec_out_", "");
48 
49  temp_out.open(
50  temp_out_filename.c_str(),
51  std::ios_base::out | std::ios_base::trunc);
52 }
53 
55 {
56  temp_out.close();
57 
58  if(temp_out_filename!="")
59  unlink(temp_out_filename.c_str());
60 
61  if(temp_result_filename!="")
62  unlink(temp_result_filename.c_str());
63 }
64 
66 {
67  // we write the problem into a file
68  smt2_temp_filet smt2_temp_file;
69 
70  // copy from string buffer into file
71  smt2_temp_file.temp_out << stringstream.str();
72 
73  // this finishes up and closes the SMT2 file
74  write_footer(smt2_temp_file.temp_out);
75  smt2_temp_file.temp_out.close();
76 
77  smt2_temp_file.temp_result_filename=
78  get_temporary_file("smt2_dec_result_", "");
79 
80  std::string command;
81 
82  switch(solver)
83  {
84  case solvert::BOOLECTOR:
85  command = "boolector --smt2 "
86  + smt2_temp_file.temp_out_filename
87  + " -m > "
88  + smt2_temp_file.temp_result_filename;
89  break;
90 
91  case solvert::CVC3:
92  command = "cvc3 +model -lang smtlib -output-lang smtlib "
93  + smt2_temp_file.temp_out_filename
94  + " > "
95  + smt2_temp_file.temp_result_filename;
96  break;
97 
98  case solvert::CVC4:
99  // The flags --bitblast=eager --bv-div-zero-const help but only
100  // work for pure bit-vector formulas.
101  command = "cvc4 -L smt2 "
102  + smt2_temp_file.temp_out_filename
103  + " > "
104  + smt2_temp_file.temp_result_filename;
105  break;
106 
107  case solvert::MATHSAT:
108  // The options below were recommended by Alberto Griggio
109  // on 10 July 2013
110  command = "mathsat -input=smt2"
111  " -preprocessor.toplevel_propagation=true"
112  " -preprocessor.simplification=7"
113  " -dpll.branching_random_frequency=0.01"
114  " -dpll.branching_random_invalidate_phase_cache=true"
115  " -dpll.restart_strategy=3"
116  " -dpll.glucose_var_activity=true"
117  " -dpll.glucose_learnt_minimization=true"
118  " -theory.bv.eager=true"
119  " -theory.bv.bit_blast_mode=1"
120  " -theory.bv.delay_propagated_eqs=true"
121  " -theory.fp.mode=1"
122  " -theory.fp.bit_blast_mode=2"
123  " -theory.arr.mode=1"
124  " < "+smt2_temp_file.temp_out_filename
125  + " > "+smt2_temp_file.temp_result_filename;
126  break;
127 
128  case solvert::YICES:
129  // command = "yices -smt -e " // Calling convention for older versions
130  command = "yices-smt2 " // Calling for 2.2.1
131  + smt2_temp_file.temp_out_filename
132  + " > "
133  + smt2_temp_file.temp_result_filename;
134  break;
135 
136  case solvert::Z3:
137  command = "z3 -smt2 "
138  + smt2_temp_file.temp_out_filename
139  + " > "
140  + smt2_temp_file.temp_result_filename;
141  break;
142 
143  default:
144  assert(false);
145  }
146 
147  #if defined(__linux__) || defined(__APPLE__)
148  command+=" 2>&1";
149  #endif
150 
151  int res=system(command.c_str());
152  if(res<0)
153  {
154  error() << "error running SMT2 solver" << eom;
156  }
157 
158  std::ifstream in(smt2_temp_file.temp_result_filename.c_str());
159 
160  return read_result(in);
161 }
162 
164 {
165  std::string line;
167 
168  boolean_assignment.clear();
170 
171  typedef std::unordered_map<irep_idt, irept> valuest;
172  valuest values;
173 
174  while(in)
175  {
176  irept parsed=smt2irep(in);
177 
178  if(parsed.id()=="sat")
180  else if(parsed.id()=="unsat")
182  else if(parsed.id()=="" &&
183  parsed.get_sub().size()==1 &&
184  parsed.get_sub().front().get_sub().size()==2)
185  {
186  const irept &s0=parsed.get_sub().front().get_sub()[0];
187  const irept &s1=parsed.get_sub().front().get_sub()[1];
188 
189  // Examples:
190  // ( (B0 true) )
191  // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
192  // ( (|some_integer| 0) )
193  // ( (|some_integer| (- 10)) )
194 
195  values[s0.id()]=s1;
196  }
197  else if(parsed.id()=="" &&
198  parsed.get_sub().size()==2 &&
199  parsed.get_sub().front().id()=="error")
200  {
201  // We ignore errors after UNSAT because get-value after check-sat
202  // returns unsat will give an error.
203  if(res!=resultt::D_UNSATISFIABLE)
204  {
205  error() << "SMT2 solver returned error message:\n"
206  << "\t\"" << parsed.get_sub()[1].id() <<"\"" << eom;
208  }
209  }
210  }
211 
212  for(auto &assignment : identifier_map)
213  {
214  std::string conv_id=convert_identifier(assignment.first);
215  const irept &value=values[conv_id];
216  assignment.second.value=parse_rec(value, assignment.second.type);
217  }
218 
219  // Booleans
220  for(unsigned v=0; v<no_boolean_variables; v++)
221  {
222  const irept &value=values["B"+std::to_string(v)];
223  boolean_assignment[v]=(value.id()==ID_true);
224  }
225 
226  return res;
227 }
irept smt2irep(std::istream &in)
Definition: smt2irep.cpp:93
std::stringstream stringstream
Definition: smt2_dec.h:30
resultt read_result(std::istream &in)
Definition: smt2_dec.cpp:163
virtual resultt dec_solve()
Definition: smt2_dec.cpp:65
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
identifier_mapt identifier_map
Definition: smt2_conv.h:293
subt & get_sub()
Definition: irep.h:317
std::string temp_result_filename
Definition: smt2_dec.h:24
const irep_idt & id() const
Definition: irep.h:259
API to expression classes.
mstreamt & error() const
Definition: message.h:302
std::string temp_out_filename
Definition: smt2_dec.h:24
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:762
virtual std::string decision_procedure_text() const
Definition: smt2_dec.cpp:30
std::ofstream temp_out
Definition: smt2_dec.h:23
API to type classes.
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
std::string to_string(const string_constraintt &expr)
Used for debug printing.
std::size_t no_boolean_variables
Definition: smt2_conv.h:315
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:445
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:316
int8_t s1
Definition: bytecode_info.h:59
solvert solver
Definition: smt2_conv.h:127
std::string logic
Definition: smt2_conv.h:126
bool use_FPA_theory
Definition: smt2_conv.h:104
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:97