Classes |
Public Types |
Public Member Functions |
Protected Types |
Protected Member Functions |
Protected Attributes |
List of all members
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, literalt > | symbolst |
| typedef std::unordered_map< exprt, literalt, irep_hash > | cachet |
| 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. 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... | |
| 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. More... | |
| std::size_t | get_number_of_solver_calls () const override |
| Return the number of incremental solver calls. More... | |
| 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'. More... | |
| void | set_to_false (const exprt &) |
For a Boolean expression expr, add the constraint 'not expr'. More... | |
| resultt | operator() () |
| Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. More... | |
| resultt | operator() (const exprt &assumption) |
| Run the decision procedure to solve the problem under the given assumption. More... | |
| 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 } |
| enum class | constraint_typet { ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF , ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_EQUALITY } |
| 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) More... | |
| 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 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 std::optional< 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 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. 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
Member Typedef Documentation
◆ array_constraint_countt
|
protected |
◆ array_equalitiest
|
protected |
◆ index_mapt
|
protected |
◆ index_sett
|
protected |
◆ SUB
| typedef equalityt arrayst::SUB |
Member Enumeration Documentation
◆ constraint_typet
|
strongprotected |
◆ lazy_typet
|
strongprotected |
Constructor & Destructor Documentation
◆ arrayst()
| arrayst::arrayst | ( | const namespacet & | _ns, |
| propt & | _prop, | ||
| message_handlert & | message_handler, | ||
| bool | get_array_constraints = false |
||
| ) |
Definition at line 28 of file arrays.cpp.
Member Function Documentation
◆ add_array_Ackermann_constraints()
|
protected |
Definition at line 324 of file arrays.cpp.
◆ add_array_constraint()
|
protected |
adds array constraints (refine=true...lazily for the refinement loop)
Definition at line 249 of file arrays.cpp.
◆ add_array_constraints() [1/2]
|
protected |
Definition at line 274 of file arrays.cpp.
◆ add_array_constraints() [2/2]
|
protected |
Definition at line 469 of file arrays.cpp.
◆ add_array_constraints_array_constant()
|
protected |
Definition at line 701 of file arrays.cpp.
◆ add_array_constraints_array_of()
|
protected |
Definition at line 676 of file arrays.cpp.
◆ add_array_constraints_comprehension()
|
protected |
Definition at line 782 of file arrays.cpp.
◆ add_array_constraints_equality()
|
protected |
Definition at line 435 of file arrays.cpp.
◆ add_array_constraints_if()
|
protected |
Definition at line 806 of file arrays.cpp.
◆ add_array_constraints_update()
|
protected |
Definition at line 619 of file arrays.cpp.
◆ add_array_constraints_with()
|
protected |
Definition at line 540 of file arrays.cpp.
◆ collect_arrays()
|
protected |
Definition at line 130 of file arrays.cpp.
◆ collect_indices() [1/2]
|
protected |
Definition at line 82 of file arrays.cpp.
◆ collect_indices() [2/2]
|
protected |
Definition at line 90 of file arrays.cpp.
◆ display_array_constraint_count()
|
protected |
Definition at line 883 of file arrays.cpp.
◆ enum_to_string()
|
protected |
Definition at line 858 of file arrays.cpp.
◆ finish_eager_conversion()
|
inlineoverridevirtual |
Reimplemented from prop_conv_solvert.
Reimplemented in bv_pointerst, and boolbvt.
◆ finish_eager_conversion_arrays()
|
inlineprotectedvirtual |
Reimplemented in bv_refinementt.
◆ is_unbounded_array()
|
protectedpure virtual |
Implemented in boolbvt.
◆ record_array_equality()
| literalt arrayst::record_array_equality | ( | const equal_exprt & | expr | ) |
Definition at line 54 of file arrays.cpp.
◆ record_array_index()
| void arrayst::record_array_index | ( | const index_exprt & | expr | ) |
Definition at line 44 of file arrays.cpp.
◆ update_index_map() [1/2]
|
protected |
Definition at line 401 of file arrays.cpp.
◆ update_index_map() [2/2]
|
protected |
merge the indices into the root
Definition at line 387 of file arrays.cpp.
Member Data Documentation
◆ array_comprehension_args
|
protected |
◆ array_constraint_count
|
protected |
◆ array_equalities
|
protected |
◆ arrays
|
protected |
◆ expr_map
◆ get_array_constraints
◆ incremental_cache
◆ index_map
|
protected |
◆ lazy_array_constraints
|
protected |
◆ lazy_arrays
◆ log
◆ message_handler
|
protected |
◆ ns
|
protected |
◆ update_indices
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
