cprover
smt2_solver.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SMT2 Solver that uses boolbv and the default SAT solver
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "smt2_parser.h"
10 
11 #include "smt2_format.h"
12 
13 #include <fstream>
14 #include <iostream>
15 
16 #include <util/message.h>
17 #include <util/namespace.h>
18 #include <util/replace_symbol.h>
19 #include <util/simplify_expr.h>
20 #include <util/symbol_table.h>
21 
22 #include <solvers/sat/satcheck.h>
24 
26 {
27 public:
28  smt2_solvert(std::istream &_in, decision_proceduret &_solver)
29  : smt2_parsert(_in), solver(_solver), status(NOT_SOLVED)
30  {
31  }
32 
33 protected:
35 
36  void command(const std::string &) override;
37  void define_constants();
39 
40  std::set<irep_idt> constants_done;
41 
42  enum
43  {
45  SAT,
47  } status;
48 };
49 
51 {
52  for(const auto &id : id_map)
53  {
54  if(id.second.type.id() == ID_mathematical_function)
55  continue;
56 
57  if(id.second.definition.is_nil())
58  continue;
59 
60  const irep_idt &identifier = id.first;
61 
62  // already done?
63  if(constants_done.find(identifier)!=constants_done.end())
64  continue;
65 
66  constants_done.insert(identifier);
67 
68  exprt def = id.second.definition;
71  equal_exprt(symbol_exprt(identifier, id.second.type), def));
72  }
73 }
74 
76 {
77  for(exprt &op : expr.operands())
79 
80  if(expr.id()==ID_function_application)
81  {
82  auto &app=to_function_application_expr(expr);
83 
84  // look it up
85  irep_idt identifier=app.function().get_identifier();
86  auto f_it=id_map.find(identifier);
87 
88  if(f_it!=id_map.end())
89  {
90  const auto &f=f_it->second;
91 
92  DATA_INVARIANT(f.type.id()==ID_mathematical_function,
93  "type of function symbol must be mathematical_function_type");
94 
95  const auto f_type=
97 
98  const auto &domain = f_type.domain();
99 
101  domain.size() == app.arguments().size(),
102  "number of function parameters");
103 
104  replace_symbolt replace_symbol;
105 
106  std::map<irep_idt, exprt> parameter_map;
107  for(std::size_t i = 0; i < domain.size(); i++)
108  {
109  const symbol_exprt s(f.parameters[i], domain[i]);
110  replace_symbol.insert(s, app.arguments()[i]);
111  }
112 
113  exprt body=f.definition;
114  replace_symbol(body);
116  expr=body;
117  }
118  }
119 }
120 
121 void smt2_solvert::command(const std::string &c)
122 {
123  {
124  if(c == "assert")
125  {
126  exprt e = expression();
127  if(e.is_not_nil())
128  {
130  solver.set_to_true(e);
131  }
132  }
133  else if(c == "check-sat")
134  {
135  // add constant definitions as constraints
137 
138  switch(solver())
139  {
141  std::cout << "sat\n";
142  status = SAT;
143  break;
144 
146  std::cout << "unsat\n";
147  status = UNSAT;
148  break;
149 
151  std::cout << "error\n";
152  status = NOT_SOLVED;
153  }
154  }
155  else if(c == "check-sat-assuming")
156  {
157  throw error("not yet implemented");
158  }
159  else if(c == "display")
160  {
161  // this is a command that Z3 appears to implement
162  exprt e = expression();
163  if(e.is_not_nil())
164  std::cout << smt2_format(e) << '\n';
165  }
166  else if(c == "get-value")
167  {
168  std::vector<exprt> ops;
169 
170  if(next_token() != OPEN)
171  throw error("get-value expects list as argument");
172 
173  while(peek() != CLOSE && peek() != END_OF_FILE)
174  ops.push_back(expression()); // any term
175 
176  if(next_token() != CLOSE)
177  throw error("get-value expects ')' at end of list");
178 
179  if(status != SAT)
180  throw error("model is not available");
181 
182  std::vector<exprt> values;
183  values.reserve(ops.size());
184 
185  for(const auto &op : ops)
186  {
187  if(op.id() != ID_symbol)
188  throw error("get-value expects symbol");
189 
190  const auto &identifier = to_symbol_expr(op).get_identifier();
191 
192  const auto id_map_it = id_map.find(identifier);
193 
194  if(id_map_it == id_map.end())
195  throw error() << "unexpected symbol `" << identifier << '\'';
196 
197  const exprt value = solver.get(op);
198 
199  if(value.is_nil())
200  throw error() << "no value for `" << identifier << '\'';
201 
202  values.push_back(value);
203  }
204 
205  std::cout << '(';
206 
207  for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
208  {
209  if(op_nr != 0)
210  std::cout << "\n ";
211 
212  std::cout << '(' << smt2_format(ops[op_nr]) << ' '
213  << smt2_format(values[op_nr]) << ')';
214  }
215 
216  std::cout << ")\n";
217  }
218  else if(c == "echo")
219  {
220  if(next_token() != STRING_LITERAL)
221  throw error("expected string literal");
222 
223  std::cout << smt2_format(constant_exprt(buffer, string_typet())) << '\n';
224  }
225  else if(c == "get-assignment")
226  {
227  // print satisfying assignment for all named expressions
228 
229  if(status != SAT)
230  throw error("model is not available");
231 
232  bool first = true;
233 
234  std::cout << '(';
235  for(const auto &named_term : named_terms)
236  {
237  const symbol_tablet symbol_table;
238  const namespacet ns(symbol_table);
239  const auto value =
240  simplify_expr(solver.get(named_term.second.term), ns);
241 
242  if(value.is_constant())
243  {
244  if(first)
245  first = false;
246  else
247  std::cout << '\n' << ' ';
248 
249  std::cout << '(' << smt2_format(named_term.second.name) << ' '
250  << smt2_format(value) << ')';
251  }
252  }
253  std::cout << ')' << '\n';
254  }
255  else if(c == "get-model")
256  {
257  // print a model for all identifiers
258 
259  if(status != SAT)
260  throw error("model is not available");
261 
262  const symbol_tablet symbol_table;
263  const namespacet ns(symbol_table);
264 
265  bool first = true;
266 
267  std::cout << '(';
268  for(const auto &id : id_map)
269  {
270  const symbol_exprt name(id.first, id.second.type);
271  const auto value = simplify_expr(solver.get(name), ns);
272 
273  if(value.is_not_nil())
274  {
275  if(first)
276  first = false;
277  else
278  std::cout << '\n' << ' ';
279 
280  std::cout << "(define-fun " << smt2_format(name) << ' ';
281 
282  if(id.second.type.id() == ID_mathematical_function)
283  throw error("models for functions unimplemented");
284  else
285  std::cout << "() " << smt2_format(id.second.type);
286 
287  std::cout << ' ' << smt2_format(value) << ')';
288  }
289  }
290  std::cout << ')' << '\n';
291  }
292  else if(c == "simplify")
293  {
294  // this is a command that Z3 appears to implement
295  exprt e = expression();
296  if(e.is_not_nil())
297  {
298  const symbol_tablet symbol_table;
299  const namespacet ns(symbol_table);
300  exprt e_simplified = simplify_expr(e, ns);
301  std::cout << smt2_format(e) << '\n';
302  }
303  }
304 #if 0
305  // TODO:
306  | ( declare-const hsymboli hsorti )
307  | ( declare-datatype hsymboli hdatatype_deci)
308  | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
309  | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
310  | ( declare-sort hsymboli hnumerali )
311  | ( define-fun hfunction_def i )
312  | ( define-fun-rec hfunction_def i )
313  | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
314  | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
315  | ( get-assertions )
316  | ( get-info hinfo_flag i )
317  | ( get-option hkeywordi )
318  | ( get-proof )
319  | ( get-unsat-assumptions )
320  | ( get-unsat-core )
321  | ( pop hnumerali )
322  | ( push hnumerali )
323  | ( reset )
324  | ( reset-assertions )
325  | ( set-info hattributei )
326  | ( set-option hoptioni )
327 #endif
328  else
330  }
331 }
332 
334 {
335 public:
336  void print(unsigned level, const std::string &message) override
337  {
338  message_handlert::print(level, message);
339 
340  if(level < 4) // errors
341  std::cout << "(error \"" << message << "\")\n";
342  else
343  std::cout << "; " << message << '\n';
344  }
345 
346  void print(unsigned level, const xmlt &xml) override
347  {
348  }
349 
350  void print(unsigned level, const jsont &json) override
351  {
352  }
353 
354  void flush(unsigned) override
355  {
356  std::cout << std::flush;
357  }
358 };
359 
360 int solver(std::istream &in)
361 {
362  symbol_tablet symbol_table;
363  namespacet ns(symbol_table);
364 
365  smt2_message_handlert message_handler;
366  messaget message(message_handler);
367 
368  // this is our default verbosity
369  message_handler.set_verbosity(messaget::M_STATISTICS);
370 
371  satcheckt satcheck;
372  boolbvt boolbv(ns, satcheck);
373  satcheck.set_message_handler(message_handler);
374  boolbv.set_message_handler(message_handler);
375 
376  smt2_solvert smt2_solver(in, boolbv);
377  smt2_solver.set_message_handler(message_handler);
378  bool error_found = false;
379 
380  while(!smt2_solver.exit)
381  {
382  try
383  {
384  smt2_solver.parse();
385  }
386  catch(const smt2_solvert::smt2_errort &error)
387  {
388  smt2_solver.skip_to_end_of_list();
389  error_found = true;
390  messaget message(message_handler);
391  message.error().source_location.set_line(error.get_line_no());
392  message.error() << error.what() << messaget::eom;
393  }
394  catch(const analysis_exceptiont &error)
395  {
396  smt2_solver.skip_to_end_of_list();
397  error_found = true;
398  messaget message(message_handler);
399  message.error() << error.what() << messaget::eom;
400  }
401  }
402 
403  if(error_found)
404  return 20;
405  else
406  return 0;
407 }
408 
409 int main(int argc, const char *argv[])
410 {
411  if(argc==1)
412  return solver(std::cin);
413 
414  if(argc!=2)
415  {
416  std::cerr << "usage: smt2_solver file\n";
417  return 1;
418  }
419 
420  std::ifstream in(argv[1]);
421  if(!in)
422  {
423  std::cerr << "failed to open " << argv[1] << '\n';
424  return 1;
425  }
426 
427  return solver(in);
428 }
void define_constants()
Definition: smt2_solver.cpp:50
unsigned get_line_no() const
void flush(unsigned) override
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
Definition: smt2_parser.cpp:31
smt2_solvert(std::istream &_in, decision_proceduret &_solver)
Definition: smt2_solver.cpp:28
exprt simplify_expr(const exprt &src, const namespacet &ns)
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:25
bool parse() override
Definition: smt2_parser.h:26
const irep_idt & get_identifier() const
Definition: std_expr.h:176
Definition: json.h:23
virtual exprt get(const exprt &expr) const =0
void print(unsigned level, const jsont &json) override
std::string what() const override
A human readable description of what went wrong.
A constant literal expression.
Definition: std_expr.h:4384
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
Definition: boolbv.h:32
String type.
Definition: std_types.h:1662
Equality.
Definition: std_expr.h:1484
void print(unsigned level, const xmlt &xml) override
const irep_idt & id() const
Definition: irep.h:259
std::string what() const override
A human readable description of what went wrong.
Replace expression or type symbols by an expression or type, respectively.
int solver(std::istream &in)
void expand_function_applications(exprt &)
Definition: smt2_solver.cpp:75
source_locationt source_location
Definition: message.h:236
tokent next_token() override
Definition: smt2_parser.cpp:19
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: std_expr.h:4523
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:386
void set_line(const irep_idt &line)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Definition: xml.h:18
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
std::set< irep_idt > constants_done
Definition: smt2_solver.cpp:40
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
int main(int argc, const char *argv[])
Author: Diffblue Ltd.
exprt expression()
#define STRING_LITERAL
id_mapt id_map
Definition: smt2_parser.h:44
static eomt eom
Definition: message.h:284
virtual void command(const std::string &)
mstreamt & status() const
Definition: message.h:401
std::string buffer
Base class for all expressions.
Definition: expr.h:54
named_termst named_terms
Definition: smt2_parser.h:53
void set_to_true(const exprt &expr)
void print(unsigned level, const std::string &message) override
#define CLOSE
Definition: xml_y.tab.cpp:155
smt2_errort error()
generate an error exception
void command(const std::string &) override
void set_verbosity(unsigned _verbosity)
Definition: message.h:48
Expression to hold a symbol (variable)
Definition: std_expr.h:143
decision_proceduret & solver
Definition: smt2_solver.cpp:34
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:58