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