CBMC
Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
invariant_sett Class Reference

#include <invariant_set.h>

+ Collaboration diagram for invariant_sett:

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 (value_setst &_value_sets, inv_object_storet &_object_store, const namespacet &_ns)
 
void output (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)
 
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
 
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
 

Detailed Description

Definition at line 79 of file invariant_set.h.

Member Typedef Documentation

◆ bounds_mapt

typedef std::map<unsigned, boundst> invariant_sett::bounds_mapt

Definition at line 94 of file invariant_set.h.

◆ boundst

typedef interval_templatet<mp_integer> invariant_sett::boundst

Definition at line 93 of file invariant_set.h.

◆ ineq_sett

typedef std::set<std::pair<unsigned, unsigned> > invariant_sett::ineq_sett

Definition at line 86 of file invariant_set.h.

Constructor & Destructor Documentation

◆ invariant_sett()

invariant_sett::invariant_sett ( value_setst &  _value_sets,
inv_object_storet &  _object_store,
const namespacet &  _ns 
)
inline

Definition at line 100 of file invariant_set.h.

Member Function Documentation

◆ add()

void invariant_sett::add ( const std::pair< unsigned, unsigned > &  p,
ineq_sett &  dest 
)
protected

Definition at line 181 of file invariant_set.cpp.

◆ add_bounds()

void invariant_sett::add_bounds ( unsigned  a,
const boundst &  bound 
)
inlineprotected

Definition at line 198 of file invariant_set.h.

◆ add_eq() [1/2]

void invariant_sett::add_eq ( const std::pair< unsigned, unsigned > &  eq)
protected

Definition at line 203 of file invariant_set.cpp.

◆ add_eq() [2/2]

void invariant_sett::add_eq ( ineq_sett &  dest,
const std::pair< unsigned, unsigned > &  eq,
const std::pair< unsigned, unsigned > &  ineq 
)
protected

Definition at line 240 of file invariant_set.cpp.

◆ add_le()

void invariant_sett::add_le ( const std::pair< unsigned, unsigned > &  p)
inlineprotected

Definition at line 260 of file invariant_set.h.

◆ add_ne()

void invariant_sett::add_ne ( const std::pair< unsigned, unsigned > &  p)
inlineprotected

Definition at line 265 of file invariant_set.h.

◆ add_type_bounds()

void invariant_sett::add_type_bounds ( const exprt &  expr,
const typet &  type 
)
protected

Definition at line 353 of file invariant_set.cpp.

◆ apply_code()

void invariant_sett::apply_code ( const codet &  code)

Definition at line 1052 of file invariant_set.cpp.

◆ assignment()

void invariant_sett::assignment ( const exprt &  lhs,
const exprt &  rhs 
)

Definition at line 1035 of file invariant_set.cpp.

◆ get_bounds()

void invariant_sett::get_bounds ( unsigned  a,
boundst &  dest 
) const
protected

Definition at line 675 of file invariant_set.cpp.

◆ get_constant()

exprt invariant_sett::get_constant ( const exprt &  expr) const
protected

Definition at line 831 of file invariant_set.cpp.

◆ get_object()

bool invariant_sett::get_object ( const exprt &  expr,
unsigned &  n 
) const
protected

Definition at line 150 of file invariant_set.cpp.

◆ has_eq()

bool invariant_sett::has_eq ( const std::pair< unsigned, unsigned > &  p) const
inlineprotected

Definition at line 219 of file invariant_set.h.

◆ has_le()

bool invariant_sett::has_le ( const std::pair< unsigned, unsigned > &  p) const
inlineprotected

Definition at line 224 of file invariant_set.h.

◆ has_ne()

bool invariant_sett::has_ne ( const std::pair< unsigned, unsigned > &  p) const
inlineprotected

Definition at line 229 of file invariant_set.h.

◆ implies()

tvt invariant_sett::implies ( const exprt &  expr) const

Definition at line 580 of file invariant_set.cpp.

◆ implies_rec()

tvt invariant_sett::implies_rec ( const exprt &  expr) const
protected

Definition at line 587 of file invariant_set.cpp.

◆ intersection()

static void invariant_sett::intersection ( ineq_sett &  dest,
const ineq_sett &  other 
)
inlinestatic

