33 for(
const auto &interval :
int_map)
35 if(interval.second.is_top())
37 if(interval.second.lower_set)
38 out << interval.second.lower <<
" <= ";
39 out << interval.first;
40 if(interval.second.upper_set)
41 out <<
" <= " << interval.second.upper;
47 if(interval.second.is_top())
49 if(interval.second.lower_set)
50 out << interval.second.lower <<
" <= ";
51 out << interval.first;
52 if(interval.second.upper_set)
53 out <<
" <= " << interval.second.upper;
64 const goto_programt::instructiont &instruction=*from;
65 switch(instruction.type)
86 assume(instruction.guard, ns);
91 assume(instruction.guard, ns);
134 for(int_mapt::iterator it=
int_map.begin();
139 const int_mapt::const_iterator b_it=b.
int_map.find(it->first);
148 it->second.
join(b_it->second);
149 if(it->second!=previous)
156 for(float_mapt::iterator it=
float_map.begin();
159 const float_mapt::const_iterator b_it=b.
float_map.begin();
168 it->second.
join(b_it->second);
169 if(it->second!=previous)
192 else if(lhs.
id()==ID_symbol)
201 else if(lhs.
id()==ID_typecast)
210 if(lhs.
id()==ID_typecast)
213 if(rhs.
id()==ID_typecast)
235 assert(
id==ID_lt ||
id==ID_le);
238 std::cout <<
"assume_rec: " 243 if(lhs.
id()==ID_symbol && rhs.
id()==ID_constant)
269 else if(lhs.
id()==ID_constant && rhs.
id()==ID_symbol)
295 else if(lhs.
id()==ID_symbol && rhs.
id()==ID_symbol)
332 if(cond.
id()==ID_lt || cond.
id()==ID_le ||
333 cond.
id()==ID_gt || cond.
id()==ID_ge ||
334 cond.
id()==ID_equal || cond.
id()==ID_notequal)
342 else if(cond.
id()==ID_le)
344 else if(cond.
id()==ID_gt)
346 else if(cond.
id()==ID_ge)
348 else if(cond.
id()==ID_equal)
350 else if(cond.
id()==ID_notequal)
356 else if(cond.
id()==ID_not)
360 else if(cond.
id()==ID_and)
366 else if(cond.
id()==ID_or)
462 if(condition.
id()==ID_and)
474 else if(condition.
id()==ID_symbol)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
void decrement(bool distinguish_zero=false)
const code_declt & to_code_decl(const codet &code)
static bool is_float(const typet &src)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
A generic base class for relations, i.e., binary predicates.
void havoc_rec(const exprt &)
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
void assume(const exprt &, const namespacet &)
void make_le_than(const T &v)
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void join(const interval_templatet< T > &i)
exprt conjunction(const exprt::operandst &op)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
The boolean constant true.
void assign(const class code_assignt &assignment)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
API to expression classes.
#define forall_operands(it, expr)
void assume_rec(const exprt &, bool negation=false)
void meet(const interval_templatet< T > &i)
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
exprt make_expression(const symbol_exprt &) const
The boolean constant false.
std::vector< exprt > operandst
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
void make_ge_than(const T &v)
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void increment(bool distinguish_zero=false)
goto_programt::const_targett locationt
Expression to hold a symbol (variable)
static bool is_int(const typet &src)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
const code_function_callt & to_code_function_call(const codet &code)