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