cprover
arrayst Class Referenceabstract

#include <arrays.h>

Inheritance diagram for arrayst:
[legend]
Collaboration diagram for arrayst:
[legend]

Classes

struct  array_equalityt
 
struct  lazy_constraintt
 

Public Types

typedef equalityt SUB
 
- Public Types inherited from prop_conv_solvert
typedef std::map< irep_idt, literaltsymbolst
 
typedef std::unordered_map< exprt, literalt, irep_hashcachet
 
- Public Types inherited from decision_proceduret
enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

 arrayst (const namespacet &_ns, propt &_prop)
 
void post_process () override
 
literalt record_array_equality (const equal_exprt &expr)
 
void record_array_index (const index_exprt &expr)
 
- Public Member Functions inherited from equalityt
 equalityt (const namespacet &_ns, propt &_prop)
 
virtual literalt equality (const exprt &e1, const exprt &e2)
 
void post_process () override
 
- Public Member Functions inherited from prop_conv_solvert
 prop_conv_solvert (const namespacet &_ns, propt &_prop)
 
virtual ~prop_conv_solvert ()
 
virtual void set_to (const exprt &expr, bool value) override
 
virtual decision_proceduret::resultt dec_solve () override
 
virtual void print_assignment (std::ostream &out) const override
 
virtual std::string decision_procedure_text () const override
 
virtual exprt get (const exprt &expr) const override
 
virtual tvt l_get (literalt a) const override
 
virtual void set_frozen (literalt a) override
 
virtual void set_assumptions (const bvt &_assumptions) override
 
virtual bool has_set_assumptions () const override
 
virtual void set_all_frozen () override
 
virtual literalt convert (const exprt &expr) override
 
virtual bool is_in_conflict (literalt l) const override
 determine whether a variable is in the final conflict More...
 
virtual bool has_is_in_conflict () const override
 
virtual bool literal (const exprt &expr, literalt &literal) const
 
virtual void clear_cache ()
 
const cachetget_cache () const
 
const symbolstget_symbols () const
 
- Public Member Functions inherited from prop_convt
 prop_convt (const namespacet &_ns)
 
virtual ~prop_convt ()
 
literalt operator() (const exprt &expr)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from decision_proceduret
 decision_proceduret (const namespacet &_ns)
 
void set_to_true (const exprt &expr)
 
void set_to_false (const exprt &expr)
 
resultt operator() ()
 
virtual bool in_core (const exprt &expr)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Protected Types

enum  lazy_typet {
  lazy_typet::ARRAY_ACKERMANN, lazy_typet::ARRAY_WITH, lazy_typet::ARRAY_IF, lazy_typet::ARRAY_OF,
  lazy_typet::ARRAY_TYPECAST
}
 
typedef std::list< array_equalitytarray_equalitiest
 
typedef std::set< exprtindex_sett
 
typedef std::map< std::size_t, index_settindex_mapt
 
- Protected Types inherited from equalityt
typedef std::unordered_map< const exprt, unsigned, irep_hashelementst
 
typedef std::map< std::pair< unsigned, unsigned >, literaltequalitiest
 
typedef std::map< unsigned, exprtelements_revt
 
typedef std::unordered_map< const typet, typestructt, irep_hashtypemapt
 

Protected Member Functions

virtual void post_process_arrays ()
 
void add_array_constraint (const lazy_constraintt &lazy, bool refine=true)
 adds array constraints (refine=true...lazily for the refinement loop) More...
 
void add_array_constraints ()
 
void add_array_Ackermann_constraints ()
 
void add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality)
 
void add_array_constraints (const index_sett &index_set, const exprt &expr)
 
void add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt)
 
void add_array_constraints_with (const index_sett &index_set, const with_exprt &expr)
 
void add_array_constraints_update (const index_sett &index_set, const update_exprt &expr)
 
void add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt)
 
void update_index_map (bool update_all)
 
void update_index_map (std::size_t i)
 merge the indices into the root More...
 
void collect_arrays (const exprt &a)
 
void collect_indices ()
 
void collect_indices (const exprt &a)
 
virtual bool is_unbounded_array (const typet &type) const =0
 
- Protected Member Functions inherited from equalityt
virtual literalt equality2 (const exprt &e1, const exprt &e2)
 
virtual void add_equality_constraints ()
 
virtual void add_equality_constraints (const typestructt &typestruct)
 
- Protected Member Functions inherited from prop_conv_solvert
virtual bool get_bool (const exprt &expr, tvt &value) const
 get a boolean value from counter example if not valid More...
 
virtual literalt convert_rest (const exprt &expr)
 
virtual literalt convert_bool (const exprt &expr)
 
virtual bool set_equality_to_true (const equal_exprt &expr)
 
virtual literalt get_literal (const irep_idt &symbol)
 
virtual void ignoring (const exprt &expr)
 

