Go to the documentation of this file.
53 for(
const auto &
id :
id_map)
55 if(
id.second.type.id() == ID_mathematical_function)
58 if(
id.second.definition.is_nil())
61 const irep_idt &identifier =
id.first;
69 exprt def =
id.second.definition;
81 if(expr.
id()==ID_function_application)
85 if(app.function().id() == ID_symbol)
89 auto f_it =
id_map.find(identifier);
93 const auto &f = f_it->second;
96 f.type.id() == ID_mathematical_function,
97 "type of function symbol must be mathematical_function_type");
102 domain.size() == app.arguments().size(),
103 "number of parameters must match number of arguments");
106 if(!f.definition.is_nil())
110 for(std::size_t i = 0; i < domain.size(); i++)
113 symbol_exprt(f.parameters[i], domain[i]), app.arguments()[i]);
116 exprt body = f.definition;
117 replace_symbol(body);
145 std::cout <<
"sat\n";
150 std::cout <<
"unsat\n";
155 std::cout <<
"error\n";
160 commands[
"check-sat-assuming"] = [
this]() {
161 std::vector<exprt> assumptions;
164 throw error(
"check-sat-assuming expects list as argument");
175 throw error(
"check-sat-assuming expects ')' at end of list");
186 std::cout <<
"sat\n";
191 std::cout <<
"unsat\n";
196 std::cout <<
"error\n";
211 commands[
"get-unsat-assumptions"] = [
this]() {
212 throw error(
"not yet implemented");
216 std::vector<exprt> ops;
219 throw error(
"get-value expects list as argument");
228 throw error(
"get-value expects ')' at end of list");
231 throw error(
"model is not available");
233 std::vector<exprt> values;
234 values.reserve(ops.size());
236 for(
const auto &op : ops)
238 if(op.id() != ID_symbol)
239 throw error(
"get-value expects symbol");
243 const auto id_map_it =
id_map.find(identifier);
245 if(id_map_it ==
id_map.end())
246 throw error() <<
"unexpected symbol '" << identifier <<
'\'';
251 throw error() <<
"no value for '" << identifier <<
'\'';
253 values.push_back(value);
258 for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
271 if(
next_token() != smt2_tokenizert::STRING_LITERAL)
272 throw error(
"expected string literal");
279 commands[
"get-assignment"] = [
this]() {
283 throw error(
"model is not available");
295 if(value.is_constant())
300 std::cout <<
'\n' <<
' ';
302 std::cout <<
'(' <<
smt2_format(named_term.second.name) <<
' '
306 std::cout <<
')' <<
'\n';
313 throw error(
"model is not available");
321 for(
const auto &
id :
id_map)
326 if(value.is_not_nil())
331 std::cout <<
'\n' <<
' ';
333 std::cout <<
"(define-fun " <<
smt2_format(name) <<
' ';
335 if(
id.second.type.id() == ID_mathematical_function)
336 throw error(
"models for functions unimplemented");
343 std::cout <<
')' <<
'\n';
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 )
371 | ( get-info hinfo_flag i )
372 | ( get-option hkeywordi )
374 | ( get-unsat-assumptions )
379 | ( reset-assertions )
380 | ( set-info hattributei )
381 | ( set-option hoptioni )
388 void print(
unsigned level,
const std::string &message)
override
393 std::cout <<
"(error \"" << message <<
"\")\n";
395 std::cout <<
"; " << message <<
'\n';
408 std::cout << std::flush;
423 satcheckt satcheck{message_handler};
424 boolbvt boolbv{ns, satcheck, message_handler};
427 bool error_found =
false;
429 while(!smt2_solver.exit)
437 smt2_solver.skip_to_end_of_list();
444 smt2_solver.skip_to_end_of_list();
456 int main(
int argc,
const char *argv[])
463 std::cerr <<
"usage: smt2_solver file\n";
467 std::ifstream in(argv[1]);
470 std::cerr <<
"failed to open " << argv[1] <<
'\n';
Class that provides messages with a built-in verbosity 'level'.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void expand_function_applications(exprt &)
smt2_tokenizert::smt2_errort error()
void print(unsigned, const xmlt &) override
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.
std::set< irep_idt > constants_done
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Base class for all expressions.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
std::unordered_map< std::string, std::function< void()> > commands
Expression to hold a symbol (variable)
virtual void print(unsigned level, const std::string &message)=0
void set_line(const irep_idt &line)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
stack_decision_proceduret & solver
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
source_locationt source_location
const irep_idt & get_identifier() const
exprt simplify_expr(exprt src, const namespacet &ns)
enum smt2_solvert::@6 status
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
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 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...
unsigned get_line_no() const
smt2_solvert(std::istream &_in, stack_decision_proceduret &_solver)
void set_verbosity(unsigned _verbosity)
void print(unsigned, const jsont &) override
int solver(std::istream &in)
smt2_tokenizert::tokent next_token()
int main(int argc, const char *argv[])
virtual void pop()=0
Pop whatever is on top of the stack.
smt2_tokenizert smt2_tokenizer
void print(unsigned level, const std::string &message) override
std::string what() const override
A human readable description of what went wrong.
std::string what() const override
A human readable description of what went wrong.
A constant literal expression.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
void flush(unsigned) override
const std::string & get_buffer() const
Replace expression or type symbols by an expression or type, respectively.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...