cprover
arrayst Class Referenceabstract

#include <arrays.h>

+ Inheritance diagram for arrayst:
+ Collaboration diagram for arrayst:

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 }
 Result of running the decision procedure. More...
 

Public Member Functions

 arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler)
 
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 (propt &_prop, message_handlert &message_handler)
 
virtual literalt equality (const exprt &e1, const exprt &e2)
 
void post_process () override
 
- Public Member Functions inherited from prop_conv_solvert
 prop_conv_solvert (propt &_prop, message_handlert &message_handler)
 
virtual ~prop_conv_solvert ()=default
 
decision_proceduret::resultt dec_solve () override
 Run the decision procedure to solve the problem. More...
 
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out. More...
 
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure. More...
 
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available. More...
 
tvt l_get (literalt a) const override
 Return value of literal l from satisfying assignment. More...
 
exprt handle (const exprt &expr) override
 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. More...
 
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. More...
 
bool is_in_conflict (const exprt &expr) const override
 Returns true if an expression is in the final conflict leading to UNSAT. More...
 
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'. More...
 
void push () override
 Push a new context on the stack This context becomes a child context nested in the current context. More...
 
void push (const std::vector< exprt > &assumptions) override
 Push assumptions in form of literal_exprt More...
 
void pop () override
 Pop whatever is on top of the stack. More...
 
bool literal (const symbol_exprt &expr, literalt &literal) const
 
virtual void clear_cache ()
 
const cachetget_cache () const
 
const symbolstget_symbols () const
 
void set_time_limit_seconds (uint32_t lim) override
 Set the limit for the solver to time out in seconds. More...
 
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls. More...
 
- 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 &expr)
 For a Boolean expression expr, add the constraint 'expr'. More...
 
void set_to_false (const exprt &expr)
 For a Boolean expression expr, add the constraint 'not expr'. More...
 
resultt operator() ()
 Run the decision procedure to solve the problem. More...
 
virtual ~decision_proceduret ()
 
- Public Member Functions inherited from solver_resource_limitst
virtual ~solver_resource_limitst ()=default
 

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, lazy_typet::ARRAY_CONSTANT, lazy_typet::ARRAY_COMPREHENSION
}
 
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 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 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 optionalt< bool > get_bool (const exprt &expr) const
 Get a boolean value from the model if the formula is satisfiable. 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

const namespacetns
 
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
 
std::unordered_set< irep_idtarray_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
 
proptprop
 
messaget log
 
bvt assumption_stack
 Assumptions on the stack. More...
 
std::size_t context_literal_counter = 0
 To generate unique literal names for contexts. More...
 
std::vector< size_t > context_size_stack
 assumption_stack is segmented in contexts; Number of assumptions in each context on the stack More...
 

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 30 of file arrays.h.

Member Typedef Documentation

◆ array_equalitiest

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

Definition at line 67 of file arrays.h.

◆ index_mapt

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

Definition at line 77 of file arrays.h.

◆ index_sett

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

Definition at line 74 of file arrays.h.

◆ SUB

Definition at line 45 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 
ARRAY_CONSTANT 
ARRAY_COMPREHENSION 

Definition at line 81 of file arrays.h.

Constructor & Destructor Documentation

◆ arrayst()

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

Definition at line 26 of file arrays.cpp.

Member Function Documentation

◆ add_array_Ackermann_constraints()

void arrayst::add_array_Ackermann_constraints ( )
protected

Definition at line 319 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 244 of file arrays.cpp.

◆ add_array_constraints() [1/2]

void arrayst::add_array_constraints ( )
protected

Definition at line 269 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 459 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 688 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 664 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 767 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 428 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 789 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 607 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 532 of file arrays.cpp.

◆ collect_arrays()

void arrayst::collect_arrays ( const exprt a)
protected

Definition at line 121 of file arrays.cpp.

◆ collect_indices() [1/2]

void arrayst::collect_indices ( )
protected

Definition at line 74 of file arrays.cpp.

◆ collect_indices() [2/2]

void arrayst::collect_indices ( const exprt a)
protected

Definition at line 82 of file arrays.cpp.

◆ is_unbounded_array()

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

Implemented in boolbvt.

◆ post_process()

void arrayst::post_process ( )
inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Reimplemented in boolbvt, and bv_pointerst.

Definition at line 38 of file arrays.h.

◆ post_process_arrays()

virtual void arrayst::post_process_arrays ( )
inlineprotectedvirtual

Reimplemented in bv_refinementt.

Definition at line 53 of file arrays.h.

◆ record_array_equality()

literalt arrayst::record_array_equality ( const equal_exprt expr)

Definition at line 46 of file arrays.cpp.

◆ record_array_index()

void arrayst::record_array_index ( const index_exprt expr)

Definition at line 36 of file arrays.cpp.

◆ update_index_map() [1/2]

void arrayst::update_index_map ( bool  update_all)
protected

Definition at line 394 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 380 of file arrays.cpp.

Member Data Documentation

◆ array_comprehension_args

std::unordered_set<irep_idt> arrayst::array_comprehension_args
protected

Definition at line 138 of file arrays.h.

◆ array_equalities

array_equalitiest arrayst::array_equalities
protected

Definition at line 68 of file arrays.h.

◆ arrays

union_find<exprt> arrayst::arrays
protected

Definition at line 71 of file arrays.h.

◆ expr_map

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

Definition at line 108 of file arrays.h.

◆ incremental_cache

bool arrayst::incremental_cache
protected

Definition at line 105 of file arrays.h.

◆ index_map

index_mapt arrayst::index_map
protected

Definition at line 78 of file arrays.h.

◆ lazy_array_constraints

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

Definition at line 106 of file arrays.h.

◆ lazy_arrays

bool arrayst::lazy_arrays
protected

Definition at line 104 of file arrays.h.

◆ ns

const namespacet& arrayst::ns
protected

Definition at line 51 of file arrays.h.

◆ update_indices

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

Definition at line 134 of file arrays.h.


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