static bool is_float(const typet &src)
std::map< irep_idt, integer_intervalt > int_mapt
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
void havoc_rec(const exprt &)
interval_templatet< mp_integer > integer_intervalt
void assume(const exprt &, const namespacet &)
ieee_float_intervalt get_float_rec(const exprt &)
std::map< irep_idt, ieee_float_intervalt > float_mapt
void assign(const class code_assignt &assignment)
bool merge(const interval_domaint &b, locationt from, locationt to)
integer_intervalt get_int_rec(const exprt &)
interval_templatet< ieee_floatt > ieee_float_intervalt
void assume_rec(const exprt &, bool negation=false)
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
exprt make_expression(const symbol_exprt &) const
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
goto_programt::const_targett locationt
static bool is_int(const typet &src)