37 void command(
const std::string &)
override;
46 for(
const auto &op : expr.
operands())
49 if(expr.
id()==ID_symbol)
59 auto f_it=
id_map.find(identifier);
63 const auto &f=f_it->second;
65 if(f.type.id()!=ID_mathematical_function &&
66 f.definition.is_not_nil())
68 exprt def=f.definition;
82 if(expr.
id()==ID_function_application)
87 irep_idt identifier=app.function().get_identifier();
88 auto f_it=
id_map.find(identifier);
92 const auto &f=f_it->second;
95 "type of function symbol must be mathematical_function_type");
101 app.arguments().size(),
102 "number of function parameters");
106 std::map<irep_idt, exprt> parameter_map;
107 for(std::size_t i=0; i<f_type.domain().size(); i++)
110 f_type.domain()[i].get_identifier();
112 replace_symbol.insert(p_identifier, app.arguments()[i]);
115 exprt body=f.definition;
116 replace_symbol(body);
137 else if(c==
"check-sat")
142 std::cout <<
"sat\n";
146 std::cout <<
"unsat\n";
150 std::cout <<
"error\n";
153 else if(c==
"check-sat-assuming")
155 std::cout <<
"not yet implemented\n";
157 else if(c==
"display")
163 std::cout << e.
pretty() <<
'\n';
166 else if(c==
"simplify")
175 std::cout << e.
pretty() <<
'\n';
180 | ( declare-
const hsymboli hsorti )
181 | ( declare-datatype hsymboli hdatatype_deci)
182 | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
183 | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
184 | ( declare-
sort hsymboli hnumerali )
185 | ( define-fun hfunction_def i )
186 | ( define-fun-rec hfunction_def i )
187 | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
188 | ( define-
sort hsymboli ( hsymboli ??? ) hsorti )
193 | (
get-info hinfo_flag i )
195 | (
get-option hkeywordi )
197 | (
get-unsat-assumptions )
199 | (
get-value ( htermi + ) )
203 | ( reset-assertions )
204 | (
set-info hattributei )
205 | (
set-option hoptioni )
210 catch(
const char *
error)
212 std::cout <<
"error: " <<
error <<
'\n';
214 catch(
const std::string &
error)
216 std::cout <<
"error: " <<
error <<
'\n';
247 int main(
int argc,
const char *argv[])
254 std::cerr <<
"usage: smt2_solver file\n";
258 std::ifstream in(argv[1]);
261 std::cerr <<
"failed to open " << argv[1] <<
'\n';
smt2_solvert(std::istream &_in, decision_proceduret &_solver)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const irep_idt & get_identifier() const
void define_constants(const exprt &)
const irep_idt & id() const
int solver(std::istream &in)
void expand_function_applications(exprt &)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
virtual void set_message_handler(message_handlert &_message_handler)
std::set< irep_idt > constants_done
int main(int argc, const char *argv[])
virtual void command(const std::string &)
Base class for all expressions.
void set_to_true(const exprt &expr)
void command(const std::string &) override
goto_programt coverage_criteriont message_handlert & message_handler
decision_proceduret & solver
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a generic typet to a mathematical_function_typet.
#define DATA_INVARIANT(CONDITION, REASON)