Skip to content

Commit a65407e

Browse files
jasigaljasigal
committed
TG-672 Grouped index sets together
1 parent 503c49d commit a65407e

File tree

2 files changed

+55
-73
lines changed

2 files changed

+55
-73
lines changed

‎src/solvers/refinement/string_refinement.cpp‎

Lines changed: 47 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -55,35 +55,30 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
5555
const replace_mapt &symbol_resolve);
5656

5757
static void initial_index_set(
58-
std::map<exprt, std::set<exprt>> &index_set,
59-
std::map<exprt, std::set<exprt>> &current_index_set,
58+
index_set_pairt &index_set,
6059
const namespacet &ns,
6160
const string_constraintt &axiom);
6261

6362
static void initial_index_set(
64-
std::map<exprt, std::set<exprt>> &index_set,
65-
std::map<exprt, std::set<exprt>> &current_index_set,
63+
index_set_pairt &index_set,
6664
const namespacet &ns,
6765
const string_not_contains_constraintt &axiom);
6866

6967
static void initial_index_set(
70-
std::map<exprt, std::set<exprt>> &index_set,
71-
std::map<exprt, std::set<exprt>> &current_index_set,
68+
index_set_pairt &index_set,
7269
const namespacet &ns,
7370
const std::vector<string_constraintt> &string_axioms,
7471
const std::vector<string_not_contains_constraintt> &nc_axioms);
7572

7673
exprt simplify_sum(const exprt &f);
7774

7875
static void update_index_set(
79-
std::map<exprt, std::set<exprt>> &index_set,
80-
std::map<exprt, std::set<exprt>> &current_index_set,
76+
index_set_pairt &index_set,
8177
const namespacet &ns,
8278
const std::vector<exprt> &current_constraints);
8379

8480
static void update_index_set(
85-
std::map<exprt, std::set<exprt>> &index_set,
86-
std::map<exprt, std::set<exprt>> &current_index_set,
81+
index_set_pairt &index_set,
8782
const namespacet &ns,
8883
const exprt &formula);
8984

