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
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
arrayst::array_equalityt::f1
exprt f1
Definition: arrays.h:54
arrayst::lazy_typet
lazy_typet
Definition: arrays.h:74
arrayst::lazy_constraintt::lazy_constraintt
lazy_constraintt(lazy_typet _type, const exprt &_lazy)
Definition: arrays.h:88
union_find.h
arrayst::record_array_equality
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:42
equality.h
arrayst::lazy_constraintt
Definition: arrays.h:83
typet
The type of an expression, extends irept.
Definition: type.h:27
arrayst::index_map
index_mapt index_map
Definition: arrays.h:71
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
arrayst::collect_arrays
void collect_arrays(const exprt &a)
Definition: arrays.cpp:108
arrayst::index_mapt
std::map< std::size_t, index_sett > index_mapt
Definition: arrays.h:70
exprt
Base class for all expressions.
Definition: expr.h:54
arrayst::collect_indices
void collect_indices()
Definition: arrays.cpp:74
equalityt::post_process
void post_process() override
Definition: equality.h:28
arrayst::array_equalityt::l
literalt l
Definition: arrays.h:53
arrayst::update_indices
std::set< std::size_t > update_indices
Definition: arrays.h:119
arrayst::lazy_constraintt::type
lazy_typet type
Definition: arrays.h:85
union_find< exprt >
equal_exprt
Equality.
Definition: std_expr.h:1484
arrayst::lazy_typet::ARRAY_IF
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
arrayst::post_process
void post_process() override
Definition: arrays.h:33
arrayst::add_array_constraints_with
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:506
arrayst::incremental_cache
bool incremental_cache
Definition: arrays.h:96
arrayst::array_equalitiest
std::list< array_equalityt > array_equalitiest
Definition: arrays.h:60
arrayst::lazy_typet::ARRAY_OF
arrayst::add_array_constraints
void add_array_constraints()
Definition: arrays.cpp:260
arrayst::lazy_array_constraints
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:97
arrayst::post_process_arrays
virtual void post_process_arrays()
Definition: arrays.h:46
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1678
arrayst::array_equalities
array_equalitiest array_equalities
Definition: arrays.h:61
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:67
arrayst::lazy_constraintt::lazy
exprt lazy
Definition: arrays.h:86
arrayst::lazy_typet::ARRAY_WITH
arrayst::expr_map
std::map< exprt, bool > expr_map
Definition: arrays.h:99
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:32
equalityt
Definition: equality.h:19
arrayst::add_array_Ackermann_constraints
void add_array_Ackermann_constraints()
Definition: arrays.cpp:295
arrayst::array_equalityt::f2
exprt f2
Definition: arrays.h:54
arrayst::lazy_typet::ARRAY_TYPECAST
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3707
arrayst::add_array_constraints_update
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:575
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
arrayst::array_equalityt
Definition: arrays.h:51
literalt
Definition: literal.h:24
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:636
arrayst::update_index_map
void update_index_map(bool update_all)
Definition: arrays.cpp:376
arrayst::lazy_typet::ARRAY_ACKERMANN
arrayst::arrays
union_find< exprt > arrays
Definition: arrays.h:64
arrayst::SUB
equalityt SUB
Definition: arrays.h:40
index_exprt
Array index operator.
Definition: std_expr.h:1595
arrayst::lazy_arrays
bool lazy_arrays
Definition: arrays.h:95
arrayst
Definition: arrays.h:28
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:235
arrayst::add_array_constraints_equality
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:410
arrayst::arrayst
arrayst(const namespacet &_ns, propt &_prop)
Definition: arrays.cpp:24
arrayst::add_array_constraints_if
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:660