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  {
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  throw error("not yet implemented");
162  };
163 
164  commands["display"] = [this]() {
165  // this is a command that Z3 appears to implement
166  exprt e = expression();
167  if(e.is_not_nil())
168  std::cout << smt2_format(e) << '\n';
169  };
170 
171  commands["get-value"] = [this]() {
172  std::vector<exprt> ops;
173 
174  if(next_token() != smt2_tokenizert::OPEN)
175  throw error("get-value expects list as argument");
176 
177  while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE &&
178  smt2_tokenizer.peek() != smt2_tokenizert::END_OF_FILE)
179  {
180  ops.push_back(expression()); // any term
181  }
182 
183  if(next_token() != smt2_tokenizert::CLOSE)
184  throw error("get-value expects ')' at end of list");
185 
186  if(status != SAT)
187  throw error("model is not available");
188 
189  std::vector<exprt> values;
190  values.reserve(ops.size());
191 
192  for(const auto &op : ops)
193  {
194  if(op.id() != ID_symbol)
195  throw error("get-value expects symbol");
196 
197  const auto &identifier = to_symbol_expr(op).get_identifier();
198 
199  const auto id_map_it = id_map.find(identifier);
200 
201  if(id_map_it == id_map.end())
202  throw error() << "unexpected symbol '" << identifier << '\'';
203 
204  const exprt value = solver.get(op);
205 
206  if(value.is_nil())
207  throw error() << "no value for '" << identifier << '\'';
208 
209  values.push_back(value);
210  }
211 
212  std::cout << '(';
213 
214  for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
215  {
216  if(op_nr != 0)
217  std::cout << "\n ";
218 
219  std::cout << '(' << smt2_format(ops[op_nr]) << ' '
220  << smt2_format(values[op_nr]) << ')';
221  }
222 
223  std::cout << ")\n";
224  };
225 
226  commands["echo"] = [this]() {
227  if(next_token() != smt2_tokenizert::STRING_LITERAL)
228  throw error("expected string literal");
229 
230  std::cout << smt2_format(constant_exprt(
232  << '\n';
233  };
234 
235  commands["get-assignment"] = [this]() {
236  // print satisfying assignment for all named expressions
237 
238  if(status != SAT)
239  throw error("model is not available");
240 
241  bool first = true;
242 
243  std::cout << '(';
244  for(const auto &named_term : named_terms)
245  {
246  const symbol_tablet symbol_table;
247  const namespacet ns(symbol_table);
248  const auto value =
249  simplify_expr(solver.get(named_term.second.term), ns);
250 
251  if(value.is_constant())
252  {
253  if(first)
254  first = false;
255  else
256  std::cout << '\n' << ' ';
257 
258  std::cout << '(' << smt2_format(named_term.second.name) << ' '
259  << smt2_format(value) << ')';
260  }
261  }
262  std::cout << ')' << '\n';
263  };
264 
265  commands["get-model"] = [this]() {
266  // print a model for all identifiers
267 
268  if(status != SAT)
269  throw error("model is not available");
270 
271  const symbol_tablet symbol_table;
272  const namespacet ns(symbol_table);
273 
274  bool first = true;
275 
276  std::cout << '(';
277  for(const auto &id : id_map)
278  {
279  const symbol_exprt name(id.first, id.second.type);
280  const auto value = simplify_expr(solver.get(name), ns);
281 
282  if(value.is_not_nil())
283  {
284  if(first)
285  first = false;
286  else
287  std::cout << '\n' << ' ';
288 
289  std::cout << "(define-fun " << smt2_format(name) << ' ';
290 
291  if(id.second.type.id() == ID_mathematical_function)
292  throw error("models for functions unimplemented");
293  else
294  std::cout << "() " << smt2_format(id.second.type);
295 
296  std::cout << ' ' << smt2_format(value) << ')';
297  }
298  }
299  std::cout << ')' << '\n';
300  };
301 
302  commands["simplify"] = [this]() {
303  // this is a command that Z3 appears to implement
304  exprt e = expression();
305  if(e.is_not_nil())
306  {
307  const symbol_tablet symbol_table;
308  const namespacet ns(symbol_table);
309  exprt e_simplified = simplify_expr(e, ns);
310  std::cout << smt2_format(e_simplified) << '\n';
311  }
312  };
313  }
314 
315 #if 0
316  // TODO:
317  | ( declare-const hsymboli hsorti )
318  | ( declare-datatype hsymboli hdatatype_deci)
319  | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
320  | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
321  | ( declare-sort hsymboli hnumerali )
322  | ( define-fun hfunction_def i )
323  | ( define-fun-rec hfunction_def i )
324  | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
325  | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
326  | ( get-assertions )
327  | ( get-info hinfo_flag i )
328  | ( get-option hkeywordi )
329  | ( get-proof )
330  | ( get-unsat-assumptions )
331  | ( get-unsat-core )
332  | ( pop hnumerali )
333  | ( push hnumerali )
334  | ( reset )
335  | ( reset-assertions )
336  | ( set-info hattributei )
337  | ( set-option hoptioni )
338 #endif
339 }
340 
342 {
343 public:
344  void print(unsigned level, const std::string &message) override
345  {
347 
348  if(level < 4) // errors
349  std::cout << "(error \"" << message << "\")\n";
350  else
351  std::cout << "; " << message << '\n';
352  }
353 
354  void print(unsigned, const xmlt &) override
355  {
356  }
357 
358  void print(unsigned, const jsont &) override
359  {
360  }
361 
362  void flush(unsigned) override
363  {
364  std::cout << std::flush;
365  }
366 };
367 
368 int solver(std::istream &in)
369 {
370  symbol_tablet symbol_table;
371  namespacet ns(symbol_table);
372 
373  smt2_message_handlert message_handler;
374  messaget message(message_handler);
375 
376  // this is our default verbosity
377  message_handler.set_verbosity(messaget::M_STATISTICS);
378 
379  satcheckt satcheck{message_handler};
380  boolbvt boolbv{ns, satcheck, message_handler};
381 
382  smt2_solvert smt2_solver{in, boolbv};
383  bool error_found = false;
384 
385  while(!smt2_solver.exit)
386  {
387  try
388  {
389  smt2_solver.parse();
390  }
391  catch(const smt2_tokenizert::smt2_errort &error)
392  {
393  smt2_solver.skip_to_end_of_list();
394  error_found = true;
395  message.error().source_location.set_line(error.get_line_no());
396  message.error() << error.what() << messaget::eom;
397  }
398  catch(const analysis_exceptiont &error)
399  {
400  smt2_solver.skip_to_end_of_list();
401  error_found = true;
402  message.error() << error.what() << messaget::eom;
403  }
404  }
405 
406  if(error_found)
407  return 20;
408  else
409  return 0;
410 }
411 
412 int main(int argc, const char *argv[])
413 {
414  if(argc==1)
415  return solver(std::cin);
416 
417  if(argc!=2)
418  {
419  std::cerr << "usage: smt2_solver file\n";
420  return 1;
421  }
422 
423  std::ifstream in(argv[1]);
424  if(!in)
425  {
426  std::cerr << "failed to open " << argv[1] << '\n';
427  return 1;
428  }
429 
430  return solver(in);
431 }
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:354
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
smt2_tokenizert::peek
tokent peek()
Definition: smt2_tokenizer.h:72
smt2_solvert::define_constants
void define_constants()
Definition: smt2_solver.cpp:51
decision_proceduret
Definition: decision_procedure.h:21
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
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
namespace.h
jsont
Definition: json.h:27
equal_exprt
Equality.
Definition: std_expr.h:1140
smt2_parsert::sort
typet sort()
Definition: smt2_parser.cpp:1093
message_handlert::print
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:59
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
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
smt2_solvert::solver
decision_proceduret & solver
Definition: smt2_solver.cpp:35
message
static const char * message(const statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:27
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
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:110
smt2_format
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:25
smt2_message_handlert
Definition: smt2_solver.cpp:342
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2529
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:190
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
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
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:740
smt2_tokenizert::smt2_errort
Definition: smt2_tokenizer.h:27
smt2_message_handlert::print
void print(unsigned, const jsont &) override
Definition: smt2_solver.cpp:358
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:368
string_typet
String type.
Definition: std_types.h:1669
smt2_parsert::next_token
smt2_tokenizert::tokent next_token()
Definition: smt2_parser.cpp:24
boolbvt
Definition: boolbv.h:41
main
int main(int argc, const char *argv[])
Definition: smt2_solver.cpp:412
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:344
smt2_solvert::smt2_solvert
smt2_solvert(std::istream &_in, decision_proceduret &_solver)
Definition: smt2_solver.cpp:28
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:2668
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:362
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