Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

void set_frozen (literalt)

void set_frozen (const bvt &)

void set_all_frozen ()

literalt convert (const exprt &expr) override

Convert a Boolean expression and return the corresponding literal.

bool is_in_conflict (const exprt &expr) const override

Returns true if an expression is in the final conflict leading to UNSAT.

void set_to (const exprt &expr, bool value) override

For a Boolean expression expr, add the constraint 'current_context => expr' if value is true, otherwise add 'current_context => not expr'.

void push () override

Push a new context on the stack This context becomes a child context nested in the current context.

void push (const std::vector< exprt > &assumptions) override

Push assumptions in form of literal_exprt

void pop () override

Pop whatever is on top of the stack.

virtual void clear_cache ()

const cachet & get_cache () const

const symbolst & get_symbols () const

void set_time_limit_seconds (uint32_t lim) override

Set the limit for the solver to time out in seconds.

std::size_t get_number_of_solver_calls () const override

Return the number of incremental solver calls.

hardness_collectort * get_hardness_collector ()

- Public Member Functions inherited from conflict_providert

virtual ~conflict_providert ()=default

- Public Member Functions inherited from prop_convt

virtual ~prop_convt ()

- Public Member Functions inherited from stack_decision_proceduret

virtual ~stack_decision_proceduret ()=default

- Public Member Functions inherited from decision_proceduret

void set_to_true (const exprt &)

For a Boolean expression expr, add the constraint 'expr'.

void set_to_false (const exprt &)

For a Boolean expression expr, add the constraint 'not expr'.

resultt operator() ()

Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.

resultt operator() (const exprt &assumption)

Run the decision procedure to solve the problem under the given assumption.

virtual ~decision_proceduret ()

- Public Member Functions inherited from solver_resource_limitst

virtual ~solver_resource_limitst ()=default

Protected Types

enum class lazy_typet {
ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF ,
ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_LET
}

enum class constraint_typet {
  ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF ,
  ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_EQUALITY ,
  ARRAY_LET
}

typedef std::list< array_equalityt > array_equalitiest

typedef std::set< exprt > index_sett

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

typedef std::map< constraint_typet, size_t > array_constraint_countt

- Protected Types inherited from equalityt

typedef std::unordered_map< const exprt, unsigned, irep_hash > elementst

typedef std::map< std::pair< unsigned, unsigned >, literalt > equalitiest

typedef std::map< unsigned, exprt > elements_revt

typedef std::unordered_map< const typet, typestructt, irep_hash > typemapt

Protected Member Functions

virtual void finish_eager_conversion_arrays ()

void add_array_constraint (const lazy_constraintt &lazy, bool refine=true)

adds array constraints (refine=true...lazily for the refinement loop)

void display_array_constraint_count ()

std::string enum_to_string (constraint_typet)

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 add_array_constraints_array_constant (const index_sett &index_set, const array_exprt &exprt)

void add_array_constraints_comprehension (const index_sett &index_set, const array_comprehension_exprt &expr)

void update_index_map (bool update_all)

void update_index_map (std::size_t i)

merge the indices into the root

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 std::optional< bool > get_bool (const exprt &expr) const

Get a boolean value from the model if the formula is satisfiable.

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

const namespacet & ns

messaget log

message_handlert & message_handler

array_equalitiest array_equalities

union_find< exprt, irep_hash > arrays

index_mapt index_map

bool lazy_arrays

bool incremental_cache

bool get_array_constraints

std::list< lazy_constraintt > lazy_array_constraints

std::map< exprt, bool > expr_map

array_constraint_countt array_constraint_count

std::set< std::size_t > update_indices

std::unordered_set< irep_idt > array_comprehension_args

- Protected Attributes inherited from equalityt

typemapt typemap

- Protected Attributes inherited from prop_conv_solvert

bool post_processing_done = false

symbolst symbols

cachet cache

propt & prop

messaget log

bvt assumption_stack

Assumptions on the stack.

std::size_t context_literal_counter = 0

To generate unique literal names for contexts.

std::vector< size_t > context_size_stack