Protected Attributes

array_equalitiest array_equalities
 
union_find< exprtarrays
 
index_mapt index_map
 
bool lazy_arrays
 
bool incremental_cache
 
std::list< lazy_constrainttlazy_array_constraints
 
std::map< exprt, bool > expr_map
 
std::set< std::size_t > update_indices
 
- Protected Attributes inherited from equalityt
typemapt typemap
 
- Protected Attributes inherited from prop_conv_solvert
bool post_processing_done
 
symbolst symbols
 
cachet cache
 
proptprop
 
- Protected Attributes inherited from decision_proceduret
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Public Attributes inherited from prop_conv_solvert
bool use_cache
 
bool equality_propagation
 
bool freeze_all
 

Detailed Description

Definition at line 28 of file arrays.h.

Member Typedef Documentation

§ array_equalitiest

typedef std::list<array_equalityt> arrayst::array_equalitiest
protected

Definition at line 60 of file arrays.h.

§ index_mapt

typedef std::map<std::size_t, index_sett> arrayst::index_mapt
protected

Definition at line 70 of file arrays.h.

§ index_sett

typedef std::set<exprt> arrayst::index_sett
protected

Definition at line 67 of file arrays.h.

§ SUB

Definition at line 40 of file arrays.h.

Member Enumeration Documentation

§ lazy_typet

enum arrayst::lazy_typet
strongprotected
Enumerator
ARRAY_ACKERMANN 
ARRAY_WITH 
ARRAY_IF 
ARRAY_OF 
ARRAY_TYPECAST 

Definition at line 74 of file arrays.h.

Constructor & Destructor Documentation

§ arrayst()

arrayst::arrayst ( const namespacet _ns,
propt _prop 
)

Definition at line 24 of file arrays.cpp.

References incremental_cache, and lazy_arrays.

Member Function Documentation

§ add_array_Ackermann_constraints()

§ add_array_constraint()

void arrayst::add_array_constraint ( const lazy_constraintt lazy,
bool  refine = true 
)
protected

§ add_array_constraints() [1/2]

§ add_array_constraints() [2/2]

§ add_array_constraints_array_of()

void arrayst::add_array_constraints_array_of ( const index_sett index_set,
const array_of_exprt exprt 
)
protected

§ add_array_constraints_equality()

void arrayst::add_array_constraints_equality ( const index_sett index_set,
const array_equalityt array_equality 
)
protected

§ add_array_constraints_if()

§ add_array_constraints_update()

§ add_array_constraints_with()

§ collect_arrays()

§ collect_indices() [1/2]

void arrayst::collect_indices ( )
protected

Definition at line 70 of file arrays.cpp.

References arrays.

Referenced by add_array_constraints(), collect_indices(), and bv_refinementt::post_process_arrays().

§ collect_indices() [2/2]

§ is_unbounded_array()

virtual bool arrayst::is_unbounded_array ( const typet type) const
protectedpure virtual

Implemented in boolbvt.

Referenced by collect_indices().

§ post_process()

void arrayst::post_process ( )
inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Reimplemented in boolbvt, and bv_pointerst.

Definition at line 33 of file arrays.h.

References equalityt::post_process(), and post_process_arrays().

Referenced by boolbvt::post_process().

§ post_process_arrays()

virtual void arrayst::post_process_arrays ( )
inlineprotectedvirtual

Reimplemented in bv_refinementt.

Definition at line 46 of file arrays.h.

References add_array_constraints().

Referenced by post_process().

§ record_array_equality()

§ record_array_index()

void arrayst::record_array_index ( const index_exprt expr)

§ update_index_map() [1/2]

void arrayst::update_index_map ( bool  update_all)
protected

§ update_index_map() [2/2]

void arrayst::update_index_map ( std::size_t  i)
protected

merge the indices into the root

Definition at line 346 of file arrays.cpp.

References arrays, union_find< T >::find_number(), index_map, and union_find< T >::is_root_number().

Member Data Documentation

§ array_equalities

array_equalitiest arrayst::array_equalities
protected

Definition at line 61 of file arrays.h.

Referenced by add_array_constraints(), and record_array_equality().

§ arrays

§ expr_map

std::map<exprt, bool> arrayst::expr_map
protected

Definition at line 99 of file arrays.h.

Referenced by add_array_constraint().

§ incremental_cache

bool arrayst::incremental_cache
protected

Definition at line 96 of file arrays.h.

Referenced by add_array_constraint(), and arrayst().

§ index_map

§ lazy_array_constraints

std::list<lazy_constraintt> arrayst::lazy_array_constraints
protected

§ lazy_arrays

bool arrayst::lazy_arrays
protected

§ update_indices

std::set<std::size_t> arrayst::update_indices
protected

Definition at line 119 of file arrays.h.

Referenced by record_array_index(), and update_index_map().


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