Go to the documentation of this file.
36 void command(
const std::string &)
override;
52 for(
const auto &
id :
id_map)
54 if(
id.second.type.id() == ID_mathematical_function)
57 if(
id.second.definition.is_nil())
60 const irep_idt &identifier =
id.first;
68 exprt def =
id.second.definition;
80 if(expr.
id()==ID_function_application)
85 irep_idt identifier=app.function().get_identifier();
86 auto f_it=
id_map.find(identifier);
90 const auto &f=f_it->second;
93 "type of function symbol must be mathematical_function_type");
98 const auto &domain = f_type.domain();
101 domain.size() == app.arguments().size(),
102 "number of function parameters");
106 std::map<irep_idt, exprt> parameter_map;
107 for(std::size_t i = 0; i < domain.size(); i++)
110 replace_symbol.
insert(s, app.arguments()[i]);
113 exprt body=f.definition;
114 replace_symbol(body);
133 else if(c ==
"check-sat")
141 std::cout <<
"sat\n";
146 std::cout <<
"unsat\n";
151 std::cout <<
"error\n";
155 else if(c ==
"check-sat-assuming")
157 throw error(
"not yet implemented");
159 else if(c ==
"display")
166 else if(c ==
"get-value")
168 std::vector<exprt> ops;
171 throw error(
"get-value expects list as argument");
177 throw error(
"get-value expects ')' at end of list");
180 throw error(
"model is not available");
182 std::vector<exprt> values;
183 values.reserve(ops.size());
185 for(
const auto &op : ops)
187 if(op.id() != ID_symbol)
188 throw error(
"get-value expects symbol");
192 const auto id_map_it =
id_map.find(identifier);
194 if(id_map_it ==
id_map.end())
195 throw error() <<
"unexpected symbol `" << identifier <<
'\'';
200 throw error() <<
"no value for `" << identifier <<
'\'';
202 values.push_back(value);
207 for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
221 throw error(
"expected string literal");
225 else if(c ==
"get-assignment")
230 throw error(
"model is not available");
242 if(value.is_constant())
247 std::cout <<
'\n' <<
' ';
249 std::cout <<
'(' <<
smt2_format(named_term.second.name) <<
' '
253 std::cout <<
')' <<
'\n';
255 else if(c ==
"get-model")
260 throw error(
"model is not available");
268 for(
const auto &
id :
id_map)
273 if(value.is_not_nil())
278 std::cout <<
'\n' <<
' ';
280 std::cout <<
"(define-fun " <<
smt2_format(name) <<
' ';
282 if(
id.second.type.id() == ID_mathematical_function)
283 throw error(
"models for functions unimplemented");
290 std::cout <<
')' <<
'\n';
292 else if(c ==
"simplify")
306 | ( declare-
const hsymboli hsorti )
307 | ( declare-datatype hsymboli hdatatype_deci)
308 | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
309 | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
310 | ( declare-
sort hsymboli hnumerali )
311 | ( define-fun hfunction_def i )
312 | ( define-fun-rec hfunction_def i )
313 | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
314 | ( define-
sort hsymboli ( hsymboli ??? ) hsorti )
316 | ( get-info hinfo_flag i )
317 | ( get-option hkeywordi )
319 | ( get-unsat-assumptions )
324 | (
reset-assertions )
325 | ( set-info hattributei )
326 | ( set-option hoptioni )
336 void print(
unsigned level,
const std::string &message)
override
341 std::cout <<
"(error \"" << message <<
"\")\n";
343 std::cout <<
"; " << message <<
'\n';
356 std::cout << std::flush;
373 satcheck.set_message_handler(message_handler);
378 bool error_found =
false;
380 while(!smt2_solver.
exit)
409 int main(
int argc,
const char *argv[])
416 std::cerr <<
"usage: smt2_solver file\n";
420 std::ifstream in(argv[1]);
423 std::cerr <<
"failed to open " << argv[1] <<
'\n';
virtual void command(const std::string &)
Class that provides messages with a built-in verbosity 'level'.
virtual exprt get(const exprt &expr) const =0
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void expand_function_applications(exprt &)
json_objectt json(const source_locationt &location)
static const commandt reset
return to default formatting, as defined by the terminal
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
tokent next_token() override
xmlt xml(const source_locationt &location)
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)
void print(unsigned level, const xmlt &xml) override
Expression to hold a symbol (variable)
exprt simplify_expr(const exprt &src, const namespacet &ns)
void command(const std::string &) override
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...
void print(unsigned level, const jsont &json) override
decision_proceduret & solver
smt2_errort error()
generate an error exception
source_locationt source_location
const irep_idt & get_identifier() const
enum smt2_solvert::@6 status
virtual void set_message_handler(message_handlert &_message_handler)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
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
void set_verbosity(unsigned _verbosity)
int solver(std::istream &in)
int main(int argc, const char *argv[])
void print(unsigned level, const std::string &message) override
smt2_solvert(std::istream &_in, decision_proceduret &_solver)
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.
void flush(unsigned) override
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
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...