Skip to content

Commit 3e688e0

Browse files
romainbrenguierromainbrenguier
committed
Create string_refinement_util for utility function
string_refinement.cpp file is becoming too large. This groups utility classes used by string_refinement in new files to reduce string_refinement.cpp a bit.
1 parent e72eacf commit 3e688e0

File tree

5 files changed

+167
-138
lines changed

5 files changed

+167
-138
lines changed

‎src/solvers/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -179,6 +179,7 @@ SRC = $(BOOLEFORCE_SRC) \
179179
refinement/refine_arithmetic.cpp \
180180
refinement/refine_arrays.cpp \
181181
refinement/string_refinement.cpp \
182+
refinement/string_refinement_util.cpp \
182183
refinement/string_constraint_generator_code_points.cpp \
183184
refinement/string_constraint_generator_comparison.cpp \
184185
refinement/string_constraint_generator_concat.cpp \

‎src/solvers/refinement/string_refinement.cpp

-91
Original file line numberDiff line numberDiff line change
@@ -488,35 +488,6 @@ static union_find_replacet generate_symbol_resolution_from_equations(
488488
return solver;
489489
}
490490

491-
/// Maps equation to expressions contained in them and conversely expressions to
492-
/// equations that contain them. This can be used on a subset of expressions
493-
/// which interests us, in particular strings. Equations are identified by an
494-
/// index of type `std::size_t` for more efficient insertion and lookup.
495-
class equation_symbol_mappingt
496-
{
497-
public:
498-
// Record index of the equations that contain a given expression
499-
std::map<exprt, std::vector<std::size_t>> equations_containing;
500-
// Record expressions that are contained in the equation with the given index
501-
std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
502-
503-
void add(const std::size_t i, const exprt &expr)
504-
{
505-
equations_containing[expr].push_back(i);
506-
strings_in_equation[i].push_back(expr);
507-
}
508-
509-
std::vector<exprt> find_expressions(const std::size_t i)
510-
{
511-
return strings_in_equation[i];
512-
}
513-
514-
std::vector<std::size_t> find_equations(const exprt &expr)
515-
{
516-
return equations_containing[expr];
517-
}
518-
};
519-
520491
/// This is meant to be used on the lhs of an equation with string subtype.
521492
/// \param lhs: expression which is either of string type, or a symbol
522493
/// representing a struct with some string members
@@ -1219,68 +1190,6 @@ void debug_model(
12191190
stream << messaget::eom;
12201191
}
12211192

1222-
sparse_arrayt::sparse_arrayt(const with_exprt &expr)
1223-
{
1224-
auto ref = std::ref(static_cast<const exprt &>(expr));
1225-
while(can_cast_expr<with_exprt>(ref.get()))
1226-
{
1227-
const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
1228-
const auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
1229-
entries.emplace_back(current_index, with_expr.new_value());
1230-
ref = with_expr.old();
1231-
}
1232-
1233-
// This function only handles 'with' and 'array_of' expressions
1234-
PRECONDITION(ref.get().id() == ID_array_of);
1235-
default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
1236-
}
1237-
1238-
exprt sparse_arrayt::to_if_expression(const exprt &index) const
1239-
{
1240-
return std::accumulate(
1241-
entries.begin(),
1242-
entries.end(),
1243-
default_value,
1244-
[&](
1245-
const exprt if_expr,
1246-
const std::pair<std::size_t, exprt> &entry) { // NOLINT
1247-
const exprt entry_index = from_integer(entry.first, index.type());
1248-
const exprt &then_expr = entry.second;
1249-
CHECK_RETURN(then_expr.type() == if_expr.type());
1250-
const equal_exprt index_equal(index, entry_index);
1251-
return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
1252-
});
1253-
}
1254-
1255-
interval_sparse_arrayt::interval_sparse_arrayt(const with_exprt &expr)
1256-
: sparse_arrayt(expr)
1257-
{
1258-
// Entries are sorted so that successive entries correspond to intervals
1259-
std::sort(
1260-
entries.begin(),
1261-
entries.end(),
1262-
[](
1263-
const std::pair<std::size_t, exprt> &a,
1264-
const std::pair<std::size_t, exprt> &b) { return a.first < b.first; });
1265-
}
1266-
1267-
exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const
1268-
{
1269-
return std::accumulate(
1270-
entries.rbegin(),
1271-
entries.rend(),
1272-
default_value,
1273-
[&](
1274-
const exprt if_expr,
1275-
const std::pair<std::size_t, exprt> &entry) { // NOLINT
1276-
const exprt entry_index = from_integer(entry.first, index.type());
1277-
const exprt &then_expr = entry.second;
1278-
CHECK_RETURN(then_expr.type() == if_expr.type());
1279-
const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
1280-
return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
1281-
});
1282-
}
1283-
12841193
/// Create a new expression where 'with' expressions on arrays are replaced by
12851194
/// 'if' expressions. e.g. for an array access arr[index], where: `arr :=
12861195
/// array_of(12) with {0:=24} with {2:=42}` the constructed expression will be:

