cprover
arrays.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Theory of Arrays with Extensionality
4 
5 Author: 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 
23 class array_of_exprt;
24 class equal_exprt;
25 class if_exprt;
26 class index_exprt;
27 class with_exprt;
28 class update_exprt;
29 
30 class arrayst:public equalityt
31 {
32 public:
33  arrayst(
34  const namespacet &_ns,
35  propt &_prop,
36  message_handlert &message_handler);
37 
38  void post_process() override
39  {
42  }
43 
44  // NOLINTNEXTLINE(readability/identifiers)
45  typedef equalityt SUB;
46 
48  void record_array_index(const index_exprt &expr);
49 
50 protected:
51  const namespacet &ns;
52 
53  virtual void post_process_arrays()
54  {
56  }
57 
59  {
62  };
63 
64  // the list of all equalities between arrays
65  // references to objects in this container need to be stable as
66  // elements are added while references are held
67  typedef std::list<array_equalityt> array_equalitiest;
69 
70  // this is used to find the clusters of arrays being compared
72 
73  // this tracks the array indicies for each array
74  typedef std::set<exprt> index_sett;
75  // references to values in this container need to be stable as
76  // elements are added while references are held
77  typedef std::map<std::size_t, index_sett> index_mapt;
79 
80  // adds array constraints lazily
81  enum class lazy_typet
82  {
84  ARRAY_WITH,
85  ARRAY_IF,
86  ARRAY_OF,
90  };
91 
93  {
96 
97  lazy_constraintt(lazy_typet _type, const exprt &_lazy)
98  {
99  type = _type;
100  lazy = _lazy;
101  }
102  };
103 
106  std::list<lazy_constraintt> lazy_array_constraints;
107  void add_array_constraint(const lazy_constraintt &lazy, bool refine = true);
108  std::map<exprt, bool> expr_map;
109 
110  // adds all the constraints eagerly
111  void add_array_constraints();
114  const index_sett &index_set, const array_equalityt &array_equality);
116  const index_sett &index_set, const exprt &expr);
118  const index_sett &index_set, const if_exprt &exprt);
120  const index_sett &index_set, const with_exprt &expr);
122  const index_sett &index_set, const update_exprt &expr);
124  const index_sett &index_set, const array_of_exprt &exprt);
126  const index_sett &index_set,
127  const array_exprt &exprt);
129  const index_sett &index_set,
130  const array_comprehension_exprt &expr);
131 
132  void update_index_map(bool update_all);
133  void update_index_map(std::size_t i);
134  std::set<std::size_t> update_indices;
135  void collect_arrays(const exprt &a);
136  void collect_indices();
137  void collect_indices(const exprt &a);
138  std::unordered_set<irep_idt> array_comprehension_args;
139 
140  virtual bool is_unbounded_array(const typet &type) const=0;
141  // (maybe this function should be partially moved here from boolbv)
142 };
143 
144 #endif // CPROVER_SOLVERS_FLATTENING_ARRAYS_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
arrayst::array_equalityt::f1
exprt f1
Definition: arrays.h:61
arrayst::lazy_typet
lazy_typet
Definition: arrays.h:82
arrayst::array_comprehension_args
std::unordered_set< irep_idt > array_comprehension_args
Definition: arrays.h:138
arrayst::lazy_constraintt::lazy_constraintt
lazy_constraintt(lazy_typet _type, const exprt &_lazy)
Definition: arrays.h:97
union_find.h
arrayst::record_array_equality
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:46
equality.h
arrayst::lazy_constraintt
Definition: arrays.h:93
typet
The type of an expression, extends irept.
Definition: type.h:29
arrayst::index_map
index_mapt index_map
Definition: arrays.h:78
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
arrayst::collect_arrays
void collect_arrays(const exprt &a)
Definition: arrays.cpp:121
arrayst::index_mapt
std::map< std::size_t, index_sett > index_mapt
Definition: arrays.h:77
exprt
Base class for all expressions.
Definition: expr.h:53
arrayst::collect_indices
void collect_indices()
Definition: arrays.cpp:74
equalityt::post_process
void post_process() override
Definition: equality.h:29
arrayst::array_equalityt::l
literalt l
Definition: arrays.h:60
arrayst::update_indices
std::set< std::size_t > update_indices
Definition: arrays.h:134
arrayst::lazy_constraintt::type
lazy_typet type
Definition: arrays.h:94
union_find< exprt >
equal_exprt
Equality.
Definition: std_expr.h:1190
arrayst::lazy_typet::ARRAY_IF
@ ARRAY_IF
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
arrayst::post_process
void post_process() override
Definition: arrays.h:38
arrayst::add_array_constraints_with
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:528
arrayst::incremental_cache
bool incremental_cache
Definition: arrays.h:105
arrayst::array_equalitiest
std::list< array_equalityt > array_equalitiest
Definition: arrays.h:67
arrayst::lazy_typet::ARRAY_OF
@ ARRAY_OF
arrayst::add_array_constraints
void add_array_constraints()
Definition: arrays.cpp:267
arrayst::lazy_array_constraints
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:106
arrayst::post_process_arrays
virtual void post_process_arrays()
Definition: arrays.h:53
lazy
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
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1367
arrayst::array_equalities
array_equalitiest array_equalities
Definition: arrays.h:68
arrayst::is_unbounded_array
virtual bool is_unbounded_array(const typet &type) const =0
arrayst::index_sett
std::set< exprt > index_sett
Definition: arrays.h:74
arrayst::lazy_constraintt::lazy
exprt lazy
Definition: arrays.h:95
arrayst::lazy_typet::ARRAY_WITH
@ ARRAY_WITH
arrayst::expr_map
std::map< exprt, bool > expr_map
Definition: arrays.h:108
message_handlert
Definition: message.h:28
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:36
equalityt
Definition: equality.h:20
arrayst::add_array_Ackermann_constraints
void add_array_Ackermann_constraints()
Definition: arrays.cpp:317
arrayst::array_equalityt::f2
exprt f2
Definition: arrays.h:61
arrayst::lazy_typet::ARRAY_TYPECAST
@ ARRAY_TYPECAST
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3234
arrayst::add_array_constraints_update
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:603
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
arrayst::array_equalityt
Definition: arrays.h:59
arrayst::add_array_constraints_comprehension
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition: arrays.cpp:763
arrayst::lazy_typet::ARRAY_CONSTANT
@ ARRAY_CONSTANT
literalt
Definition: literal.h:26
arrayst::add_array_constraints_array_constant
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition: arrays.cpp:684
arrayst::add_array_constraints_array_of
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition: arrays.cpp:660
arrayst::update_index_map
void update_index_map(bool update_all)
Definition: arrays.cpp:392
arrayst::lazy_typet::ARRAY_ACKERMANN
@ ARRAY_ACKERMANN
arrayst::arrays
union_find< exprt > arrays
Definition: arrays.h:71
arrayst::SUB
equalityt SUB
Definition: arrays.h:45
index_exprt
Array index operator.
Definition: std_expr.h:1293
arrayst::lazy_arrays
bool lazy_arrays
Definition: arrays.h:104
arrayst
Definition: arrays.h:31
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4422
arrayst::add_array_constraint
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition: arrays.cpp:242
arrayst::lazy_typet::ARRAY_COMPREHENSION
@ ARRAY_COMPREHENSION
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
arrayst::add_array_constraints_equality
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:426
arrayst::arrayst
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
Definition: arrays.cpp:26
arrayst::add_array_constraints_if
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:785