Skip to content

Commit f4c79a6

Browse files
kroeningkroening
committed
cleanup array theory solver
1 parent 13a7538 commit f4c79a6

File tree

2 files changed

+65
-162
lines changed

2 files changed

+65
-162
lines changed

‎src/solvers/flattening/arrays.cpp‎

Lines changed: 65 additions & 160 deletions
Original file line numberDiff line numberDiff line change
@@ -108,73 +108,64 @@ void arrayst::collect_arrays(const exprt &a)
108108

109109
if(a.id()==ID_with)
110110
{
111-
if(a.operands().size()!=3)
112-
throw "with expected to have three operands";
111+
const with_exprt &with_expr=to_with_expr(a);
113112

114113
// check types
115-
if(!base_type_eq(array_type, a.op0().type(), ns))
114+
if(!base_type_eq(array_type, with_expr.old().type(), ns))
116115
{
117116
std::cout << a.pretty() << '\n';
118117
throw "collect_arrays got 'with' without matching types";
119118
}
120119

121-
arrays.make_union(a, a.op0());
122-
collect_arrays(a.op0());
120+
arrays.make_union(a, with_expr.old());
121+
collect_arrays(with_expr.old());
123122

124123
// make sure this shows as an application
125-
index_exprt index_expr;
126-
index_expr.type()=array_type.subtype();
127-
index_expr.array()=a.op0();
128-
index_expr.index()=a.op1();
124+
index_exprt index_expr(with_expr.old(), with_expr.where());
129125
record_array_index(index_expr);
130126
}
131-
else if(a.id()==ID_update) // TODO: is this obsolete?
127+
else if(a.id()==ID_update)
132128
{
133-
if(a.operands().size()!=3)
134-
throw "update expected to have three operands";
129+
const update_exprt &update_expr=to_update_expr(a);
135130

136131
// check types
137-
if(!base_type_eq(array_type, a.op0().type(), ns))
132+
if(!base_type_eq(array_type, update_expr.old().type(), ns))
138133
{
139134
std::cout << a.pretty() << '\n';
140135
throw "collect_arrays got 'update' without matching types";
141136
}
142137

143-
arrays.make_union(a, a.op0());
144-
collect_arrays(a.op0());
138+
arrays.make_union(a, update_expr.old());
139+
collect_arrays(update_expr.old());
145140

146141
#if 0
147142
// make sure this shows as an application
148-
index_exprt index_expr;
149-
index_expr.type()=array_type.subtype();
150-
index_expr.array()=a.op0();
151-
index_expr.index()=a.op1();
143+
index_exprt index_expr(update_expr.old(), update_expr.index());
152144
record_array_index(index_expr);
153145
#endif
154146
}
155147
else if(a.id()==ID_if)
156148
{
157-
if(a.operands().size()!=3)
158-
throw "if expected to have three operands";
149+
const if_exprt &if_expr=to_if_expr(a);
159150

160151
// check types
161-
if(!base_type_eq(array_type, a.op1().type(), ns))
152+
if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
162153
{
163154
std::cout << a.pretty() << '\n';
164155
throw "collect_arrays got if without matching types";
165156
}
166157

167158
// check types
168-
if(!base_type_eq(array_type, a.op2().type(), ns))
159+
if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
169160
{
170161
std::cout << a.pretty() << '\n';
171162
throw "collect_arrays got if without matching types";
172163
}
173164

174-
arrays.make_union(a, a.op1());
175-
arrays.make_union(a, a.op2());
176-
collect_arrays(a.op1());
177-
collect_arrays(a.op2());
165+
arrays.make_union(a, if_expr.true_case());
166+
arrays.make_union(a, if_expr.false_case());
167+
collect_arrays(if_expr.true_case());
168+
collect_arrays(if_expr.false_case());
178169
}
179170
else if(a.id()==ID_symbol)
180171
{
@@ -272,14 +263,11 @@ void arrayst::add_array_constraints()
272263
}
273264

