Skip to content

Commit 0f6b06c

Browse files
danpoedanpoe
committed
Refactor usage of datatype_map in smt2_conv.cpp
1 parent d790011 commit 0f6b06c

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 =
@@ -1807,11 +1798,7 @@ void smt2_convt::convert_expr(const exprt &expr)
18071798

18081799
if(use_datatypes)
18091800
{
1810-
INVARIANT(
1811-
datatype_map.find(vector_type) != datatype_map.end(),
1812-
"type shall have been mapped to Z3 datatype");
1813-
1814-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
1801+
const std::string &smt_typename = datatype_map.at(vector_type);
18151802

18161803
out << "(mk-" << smt_typename;
18171804
}
@@ -2596,10 +2583,7 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
25962583

25972584
if(use_datatypes)
25982585
{
2599-
INVARIANT(
2600-
datatype_map.find(struct_type) != datatype_map.end(),
2601-
"type should have been mapped to Z3 datatype");
2602-
const std::string &smt_typename = datatype_map.find(struct_type)->second;
2586+
const std::string &smt_typename = datatype_map.at(struct_type);
26032587

26042588
// use the constructor for the Z3 datatype
26052589
out << "(mk-" << smt_typename;
@@ -3083,11 +3067,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
30833067

30843068
if(use_datatypes)
30853069
{
3086-
INVARIANT(
3087-
datatype_map.find(vector_type) != datatype_map.end(),
3088-
"type should have been mapped to Z3 datatype");
3089-
3090-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
3070+
const std::string &smt_typename = datatype_map.at(vector_type);
30913071

30923072
out << "(mk-" << smt_typename;
30933073
}
@@ -3285,11 +3265,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
32853265

32863266
if(use_datatypes)
32873267
{
3288-
INVARIANT(
3289-
datatype_map.find(vector_type) != datatype_map.end(),
3290-
"type should have been mapped to Z3 datatype");
3291-
3292-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
3268+
const std::string &smt_typename = datatype_map.at(vector_type);
32933269

32943270
out << "(mk-" << smt_typename;
32953271
}
@@ -3594,10 +3570,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
35943570

35953571
if(use_datatypes)
35963572
{
3597-
INVARIANT(
3598-
datatype_map.find(expr_type) != datatype_map.end(),
3599-
"type shall have been mapped to Z3 datatype");
3600-
const std::string &smt_typename = datatype_map.find(expr_type)->second;
3573+
const std::string &smt_typename = datatype_map.at(expr_type);
36013574

36023575
out << "(update-" << smt_typename << "." << component_name << " ";
36033576
convert_expr(expr.op0());
@@ -3825,10 +3798,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
38253798

38263799
if(use_datatypes)
38273800
{
3828-
INVARIANT(
3829-
datatype_map.find(vector_type) != datatype_map.end(),
3830-
"type should have been mapped to Z3 datatype");
3831-
const std::string &smt_typename = datatype_map.find(vector_type)->second;
3801+
const std::string &smt_typename = datatype_map.at(vector_type);
38323802

38333803
// this is easy for constant indicies
38343804

@@ -3871,10 +3841,7 @@ void smt2_convt::convert_member(const member_exprt &expr)
38713841

38723842
if(use_datatypes)
38733843
{
3874-
INVARIANT(
3875-
datatype_map.find(struct_type) != datatype_map.end(),
3876-
"type should have been mapped to Z3 datatype");
3877-
const std::string &smt_typename = datatype_map.find(struct_type)->second;
3844+
const std::string &smt_typename = datatype_map.at(struct_type);
38783845

38793846
out << "(" << smt_typename << "."
38803847
<< struct_type.get_component(name).get_name()
@@ -3931,11 +3898,7 @@ void smt2_convt::flatten2bv(const exprt &expr)
39313898
{
39323899
if(use_datatypes)
39333900
{
3934-
INVARIANT(
3935-
datatype_map.find(type) != datatype_map.end(),
3936-
"type should have been mapped to Z3 datatype");
3937-
3938-
const std::string &smt_typename = datatype_map.find(type)->second;
3901+
const std::string &smt_typename = datatype_map.at(type);
39393902

39403903
// concatenate elements
39413904
const vector_typet &vector_type=to_vector_type(type);
@@ -3966,11 +3929,7 @@ void smt2_convt::flatten2bv(const exprt &expr)
39663929
{
39673930
if(use_datatypes)
39683931
{
3969-
INVARIANT(
3970-
datatype_map.find(type) != datatype_map.end(),
3971-
"type should have been mapped to Z3 datatype");
3972-
3973-
const std::string &smt_typename = datatype_map.find(type)->second;
3932+
const std::string &smt_typename = datatype_map.at(type);
39743933

39753934
// concatenate elements
39763935
const struct_typet &struct_type=to_struct_type(type);
@@ -4033,11 +3992,7 @@ void smt2_convt::unflatten(
40333992
{
40343993
if(use_datatypes)
40353994
{
4036-
INVARIANT(
4037-
datatype_map.find(type) != datatype_map.end(),
4038-
"type should have been mapped to Z3 datatype");
4039-
4040-
const std::string &smt_typename = datatype_map.find(type)->second;
3995+
const std::string &smt_typename = datatype_map.at(type);
40413996

40423997
// extract elements
40433998
const vector_typet &vector_type=to_vector_type(type);
@@ -4084,11 +4039,7 @@ void smt2_convt::unflatten(
40844039
{
40854040
out << ")) ";
40864041

4087-
INVARIANT(
4088-
datatype_map.find(type) != datatype_map.end(),
4089-
"type should have been mapped to Z3 datatype");
4090-
4091-
const std::string &smt_typename = datatype_map.find(type)->second;
4042+
const std::string &smt_typename = datatype_map.at(type);
40924043

40934044
out << "(mk-" << smt_typename;
40944045

@@ -4467,10 +4418,7 @@ void smt2_convt::convert_type(const typet &type)
44674418
{
44684419
if(use_datatypes)
44694420
{
4470-
INVARIANT(
4471-
datatype_map.find(type) != datatype_map.end(),
4472-
"type should have been converted to Z3 datatype");
4473-
out << datatype_map.find(type)->second;
4421+
out << datatype_map.at(type);
44744422
}
44754423
else
44764424
{
@@ -4485,10 +4433,7 @@ void smt2_convt::convert_type(const typet &type)
44854433
{
44864434
if(use_datatypes)
44874435
{
4488-
INVARIANT(
4489-
datatype_map.find(type) != datatype_map.end(),
4490-
"type should have been converted to Z3 datatype");
4491-
out << datatype_map.find(type)->second;
4436+
out << datatype_map.at(type);
44924437
}
44934438
else
44944439
{
@@ -4564,10 +4509,7 @@ void smt2_convt::convert_type(const typet &type)
45644509
{
45654510
if(use_datatypes)
45664511
{
4567-
INVARIANT(
4568-
datatype_map.find(type) != datatype_map.end(),
4569-
"type should have been converted to Z3 datatype");
4570-
out << datatype_map.find(type)->second;
4512+
out << datatype_map.at(type);
45714513
}
45724514
else
45734515
{
@@ -4617,7 +4559,8 @@ void smt2_convt::find_symbols_rec(
46174559
if(use_datatypes &&
46184560
datatype_map.find(type)==datatype_map.end())
46194561
{
4620-
std::string smt_typename = "complex."+std::to_string(datatype_map.size());
4562+
const std::string smt_typename =
4563+
"complex." + std::to_string(datatype_map.size());
46214564
datatype_map[type] = smt_typename;
46224565

46234566
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4645,7 +4588,8 @@ void smt2_convt::find_symbols_rec(
46454588

46464589
mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
46474590

4648-
std::string smt_typename = "vector."+std::to_string(datatype_map.size());
4591+
const std::string smt_typename =
4592+
"vector." + std::to_string(datatype_map.size());
46494593
datatype_map[type] = smt_typename;
46504594

46514595
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4668,7 +4612,8 @@ void smt2_convt::find_symbols_rec(
46684612
if(use_datatypes &&
46694613
datatype_map.find(type)==datatype_map.end())
46704614
{
4671-
std::string smt_typename = "struct."+std::to_string(datatype_map.size());
4615+
const std::string smt_typename =
4616+
"struct." + std::to_string(datatype_map.size());
46724617
datatype_map[type] = smt_typename;
46734618
need_decl=true;
46744619
}
@@ -4682,7 +4627,7 @@ void smt2_convt::find_symbols_rec(
46824627
// Declare the corresponding SMT type if we haven't already.
46834628
if(need_decl)
46844629
{
4685-
std::string smt_typename = datatype_map[type];
4630+
const std::string &smt_typename = datatype_map.at(type);
46864631

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

0 commit comments

Comments
 (0)