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 <set>
16 
17 #include <util/union_find.h>
18 
19 #include "equality.h"
20 
21 class array_of_exprt;
22 class equal_exprt;
23 class if_exprt;
24 class index_exprt;
25 class with_exprt;
26 class update_exprt;
27 
28 class arrayst:public equalityt
29 {
30 public:
31  arrayst(const namespacet &_ns, propt &_prop);
32 
33  void post_process() override
34  {
37  }
38 
39  // NOLINTNEXTLINE(readability/identifiers)
40  typedef equalityt SUB;
41 
43  void record_array_index(const index_exprt &expr);
44 
45 protected:
46  virtual void post_process_arrays()
47  {
49  }
50 
52  {
55  };
56 
57  // the list of all equalities between arrays
58  // references to objects in this container need to be stable as
59  // elements are added while references are held
60  typedef std::list<array_equalityt> array_equalitiest;
62 
63  // this is used to find the clusters of arrays being compared
65 
66  // this tracks the array indicies for each array
67  typedef std::set<exprt> index_sett;
68  // references to values in this container need to be stable as
69  // elements are added while references are held
70  typedef std::map<std::size_t, index_sett> index_mapt;
72 
73  // adds array constraints lazily
74  enum class lazy_typet
75  {
77  ARRAY_WITH,
78  ARRAY_IF,
79  ARRAY_OF,
81  };
82 
84  {
87 
88  lazy_constraintt(lazy_typet _type, const exprt &_lazy)
89  {
90  type = _type;
91  lazy = _lazy;
92  }
93  };
94 
97  std::list<lazy_constraintt> lazy_array_constraints;
98  void add_array_constraint(const lazy_constraintt &lazy, bool refine = true);
99  std::map<exprt, bool> expr_map;
100 
101  // adds all the constraints eagerly
102  void add_array_constraints();
105  const index_sett &index_set, const array_equalityt &array_equality);
107  const index_sett &index_set, const exprt &expr);
109  const index_sett &index_set, const if_exprt &exprt);
111  const index_sett &index_set, const with_exprt &expr);
113  const index_sett &index_set, const update_exprt &expr);
115  const index_sett &index_set, const array_of_exprt &exprt);
116 
117  void update_index_map(bool update_all);
118  void update_index_map(std::size_t i);
119  std::set<std::size_t> update_indices;
120  void collect_arrays(const exprt &a);
121  void collect_indices();
122  void collect_indices(const exprt &a);
123 
124  virtual bool is_unbounded_array(const typet &type) const=0;
125  // (maybe this function should be partially moved here from boolbv)
126 };
127 
128 #endif // CPROVER_SOLVERS_FLATTENING_ARRAYS_H
The type of an expression, extends irept.
Definition: type.h:27
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition: arrays.cpp:235
virtual void post_process_arrays()
Definition: arrays.h:46
void collect_arrays(const exprt &a)
Definition: arrays.cpp:108
bool lazy_arrays
Definition: arrays.h:95
union_find< exprt > arrays
Definition: arrays.h:64
void post_process() override
Definition: arrays.h:33
index_mapt index_map
Definition: arrays.h:71
lazy_constraintt(lazy_typet _type, const exprt &_lazy)
Definition: arrays.h:88
void add_array_constraints()
Definition: arrays.cpp:260
Operator to update elements in structs and arrays.
Definition: std_expr.h:3707
std::set< exprt > index_sett
Definition: arrays.h:67
The trinary if-then-else operator.
Definition: std_expr.h:3427
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:506
Equality.
Definition: std_expr.h:1484
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:410
arrayst(const namespacet &_ns, propt &_prop)
Definition: arrays.cpp:24
bool incremental_cache
Definition: arrays.h:96
void update_index_map(bool update_all)
Definition: arrays.cpp:376
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
std::map< std::size_t, index_sett > index_mapt
Definition: arrays.h:70
void collect_indices()
Definition: arrays.cpp:74
Array constructor from single element.
Definition: std_expr.h:1678
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:42
Definition: arrays.h:28
void post_process() override
Definition: equality.h:28
TO_BE_DOCUMENTED.
Definition: prop.h:24
std::set< std::size_t > update_indices
Definition: arrays.h:119
array_equalitiest array_equalities
Definition: arrays.h:61
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition: arrays.cpp:636
equalityt SUB
Definition: arrays.h:40
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:32
lazy_typet
Definition: arrays.h:74
Base class for all expressions.
Definition: expr.h:54
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:575
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:97
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
virtual bool is_unbounded_array(const typet &type) const =0
std::list< array_equalityt > array_equalitiest
Definition: arrays.h:60
void add_array_Ackermann_constraints()
Definition: arrays.cpp:295
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:660
std::map< exprt, bool > expr_map
Definition: arrays.h:99
Array index operator.
Definition: std_expr.h:1595