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");
107 for(std::size_t i = 0; i < domain.size(); i++)
110 symbol_exprt(f.parameters[i], domain[i]), app.arguments()[i]);
113 exprt body = f.definition;
114 replace_symbol(body);
141 std::cout <<
"sat\n";
146 std::cout <<
"unsat\n";
151 std::cout <<
"error\n";
156 commands[
"check-sat-assuming"] = [
this]() {
157 throw error(
"not yet implemented");
168 std::vector<exprt> ops;
171 throw error(
"get-value expects list as argument");
180 throw error(
"get-value expects ')' at end of list");
183 throw error(
"model is not available");
185 std::vector<exprt> values;
186 values.reserve(ops.size());
188 for(
const auto &op : ops)
190 if(op.id() != ID_symbol)
191 throw error(
"get-value expects symbol");
195 const auto id_map_it =
id_map.find(identifier);
197 if(id_map_it ==
id_map.end())
198 throw error() <<
"unexpected symbol '" << identifier <<
'\'';
203 throw error() <<
"no value for '" << identifier <<
'\'';
205 values.push_back(value);
210 for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
223 if(
next_token() != smt2_tokenizert::STRING_LITERAL)
224 throw error(
"expected string literal");
231 commands[
"get-assignment"] = [
this]() {
235 throw error(
"model is not available");
247 if(value.is_constant())
252 std::cout <<
'\n' <<
' ';
254 std::cout <<
'(' <<
smt2_format(named_term.second.name) <<
' '
258 std::cout <<
')' <<
'\n';
265 throw error(
"model is not available");
273 for(
const auto &
id :
id_map)
278 if(value.is_not_nil())
283 std::cout <<
'\n' <<
' ';
285 std::cout <<
"(define-fun " <<
smt2_format(name) <<
' ';
287 if(
id.second.type.id() == ID_mathematical_function)
288 throw error(
"models for functions unimplemented");
295 std::cout <<
')' <<
'\n';
313 | ( declare-
const hsymboli hsorti )
314 | ( declare-datatype hsymboli hdatatype_deci)
315 | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
316 | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
317 | ( declare-
sort hsymboli hnumerali )
318 | ( define-fun hfunction_def i )
319 | ( define-fun-rec hfunction_def i )
320 | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
321 | ( define-
sort hsymboli ( hsymboli ??? ) hsorti )
323 | ( get-info hinfo_flag i )
324 | ( get-option hkeywordi )
326 | ( get-unsat-assumptions )
331 | ( reset-assertions )
332 | ( set-info hattributei )
333 | ( set-option hoptioni )
345 std::cout <<
"(error \"" <<
message <<
"\")\n";
347 std::cout <<
"; " <<
message <<
'\n';
360 std::cout << std::flush;
375 satcheckt satcheck{message_handler};
376 boolbvt boolbv{ns, satcheck, message_handler};
379 bool error_found =
false;
381 while(!smt2_solver.exit)
389 smt2_solver.skip_to_end_of_list();
396 smt2_solver.skip_to_end_of_list();
408 int main(
int argc,
const char *argv[])
415 std::cerr <<
"usage: smt2_solver file\n";
419 std::ifstream in(argv[1]);
422 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
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
decision_proceduret & solver
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const irep_idt & get_identifier() const
enum smt2_solvert::@4 status
exprt simplify_expr(exprt src, const namespacet &ns)
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)
void print(unsigned, const jsont &) override
int solver(std::istream &in)
smt2_tokenizert::tokent next_token()
int main(int argc, const char *argv[])
smt2_tokenizert smt2_tokenizer
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.
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...