@@ -95,8 +90,7 @@ static exprt instantiate(
9590

9691
static std::vector<exprt> instantiate(
9792
const string_not_contains_constraintt &axiom,
98-
const std::map<exprt, std::set<exprt>> &index_set,
99-
const std::map<exprt, std::set<exprt>> &current_index_set,
93+
const index_set_pairt &index_set,
10094
const string_constraint_generatort &generator);
10195

10296
static exprt get_array(
@@ -211,21 +205,20 @@ string_refinementt::string_refinementt(const infot &info):
211205
static void display_index_set(
212206
messaget::mstreamt stream,
213207
const namespacet &ns,
214-
const std::map<exprt, std::set<exprt>> &current_index_set,
215-
const std::map<exprt, std::set<exprt>> &index_set)
208+
const index_set_pairt &index_set)
216209
{
217210
const auto eom=messaget::eom;
218211
std::size_t count=0;
219212
std::size_t count_current=0;
220-
for(const auto &i : index_set)
213+
for(const auto &i : index_set.cumulative)
221214
{
222215
const exprt &s=i.first;
223216
stream << "IS(" << from_expr(ns, "", s) << ")=={" << eom;
224217

225218
for(const auto &j : i.second)
226219
{
227-
const auto it=current_index_set.find(i.first);
228-
if(it!=current_index_set.end() && it->second.find(j)!=it->second.end())
220+
const auto it=index_set.current.find(i.first);
221+
if(it!=index_set.current.end() && it->second.find(j)!=it->second.end())
229222
{
230223
count_current++;
231224
stream << "**";
@@ -243,13 +236,12 @@ static std::vector<exprt> generate_instantiations(
243236
messaget::mstreamt &stream,
244237
const namespacet &ns,
245238
string_constraint_generatort &generator,
246-
const std::map<exprt, std::set<exprt>> &index_set,
247-
const std::map<exprt, std::set<exprt>> &current_index_set,
239+
const index_set_pairt &index_set,
248240
const std::vector<string_constraintt> &universal_axioms,
249241
const std::vector<string_not_contains_constraintt> &not_contains_axioms)
250242
{
251243
std::vector<exprt> lemmas;
252-
for(const auto &i : current_index_set)
244+
for(const auto &i : index_set.current)
253245
{
254246
for(const auto &univ_axiom : universal_axioms)
255247
{
@@ -260,7 +252,7 @@ static std::vector<exprt> generate_instantiations(
260252
for(const auto &nc_axiom : not_contains_axioms)
261253
{
262254
for(const auto &instance :
263-
instantiate(nc_axiom, index_set, current_index_set, generator))
255+
instantiate(nc_axiom, index_set, generator))
264256
lemmas.push_back(instance);
265257
}
266258
return lemmas;
@@ -758,21 +750,19 @@ decision_proceduret::resultt string_refinementt::dec_solve()
758750
}
759751

760752
initial_index_set(
761-
index_set,
762-
current_index_set,
753+
index_sets,
763754
ns,
764755
universal_axioms,
765756
not_contains_axioms);
766-
update_index_set(index_set, current_index_set, ns, current_constraints);
767-
display_index_set(debug(), ns, current_index_set, index_set);
757+
update_index_set(index_sets, ns, current_constraints);
758+
display_index_set(debug(), ns, index_sets);
768759
current_constraints.clear();
769760
for(const auto &instance :
770761
generate_instantiations(
771762
debug(),
772763
ns,
773764
generator,
774-
index_set,
775-
current_index_set,
765+
index_sets,
776766
universal_axioms,
777767
not_contains_axioms))
778768
add_lemma(instance);
@@ -818,24 +808,23 @@ decision_proceduret::resultt string_refinementt::dec_solve()
818808
// the property we are checking by adding more indices to the index set,
819809
// and instantiating universal formulas with this indices.
820810
// We will then relaunch the solver with these added lemmas.
821-
current_index_set.clear();
822-
update_index_set(index_set, current_index_set, ns, current_constraints);
811+
index_sets.current.clear();
812+
update_index_set(index_sets, ns, current_constraints);
823813

824-
if(current_index_set.empty())
814+
if(index_sets.current.empty())
825815
{
826816
debug() << "current index set is empty" << eom;
827817
return resultt::D_ERROR;
828818
}
829819

830-
display_index_set(debug(), ns, current_index_set, index_set);
820+
display_index_set(debug(), ns, index_sets);
831821
current_constraints.clear();
832822
for(const auto &instance :
833823
generate_instantiations(
834824
debug(),
835825
ns,
836826
generator,
837-
index_set,
838-
current_index_set,
827+
index_sets,
839828
universal_axioms,
840829
not_contains_axioms))
841830
add_lemma(instance);
@@ -1730,28 +1719,26 @@ static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
17301719
/// upper bound minus one
17311720
/// \par parameters: a list of string constraints
17321721
static void initial_index_set(
1733-
std::map<exprt, std::set<exprt>> &index_set,
1734-
std::map<exprt, std::set<exprt>> &current_index_set,
1722+
index_set_pairt &index_set,
17351723
const namespacet &ns,
17361724
const std::vector<string_constraintt> &string_axioms,
17371725
const std::vector<string_not_contains_constraintt> &nc_axioms)
17381726
{
17391727
for(const auto &axiom : string_axioms)
1740-
initial_index_set(index_set, current_index_set, ns, axiom);
1728+
initial_index_set(index_set, ns, axiom);
17411729
for(const auto &axiom : nc_axioms)
1742-
initial_index_set(index_set, current_index_set, ns, axiom);
1730+
initial_index_set(index_set, ns, axiom);
17431731
}
17441732

17451733
/// add to the index set all the indices that appear in the formulas
17461734
/// \par parameters: a list of string constraints
17471735
static void update_index_set(
1748-
std::map<exprt, std::set<exprt>> &index_set,
1749-
std::map<exprt, std::set<exprt>> &current_index_set,
1736+
index_set_pairt &index_set,
17501737
const namespacet &ns,
17511738
const std::vector<exprt> &current_constraints)
17521739
{
17531740
for(const auto &axiom : current_constraints)
1754-
update_index_set(index_set, current_index_set, ns, axiom);
1741+
update_index_set(index_set, ns, axiom);
17551742
}
17561743

17571744
/// An expression representing an array of characters can be in the form of an
@@ -1782,8 +1769,7 @@ static std::vector<exprt> sub_arrays(const exprt &array_expr)
17821769
/// upper bound minus one
17831770
/// \par parameters: a string constraint
17841771
static void add_to_index_set(
1785-
std::map<exprt, std::set<exprt>> &index_set,
1786-
std::map<exprt, std::set<exprt>> &current_index_set,
1772+
index_set_pairt &index_set,
17871773
const namespacet &ns,
17881774
const exprt &s,
17891775
exprt i)
@@ -1793,14 +1779,13 @@ static void add_to_index_set(
17931779
if(i.id()!=ID_constant || is_size_t)
17941780
{
17951781
for(const auto &sub : sub_arrays(s))
1796-
if(index_set[sub].insert(i).second)
1797-
current_index_set[sub].insert(i);
1782+
if(index_set.cumulative[sub].insert(i).second)
1783+
index_set.current[sub].insert(i);
17981784
}
17991785
}
18001786

18011787
static void initial_index_set(
1802-
std::map<exprt, std::set<exprt>> &index_set,
1803-
std::map<exprt, std::set<exprt>> &current_index_set,
1788+
index_set_pairt &index_set,
18041789
const namespacet &ns,
18051790
const string_constraintt &axiom)
18061791
{
@@ -1822,7 +1807,7 @@ static void initial_index_set(
18221807
// if cur is of the form s[i] and no quantified variable appears in i
18231808
if(!has_quant_var)
18241809
{
1825-
add_to_index_set(index_set, current_index_set, ns, s, i);
1810+
add_to_index_set(index_set, ns, s, i);
18261811
}
18271812
else
18281813
{
@@ -1832,7 +1817,7 @@ static void initial_index_set(
18321817
axiom.upper_bound(),
18331818
from_integer(1, axiom.upper_bound().type()));
18341819
replace_expr(qvar, kminus1, e);
1835-
add_to_index_set(index_set, current_index_set, ns, s, e);
1820+
add_to_index_set(index_set, ns, s, e);
18361821
}
18371822
}
18381823
else
@@ -1842,8 +1827,7 @@ static void initial_index_set(
18421827
}
18431828

18441829
static void initial_index_set(
1845-
std::map<exprt, std::set<exprt>> &index_set,
1846-
std::map<exprt, std::set<exprt>> &current_index_set,
1830+
index_set_pairt &index_set,
18471831
const namespacet &ns,
18481832
const string_not_contains_constraintt &axiom)
18491833
{
@@ -1857,7 +1841,7 @@ static void initial_index_set(
18571841
const exprt &i=it->op1();
18581842

18591843
// cur is of the form s[i] and no quantified variable appears in i
1860-
add_to_index_set(index_set, current_index_set, ns, s, i);
1844+
add_to_index_set(index_set, ns, s, i);
18611845

18621846
it.next_sibling_or_parent();
18631847
}
@@ -1868,19 +1852,13 @@ static void initial_index_set(
18681852
minus_exprt kminus1(
18691853
axiom.exists_upper_bound(),
18701854
from_integer(1, axiom.exists_upper_bound().type()));
1871-
add_to_index_set(
1872-
index_set,
1873-
current_index_set,
1874-
ns,
1875-
axiom.s1().content(),
1876-
kminus1);
1855+
add_to_index_set(index_set, ns, axiom.s1().content(), kminus1);
18771856
}
18781857

18791858
/// add to the index set all the indices that appear in the formula
18801859
/// \par parameters: a string constraint
18811860
static void update_index_set(
1882-
std::map<exprt, std::set<exprt>> &index_set,
1883-
std::map<exprt, std::set<exprt>> &current_index_set,
1861+
index_set_pairt &index_set,
18841862
const namespacet &ns,
18851863
const exprt &formula)
18861864
{
@@ -1899,7 +1877,7 @@ static void update_index_set(
18991877
s.type().id()==ID_array,
19001878
string_refinement_invariantt("index expressions must index on arrays"));
19011879
exprt simplified=simplify_sum(i);
1902-
add_to_index_set(index_set, current_index_set, ns, s, simplified);
1880+
add_to_index_set(index_set, ns, s, simplified);
19031881
}
19041882
else
19051883
{
@@ -1987,22 +1965,21 @@ static exprt instantiate(
19871965
/// \return the lemmas produced through instantiation
19881966
static std::vector<exprt> instantiate(
19891967
const string_not_contains_constraintt &axiom,
1990-
const std::map<exprt, std::set<exprt>> &index_set,
1991-
const std::map<exprt, std::set<exprt>> &current_index_set,
1968+
const index_set_pairt &index_set,
19921969
const string_constraint_generatort &generator)
19931970
{
19941971
const string_exprt &s0=axiom.s0();
19951972
const string_exprt &s1=axiom.s1();
19961973

1997-
const auto &index_set0=index_set.find(s0.content());
1998-
const auto &index_set1=index_set.find(s1.content());
1999-
const auto &current_index_set0=current_index_set.find(s0.content());
2000-
const auto &current_index_set1=current_index_set.find(s1.content());
1974+
const auto &index_set0=index_set.cumulative.find(s0.content());
1975+
const auto &index_set1=index_set.cumulative.find(s1.content());
1976+
const auto &current_index_set0=index_set.current.find(s0.content());
1977+
const auto &current_index_set1=index_set.current.find(s1.content());
20011978

2002-
if(index_set0!=index_set.end() &&
2003-
index_set1!=index_set.end() &&
2004-
current_index_set0!=index_set.end() &&
2005-
current_index_set1!=index_set.end())
1979+
if(index_set0!=index_set.cumulative.end() &&
1980+
index_set1!=index_set.cumulative.end() &&
1981+
current_index_set0!=index_set.current.end() &&
1982+
current_index_set1!=index_set.current.end())
20061983
{
20071984
typedef std::pair<exprt, exprt> expr_pairt;
20081985
std::set<expr_pairt> index_pairs;

‎src/solvers/refinement/string_refinement.h‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,12 @@ Author: Alberto Griggio, [email protected]
2929

3030
#define MAX_NB_REFINEMENT 100
3131

32+
struct index_set_pairt
33+
{
34+
std::map<exprt, std::set<exprt>> cumulative;
35+
std::map<exprt, std::set<exprt>> current;
36+
};
37+
3238
class string_refinementt final: public bv_refinementt
3339
{
3440
private:
@@ -74,16 +80,15 @@ class string_refinementt final: public bv_refinementt
7480
expr_sett seen_instances;
7581

7682
std::vector<string_constraintt> universal_axioms;
77-
7883
std::vector<string_not_contains_constraintt> not_contains_axioms;
7984

8085
// Unquantified lemmas that have newly been added
8186
std::vector<exprt> current_constraints;
8287

8388
// See the definition in the PASS article
8489
// Warning: this is indexed by array_expressions and not string expressions
85-
std::map<exprt, expr_sett> current_index_set;
86-
std::map<exprt, expr_sett> index_set;
90+
91+
index_set_pairt index_sets;
8792
replace_mapt symbol_resolve;
8893
std::map<exprt, exprt_listt> reverse_symbol_resolve;
8994
std::list<std::pair<exprt, bool>> non_string_axioms;

0 commit comments

Comments
 (0)