274265
// add constraints for equalities
275-
for(array_equalitiest::const_iterator it=
276-
array_equalities.begin();
277-
it!=array_equalities.end();
278-
it++)
266+
for(const auto &equality : array_equalities)
279267
{
280-
add_array_constraints(
281-
index_map[arrays.find_number(it->f1)],
282-
*it);
268+
add_array_constraints_equality(
269+
index_map[arrays.find_number(equality.f1)],
270+
equality);
283271

284272
// update_index_map should not be necessary here
285273
}
@@ -333,10 +321,8 @@ void arrayst::add_array_Ackermann_constraints()
333321

334322
if(indices_equal_lit!=const_literal(false))
335323
{
336-
index_exprt index_expr1;
337-
index_expr1.type()=ns.follow(arrays[i].type()).subtype();
338-
index_expr1.array()=arrays[i];
339-
index_expr1.index()=*i1;
324+
const typet &subtype=ns.follow(arrays[i].type()).subtype();
325+
index_exprt index_expr1(arrays[i], *i1, subtype);
340326

341327
index_exprt index_expr2=index_expr1;
342328
index_expr2.index()=*i2;
@@ -387,52 +373,39 @@ void arrayst::update_index_map(bool update_all)
387373
}
388374
else
389375
{
390-
for(std::set<std::size_t>::const_iterator
391-
it=update_indices.begin();
392-
it!=update_indices.end(); it++)
393-
update_index_map(*it);
376+
for(const auto &index : update_indices)
377+
update_index_map(index);
378+
394379
update_indices.clear();
395380
}
396381

397382
#ifdef DEBUG
398383
// print index sets
399-
for(index_mapt::const_iterator
400-
i1=index_map.begin();
401-
i1!=index_map.end();
402-
i1++)
403-
for(index_sett::const_iterator
404-
i2=i1->second.begin();
405-
i2!=i1->second.end();
406-
i2++)
407-
std::cout << "Index set (" << i1->first << " = "
408-
<< arrays.find_number(i1->first) << " = "
409-
<< from_expr(ns, "", arrays[arrays.find_number(i1->first)])
384+
for(const auto &index_entry : index_map)
385+
for(const auto &index : index_entry.second)
386+
std::cout << "Index set (" << index_entry.first << " = "
387+
<< arrays.find_number(index_entry.first) << " = "
388+
<< from_expr(ns, "",
389+
arrays[arrays.find_number(index_entry.first)])
410390
<< "): "
411-
<< from_expr(ns, "", *i2) << '\n';
391+
<< from_expr(ns, "", index) << '\n';
412392
std::cout << "-----\n";
413393
#endif
414394
}
415395

416-
void arrayst::add_array_constraints(
396+
void arrayst::add_array_constraints_equality(
417397
const index_sett &index_set,
418398
const array_equalityt &array_equality)
419399
{
420400
// add constraints x=y => x[i]=y[i]
421401

422-
for(index_sett::const_iterator
423-
it=index_set.begin();
424-
it!=index_set.end();
425-
it++)
402+
for(const auto &index : index_set)
426403
{
427-
index_exprt index_expr1;
428-
index_expr1.type()=ns.follow(array_equality.f1.type()).subtype();
429-
index_expr1.array()=array_equality.f1;
430-
index_expr1.index()=*it;
404+
const typet &subtype1=ns.follow(array_equality.f1.type()).subtype();
405+
index_exprt index_expr1(array_equality.f1, index, subtype1);
431406

432-
index_exprt index_expr2;
433-
index_expr2.type()=ns.follow(array_equality.f2.type()).subtype();
434-
index_expr2.array()=array_equality.f2;
435-
index_expr2.index()=*it;
407+
const typet &subtype2=ns.follow(array_equality.f2.type()).subtype();
408+
index_exprt index_expr2(array_equality.f2, index, subtype2);
436409

437410
assert(index_expr1.type()==index_expr2.type());
438411

@@ -484,20 +457,11 @@ void arrayst::add_array_constraints(
484457
assert(expr.operands().size()==1);
485458

486459
// add a[i]=b[i]
487-
for(index_sett::const_iterator
488-
it=index_set.begin();
489-
it!=index_set.end();
490-
it++)
460+
for(const auto &index : index_set)
491461
{
492-
index_exprt index_expr1;
493-
index_expr1.type()=ns.follow(expr.type()).subtype();
494-
index_expr1.array()=expr;
495-
index_expr1.index()=*it;
496-
497-
index_exprt index_expr2;
498-
index_expr2.type()=ns.follow(expr.type()).subtype();
499-
index_expr2.array()=expr.op0();
500-
index_expr2.index()=*it;
462+
const typet &subtype=ns.follow(expr.type()).subtype();
463+
index_exprt index_expr1(expr, index, subtype);
464+
index_exprt index_expr2(expr.op0(), index, subtype);
501465

502466
assert(index_expr1.type()==index_expr2.type());
503467

@@ -527,10 +491,7 @@ void arrayst::add_array_constraints_with(
527491
const exprt &value=expr.new_value();
528492

529493
{
530-
index_exprt index_expr;
531-
index_expr.type()=ns.follow(expr.type()).subtype();
532-
index_expr.array()=expr;
533-
index_expr.index()=index;
494+
index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
534495

535496
if(index_expr.type()!=value.type())
536497
{
@@ -546,13 +507,8 @@ void arrayst::add_array_constraints_with(
546507
// use other array index applications for "else" case
547508
// add constraint x[I]=y[I] for I!=i
548509

549-
for(index_sett::const_iterator
550-
it=index_set.begin();
551-
it!=index_set.end();
552-
it++)
510+
for(auto other_index : index_set)
553511
{
554-
exprt other_index=*it;
555-
556512
if(other_index!=index)
557513
{
558514
// we first build the guard
@@ -564,17 +520,9 @@ void arrayst::add_array_constraints_with(
564520

565521
if(guard_lit!=const_literal(true))
566522
{
567-
index_exprt index_expr1;
568-
index_expr1.type()=ns.follow(expr.type()).subtype();
569-
index_expr1.array()=expr;
570-
index_expr1.index()=other_index;
571-
572-
index_exprt index_expr2;
573-
index_expr2.type()=ns.follow(expr.type()).subtype();
574-
index_expr2.array()=expr.op0();
575-
index_expr2.index()=other_index;
576-
577-
assert(index_expr1.type()==index_expr2.type());
523+
const typet &subtype=ns.follow(expr.type()).subtype();
524+
index_exprt index_expr1(expr, other_index, subtype);
525+
index_exprt index_expr2(expr.op0(), other_index, subtype);
578526

579527
equal_exprt equality_expr(index_expr1, index_expr2);
580528

@@ -611,10 +559,7 @@ void arrayst::add_array_constraints_update(
611559
const exprt &value=expr.new_value();
612560

613561
{
614-
index_exprt index_expr;
615-
index_expr.type()=ns.follow(expr.type()).subtype();
616-
index_expr.array()=expr;
617-
index_expr.index()=index;
562+
index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
618563

619564
if(index_expr.type()!=value.type())
620565
{
@@ -628,13 +573,8 @@ void arrayst::add_array_constraints_update(
628573
// use other array index applications for "else" case
629574
// add constraint x[I]=y[I] for I!=i
630575

631-
for(index_sett::const_iterator
632-
it=index_set.begin();
633-
it!=index_set.end();
634-
it++)
576+
for(auto other_index : index_set)
635577
{
636-
exprt other_index=*it;
637-
638578
if(other_index!=index)
639579
{
640580
// we first build the guard
@@ -646,17 +586,9 @@ void arrayst::add_array_constraints_update(
646586

647587
if(guard_lit!=const_literal(true))
648588
{
649-
index_exprt index_expr1;
650-
index_expr1.type()=ns.follow(expr.type()).subtype();
651-
index_expr1.array()=expr;
652-
index_expr1.index()=other_index;
653-
654-
index_exprt index_expr2;
655-
index_expr2.type()=ns.follow(expr.type()).subtype();
656-
index_expr2.array()=expr.op0();
657-
index_expr2.index()=other_index;
658-
659-
assert(index_expr1.type()==index_expr2.type());
589+
const typet &subtype=ns.follow(expr.type()).subtype();
590+
index_exprt index_expr1(expr, other_index, subtype);
591+
index_exprt index_expr2(expr.op0(), other_index, subtype);
660592

661593
equal_exprt equality_expr(index_expr1, index_expr2);
662594

@@ -682,15 +614,10 @@ void arrayst::add_array_constraints_array_of(
682614
// get other array index applications
683615
// and add constraint x[i]=v
684616

685-
for(index_sett::const_iterator
686-
it=index_set.begin();
687-
it!=index_set.end();
688-
it++)
617+
for(const auto &index : index_set)
689618
{
690-
index_exprt index_expr;
691-
index_expr.type()=ns.follow(expr.type()).subtype();
692-
index_expr.array()=expr;
693-
index_expr.index()=*it;
619+
const typet &subtype=ns.follow(expr.type()).subtype();
620+
index_exprt index_expr(expr, index, subtype);
694621

695622
assert(base_type_eq(index_expr.type(), expr.op0().type(), ns));
696623

@@ -714,22 +641,11 @@ void arrayst::add_array_constraints_if(
714641

715642
// first do true case
716643

717-
for(index_sett::const_iterator
718-
it=index_set.begin();
719-
it!=index_set.end();
720-
it++)
644+
for(const auto &index : index_set)
721645
{
722-
index_exprt index_expr1;
723-
index_expr1.type()=ns.follow(expr.type()).subtype();
724-
index_expr1.array()=expr;
725-
index_expr1.index()=*it;
726-
727-
index_exprt index_expr2;
728-
index_expr2.type()=ns.follow(expr.type()).subtype();
729-
index_expr2.array()=expr.true_case();
730-
index_expr2.index()=*it;
731-
732-
assert(index_expr1.type()==index_expr2.type());
646+
const typet subtype=ns.follow(expr.type()).subtype();
647+
index_exprt index_expr1(expr, index, subtype);
648+
index_exprt index_expr2(expr.true_case(), index, subtype);
733649

734650
// add implication
735651
lazy_constraintt lazy(lazy_typet::ARRAY_IF,
@@ -743,22 +659,11 @@ void arrayst::add_array_constraints_if(
743659
}
744660

745661
// now the false case
746-
for(index_sett::const_iterator
747-
it=index_set.begin();
748-
it!=index_set.end();
749-
it++)
662+
for(const auto &index : index_set)
750663
{
751-
index_exprt index_expr1;
752-
index_expr1.type()=ns.follow(expr.type()).subtype();
753-
index_expr1.array()=expr;
754-
index_expr1.index()=*it;
755-
756-
index_exprt index_expr2;
757-
index_expr2.type()=ns.follow(expr.type()).subtype();
758-
index_expr2.array()=expr.false_case();
759-
index_expr2.index()=*it;
760-
761-
assert(index_expr1.type()==index_expr2.type());
664+
const typet subtype=ns.follow(expr.type()).subtype();
665+
index_exprt index_expr1(expr, index, subtype);
666+
index_exprt index_expr2(expr.false_case(), index, subtype);
762667

763668
// add implication
764669
lazy_constraintt lazy(

‎src/solvers/flattening/arrays.h‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -105,8 +105,6 @@ class arrayst:public equalityt
105105
const index_sett &index_set, const array_equalityt &array_equality);
106106
void add_array_constraints(
107107
const index_sett &index_set, const exprt &expr);
108-
void add_array_constraints(
109-
const index_sett &index_set, const array_equalityt &array_equality);
110108
void add_array_constraints_if(
111109
const index_sett &index_set, const if_exprt &exprt);
112110
void add_array_constraints_with(

0 commit comments

Comments
 (0)