cprover
invariant_sett Class Reference

#include <invariant_set.h>

Collaboration diagram for invariant_sett:
[legend]

Public Types

typedef std::set< std::pair< unsigned, unsigned > > ineq_sett
 
typedef interval_templatet< mp_integerboundst
 
typedef std::map< unsigned, boundstbounds_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_setstvalue_sets
 
inv_object_storetobject_store
 
const namespacetns
 

Detailed Description

Definition at line 77 of file invariant_set.h.

Member Typedef Documentation

◆ bounds_mapt

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

Definition at line 92 of file invariant_set.h.

◆ boundst

◆ ineq_sett

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

Definition at line 84 of file invariant_set.h.

Constructor & Destructor Documentation

◆ invariant_sett()

invariant_sett::invariant_sett ( )
inline

Definition at line 98 of file invariant_set.h.

Member Function Documentation

◆ add()

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

◆ add_bounds()

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

Definition at line 210 of file invariant_set.h.

References bounds_map.

Referenced by add_type_bounds(), and strengthen_rec().

◆ add_eq() [1/2]

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

◆ 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 239 of file invariant_set.cpp.

◆ add_le()

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

Definition at line 274 of file invariant_set.h.

References add(), and le_set.

Referenced by strengthen_rec().

◆ add_ne()

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

Definition at line 279 of file invariant_set.h.

References add(), and ne_set.

Referenced by strengthen_rec().

◆ add_type_bounds()

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

◆ apply_code()

void invariant_sett::apply_code ( const codet code)

◆ assignment()

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

◆ get_bounds()

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

◆ get_constant()

◆ get_object()

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

◆ has_eq()

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

Definition at line 233 of file invariant_set.h.

References eq_set, and unsigned_union_find::same_set().

Referenced by is_eq(), is_le(), and strengthen_rec().

◆ has_le()

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

Definition at line 238 of file invariant_set.h.

References le_set.

Referenced by is_le().

◆ has_ne()

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

Definition at line 243 of file invariant_set.h.

References ne_set.

Referenced by is_eq(), is_le(), and strengthen_rec().

◆ implies()

tvt invariant_sett::implies ( const exprt expr) const

Definition at line 591 of file invariant_set.cpp.

References implies_rec(), and nnf().

Referenced by invariant_propagationt::simplify().

◆ implies_rec()

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

◆ intersection()

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

Definition at line 163 of file invariant_set.h.

Referenced by make_union().

◆ is_eq()

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

Definition at line 277 of file invariant_set.cpp.

References has_eq(), has_ne(), and tvt::unknown().

Referenced by implies_rec(), is_ge(), is_lt(), and is_ne().

◆ is_ge()

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

Definition at line 256 of file invariant_set.h.

References is_eq(), and is_lt().

◆ is_gt()

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

Definition at line 262 of file invariant_set.h.

References is_le().

◆ is_le()

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

Definition at line 291 of file invariant_set.cpp.

References has_eq(), has_le(), has_ne(), and tvt::unknown().

Referenced by implies_rec(), is_gt(), and is_lt().

◆ is_lt()

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

Definition at line 251 of file invariant_set.h.

References is_eq(), and is_le().

Referenced by implies_rec(), and is_ge().

◆ is_ne()

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

Definition at line 267 of file invariant_set.h.

References is_eq().

Referenced by implies_rec().

◆ make_false()

void invariant_sett::make_false ( )
inline

◆ make_threaded()

void invariant_sett::make_threaded ( )
inline

Definition at line 132 of file invariant_set.h.

References make_true(), and threaded.

Referenced by make_union(), and invariant_set_domaint::transform().

◆ make_true()

◆ make_union()

◆ make_union_bounds_map()

bool invariant_sett::make_union_bounds_map ( const bounds_mapt other)
protected

Definition at line 959 of file invariant_set.cpp.

References bounds_map.

Referenced by make_union().

◆ modifies() [1/2]

void invariant_sett::modifies ( const exprt lhs)

◆ modifies() [2/2]

void invariant_sett::modifies ( unsigned  a)
protected

Definition at line 991 of file invariant_set.cpp.

References bounds_map, eq_set, unsigned_union_find::isolate(), le_set, and ne_set.

◆ nnf()

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

◆ output()

void invariant_sett::output ( const irep_idt identifier,
std::ostream &  out 
) const

◆ remove()

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

Definition at line 179 of file invariant_set.h.

◆ set_namespace()

void invariant_sett::set_namespace ( const namespacet _ns)
inline

Definition at line 158 of file invariant_set.h.

References ns.

Referenced by invariant_propagationt::initialize().

◆ set_object_store()

void invariant_sett::set_object_store ( inv_object_storet _object_store)
inline

Definition at line 153 of file invariant_set.h.

References object_store.

Referenced by invariant_propagationt::initialize().

◆ set_value_sets()

void invariant_sett::set_value_sets ( value_setst _value_sets)
inline

Definition at line 148 of file invariant_set.h.

References value_sets.

Referenced by invariant_propagationt::initialize().

◆ simplify()

void invariant_sett::simplify ( exprt expr) const

◆ strengthen()

void invariant_sett::strengthen ( const exprt expr)

Definition at line 383 of file invariant_set.cpp.

References nnf(), and strengthen_rec().

Referenced by assignment(), and invariant_set_domaint::transform().

◆ strengthen_rec()

◆ to_string()

std::string invariant_sett::to_string ( unsigned  a,
const irep_idt identifier 
) const
protected

Definition at line 900 of file invariant_set.cpp.

References object_store, PRECONDITION, and inv_object_storet::to_string().

Referenced by output().

Member Data Documentation

◆ bounds_map

bounds_mapt invariant_sett::bounds_map

◆ eq_set

unsigned_union_find invariant_sett::eq_set

◆ is_false

bool invariant_sett::is_false

Definition at line 96 of file invariant_set.h.

Referenced by implies_rec(), make_false(), make_true(), make_union(), output(), and strengthen_rec().

◆ le_set

ineq_sett invariant_sett::le_set

Definition at line 85 of file invariant_set.h.

Referenced by add_eq(), add_le(), has_le(), make_false(), make_true(), make_union(), modifies(), and output().

◆ ne_set

ineq_sett invariant_sett::ne_set

Definition at line 88 of file invariant_set.h.

Referenced by add_eq(), add_ne(), has_ne(), make_false(), make_true(), make_union(), modifies(), and output().

◆ ns

const namespacet* invariant_sett::ns
protected

Definition at line 202 of file invariant_set.h.

Referenced by assignment(), implies_rec(), set_namespace(), and strengthen_rec().

◆ object_store

inv_object_storet* invariant_sett::object_store
protected

◆ threaded

bool invariant_sett::threaded

Definition at line 95 of file invariant_set.h.

Referenced by make_threaded(), and make_union().

◆ value_sets

value_setst* invariant_sett::value_sets
protected

Definition at line 200 of file invariant_set.h.

Referenced by set_value_sets().


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