Skip to content

Commit b0f5db1

Browse files
danpoedanpoe
committed
Refactor usage of datatype_map in smt2_conv.cpp
1 parent 472fb38 commit b0f5db1

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
}
@@ -3284,11 +3264,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
32843264

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

32933269
out << "(mk-" << smt_typename;
32943270
}
@@ -3593,10 +3569,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
35933569

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

36013574
out << "(update-" << smt_typename << "." << component_name << " ";
36023575
convert_expr(expr.op0());
@@ -3824,10 +3797,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
38243797

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

38323802
// this is easy for constant indicies
38333803

@@ -3870,10 +3840,7 @@ void smt2_convt::convert_member(const member_exprt &expr)
38703840

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

38783845
out << "(" << smt_typename << "."
38793846
<< struct_type.get_component(name).get_name()
@@ -3930,11 +3897,7 @@ void smt2_convt::flatten2bv(const exprt &expr)
39303897
{
39313898
if(use_datatypes)
39323899
{
3933-
INVARIANT(
3934-
datatype_map.find(type) != datatype_map.end(),
3935-
"type should have been mapped to Z3 datatype");
3936-
3937-
const std::string &smt_typename = datatype_map.find(type)->second;
3900+
const std::string &smt_typename = datatype_map.at(type);
39383901

39393902
// concatenate elements
39403903
const vector_typet &vector_type=to_vector_type(type);
@@ -3965,11 +3928,7 @@ void smt2_convt::flatten2bv(const exprt &expr)
39653928
{
39663929
if(use_datatypes)
39673930
{
3968-
INVARIANT(
3969-
datatype_map.find(type) != datatype_map.end(),
3970-
"type should have been mapped to Z3 datatype");
3971-
3972-
const std::string &smt_typename = datatype_map.find(type)->second;
3931+
const std::string &smt_typename = datatype_map.at(type);
39733932

39743933
// concatenate elements
39753934
const struct_typet &struct_type=to_struct_type(type);
@@ -4032,11 +3991,7 @@ void smt2_convt::unflatten(
40323991
{
40333992
if(use_datatypes)
40343993
{
4035-
INVARIANT(
4036-
datatype_map.find(type) != datatype_map.end(),
4037-
"type should have been mapped to Z3 datatype");
4038-
4039-
const std::string &smt_typename = datatype_map.find(type)->second;
3994+
const std::string &smt_typename = datatype_map.at(type);
40403995

40413996
// extract elements
40423997
const vector_typet &vector_type=to_vector_type(type);
@@ -4083,11 +4038,7 @@ void smt2_convt::unflatten(
40834038
{
40844039
out << ")) ";
40854040

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

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

@@ -4466,10 +4417,7 @@ void smt2_convt::convert_type(const typet &type)
44664417
{
44674418
if(use_datatypes)
44684419
{
4469-
INVARIANT(
4470-
datatype_map.find(type) != datatype_map.end(),
4471-
"type should have been converted to Z3 datatype");
4472-
out << datatype_map.find(type)->second;
4420+
out << datatype_map.at(type);
44734421
}
44744422
else
44754423
{
@@ -4484,10 +4432,7 @@ void smt2_convt::convert_type(const typet &type)
44844432
{
44854433
if(use_datatypes)
44864434
{
4487-
INVARIANT(
4488-
datatype_map.find(type) != datatype_map.end(),
4489-
"type should have been converted to Z3 datatype");
4490-
out << datatype_map.find(type)->second;
4435+
out << datatype_map.at(type);
44914436
}
44924437
else
44934438
{
@@ -4563,10 +4508,7 @@ void smt2_convt::convert_type(const typet &type)
45634508
{
45644509
if(use_datatypes)
45654510
{
4566-
INVARIANT(
4567-
datatype_map.find(type) != datatype_map.end(),
4568-
"type should have been converted to Z3 datatype");
4569-
out << datatype_map.find(type)->second;
4511+
out << datatype_map.at(type);
45704512
}
45714513
else
45724514
{
@@ -4616,7 +4558,8 @@ void smt2_convt::find_symbols_rec(
46164558
if(use_datatypes &&
46174559
datatype_map.find(type)==datatype_map.end())
46184560
{
4619-
std::string smt_typename = "complex."+std::to_string(datatype_map.size());
4561+
const std::string smt_typename =
4562+
"complex." + std::to_string(datatype_map.size());
46204563
datatype_map[type] = smt_typename;
46214564

46224565
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4644,7 +4587,8 @@ void smt2_convt::find_symbols_rec(
46444587

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

4647-
std::string smt_typename = "vector."+std::to_string(datatype_map.size());
4590+
const std::string smt_typename =
4591+
"vector." + std::to_string(datatype_map.size());
46484592
datatype_map[type] = smt_typename;
46494593

46504594
out << "(declare-datatypes () ((" << smt_typename << " "
@@ -4667,7 +4611,8 @@ void smt2_convt::find_symbols_rec(
46674611
if(use_datatypes &&
46684612
datatype_map.find(type)==datatype_map.end())
46694613
{
4670-
std::string smt_typename = "struct."+std::to_string(datatype_map.size());
4614+
const std::string smt_typename =
4615+
"struct." + std::to_string(datatype_map.size());
46714616
datatype_map[type] = smt_typename;
46724617
need_decl=true;
46734618
}
@@ -4681,7 +4626,7 @@ void smt2_convt::find_symbols_rec(
46814626
// Declare the corresponding SMT type if we haven't already.
46824627
if(need_decl)
46834628
{
4684-
std::string smt_typename = datatype_map[type];
4629+
const std::string &smt_typename = datatype_map.at(type);
46854630

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

0 commit comments

Comments
 (0)