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
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
arrayst::constraint_typet::ARRAY_WITH
@ ARRAY_WITH
arrayst::constraint_typet::ARRAY_COMPREHENSION
@ ARRAY_COMPREHENSION
arrayst::array_equalityt::f1
exprt f1
Definition: arrays.h:66
arrayst::constraint_typet::ARRAY_IF
@ ARRAY_IF
arrayst::constraint_typet
constraint_typet
Definition: arrays.h:117
arrayst::lazy_typet
lazy_typet
Definition: arrays.h:87
arrayst::array_comprehension_args
std::unordered_set< irep_idt > array_comprehension_args
Definition: arrays.h:161
arrayst::lazy_constraintt::lazy_constraintt
lazy_constraintt(lazy_typet _type, const exprt &_lazy)
Definition: arrays.h:102
union_find.h
arrayst::record_array_equality
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:55
equality.h
arrayst::log
messaget log
Definition: arrays.h:55
arrayst::lazy_constraintt
Definition: arrays.h:98
typet
The type of an expression, extends irept.
Definition: type.h:28
arrayst::index_map
index_mapt index_map
Definition: arrays.h:83
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
arrayst::collect_arrays
void collect_arrays(const exprt &a)
Definition: arrays.cpp:130
arrayst::index_mapt
std::map< std::size_t, index_sett > index_mapt
Definition: arrays.h:82
exprt
Base class for all expressions.
Definition: expr.h:54
arrayst::collect_indices
void collect_indices()
Definition: arrays.cpp:83
equalityt::post_process
void post_process() override
Definition: equality.h:29
arrayst::array_equalityt::l
literalt l
Definition: arrays.h:65
arrayst::update_indices
std::set< std::size_t > update_indices
Definition: arrays.h:157
arrayst::array_constraint_count
array_constraint_countt array_constraint_count
Definition: arrays.h:129
arrayst::lazy_constraintt::type
lazy_typet type
Definition: arrays.h:99
union_find< exprt, irep_hash >
equal_exprt
Equality.
Definition: std_expr.h:1140
arrayst::constraint_typet::ARRAY_ACKERMANN
@ ARRAY_ACKERMANN
arrayst::lazy_typet::ARRAY_IF
@ ARRAY_IF
arrayst::constraint_typet::ARRAY_OF
@ ARRAY_OF
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:39
arrayst::add_array_constraints_with
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:540
arrayst::incremental_cache
bool incremental_cache
Definition: arrays.h:110
arrayst::array_equalitiest
std::list< array_equalityt > array_equalitiest
Definition: arrays.h:72
arrayst::lazy_typet::ARRAY_OF
@ ARRAY_OF
arrayst::add_array_constraints
void add_array_constraints()
Definition: arrays.cpp:276
arrayst::lazy_array_constraints
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:112
arrayst::post_process_arrays
virtual void post_process_arrays()
Definition: arrays.h:58
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:54
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1317
arrayst::array_equalities
array_equalitiest array_equalities
Definition: arrays.h:73
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:79
arrayst::lazy_constraintt::lazy
exprt lazy
Definition: arrays.h:100
arrayst::lazy_typet::ARRAY_WITH
@ ARRAY_WITH
arrayst::expr_map
std::map< exprt, bool > expr_map
Definition: arrays.h:114
message_handlert
Definition: message.h:28
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:45
equalityt
Definition: equality.h:20
arrayst::constraint_typet::ARRAY_CONSTANT
@ ARRAY_CONSTANT
arrayst::add_array_Ackermann_constraints
void add_array_Ackermann_constraints()
Definition: arrays.cpp:326
arrayst::array_equalityt::f2
exprt f2
Definition: arrays.h:66
arrayst::lazy_typet::ARRAY_TYPECAST
@ ARRAY_TYPECAST
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
arrayst::display_array_constraint_count
void display_array_constraint_count()
Definition: arrays.cpp:882
arrayst::add_array_constraints_update
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:618
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
arrayst::array_equalityt
Definition: arrays.h:64
arrayst::add_array_constraints_comprehension
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition: arrays.cpp:781
arrayst::lazy_typet::ARRAY_CONSTANT
@ ARRAY_CONSTANT
literalt
Definition: literal.h:26
arrayst::array_constraint_countt
std::map< constraint_typet, size_t > array_constraint_countt
Definition: arrays.h:128
arrayst::add_array_constraints_array_constant
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition: arrays.cpp:700
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:675
arrayst::update_index_map
void update_index_map(bool update_all)
Definition: arrays.cpp:402
arrayst::arrays
union_find< exprt, irep_hash > arrays
Definition: arrays.h:76
arrayst::lazy_typet::ARRAY_ACKERMANN
@ ARRAY_ACKERMANN
arrayst::SUB
equalityt SUB
Definition: arrays.h:48
index_exprt
Array index operator.
Definition: std_expr.h:1243
arrayst::lazy_arrays
bool lazy_arrays
Definition: arrays.h:109
arrayst
Definition: arrays.h:31
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3025
arrayst::constraint_typet::ARRAY_EQUALITY
@ ARRAY_EQUALITY
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:251
arrayst::get_array_constraints
bool get_array_constraints
Definition: arrays.h:111
arrayst::lazy_typet::ARRAY_COMPREHENSION
@ ARRAY_COMPREHENSION
arrayst::message_handler
message_handlert & message_handler
Definition: arrays.h:56
arrayst::constraint_typet::ARRAY_TYPECAST
@ ARRAY_TYPECAST
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1382
arrayst::add_array_constraints_equality
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:436
arrayst::arrayst
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition: arrays.cpp:29
arrayst::enum_to_string
std::string enum_to_string(constraint_typet)
Definition: arrays.cpp:857
arrayst::add_array_constraints_if
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:805