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';
unsigned get_line_no() const
void flush(unsigned) override
void skip_to_end_of_list()
This skips tokens until all bracketed expressions are closed.
smt2_solvert(std::istream &_in, decision_proceduret &_solver)
exprt simplify_expr(const exprt &src, const namespacet &ns)
const irep_idt & get_identifier() const
virtual exprt get(const exprt &expr) const =0
void print(unsigned level, const jsont &json) override
std::string what() const override
A human readable description of what went wrong.
A constant literal expression.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
xmlt xml(const source_locationt &location)
static const commandt reset
return to default formatting, as defined by the terminal
void print(unsigned level, const xmlt &xml) override
const irep_idt & id() const
std::string what() const override
A human readable description of what went wrong.
Replace expression or type symbols by an expression or type, respectively.
int solver(std::istream &in)
void expand_function_applications(exprt &)
source_locationt source_location
tokent next_token() override
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
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...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
virtual void set_message_handler(message_handlert &_message_handler)
std::set< irep_idt > constants_done
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
int main(int argc, const char *argv[])
virtual void command(const std::string &)
mstreamt & status() const
Base class for all expressions.
void set_to_true(const exprt &expr)
void print(unsigned level, const std::string &message) override
smt2_errort error()
generate an error exception
void command(const std::string &) override
void set_verbosity(unsigned _verbosity)
Expression to hold a symbol (variable)
decision_proceduret & solver
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
json_objectt json(const source_locationt &location)
virtual void print(unsigned level, const std::string &message)=0