cprover
|
#include <invariant_set.h>
Public Types | |
typedef std::set< std::pair< unsigned, unsigned > > | ineq_sett |
typedef interval_templatet< mp_integer > | boundst |
typedef std::map< unsigned, boundst > | bounds_mapt |
Public Member Functions | |
invariant_sett () | |
void | output (const irep_idt &identifier, std::ostream &out) const |
bool | make_union (const invariant_sett &other_invariants) |
void | strengthen (const exprt &expr) |
void | make_true () |
void | make_false () |
void | make_threaded () |
void | apply_code (const codet &code) |
void | modifies (const exprt &lhs) |
void | assignment (const exprt &lhs, const exprt &rhs) |
void | set_value_sets (value_setst &_value_sets) |
void | set_object_store (inv_object_storet &_object_store) |
void | set_namespace (const namespacet &_ns) |
tvt | implies (const exprt &expr) const |
void | simplify (exprt &expr) const |
Static Public Member Functions | |
static void | intersection (ineq_sett &dest, const ineq_sett &other) |
static void | remove (ineq_sett &dest, unsigned a) |
Public Attributes | |
unsigned_union_find | eq_set |
ineq_sett | le_set |
ineq_sett | ne_set |
bounds_mapt | bounds_map |
bool | threaded |
bool | is_false |
Protected Member Functions | |
tvt | implies_rec (const exprt &expr) const |
void | strengthen_rec (const exprt &expr) |
void | add_type_bounds (const exprt &expr, const typet &type) |
void | add_bounds (unsigned a, const boundst &bound) |
void | get_bounds (unsigned a, boundst &dest) const |
bool | make_union_bounds_map (const bounds_mapt &other) |
void | modifies (unsigned a) |
std::string | to_string (unsigned a, const irep_idt &identifier) const |
bool | get_object (const exprt &expr, unsigned &n) const |
exprt | get_constant (const exprt &expr) const |
bool | has_eq (const std::pair< unsigned, unsigned > &p) const |
bool | has_le (const std::pair< unsigned, unsigned > &p) const |
bool | has_ne (const std::pair< unsigned, unsigned > &p) const |
tvt | is_eq (std::pair< unsigned, unsigned > p) const |
tvt | is_le (std::pair< unsigned, unsigned > p) const |
tvt | is_lt (std::pair< unsigned, unsigned > p) const |
tvt | is_ge (std::pair< unsigned, unsigned > p) const |
tvt | is_gt (std::pair< unsigned, unsigned > p) const |
tvt | is_ne (std::pair< unsigned, unsigned > p) const |
void | add (const std::pair< unsigned, unsigned > &p, ineq_sett &dest) |
void | add_le (const std::pair< unsigned, unsigned > &p) |
void | add_ne (const std::pair< unsigned, unsigned > &p) |
void | add_eq (const std::pair< unsigned, unsigned > &eq) |
void | add_eq (ineq_sett &dest, const std::pair< unsigned, unsigned > &eq, const std::pair< unsigned, unsigned > &ineq) |
Static Protected Member Functions | |
static void | nnf (exprt &expr, bool negate=false) |
Protected Attributes | |
value_setst * | value_sets |
inv_object_storet * | object_store |
const namespacet * | ns |
Definition at line 77 of file invariant_set.h.
typedef std::map<unsigned, boundst> invariant_sett::bounds_mapt |
Definition at line 92 of file invariant_set.h.
Definition at line 91 of file invariant_set.h.
typedef std::set<std::pair<unsigned, unsigned> > invariant_sett::ineq_sett |
Definition at line 84 of file invariant_set.h.
|
inline |
Definition at line 98 of file invariant_set.h.
|
protected |
Definition at line 188 of file invariant_set.cpp.
|
inlineprotected |
Definition at line 210 of file invariant_set.h.
|
protected |
Definition at line 210 of file invariant_set.cpp.
|
protected |
Definition at line 247 of file invariant_set.cpp.
|
inlineprotected |
Definition at line 274 of file invariant_set.h.
|
inlineprotected |
Definition at line 279 of file invariant_set.h.
Definition at line 371 of file invariant_set.cpp.
void invariant_sett::apply_code | ( | const codet & | code | ) |
Definition at line 1072 of file invariant_set.cpp.
Definition at line 1053 of file invariant_set.cpp.
|
protected |
Definition at line 686 of file invariant_set.cpp.
Definition at line 839 of file invariant_set.cpp.
|
protected |
Definition at line 156 of file invariant_set.cpp.
|
inlineprotected |
Definition at line 233 of file invariant_set.h.
|
inlineprotected |
Definition at line 238 of file invariant_set.h.
|
inlineprotected |
Definition at line 243 of file invariant_set.h.
Definition at line 595 of file invariant_set.cpp.
Definition at line 602 of file invariant_set.cpp.
Definition at line 163 of file invariant_set.h.
|
protected |
Definition at line 285 of file invariant_set.cpp.
|
inlineprotected |
Definition at line 256 of file invariant_set.h.
|
inlineprotected |
Definition at line 262 of file invariant_set.h.
|
protected |
Definition at line 299 of file invariant_set.cpp.
|
inlineprotected |
Definition at line 251 of file invariant_set.h.
|
inlineprotected |
Definition at line 267 of file invariant_set.h.
|
inline |
Definition at line 124 of file invariant_set.h.
|
inline |
Definition at line 132 of file invariant_set.h.
|
inline |
Definition at line 116 of file invariant_set.h.
bool invariant_sett::make_union | ( | const invariant_sett & | other_invariants | ) |
Definition at line 902 of file invariant_set.cpp.
|
protected |
Definition at line 953 of file invariant_set.cpp.
void invariant_sett::modifies | ( | const exprt & | lhs | ) |
Definition at line 993 of file invariant_set.cpp.
|
protected |
Definition at line 985 of file invariant_set.cpp.
|
staticprotected |
Definition at line 710 of file invariant_set.cpp.
void invariant_sett::output | ( | const irep_idt & | identifier, |
std::ostream & | out | ||
) | const |
Definition at line 317 of file invariant_set.cpp.
|
inlinestatic |
Definition at line 179 of file invariant_set.h.
|
inline |
Definition at line 158 of file invariant_set.h.
|
inline |
Definition at line 153 of file invariant_set.h.
|
inline |
Definition at line 148 of file invariant_set.h.
void invariant_sett::simplify | ( | exprt & | expr | ) | const |
Definition at line 821 of file invariant_set.cpp.
void invariant_sett::strengthen | ( | const exprt & | expr | ) |
Definition at line 391 of file invariant_set.cpp.
|
protected |
Definition at line 398 of file invariant_set.cpp.
|
protected |
Definition at line 894 of file invariant_set.cpp.
bounds_mapt invariant_sett::bounds_map |
Definition at line 93 of file invariant_set.h.
unsigned_union_find invariant_sett::eq_set |
Definition at line 81 of file invariant_set.h.
bool invariant_sett::is_false |
Definition at line 96 of file invariant_set.h.
ineq_sett invariant_sett::le_set |
Definition at line 85 of file invariant_set.h.
ineq_sett invariant_sett::ne_set |
Definition at line 88 of file invariant_set.h.
|
protected |
Definition at line 202 of file invariant_set.h.
|
protected |
Definition at line 201 of file invariant_set.h.
bool invariant_sett::threaded |
Definition at line 95 of file invariant_set.h.
|
protected |
Definition at line 200 of file invariant_set.h.