Definition at line 151 of file invariant_set.h.

◆ is_eq()

tvt invariant_sett::is_eq ( std::pair< unsigned, unsigned >  p) const
protected

Definition at line 278 of file invariant_set.cpp.

◆ is_ge()

tvt invariant_sett::is_ge ( std::pair< unsigned, unsigned >  p) const
inlineprotected

Definition at line 242 of file invariant_set.h.

◆ is_gt()

tvt invariant_sett::is_gt ( std::pair< unsigned, unsigned >  p) const
inlineprotected

Definition at line 248 of file invariant_set.h.

◆ is_le()

tvt invariant_sett::is_le ( std::pair< unsigned, unsigned >  p) const
protected

Definition at line 292 of file invariant_set.cpp.

◆ is_lt()

tvt invariant_sett::is_lt ( std::pair< unsigned, unsigned >  p) const
inlineprotected

Definition at line 237 of file invariant_set.h.

◆ is_ne()

tvt invariant_sett::is_ne ( std::pair< unsigned, unsigned >  p) const
inlineprotected

Definition at line 253 of file invariant_set.h.

◆ make_false()

void invariant_sett::make_false ( )
inline

Definition at line 127 of file invariant_set.h.

◆ make_threaded()

void invariant_sett::make_threaded ( )
inline

Definition at line 135 of file invariant_set.h.

◆ make_true()

void invariant_sett::make_true ( )
inline

Definition at line 119 of file invariant_set.h.

◆ make_union()

bool invariant_sett::make_union ( const invariant_sett &  other_invariants)

Definition at line 890 of file invariant_set.cpp.

◆ make_union_bounds_map()

bool invariant_sett::make_union_bounds_map ( const bounds_mapt &  other)
protected

Definition at line 941 of file invariant_set.cpp.

◆ modifies() [1/2]

void invariant_sett::modifies ( const exprt &  lhs)

Definition at line 981 of file invariant_set.cpp.

◆ modifies() [2/2]

void invariant_sett::modifies ( unsigned  a)
protected

Definition at line 973 of file invariant_set.cpp.

◆ nnf()

void invariant_sett::nnf ( exprt &  expr,
bool  negate = false 
)
staticprotected

Definition at line 699 of file invariant_set.cpp.

◆ output()

void invariant_sett::output ( std::ostream &  out) const

Definition at line 310 of file invariant_set.cpp.

◆ remove()

static void invariant_sett::remove ( ineq_sett &  dest,
unsigned  a 
)
inlinestatic

Definition at line 167 of file invariant_set.h.

◆ simplify()

void invariant_sett::simplify ( exprt &  expr) const

Definition at line 813 of file invariant_set.cpp.

◆ strengthen()

void invariant_sett::strengthen ( const exprt &  expr)

Definition at line 375 of file invariant_set.cpp.

◆ strengthen_rec()

void invariant_sett::strengthen_rec ( const exprt &  expr)
protected

Definition at line 382 of file invariant_set.cpp.

◆ to_string()

std::string invariant_sett::to_string ( unsigned  a) const
protected

Definition at line 885 of file invariant_set.cpp.

Member Data Documentation

◆ bounds_map

bounds_mapt invariant_sett::bounds_map

Definition at line 95 of file invariant_set.h.

◆ eq_set

unsigned_union_find invariant_sett::eq_set

Definition at line 83 of file invariant_set.h.

◆ is_false

bool invariant_sett::is_false

Definition at line 98 of file invariant_set.h.

◆ le_set

ineq_sett invariant_sett::le_set

Definition at line 87 of file invariant_set.h.

◆ ne_set

ineq_sett invariant_sett::ne_set

Definition at line 90 of file invariant_set.h.

◆ ns

const namespacet& invariant_sett::ns
protected

Definition at line 190 of file invariant_set.h.

◆ object_store

inv_object_storet& invariant_sett::object_store
protected

Definition at line 189 of file invariant_set.h.

◆ threaded

bool invariant_sett::threaded

Definition at line 97 of file invariant_set.h.

◆ value_sets

value_setst& invariant_sett::value_sets
protected

Definition at line 188 of file invariant_set.h.

The documentation for this class was generated from the following files: