Skip to content

Commit f88fcae

Browse files
danpoedanpoe
committed
Refactor usage of datatype_map in smt2_conv.cpp
1 parent cff2694 commit f88fcae

File tree

1 file changed

+23
-78
lines changed

1 file changed

+23
-78
lines changed

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 23 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -942,12 +942,7 @@ void smt2_convt::convert_expr(const exprt &expr)
942942
{
943943
if(use_datatypes)
944944
{
945-
INVARIANT(
946-
datatype_map.find(bitnot_expr.type()) != datatype_map.end(),
947-
"type shall have been mapped to Z3 datatype");
948-
949-
const std::string &smt_typename =
950-
datatype_map.find(bitnot_expr.type())->second;
945+
const std::string &smt_typename = datatype_map.at(bitnot_expr.type());
951946

952947
// extract elements
953948
const vector_typet &vector_type = to_vector_type(bitnot_expr.type());
@@ -1010,12 +1005,8 @@ void smt2_convt::convert_expr(const exprt &expr)
10101005
{
10111006
if(use_datatypes)
10121007
{
1013-
INVARIANT(
1014-
datatype_map.find(unary_minus_expr.type()) != datatype_map.end(),
1015-
"type shall have been mapped to Z3 datatype");
1016-
10171008
const std::string &smt_typename =
1018-
datatype_map.find(unary_minus_expr.type())->second;
1009+
datatype_map.at(unary_minus_expr.type());
10191010

10201011
// extract elements
10211012
const vector_typet &vector_type =
@@ -1803,11 +1794,7 @@ void smt2_convt::convert_expr(const exprt &expr)
18031794

18041795
if(use_datatypes)
18051796
{
1806-
INVARIANT(
1807-
datatype_map.find(vector_type) != datatype_map.end(),
1808-
"type shall have been mapped to Z3 datatype");
1809-
1810-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
1797+
const std::string &smt_typename = datatype_map.at(vector_type);
18111798

18121799
out << "(mk-" << smt_typename;
18131800
}
@@ -2592,10 +2579,7 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
25922579

25932580
if(use_datatypes)
25942581
{
2595-
INVARIANT(
2596-
datatype_map.find(struct_type) != datatype_map.end(),
2597-
"type should have been mapped to Z3 datatype");
2598-
const std::string &smt_typename = datatype_map.find(struct_type)->second;
2582+
const std::string &smt_typename = datatype_map.at(struct_type);
25992583

26002584
// use the constructor for the Z3 datatype
26012585
out << "(mk-" << smt_typename;
@@ -3079,11 +3063,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
30793063

30803064
if(use_datatypes)
30813065
{
3082-
INVARIANT(
3083-
datatype_map.find(vector_type) != datatype_map.end(),
3084-
"type should have been mapped to Z3 datatype");
3085-
3086-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
3066+
const std::string &smt_typename = datatype_map.at(vector_type);
30873067

30883068
out << "(mk-" << smt_typename;
30893069
}
@@ -3280,11 +3260,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
32803260

32813261
if(use_datatypes)
32823262
{
3283-
INVARIANT(
3284-
datatype_map.find(vector_type) != datatype_map.end(),
3285-
"type should have been mapped to Z3 datatype");
3286-
3287-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
3263+
const std::string &smt_typename = datatype_map.at(vector_type);
32883264

32893265
out << "(mk-" << smt_typename;
32903266
}
@@ -3589,10 +3565,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
35893565

35903566
if(use_datatypes)
35913567
{
3592-
INVARIANT(
3593-
datatype_map.find(expr_type) != datatype_map.end(),
3594-
"type shall have been mapped to Z3 datatype");
3595-
const std::string &smt_typename = datatype_map.find(expr_type)->second;
3568+
const std::string &smt_typename = datatype_map.at(expr_type);
35963569

35973570
out << "(update-" << smt_typename << "." << component_name << " ";
35983571
convert_expr(expr.op0());
@@ -3820,10 +3793,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
38203793

38213794
if(use_datatypes)
38223795
{
3823-
INVARIANT(
3824-
datatype_map.find(vector_type) != datatype_map.end(),
3825-
"type should have been mapped to Z3 datatype");
3826-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
3796+
const std::string &smt_typename = datatype_map.at(vector_type);
38273797

38283798
// this is easy for constant indicies
38293799

@@ -3866,10 +3836,7 @@ void smt2_convt::convert_member(const member_exprt &expr)
38663836

38673837
if(use_datatypes)
38683838
{
3869-
INVARIANT(
3870-
datatype_map.find(struct_type) != datatype_map.end(),
3871-
"type should have been mapped to Z3 datatype");
3872-
const std::string &smt_typename = datatype_map.find(struct_type)->second;
3839+
const std::string &smt_typename = datatype_map.at(struct_type);
38733840

38743841
out << "(" << smt_typename << "."
38753842
<< struct_type.get_component(name).get_name()
@@ -3926,11 +3893,7 @@ void smt2_convt::flatten2bv(const exprt &expr)
39263893
{
39273894
if(use_datatypes)
39283895
{
3929-
INVARIANT(
3930-
datatype_map.find(type) != datatype_map.end(),
3931-
"type should have been mapped to Z3 datatype");
3932-
3933-
const std::string &smt_typename = datatype_map.find(type)->second;
3896+
const std::string &smt_typename = datatype_map.at(type);
39343897

39353898
// concatenate elements
39363899
const vector_typet &vector_type=to_vector_type(type);
@@ -3961,11 +3924,7 @@ void smt2_convt::flatten2bv(const exprt &expr)
39613924
{
39623925
if(use_datatypes)
39633926
{
3964-
INVARIANT(
3965-
datatype_map.find(type) != datatype_map.end(),
3966-
"type should have been mapped to Z3 datatype");
3967-
3968-
const std::string &smt_typename = datatype_map.find(type)->second;
3927+
const std::string &smt_typename = datatype_map.at(type);
39693928

39703929
// concatenate elements
39713930
const struct_typet &struct_type=to_struct_type(type);
@@ -4028,11 +3987,7 @@ void smt2_convt::unflatten(
40283987
{
40293988
if(use_datatypes)
40303989
{
4031-
INVARIANT(
4032-
datatype_map.find(type) != datatype_map.end(),
4033-
"type should have been mapped to Z3 datatype");
4034-
4035-
const std::string &smt_typename = datatype_map.find(type)->second;
3990+
const std::string &smt_typename = datatype_map.at(type);
40363991

40373992
// extract elements
40383993
const vector_typet &vector_type=to_vector_type(type);
@@ -4079,11 +4034,7 @@ void smt2_convt::unflatten(
40794034
{
40804035
out << ")) ";
40814036

4082-
INVARIANT(
4083-
datatype_map.find(type) != datatype_map.end(),
4084-
"type should have been mapped to Z3 datatype");
4085-
4086-
const std::string &smt_typename = datatype_map.find(type)->second;
4037+
const std::string &smt_typename = datatype_map.at(type);
40874038

40884039
out << "(mk-" << smt_typename;
40894040

@@ -4459,10 +4410,7 @@ void smt2_convt::convert_type(const typet &type)
44594410
{
44604411
if(use_datatypes)
44614412
{
4462-
INVARIANT(
4463-
datatype_map.find(type) != datatype_map.end(),
4464-
"type should have been converted to Z3 datatype");
4465-
out << datatype_map.find(type)->second;
4413+
out << datatype_map.at(type);
44664414
}
44674415
else
44684416
{
@@ -4477,10 +4425,7 @@ void smt2_convt::convert_type(const typet &type)
44774425
{
44784426
if(use_datatypes)
44794427
{
4480-
INVARIANT(
4481-
datatype_map.find(type) != datatype_map.end(),
4482-
"type should have been converted to Z3 datatype");
4483-
out << datatype_map.find(type)->second;
4428+
out << datatype_map.at(type);
44844429
}
44854430
else
44864431
{
@@ -4556,10 +4501,7 @@ void smt2_convt::convert_type(const typet &type)
45564501
{
45574502
if(use_datatypes)
45584503
{
4559-
INVARIANT(
4560-
datatype_map.find(type) != datatype_map.end(),
4561-
"type should have been converted to Z3 datatype");
4562-
out << datatype_map.find(type)->second;
4504+
out << datatype_map.at(type);
45634505
}
45644506
else
45654507
{
@@ -4609,7 +4551,8 @@ void smt2_convt::find_symbols_rec(
46094551
if(use_datatypes &&
46104552
datatype_map.find(type)==datatype_map.end())
46114553
{
4612-
std::string smt_typename = "complex."+std::to_string(datatype_map.size());
4554+
const std::string smt_typename =
4555+
"complex." + std::to_string(datatype_map.size());
46134556
datatype_map[type] = smt_typename;
46144557

46154558
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4637,7 +4580,8 @@ void smt2_convt::find_symbols_rec(
46374580

46384581
mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
46394582

4640-
std::string smt_typename = "vector."+std::to_string(datatype_map.size());
4583+
const std::string smt_typename =
4584+
"vector." + std::to_string(datatype_map.size());
46414585
datatype_map[type] = smt_typename;
46424586

46434587
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4660,7 +4604,8 @@ void smt2_convt::find_symbols_rec(
46604604
if(use_datatypes &&
46614605
datatype_map.find(type)==datatype_map.end())
46624606
{
4663-
std::string smt_typename = "struct."+std::to_string(datatype_map.size());
4607+
const std::string smt_typename =
4608+
"struct." + std::to_string(datatype_map.size());
46644609
datatype_map[type] = smt_typename;
46654610
need_decl=true;
46664611
}
@@ -4674,7 +4619,7 @@ void smt2_convt::find_symbols_rec(
46744619
// Declare the corresponding SMT type if we haven't already.
46754620
if(need_decl)
46764621
{
4677-
std::string smt_typename = datatype_map[type];
4622+
const std::string &smt_typename = datatype_map.at(type);
46784623

46794624
// We're going to create a datatype named something like `struct.0'.
46804625
// It's going to have a single constructor named `mk-struct.0' with an

0 commit comments

Comments
 (0)