assumption_stack is segmented in contexts; Number of assumptions in each context on the stack

Additional Inherited Members

- Public Attributes inherited from prop_conv_solvert

bool use_cache = true

bool equality_propagation = true

bool freeze_all = false

- Static Protected Attributes inherited from prop_conv_solvert

static const char * context_prefix = "prop_conv::context$"

Detailed Description

Definition at line 33 of file arrays.h.

Member Typedef Documentation

◆ array_constraint_countt

typedef std::map<constraint_typet, size_t> arrayst::array_constraint_countt

protected

Definition at line 141 of file arrays.h.

◆ array_equalitiest

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

protected

Definition at line 83 of file arrays.h.

◆ index_mapt

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

protected

Definition at line 93 of file arrays.h.

◆ index_sett

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

protected

Definition at line 90 of file arrays.h.

◆ SUB

typedef equalityt arrayst::SUB

Definition at line 51 of file arrays.h.

Member Enumeration Documentation

◆ constraint_typet

enum class arrayst::constraint_typet

strongprotected

Enumerator
ARRAY_ACKERMANN
ARRAY_WITH
ARRAY_IF
ARRAY_OF
ARRAY_TYPECAST
ARRAY_CONSTANT
ARRAY_COMPREHENSION
ARRAY_EQUALITY
ARRAY_LET

Definition at line 128 of file arrays.h.

◆ lazy_typet

enum class arrayst::lazy_typet

strongprotected

Enumerator
ARRAY_ACKERMANN
ARRAY_WITH
ARRAY_IF
ARRAY_OF
ARRAY_TYPECAST
ARRAY_CONSTANT
ARRAY_COMPREHENSION
ARRAY_LET

Definition at line 97 of file arrays.h.

Constructor & Destructor Documentation

◆ arrayst()

arrayst::arrayst ( const namespacet & _ns,

propt & _prop,

message_handlert & message_handler,

bool get_array_constraints = false

)

Definition at line 29 of file arrays.cpp.

Member Function Documentation

◆ add_array_Ackermann_constraints()

void arrayst::add_array_Ackermann_constraints ( )

protected

Definition at line 340 of file arrays.cpp.

◆ add_array_constraint()

void arrayst::add_array_constraint ( const lazy_constraintt & lazy,

bool refine = true

)

protected

adds array constraints (refine=true...lazily for the refinement loop)

Definition at line 265 of file arrays.cpp.

◆ add_array_constraints() [1/2]

void arrayst::add_array_constraints ( )

protected

Definition at line 290 of file arrays.cpp.

◆ add_array_constraints() [2/2]

void arrayst::add_array_constraints ( const index_sett & index_set,

const exprt & expr

)

protected

Definition at line 485 of file arrays.cpp.

◆ add_array_constraints_array_constant()

void arrayst::add_array_constraints_array_constant ( const index_sett & index_set,

const array_exprt & exprt

)

protected

Definition at line 737 of file arrays.cpp.

◆ add_array_constraints_array_of()

void arrayst::add_array_constraints_array_of ( const index_sett & index_set,

const array_of_exprt & exprt

)

protected

Definition at line 712 of file arrays.cpp.

◆ add_array_constraints_comprehension()

void arrayst::add_array_constraints_comprehension ( const index_sett & index_set,

const array_comprehension_exprt & expr

)

protected

Definition at line 818 of file arrays.cpp.

◆ add_array_constraints_equality()

void arrayst::add_array_constraints_equality ( const index_sett & index_set,

const array_equalityt & array_equality

)

protected

Definition at line 451 of file arrays.cpp.

◆ add_array_constraints_if()

void arrayst::add_array_constraints_if ( const index_sett & index_set,

const if_exprt & exprt

)

protected

Definition at line 842 of file arrays.cpp.

◆ add_array_constraints_update()

void arrayst::add_array_constraints_update ( const index_sett & index_set,

const update_exprt & expr

)

protected

Definition at line 655 of file arrays.cpp.

◆ add_array_constraints_with()

void arrayst::add_array_constraints_with ( const index_sett & index_set,

const with_exprt & expr

)

