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, stack_decision_proceduret &_solver)
29  : smt2_parsert(_in), solver(_solver), status(NOT_SOLVED)
30  {
32  }
33 
34 protected:
36 
37  void setup_commands();
38  void define_constants();
40 
41  std::set<irep_idt> constants_done;
42 
43  enum
44  {
46  SAT,
47  UNSAT
48  } status;
49 };
50 
52 {
53  for(const auto &id : id_map)
54  {
55  if(id.second.type.id() == ID_mathematical_function)
56  continue;
57 
58  if(id.second.definition.is_nil())
59  continue;
60 
61  const irep_idt &identifier = id.first;
62 
63  // already done?
64  if(constants_done.find(identifier)!=constants_done.end())
65  continue;
66 
67  constants_done.insert(identifier);
68 
69  exprt def = id.second.definition;
72  equal_exprt(symbol_exprt(identifier, id.second.type), def));
73  }
74 }
75 
77 {
78  for(exprt &op : expr.operands())
80 
81  if(expr.id()==ID_function_application)
82  {
83  auto &app=to_function_application_expr(expr);
84 
85  if(app.function().id() == ID_symbol)
86  {
87  // look up the symbol
88  auto identifier = to_symbol_expr(app.function()).get_identifier();
89  auto f_it = id_map.find(identifier);
90 
91  if(f_it != id_map.end())
92  {
93  const auto &f = f_it->second;
94 
96  f.type.id() == ID_mathematical_function,
97  "type of function symbol must be mathematical_function_type");
98 
99  const auto &domain = to_mathematical_function_type(f.type).domain();
100 
102  domain.size() == app.arguments().size(),
103  "number of parameters must match number of arguments");
104 
105  // Does it have a definition? It's otherwise uninterpreted.
106  if(!f.definition.is_nil())
107  {
108  exprt body = f.definition;
109 
110  if(body.id() == ID_lambda)
111  body = to_lambda_expr(body).application(app.arguments());
112 
113  expand_function_applications(body); // rec. call
114  expr = body;
115  }
116  }
117  }
118  }
119 }
120 
122 {
123  {
124  commands["assert"] = [this]() {
125  exprt e = expression();
126  if(e.is_not_nil())
127  {
129  solver.set_to_true(e);
130  }
131  };
132 
133  commands["check-sat"] = [this]() {
134  // add constant definitions as constraints
136 
137  switch(solver())
138  {
140  std::cout << "sat\n";
141  status = SAT;
142  break;
143 
145  std::cout << "unsat\n";
146  status = UNSAT;
147  break;
148 
150  std::cout << "error\n";
151  status = NOT_SOLVED;
152  }
153  };
154 
155  commands["check-sat-assuming"] = [this]() {
156  std::vector<exprt> assumptions;
157 
158  if(next_token() != smt2_tokenizert::OPEN)
159  throw error("check-sat-assuming expects list as argument");
160 
161  while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE &&
162  smt2_tokenizer.peek() != smt2_tokenizert::END_OF_FILE)
163  {
164  auto e = expression(); // any term
166  assumptions.push_back(solver.handle(e));
167  }
168 
169  if(next_token() != smt2_tokenizert::CLOSE)
170  throw error("check-sat-assuming expects ')' at end of list");
171 
172  // add constant definitions as constraints
174 
175  // add the assumptions
176  solver.push(assumptions);
177 
178  switch(solver())
179  {
181  std::cout << "sat\n";
182  status = SAT;
183  break;
184 
186  std::cout << "unsat\n";
187  status = UNSAT;
188  break;
189 
191  std::cout << "error\n";
192  status = NOT_SOLVED;
193  }
194 
195  // remove the assumptions again
196  solver.pop();
197  };
198 
199  commands["display"] = [this]() {
200  // this is a command that Z3 appears to implement
201  exprt e = expression();
202  if(e.is_not_nil())
203  std::cout << smt2_format(e) << '\n';
204  };
205 
206  commands["get-unsat-assumptions"] = [this]() {
207  throw error("not yet implemented");
208  };
209 
210  commands["get-value"] = [this]() {
211  std::vector<exprt> ops;
212 
213  if(next_token() != smt2_tokenizert::OPEN)
214  throw error("get-value expects list as argument");
215 
216  while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE &&
217  smt2_tokenizer.peek() != smt2_tokenizert::END_OF_FILE)
218  {
219  ops.push_back(expression()); // any term
220  }
221 
222  if(next_token() != smt2_tokenizert::CLOSE)
223  throw error("get-value expects ')' at end of list");
224 
225  if(status != SAT)
226  throw error("model is not available");
227 
228  std::vector<exprt> values;
229  values.reserve(ops.size());
230 
231  for(const auto &op : ops)
232  {
233  if(op.id() != ID_symbol)
234  throw error("get-value expects symbol");
235 
236  const auto &identifier = to_symbol_expr(op).get_identifier();
237 
238  const auto id_map_it = id_map.find(identifier);
239 
240  if(id_map_it == id_map.end())
241  throw error() << "unexpected symbol '" << identifier << '\'';
242 
243  const exprt value = solver.get(op);
244 
245  if(value.is_nil())
246  throw error() << "no value for '" << identifier << '\'';
247 
248  values.push_back(value);
249  }
250 
251  std::cout << '(';
252 
253  for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
254  {
255  if(op_nr != 0)
256  std::cout << "\n ";
257 
258  std::cout << '(' << smt2_format(ops[op_nr]) << ' '
259  << smt2_format(values[op_nr]) << ')';
260  }
261 
262  std::cout << ")\n";
263  };
264 
265  commands["echo"] = [this]() {
266  if(next_token() != smt2_tokenizert::STRING_LITERAL)
267  throw error("expected string literal");
268 
269  std::cout << smt2_format(constant_exprt(
271  << '\n';
272  };
273 
274  commands["get-assignment"] = [this]() {
275  // print satisfying assignment for all named expressions
276 
277  if(status != SAT)
278  throw error("model is not available");
279 
280  bool first = true;
281 
282  std::cout << '(';
283  for(const auto &named_term : named_terms)
284  {
285  const symbol_tablet symbol_table;
286  const namespacet ns(symbol_table);
287  const auto value =
288  simplify_expr(solver.get(named_term.second.term), ns);
289 
290  if(value.is_constant())
291  {
292  if(first)
293  first = false;
294  else
295  std::cout << '\n' << ' ';
296 
297  std::cout << '(' << smt2_format(named_term.second.name) << ' '
298  << smt2_format(value) << ')';
299  }
300  }
301  std::cout << ')' << '\n';
302  };
303 
304  commands["get-model"] = [this]() {
305  // print a model for all identifiers
306 
307  if(status != SAT)
308  throw error("model is not available");
309 
310  const symbol_tablet symbol_table;
311  const namespacet ns(symbol_table);
312 
313  bool first = true;
314 
315  std::cout << '(';
316  for(const auto &id : id_map)
317  {
318  const symbol_exprt name(id.first, id.second.type);
319  const auto value = simplify_expr(solver.get(name), ns);
320 
321  if(value.is_not_nil())
322  {
323  if(first)
324  first = false;
325  else
326  std::cout << '\n' << ' ';
327 
328  std::cout << "(define-fun " << smt2_format(name) << ' ';
329 
330  if(id.second.type.id() == ID_mathematical_function)
331  throw error("models for functions unimplemented");
332  else
333  std::cout << "() " << smt2_format(id.second.type);
334 
335  std::cout << ' ' << smt2_format(value) << ')';
336  }
337  }
338  std::cout << ')' << '\n';
339  };
340 
341  commands["simplify"] = [this]() {
342  // this is a command that Z3 appears to implement
343  exprt e = expression();
344  if(e.is_not_nil())
345  {
346  const symbol_tablet symbol_table;
347  const namespacet ns(symbol_table);
348  exprt e_simplified = simplify_expr(e, ns);
349  std::cout << smt2_format(e_simplified) << '\n';
350  }
351  };
352  }
353 
354 #if 0
355  // TODO:
356  | ( declare-const hsymboli hsorti )
357  | ( declare-datatype hsymboli hdatatype_deci)
358  | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
359  | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
360  | ( declare-sort hsymboli hnumerali )
361  | ( define-fun hfunction_def i )
362  | ( define-fun-rec hfunction_def i )
363  | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
364  | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
365  | ( get-assertions )
366  | ( get-info hinfo_flag i )
367  | ( get-option hkeywordi )
368  | ( get-proof )
369  | ( get-unsat-assumptions )
370  | ( get-unsat-core )
371  | ( pop hnumerali )
372  | ( push hnumerali )
373  | ( reset )
374  | ( reset-assertions )
375  | ( set-info hattributei )
376  | ( set-option hoptioni )
377 #endif
378 }
379 
381 {
382 public:
383  void print(unsigned level, const std::string &message) override
384  {
385  message_handlert::print(level, message);
386 
387  if(level < 4) // errors
388  std::cout << "(error \"" << message << "\")\n";
389  else
390  std::cout << "; " << message << '\n';
391  }
392 
393  void print(unsigned, const xmlt &) override
394  {
395  }
396 
397  void print(unsigned, const jsont &) override
398  {
399  }
400 
401  void flush(unsigned) override
402  {
403  std::cout << std::flush;
404  }
405 };
406 
407 int solver(std::istream &in)
408 {
409  symbol_tablet symbol_table;
410  namespacet ns(symbol_table);
411 
412  smt2_message_handlert message_handler;
413  messaget message(message_handler);
414 
415  // this is our default verbosity
416  message_handler.set_verbosity(messaget::M_STATISTICS);
417 
418  satcheckt satcheck{message_handler};
419  boolbvt boolbv{ns, satcheck, message_handler};
420 
421  smt2_solvert smt2_solver{in, boolbv};
422  bool error_found = false;
423 
424  while(!smt2_solver.exit)
425  {
426  try
427  {
428  smt2_solver.parse();
429  }
430  catch(const smt2_tokenizert::smt2_errort &error)
431  {
432  smt2_solver.skip_to_end_of_list();
433  error_found = true;
434  message.error().source_location.set_line(error.get_line_no());
435  message.error() << error.what() << messaget::eom;
436  }
437  catch(const analysis_exceptiont &error)
438  {
439  smt2_solver.skip_to_end_of_list();
440  error_found = true;
441  message.error() << error.what() << messaget::eom;
442  }
443  }
444 
445  if(error_found)
446  return 20;
447  else
448  return 0;
449 }
450 
451 int main(int argc, const char *argv[])
452 {
453  if(argc==1)
454  return solver(std::cin);
455 
456  if(argc!=2)
457  {
458  std::cerr << "usage: smt2_solver file\n";
459  return 1;
460  }
461 
462  std::ifstream in(argv[1]);
463  if(!in)
464  {
465  std::cerr << "failed to open " << argv[1] << '\n';
466  return 1;
467  }
468 
469  return solver(in);
470 }
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Definition: boolbv.h:44
A constant literal expression.
Definition: std_expr.h:2807
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
virtual exprt handle(const exprt &expr)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
operandst & operands()
Definition: expr.h:92
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Definition: json.h:27
exprt application(const operandst &arguments) const
void set_verbosity(unsigned _verbosity)
Definition: message.h:53
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:60
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
void print(unsigned level, const std::string &message) override
void flush(unsigned) override
void print(unsigned, const xmlt &) override
void print(unsigned, const jsont &) override
named_termst named_terms
Definition: smt2_parser.h:74
id_mapt id_map
Definition: smt2_parser.h:58
std::unordered_map< std::string, std::function< void()> > commands
Definition: smt2_parser.h:190
void parse()
Definition: smt2_parser.h:31
exprt expression()
smt2_tokenizert::smt2_errort error() const
Definition: smt2_parser.h:83
smt2_tokenizert::tokent next_token()
Definition: smt2_parser.cpp:25
smt2_tokenizert smt2_tokenizer
Definition: smt2_parser.h:92
smt2_solvert(std::istream &_in, stack_decision_proceduret &_solver)
Definition: smt2_solver.cpp:28
void expand_function_applications(exprt &)
Definition: smt2_solver.cpp:76
stack_decision_proceduret & solver
Definition: smt2_solver.cpp:35
enum smt2_solvert::@5 status
void setup_commands()
std::set< irep_idt > constants_done
Definition: smt2_solver.cpp:41
void define_constants()
Definition: smt2_solver.cpp:51
std::string what() const override
A human readable description of what went wrong.
unsigned get_line_no() const
const std::string & get_buffer() const
void set_line(const irep_idt &line)
virtual void pop()=0
Pop whatever is on top of the stack.
virtual void push(const std::vector< exprt > &assumptions)=0
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
String type.
Definition: std_types.h:901
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The symbol table.
Definition: symbol_table.h:14
Definition: xml.h:21
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:28
int solver(std::istream &in)
int main(int argc, const char *argv[])
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
Author: Diffblue Ltd.