cprover
Loading...
Searching...
No Matches
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 equalityt
using SUB = prop_conv_solvert
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 class  resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
 Result of running the decision procedure. More...

Public Member Functions

 arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
void finish_eager_conversion () 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 finish_eager_conversion () 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 (const exprt &) override
 Implementation of the decision procedure.
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out.
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure.
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available.
tvt l_get (literalt a) const override
 Return value of literal l from satisfying assignment.
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.
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 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.
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls.
hardness_collectortget_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_equalitytarray_equalitiest
typedef std::set< exprtindex_sett
typedef std::map< std::size_t, index_settindex_mapt
typedef std::map< constraint_typet, size_t > array_constraint_countt
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 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 namespacetns
messaget log
message_handlertmessage_handler
array_equalitiest array_equalities
union_find< exprt, irep_hasharrays
index_mapt index_map
bool lazy_arrays
bool incremental_cache
bool get_array_constraints
std::list< lazy_constrainttlazy_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_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.
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 32 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 132 of file arrays.h.

◆ array_equalitiest

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

Definition at line 74 of file arrays.h.

◆ index_mapt

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

Definition at line 84 of file arrays.h.

◆ index_sett

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

Definition at line 81 of file arrays.h.

◆ SUB

Definition at line 50 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 119 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 88 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 330 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 255 of file arrays.cpp.

◆ add_array_constraints() [1/2]

void arrayst::add_array_constraints ( )
protected

Definition at line 280 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 475 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 734 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 709 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 815 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 441 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 839 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 652 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 573 of file arrays.cpp.

◆ collect_arrays()

void arrayst::collect_arrays ( const exprt & a)
protected

Definition at line 131 of file arrays.cpp.

◆ collect_indices() [1/2]

void arrayst::collect_indices ( )
protected

Definition at line 83 of file arrays.cpp.

◆ collect_indices() [2/2]

void arrayst::collect_indices ( const exprt & a)
protected

Definition at line 91 of file arrays.cpp.

◆ display_array_constraint_count()

void arrayst::display_array_constraint_count ( )
protected

Definition at line 918 of file arrays.cpp.

◆ enum_to_string()

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

Definition at line 891 of file arrays.cpp.

◆ finish_eager_conversion()

void arrayst::finish_eager_conversion ( )
inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Reimplemented in boolbvt, bv_pointers_widet, and bv_pointerst.

Definition at line 41 of file arrays.h.

◆ finish_eager_conversion_arrays()

virtual void arrayst::finish_eager_conversion_arrays ( )
inlineprotectedvirtual

Reimplemented in bv_refinementt.

Definition at line 60 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.

◆ update_index_map() [1/2]

void arrayst::update_index_map ( bool update_all)
protected

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

Member Data Documentation

◆ array_comprehension_args

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

Definition at line 165 of file arrays.h.

◆ array_constraint_count

array_constraint_countt arrayst::array_constraint_count
protected

Definition at line 133 of file arrays.h.

◆ array_equalities

array_equalitiest arrayst::array_equalities
protected

Definition at line 75 of file arrays.h.

◆ arrays

union_find<exprt, irep_hash> arrayst::arrays
protected

Definition at line 78 of file arrays.h.

◆ expr_map

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

Definition at line 117 of file arrays.h.

◆ get_array_constraints

bool arrayst::get_array_constraints
protected

Definition at line 114 of file arrays.h.

◆ incremental_cache

bool arrayst::incremental_cache
protected

Definition at line 113 of file arrays.h.

◆ index_map

index_mapt arrayst::index_map
protected

Definition at line 85 of file arrays.h.

◆ lazy_array_constraints

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

Definition at line 115 of file arrays.h.

◆ lazy_arrays

bool arrayst::lazy_arrays
protected

Definition at line 112 of file arrays.h.

◆ log

messaget arrayst::log
protected

Definition at line 57 of file arrays.h.

◆ message_handler

message_handlert& arrayst::message_handler
protected

Definition at line 58 of file arrays.h.

◆ ns

const namespacet& arrayst::ns
protected

Definition at line 56 of file arrays.h.

◆ update_indices

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

Definition at line 161 of file arrays.h.


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