protected

Definition at line 583 of file arrays.cpp.

◆ collect_arrays()

void arrayst::collect_arrays ( const exprt & a )

protected

Definition at line 144 of file arrays.cpp.

◆ collect_indices() [1/2]

void arrayst::collect_indices ( )

protected

Definition at line 96 of file arrays.cpp.

◆ collect_indices() [2/2]

void arrayst::collect_indices ( const exprt & a )

protected

Definition at line 104 of file arrays.cpp.

◆ display_array_constraint_count()

void arrayst::display_array_constraint_count ( )

protected

Definition at line 921 of file arrays.cpp.

◆ enum_to_string()

std::string arrayst::enum_to_string ( constraint_typet type )

protected

Definition at line 894 of file arrays.cpp.

◆ finish_eager_conversion()

void arrayst::finish_eager_conversion ( )

inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Reimplemented in bv_pointers_widet, boolbvt, and bv_pointerst.

Definition at line 42 of file arrays.h.

◆ finish_eager_conversion_arrays()

virtual void arrayst::finish_eager_conversion_arrays ( )

inlineprotectedvirtual

Reimplemented in bv_refinementt.

Definition at line 69 of file arrays.h.

◆ is_unbounded_array()

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

protectedpure virtual

Implemented in boolbvt.

◆ record_array_equality()

literalt arrayst::record_array_equality ( const equal_exprt & expr )

Definition at line 55 of file arrays.cpp.

◆ record_array_index()

void arrayst::record_array_index ( const index_exprt & expr )

Definition at line 45 of file arrays.cpp.

◆ record_array_let_binding()

void arrayst::record_array_let_binding ( const symbol_exprt & symbol,

const exprt & value

)

Record that symbol is equal to value for the purposes of the array theory.

For unbounded-array-typed bindings this connects the two expressions in the union-find so that element-wise constraints propagate correctly.

Precondition: value must be free of byte_update operators; lower them at the call site (collect_arrays otherwise fails a DATA_INVARIANT).

Definition at line 83 of file arrays.cpp.

◆ update_index_map() [1/2]

void arrayst::update_index_map ( bool update_all )

protected

Definition at line 417 of file arrays.cpp.

◆ update_index_map() [2/2]

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

protected

merge the indices into the root

Definition at line 403 of file arrays.cpp.

Member Data Documentation

◆ array_comprehension_args

std::unordered_set<irep_idt> arrayst::array_comprehension_args

protected

Definition at line 174 of file arrays.h.

◆ array_constraint_count

array_constraint_countt arrayst::array_constraint_count

protected

Definition at line 142 of file arrays.h.

◆ array_equalities

array_equalitiest arrayst::array_equalities

protected

Definition at line 84 of file arrays.h.

◆ arrays

union_find<exprt, irep_hash> arrayst::arrays

protected

Definition at line 87 of file arrays.h.

◆ expr_map

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

protected

Definition at line 126 of file arrays.h.

◆ get_array_constraints

bool arrayst::get_array_constraints

protected

Definition at line 123 of file arrays.h.

◆ incremental_cache

bool arrayst::incremental_cache

protected

Definition at line 122 of file arrays.h.

◆ index_map

index_mapt arrayst::index_map

protected

Definition at line 94 of file arrays.h.

◆ lazy_array_constraints

std::list<lazy_constraintt> arrayst::lazy_array_constraints

protected

Definition at line 124 of file arrays.h.

◆ lazy_arrays

bool arrayst::lazy_arrays

protected

Definition at line 121 of file arrays.h.

◆ log

messaget arrayst::log

protected

Definition at line 66 of file arrays.h.

◆ message_handler

message_handlert& arrayst::message_handler

protected

Definition at line 67 of file arrays.h.

◆ ns

const namespacet& arrayst::ns

protected

Definition at line 65 of file arrays.h.

◆ update_indices

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

protected

Definition at line 170 of file arrays.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/flattening/arrays.h
/home/runner/work/cbmc/cbmc/src/solvers/flattening/arrays.cpp

arrayst
Generated by doxygen 1.9.8