‎src/solvers/refinement/string_refinement.h

+1-47
Original file line numberDiff line numberDiff line change
@@ -27,57 +27,11 @@ Author: Alberto Griggio, [email protected]
2727
#include <solvers/refinement/string_constraint.h>
2828
#include <solvers/refinement/string_constraint_generator.h>
2929
#include <solvers/refinement/string_refinement_invariant.h>
30+
#include <solvers/refinement/string_refinement_util.h>
3031

3132
#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
3233
#define CHARACTER_FOR_UNKNOWN '?'
3334

34-
struct index_set_pairt
35-
{
36-
std::map<exprt, std::set<exprt>> cumulative;
37-
std::map<exprt, std::set<exprt>> current;
38-
};
39-
40-
struct string_axiomst
41-
{
42-
std::vector<string_constraintt> universal;
43-
std::vector<string_not_contains_constraintt> not_contains;
44-
};
45-
46-
/// Represents arrays of the form `array_of(x) with {i:=a} with {j:=b} ...`
47-
/// by a default value `x` and a list of entries `(i,a)`, `(j,b)` etc.
48-
class sparse_arrayt
49-
{
50-
public:
51-
/// Initialize a sparse array from an expression of the form
52-
/// `array_of(x) with {i:=a} with {j:=b} ...`
53-
/// This is the form in which array valuations coming from the underlying
54-
/// solver are given.
55-
explicit sparse_arrayt(const with_exprt &expr);
56-
57-
/// Creates an if_expr corresponding to the result of accessing the array
58-
/// at the given index
59-
virtual exprt to_if_expression(const exprt &index) const;
60-
61-
protected:
62-
exprt default_value;
63-
std::vector<std::pair<std::size_t, exprt>> entries;
64-
};
65-
66-
/// Represents arrays by the indexes up to which the value remains the same.
67-
/// For instance `{'a', 'a', 'a', 'b', 'b', 'c'}` would be represented by
68-
/// by ('a', 2) ; ('b', 4), ('c', 5).
69-
/// This is particularly useful when the array is constant on intervals.
70-
class interval_sparse_arrayt final : public sparse_arrayt
71-
{
72-
public:
73-
/// An expression of the form `array_of(x) with {i:=a} with {j:=b}` is
74-
/// converted to an array `arr` where for all index `k` smaller than `i`,
75-
/// `arr[k]` is `a`, for all index between `i` (exclusive) and `j` it is `b`
76-
/// and for the others it is `x`.
77-
explicit interval_sparse_arrayt(const with_exprt &expr);
78-
exprt to_if_expression(const exprt &index) const override;
79-
};
80-
8135
class string_refinementt final: public bv_refinementt
8236
{
8337
private:

‎src/solvers/refinement/string_refinement_util.cpp

+75
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
/*******************************************************************\
2+
3+
Module: String solver
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
#include <algorithm>
10+
#include <numeric>
11+
#include <util/arith_tools.h>
12+
#include <util/std_expr.h>
13+
#include "string_refinement_util.h"
14+
15+
sparse_arrayt::sparse_arrayt(const with_exprt &expr)
16+
{
17+
auto ref = std::ref(static_cast<const exprt &>(expr));
18+
while(can_cast_expr<with_exprt>(ref.get()))
19+
{
20+
const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
21+
const auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
22+
entries.emplace_back(current_index, with_expr.new_value());
23+
ref = with_expr.old();
24+
}
25+
26+
// This function only handles 'with' and 'array_of' expressions
27+
PRECONDITION(ref.get().id() == ID_array_of);
28+
default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
29+
}
30+
31+
exprt sparse_arrayt::to_if_expression(const exprt &index) const
32+
{
33+
return std::accumulate(
34+
entries.begin(),
35+
entries.end(),
36+
default_value,
37+
[&](
38+
const exprt if_expr,
39+
const std::pair<std::size_t, exprt> &entry) { // NOLINT
40+
const exprt entry_index = from_integer(entry.first, index.type());
41+
const exprt &then_expr = entry.second;
42+
CHECK_RETURN(then_expr.type() == if_expr.type());
43+
const equal_exprt index_equal(index, entry_index);
44+
return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
45+
});
46+
}
47+
48+
interval_sparse_arrayt::interval_sparse_arrayt(const with_exprt &expr)
49+
: sparse_arrayt(expr)
50+
{
51+
// Entries are sorted so that successive entries correspond to intervals
52+
std::sort(
53+
entries.begin(),
54+
entries.end(),
55+
[](
56+
const std::pair<std::size_t, exprt> &a,
57+
const std::pair<std::size_t, exprt> &b) { return a.first < b.first; });
58+
}
59+
60+
exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const
61+
{
62+
return std::accumulate(
63+
entries.rbegin(),
64+
entries.rend(),
65+
default_value,
66+
[&](
67+
const exprt if_expr,
68+
const std::pair<std::size_t, exprt> &entry) { // NOLINT
69+
const exprt entry_index = from_integer(entry.first, index.type());
70+
const exprt &then_expr = entry.second;
71+
CHECK_RETURN(then_expr.type() == if_expr.type());
72+
const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
73+
return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
74+
});
75+
}

‎src/solvers/refinement/string_refinement_util.h

+90
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
/*******************************************************************\
2+
3+
Module: String solver
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
10+
#define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
11+
12+
#include "string_constraint.h"
13+
14+
struct index_set_pairt
15+
{
16+
std::map<exprt, std::set<exprt>> cumulative;
17+
std::map<exprt, std::set<exprt>> current;
18+
};
19+
20+
struct string_axiomst
21+
{
22+
std::vector<string_constraintt> universal;
23+
std::vector<string_not_contains_constraintt> not_contains;
24+
};
25+
26+
/// Represents arrays of the form `array_of(x) with {i:=a} with {j:=b} ...`
27+
/// by a default value `x` and a list of entries `(i,a)`, `(j,b)` etc.
28+
class sparse_arrayt
29+
{
30+
public:
31+
/// Initialize a sparse array from an expression of the form
32+
/// `array_of(x) with {i:=a} with {j:=b} ...`
33+
/// This is the form in which array valuations coming from the underlying
34+
/// solver are given.
35+
explicit sparse_arrayt(const with_exprt &expr);
36+
37+
/// Creates an if_expr corresponding to the result of accessing the array
38+
/// at the given index
39+
virtual exprt to_if_expression(const exprt &index) const;
40+
41+
protected:
42+
exprt default_value;
43+
std::vector<std::pair<std::size_t, exprt>> entries;
44+
};
45+
46+
/// Represents arrays by the indexes up to which the value remains the same.
47+
/// For instance `{'a', 'a', 'a', 'b', 'b', 'c'}` would be represented by
48+
/// by ('a', 2) ; ('b', 4), ('c', 5).
49+
/// This is particularly useful when the array is constant on intervals.
50+
class interval_sparse_arrayt final : public sparse_arrayt
51+
{
52+
public:
53+
/// An expression of the form `array_of(x) with {i:=a} with {j:=b}` is
54+
/// converted to an array `arr` where for all index `k` smaller than `i`,
55+
/// `arr[k]` is `a`, for all index between `i` (exclusive) and `j` it is `b`
56+
/// and for the others it is `x`.
57+
explicit interval_sparse_arrayt(const with_exprt &expr);
58+
exprt to_if_expression(const exprt &index) const override;
59+
};
60+
61+
/// Maps equation to expressions contained in them and conversely expressions to
62+
/// equations that contain them. This can be used on a subset of expressions
63+
/// which interests us, in particular strings. Equations are identified by an
64+
/// index of type `std::size_t` for more efficient insertion and lookup.
65+
class equation_symbol_mappingt
66+
{
67+
public:
68+
// Record index of the equations that contain a given expression
69+
std::map<exprt, std::vector<std::size_t>> equations_containing;
70+
// Record expressions that are contained in the equation with the given index
71+
std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
72+
73+
void add(const std::size_t i, const exprt &expr)
74+
{
75+
equations_containing[expr].push_back(i);
76+
strings_in_equation[i].push_back(expr);
77+
}
78+
79+
std::vector<exprt> find_expressions(const std::size_t i)
80+
{
81+
return strings_in_equation[i];
82+
}
83+
84+
std::vector<std::size_t> find_equations(const exprt &expr)
85+
{
86+
return equations_containing[expr];
87+
}
88+
};
89+
90+
#endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H

0 commit comments

Comments
 (0)