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