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 
24 class array_exprt;
25 class array_of_exprt;
26 class equal_exprt;
27 class if_exprt;
28 class index_exprt;
29 class with_exprt;
30 class update_exprt;
31 
32 class arrayst:public equalityt
33 {
34 public:
35  arrayst(
36  const namespacet &_ns,
37  propt &_prop,
39  bool get_array_constraints = false);
40 
41  void finish_eager_conversion() override
42  {
47  }
48 
49  // NOLINTNEXTLINE(readability/identifiers)
50  typedef equalityt SUB;
51 
53  void record_array_index(const index_exprt &expr);
54 
55 protected:
56  const namespacet &ns;
59 
61  {
63  }
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
88  enum class lazy_typet
89  {
91  ARRAY_WITH,
92  ARRAY_IF,
93  ARRAY_OF,
97  };
98 
100  {
103 
104  lazy_constraintt(lazy_typet _type, const exprt &_lazy)
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 
118  enum class constraint_typet
119  {
121  ARRAY_WITH,
122  ARRAY_IF,
123  ARRAY_OF,
128  };
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
136  void add_array_constraints();
139  const index_sett &index_set, const array_equalityt &array_equality);
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);
149  const index_sett &index_set, const array_of_exprt &exprt);
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
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3182
Array constructor from list of elements.
Definition: std_expr.h:1476
Array constructor from single element.
Definition: std_expr.h:1411
Definition: arrays.h:33
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:434
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:323
bool lazy_arrays
Definition: arrays.h:111
void collect_indices()
Definition: arrays.cpp:80
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:127
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:52
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:26
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:273
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:42
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:248
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:400
messaget log
Definition: arrays.h:57
Equality.
Definition: std_expr.h:1225
void finish_eager_conversion() override
Definition: equality.h:31
Base class for all expressions.
Definition: expr.h:54
The trinary if-then-else operator.
Definition: std_expr.h:2226
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:29
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
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