Skip to content

Commit 244316c

Browse files
danpoedanpoe
committed
Refactor usage of datatype_map in smt2_conv.cpp
1 parent f885e6c commit 244316c

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

@@ -4462,10 +4413,7 @@ void smt2_convt::convert_type(const typet &type)
44624413
{
44634414
if(use_datatypes)
44644415
{
4465-
INVARIANT(
4466-
datatype_map.find(type) != datatype_map.end(),
4467-
"type should have been converted to Z3 datatype");
4468-
out << datatype_map.find(type)->second;
4416+
out << datatype_map.at(type);
44694417
}
44704418
else
44714419
{
@@ -4480,10 +4428,7 @@ void smt2_convt::convert_type(const typet &type)
44804428
{
44814429
if(use_datatypes)
44824430
{
4483-
INVARIANT(
4484-
datatype_map.find(type) != datatype_map.end(),
4485-
"type should have been converted to Z3 datatype");
4486-
out << datatype_map.find(type)->second;
4431+
out << datatype_map.at(type);
44874432
}
44884433
else
44894434
{
@@ -4559,10 +4504,7 @@ void smt2_convt::convert_type(const typet &type)
45594504
{
45604505
if(use_datatypes)
45614506
{
4562-
INVARIANT(
4563-
datatype_map.find(type) != datatype_map.end(),
4564-
"type should have been converted to Z3 datatype");
4565-
out << datatype_map.find(type)->second;
4507+
out << datatype_map.at(type);
45664508
}
45674509
else
45684510
{
@@ -4612,7 +4554,8 @@ void smt2_convt::find_symbols_rec(
46124554
if(use_datatypes &&
46134555
datatype_map.find(type)==datatype_map.end())
46144556
{
4615-
std::string smt_typename = "complex."+std::to_string(datatype_map.size());
4557+
const std::string smt_typename =
4558+
"complex." + std::to_string(datatype_map.size());
46164559
datatype_map[type] = smt_typename;
46174560

46184561
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4640,7 +4583,8 @@ void smt2_convt::find_symbols_rec(
46404583

46414584
mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
46424585

4643-
std::string smt_typename = "vector."+std::to_string(datatype_map.size());
4586+
const std::string smt_typename =
4587+
"vector." + std::to_string(datatype_map.size());
46444588
datatype_map[type] = smt_typename;
46454589

46464590
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4663,7 +4607,8 @@ void smt2_convt::find_symbols_rec(
46634607
if(use_datatypes &&
46644608
datatype_map.find(type)==datatype_map.end())
46654609
{
4666-
std::string smt_typename = "struct."+std::to_string(datatype_map.size());
4610+
const std::string smt_typename =
4611+
"struct." + std::to_string(datatype_map.size());
46674612
datatype_map[type] = smt_typename;
46684613
need_decl=true;
46694614
}
@@ -4677,7 +4622,7 @@ void smt2_convt::find_symbols_rec(
46774622
// Declare the corresponding SMT type if we haven't already.
46784623
if(need_decl)
46794624
{
4680-
std::string smt_typename = datatype_map[type];
4625+
const std::string &smt_typename = datatype_map.at(type);
46814626

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

0 commit comments

Comments
 (0)