12 #ifndef CPROVER_ANALYSES_INVARIANT_SET_H 13 #define CPROVER_ANALYSES_INVARIANT_SET_H 32 bool get(
const exprt &expr,
unsigned &n);
52 void output(std::ostream &out)
const;
84 typedef std::set<std::pair<unsigned, unsigned> >
ineq_sett;
102 object_store(nullptr),
109 std::ostream &out)
const;
150 value_sets=&_value_sets;
155 object_store=&_object_store;
165 ineq_sett::iterator it_d=dest.begin();
167 while(it_d!=dest.end())
169 ineq_sett::iterator next_d(it_d);
172 if(other.find(*it_d)==other.end())
179 static void remove(ineq_sett &dest,
unsigned a)
181 for(ineq_sett::iterator it=dest.begin();
185 ineq_sett::iterator next(it);
188 if(it->first==a || it->second==a)
195 tvt implies(
const exprt &expr)
const;
204 tvt implies_rec(
const exprt &expr)
const;
205 static void nnf(
exprt &expr,
bool negate=
false);
206 void strengthen_rec(
const exprt &expr);
208 void add_type_bounds(
const exprt &expr,
const typet &type);
212 bounds_map[a].intersect_with(bound);
215 void get_bounds(
unsigned a, boundst &dest)
const;
218 bool make_union_bounds_map(
const bounds_mapt &other);
220 void modifies(
unsigned a);
233 bool has_eq(
const std::pair<unsigned, unsigned> &p)
const 235 return eq_set.
same_set(p.first, p.second);
238 bool has_le(
const std::pair<unsigned, unsigned> &p)
const 240 return le_set.find(p)!=le_set.end();
243 bool has_ne(
const std::pair<unsigned, unsigned> &p)
const 245 return ne_set.find(p)!=ne_set.end();
248 tvt is_eq(std::pair<unsigned, unsigned> p)
const;
249 tvt is_le(std::pair<unsigned, unsigned> p)
const;
253 return is_le(p) && !is_eq(p);
258 std::swap(p.first, p.second);
259 return is_eq(p) || is_lt(p);
272 void add(
const std::pair<unsigned, unsigned> &p, ineq_sett &dest);
274 void add_le(
const std::pair<unsigned, unsigned> &p)
279 void add_ne(
const std::pair<unsigned, unsigned> &p)
284 void add_eq(
const std::pair<unsigned, unsigned> &eq);
288 const std::pair<unsigned, unsigned> &eq,
289 const std::pair<unsigned, unsigned> &ineq);
292 #endif // CPROVER_ANALYSES_INVARIANT_SET_H The type of an expression.
tvt is_lt(std::pair< unsigned, unsigned > p) const
static bool is_constant_address(const exprt &expr)
static void intersection(ineq_sett &dest, const ineq_sett &other)
void add_ne(const std::pair< unsigned, unsigned > &p)
const exprt & get_expr(unsigned n) const
hash_numbering< irep_idt, irep_id_hash > mapt
std::string build_string(const exprt &expr) const
void add_bounds(unsigned a, const boundst &bound)
tvt is_gt(std::pair< unsigned, unsigned > p) const
void output(std::ostream &out) const
bool has_eq(const std::pair< unsigned, unsigned > &p) const
const irep_idt & operator[](unsigned n) const
void set_value_sets(value_setst &_value_sets)
unsigned add(const exprt &expr)
bool is_constant(unsigned n) const
tvt is_ge(std::pair< unsigned, unsigned > p) const
unsigned_union_find eq_set
std::map< unsigned, boundst > bounds_mapt
std::string to_string(unsigned n, const irep_idt &identifier) const
interval_templatet< mp_integer > boundst
tvt is_ne(std::pair< unsigned, unsigned > p) const
bool has_ne(const std::pair< unsigned, unsigned > &p) const
void set_object_store(inv_object_storet &_object_store)
Base class for all expressions.
inv_object_storet * object_store
static bool is_constant_address_rec(const exprt &expr)
std::vector< entryt > entries
std::set< std::pair< unsigned, unsigned > > ineq_sett
A statement in a programming language.
bool has_le(const std::pair< unsigned, unsigned > &p) const
bool same_set(size_type a, size_type b) const
inv_object_storet(const namespacet &_ns)
bool simplify(exprt &expr, const namespacet &ns)
void set_namespace(const namespacet &_ns)
void add_le(const std::pair< unsigned, unsigned > &p)