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,
37  bool get_array_constraints = false);
38 
39  void post_process() override
40  {
45  }
46 
47  // NOLINTNEXTLINE(readability/identifiers)
48  typedef equalityt SUB;
49 
51  void record_array_index(const index_exprt &expr);
52 
53 protected:
54  const namespacet &ns;
57 
58  virtual void post_process_arrays()
59  {
61  }
62 
64  {
67  };
68 
69  // the list of all equalities between arrays
70  // references to objects in this container need to be stable as
71  // elements are added while references are held
72  typedef std::list<array_equalityt> array_equalitiest;
74 
75  // this is used to find the clusters of arrays being compared
77 
78  // this tracks the array indicies for each array
79  typedef std::set<exprt> index_sett;
80  // references to values in this container need to be stable as
81  // elements are added while references are held
82  typedef std::map<std::size_t, index_sett> index_mapt;
84 
85  // adds array constraints lazily
86  enum class lazy_typet
87  {
89  ARRAY_WITH,
90  ARRAY_IF,
91  ARRAY_OF,
95  };
96 
98  {
101 
102  lazy_constraintt(lazy_typet _type, const exprt &_lazy)
103  {
104  type = _type;
105  lazy = _lazy;
106  }
107  };
108 
112  std::list<lazy_constraintt> lazy_array_constraints;
113  void add_array_constraint(const lazy_constraintt &lazy, bool refine = true);
114  std::map<exprt, bool> expr_map;
115 
116  enum class constraint_typet
117  {
119  ARRAY_WITH,
120  ARRAY_IF,
121  ARRAY_OF,
126  };
127 
128  typedef std::map<constraint_typet, size_t> array_constraint_countt;
131  std::string enum_to_string(constraint_typet);
132 
133  // adds all the constraints eagerly
134  void add_array_constraints();
137  const index_sett &index_set, const array_equalityt &array_equality);
139  const index_sett &index_set, const exprt &expr);
141  const index_sett &index_set, const if_exprt &exprt);
143  const index_sett &index_set, const with_exprt &expr);
145  const index_sett &index_set, const update_exprt &expr);
147  const index_sett &index_set, const array_of_exprt &exprt);
149  const index_sett &index_set,
150  const array_exprt &exprt);
152  const index_sett &index_set,
153  const array_comprehension_exprt &expr);
154 
155  void update_index_map(bool update_all);
156  void update_index_map(std::size_t i);
157  std::set<std::size_t> update_indices;
158  void collect_arrays(const exprt &a);
159  void collect_indices();
160  void collect_indices(const exprt &a);
161  std::unordered_set<irep_idt> array_comprehension_args;
162 
163  virtual bool is_unbounded_array(const typet &type) const=0;
164  // (maybe this function should be partially moved here from boolbv)
165 };
166 
167 #endif // CPROVER_SOLVERS_FLATTENING_ARRAYS_H
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3128
Array constructor from list of elements.
Definition: std_expr.h:1467
Array constructor from single element.
Definition: std_expr.h:1402
Definition: arrays.h:31
void post_process() override
Definition: arrays.h:39
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:112
std::unordered_set< irep_idt > array_comprehension_args
Definition: arrays.h:161
index_mapt index_map
Definition: arrays.h:83
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:433
std::set< std::size_t > update_indices
Definition: arrays.h:157
const namespacet & ns
Definition: arrays.h:54
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition: arrays.cpp:672
void add_array_Ackermann_constraints()
Definition: arrays.cpp:323
virtual void post_process_arrays()
Definition: arrays.h:58
bool lazy_arrays
Definition: arrays.h:109
void collect_indices()
Definition: arrays.cpp:80
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:615
void collect_arrays(const exprt &a)
Definition: arrays.cpp:127
message_handlert & message_handler
Definition: arrays.h:56
union_find< exprt, irep_hash > arrays
Definition: arrays.h:76
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:52
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition: arrays.cpp:697
std::list< array_equalityt > array_equalitiest
Definition: arrays.h:72
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition: arrays.cpp:26
constraint_typet
Definition: arrays.h:117
std::map< exprt, bool > expr_map
Definition: arrays.h:114
equalityt SUB
Definition: arrays.h:48
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:802
std::string enum_to_string(constraint_typet)
Definition: arrays.cpp:854
bool get_array_constraints
Definition: arrays.h:111
void add_array_constraints()
Definition: arrays.cpp:273
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition: arrays.cpp:778
virtual bool is_unbounded_array(const typet &type) const =0
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:42
array_equalitiest array_equalities
Definition: arrays.h:73
lazy_typet
Definition: arrays.h:87
std::map< constraint_typet, size_t > array_constraint_countt
Definition: arrays.h:128
std::set< exprt > index_sett
Definition: arrays.h:79
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition: arrays.cpp:248
array_constraint_countt array_constraint_count
Definition: arrays.h:129
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:537
bool incremental_cache
Definition: arrays.h:110
std::map< std::size_t, index_sett > index_mapt
Definition: arrays.h:82
void display_array_constraint_count()
Definition: arrays.cpp:879
void update_index_map(bool update_all)
Definition: arrays.cpp:399
messaget log
Definition: arrays.h:55
Equality.
Definition: std_expr.h:1225
void post_process() override
Definition: equality.h:29
Base class for all expressions.
Definition: expr.h:54
The trinary if-then-else operator.
Definition: std_expr.h:2172
Array index operator.
Definition: std_expr.h:1328
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:23
The type of an expression, extends irept.
Definition: type.h:28
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
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:102