cprover
Loading...
Searching...
No Matches
arrays.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Theory of Arrays with Extensionality
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_SOLVERS_FLATTENING_ARRAYS_H
13#define CPROVER_SOLVERS_FLATTENING_ARRAYS_H
14
15#include <list>
16#include <set>
17#include <unordered_set>
18
19#include <util/union_find.h>
20
21#include "equality.h"
22
24class array_exprt;
25class array_of_exprt;
26class equal_exprt;
27class if_exprt;
28class index_exprt;
29class with_exprt;
30class update_exprt;
31
32class arrayst:public equalityt
33{
34public:
35 arrayst(
36 const namespacet &_ns,
37 propt &_prop,
39 bool get_array_constraints = false);
40
48
49 // NOLINTNEXTLINE(readability/identifiers)
50 typedef equalityt SUB;
51
53 void record_array_index(const index_exprt &expr);
54
55protected:
56 const namespacet &ns;
59
64
66 {
69 };
70
71 // the list of all equalities between arrays
72 // references to objects in this container need to be stable as
73 // elements are added while references are held
74 typedef std::list<array_equalityt> array_equalitiest;
76
77 // this is used to find the clusters of arrays being compared
79
80 // this tracks the array indicies for each array
81 typedef std::set<exprt> index_sett;
82 // references to values in this container need to be stable as
83 // elements are added while references are held
84 typedef std::map<std::size_t, index_sett> index_mapt;
86
87 // adds array constraints lazily
98
100 {
103
105 {
106 type = _type;
107 lazy = _lazy;
108 }
109 };
110
114 std::list<lazy_constraintt> lazy_array_constraints;
115 void add_array_constraint(const lazy_constraintt &lazy, bool refine = true);
116 std::map<exprt, bool> expr_map;
117
129
130 typedef std::map<constraint_typet, size_t> array_constraint_countt;
133 std::string enum_to_string(constraint_typet);
134
135 // adds all the constraints eagerly
141 const index_sett &index_set, const exprt &expr);
143 const index_sett &index_set, const if_exprt &exprt);
145 const index_sett &index_set, const with_exprt &expr);
147 const index_sett &index_set, const update_exprt &expr);
151 const index_sett &index_set,
152 const array_exprt &exprt);
154 const index_sett &index_set,
155 const array_comprehension_exprt &expr);
156
157 void update_index_map(bool update_all);
158 void update_index_map(std::size_t i);
159 std::set<std::size_t> update_indices;
160 void collect_arrays(const exprt &a);
161 void collect_indices();
162 void collect_indices(const exprt &a);
163 std::unordered_set<irep_idt> array_comprehension_args;
164
165 virtual bool is_unbounded_array(const typet &type) const=0;
166 // (maybe this function should be partially moved here from boolbv)
167};
168
169#endif // CPROVER_SOLVERS_FLATTENING_ARRAYS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3358
Array constructor from list of elements.
Definition std_expr.h:1563
Array constructor from single element.
Definition std_expr.h:1498
std::list< lazy_constraintt > lazy_array_constraints
Definition arrays.h:114
std::unordered_set< irep_idt > array_comprehension_args
Definition arrays.h:163
index_mapt index_map
Definition arrays.h:85
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition arrays.cpp:435
std::set< std::size_t > update_indices
Definition arrays.h:159
const namespacet & ns
Definition arrays.h:56
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition arrays.cpp:676
void add_array_Ackermann_constraints()
Definition arrays.cpp:324
bool lazy_arrays
Definition arrays.h:111
void collect_indices()
Definition arrays.cpp:82
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition arrays.cpp:619
void collect_arrays(const exprt &a)
Definition arrays.cpp:130
message_handlert & message_handler
Definition arrays.h:58
union_find< exprt, irep_hash > arrays
Definition arrays.h:78
literalt record_array_equality(const equal_exprt &expr)
Definition arrays.cpp:54
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition arrays.cpp:701
std::list< array_equalityt > array_equalitiest
Definition arrays.h:74
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition arrays.cpp:28
constraint_typet
Definition arrays.h:119
std::map< exprt, bool > expr_map
Definition arrays.h:116
equalityt SUB
Definition arrays.h:50
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition arrays.cpp:806
void finish_eager_conversion() override
Definition arrays.h:41
std::string enum_to_string(constraint_typet)
Definition arrays.cpp:858
bool get_array_constraints
Definition arrays.h:113
virtual void finish_eager_conversion_arrays()
Definition arrays.h:60
void add_array_constraints()
Definition arrays.cpp:274
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition arrays.cpp:782
virtual bool is_unbounded_array(const typet &type) const =0
void record_array_index(const index_exprt &expr)
Definition arrays.cpp:44
array_equalitiest array_equalities
Definition arrays.h:75
lazy_typet
Definition arrays.h:89
std::map< constraint_typet, size_t > array_constraint_countt
Definition arrays.h:130
std::set< exprt > index_sett
Definition arrays.h:81
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition arrays.cpp:249
array_constraint_countt array_constraint_count
Definition arrays.h:131
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition arrays.cpp:540
bool incremental_cache
Definition arrays.h:112
std::map< std::size_t, index_sett > index_mapt
Definition arrays.h:84
void display_array_constraint_count()
Definition arrays.cpp:883
void update_index_map(bool update_all)
Definition arrays.cpp:401
messaget log
Definition arrays.h:57
Equality.
Definition std_expr.h:1306
void finish_eager_conversion() override
Definition equality.h:31
Base class for all expressions.
Definition expr.h:56
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
TO_BE_DOCUMENTED.
Definition prop.h:25
The type of an expression, extends irept.
Definition type.h:29
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
auto lazy(funt fun) -> lazyt< decltype(fun())>
Delay the computation of fun to the next time the force method is called.
Definition lazy.h:49
lazy_constraintt(lazy_typet _type, const exprt &_lazy)
Definition arrays.h:104