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 throw error(
"not yet implemented");
172 std::vector<exprt> ops;
175 throw error(
"get-value expects list as argument");
184 throw error(
"get-value expects ')' at end of list");
187 throw error(
"model is not available");
189 std::vector<exprt> values;
190 values.reserve(ops.size());
192 for(
const auto &op : ops)
194 if(op.id() != ID_symbol)
195 throw error(
"get-value expects symbol");
199 const auto id_map_it =
id_map.find(identifier);
201 if(id_map_it ==
id_map.end())
202 throw error() <<
"unexpected symbol '" << identifier <<
'\'';
207 throw error() <<
"no value for '" << identifier <<
'\'';
209 values.push_back(value);
214 for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
227 if(
next_token() != smt2_tokenizert::STRING_LITERAL)
228 throw error(
"expected string literal");
235 commands[
"get-assignment"] = [
this]() {
239 throw error(
"model is not available");
251 if(value.is_constant())
256 std::cout <<
'\n' <<
' ';
258 std::cout <<
'(' <<
smt2_format(named_term.second.name) <<
' '
262 std::cout <<
')' <<
'\n';
269 throw error(
"model is not available");
277 for(
const auto &
id :
id_map)
282 if(value.is_not_nil())
287 std::cout <<
'\n' <<
' ';
289 std::cout <<
"(define-fun " <<
smt2_format(name) <<
' ';
291 if(
id.second.type.id() == ID_mathematical_function)
292 throw error(
"models for functions unimplemented");
299 std::cout <<
')' <<
'\n';
317 | ( declare-
const hsymboli hsorti )
318 | ( declare-datatype hsymboli hdatatype_deci)
319 | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
320 | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
321 | ( declare-
sort hsymboli hnumerali )
322 | ( define-fun hfunction_def i )
323 | ( define-fun-rec hfunction_def i )
324 | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
325 | ( define-
sort hsymboli ( hsymboli ??? ) hsorti )
327 | ( get-info hinfo_flag i )
328 | ( get-option hkeywordi )
330 | ( get-unsat-assumptions )
335 | ( reset-assertions )
336 | ( set-info hattributei )
337 | ( set-option hoptioni )
349 std::cout <<
"(error \"" <<
message <<
"\")\n";
351 std::cout <<
"; " <<
message <<
'\n';
364 std::cout << std::flush;
379 satcheckt satcheck{message_handler};
380 boolbvt boolbv{ns, satcheck, message_handler};
383 bool error_found =
false;
385 while(!smt2_solver.exit)
393 smt2_solver.skip_to_end_of_list();
400 smt2_solver.skip_to_end_of_list();
412 int main(
int argc,
const char *argv[])
419 std::cerr <<
"usage: smt2_solver file\n";
423 std::ifstream in(argv[1]);
426 std::cerr <<
"failed to open " << argv[1] <<
'\n';
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
A constant literal expression.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
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.
Base class for all expressions.
const irep_idt & id() const
void set_verbosity(unsigned _verbosity)
virtual void print(unsigned level, const std::string &message)=0
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Replace expression or type symbols by an expression or type, respectively.
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...
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
std::unordered_map< std::string, std::function< void()> > commands
smt2_tokenizert::tokent next_token()
smt2_tokenizert::smt2_errort error()
smt2_tokenizert smt2_tokenizer
smt2_solvert(std::istream &_in, decision_proceduret &_solver)
enum smt2_solvert::@6 status
void expand_function_applications(exprt &)
std::set< irep_idt > constants_done
decision_proceduret & solver
std::string what() const override
A human readable description of what went wrong.
unsigned get_line_no() const
const std::string & get_buffer() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_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)
int solver(std::istream &in)
int main(int argc, const char *argv[])
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
static const char * message(const statust &status)
Makes a status message string from a status.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.