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