cprover
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 "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
24
26{
27public:
33
34protected:
36
37 void setup_commands();
38 void define_constants();
40
41 std::set<irep_idt> constants_done;
42
43 enum
44 {
47 UNSAT
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 {
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 {
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";
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";
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);
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 )
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{
382public:
383 void print(unsigned level, const std::string &message) override
384 {
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
407int 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
451int 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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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: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
exprt expression()
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()
std::string what() const override
A human readable description of what went wrong.
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 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: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.