Skip to content

Feature invariant cleanup flattening/boolbv_equality.cpp #3038

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Sep 25, 2018
Merged

Feature invariant cleanup flattening/boolbv_equality.cpp #3038

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4cae2a3
Rename variables in boolbv_equality for readability
hannes-steffenhagen-diffblue Sep 21, 2018
cbc78db
Replace throws with invariants in boolbv_equality
hannes-steffenhagen-diffblue Sep 21, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
62 changes: 31 additions & 31 deletions src/solvers/flattening/boolbv_equality.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,13 +19,11 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
{
const bool is_base_type_eq =
base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
if(!is_base_type_eq)
{
const std::string error_msg =
std::string("equality without matching types:\n") + "######### lhs: " +
expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty();
throw bitvector_conversion_exceptiont(error_msg, expr);
}
DATA_INVARIANT_WITH_DIAGNOSTICS(
is_base_type_eq,
"types of expressions on each side of equality should match",
irep_pretty_diagnosticst{expr.lhs()},
irep_pretty_diagnosticst{expr.rhs()});

// see if it is an unbounded array
if(is_unbounded_array(expr.lhs().type()))
Expand All @@ -41,24 +39,25 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
return record_array_equality(expr);
}

const bvt &bv0=convert_bv(expr.lhs());
const bvt &bv1=convert_bv(expr.rhs());
const bvt &lhs_bv = convert_bv(expr.lhs());
const bvt &rhs_bv = convert_bv(expr.rhs());

DATA_INVARIANT(
bv0.size() == bv1.size(),
std::string("unexpected size mismatch on equality:\n") + "lhs: " +
expr.lhs().pretty() + '\n' + "lhs size: " + std::to_string(bv0.size()) +
'\n' + "rhs: " + expr.rhs().pretty() + '\n' +
"rhs size: " + std::to_string(bv1.size()));
DATA_INVARIANT_WITH_DIAGNOSTICS(
lhs_bv.size() == rhs_bv.size(),
"sizes of lhs and rhs bitvectors should match",
irep_pretty_diagnosticst{expr.lhs()},
"lhs size: " + std::to_string(lhs_bv.size()),
irep_pretty_diagnosticst{expr.rhs()},
"rhs size: " + std::to_string(rhs_bv.size()));

if(bv0.empty())
if(lhs_bv.empty())
{
// An empty bit-vector comparison. It's not clear
// what this is meant to say.
return prop.new_variable();
}

return bv_utils.equal(bv0, bv1);
return bv_utils.equal(lhs_bv, rhs_bv);
}

literalt boolbvt::convert_verilog_case_equality(
Expand All @@ -69,24 +68,25 @@ literalt boolbvt::convert_verilog_case_equality(

const bool is_base_type_eq =
base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
DATA_INVARIANT(
DATA_INVARIANT_WITH_DIAGNOSTICS(
is_base_type_eq,
std::string("verilog_case_equality without matching types:\n") +
"######### lhs: " + expr.lhs().pretty() + '\n' +
"######### rhs: " + expr.rhs().pretty());
"lhs and rhs types should match in verilog_case_equality",
irep_pretty_diagnosticst{expr.lhs()},
irep_pretty_diagnosticst{expr.rhs()});

const bvt &bv0=convert_bv(expr.lhs());
const bvt &bv1=convert_bv(expr.rhs());
const bvt &lhs_bv = convert_bv(expr.lhs());
const bvt &rhs_bv = convert_bv(expr.rhs());

DATA_INVARIANT(
bv0.size() == bv1.size(),
std::string("unexpected size mismatch on verilog_case_equality:\n") +
"lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " +
std::to_string(bv0.size()) + '\n' + "rhs: " + expr.rhs().pretty() + '\n' +
"rhs size: " + std::to_string(bv1.size()));
DATA_INVARIANT_WITH_DIAGNOSTICS(
lhs_bv.size() == rhs_bv.size(),
"bitvector arguments to verilog_case_equality should have the same size",
irep_pretty_diagnosticst{expr.lhs()},
"lhs size: " + std::to_string(lhs_bv.size()),
irep_pretty_diagnosticst{expr.rhs()},
"rhs size: " + std::to_string(rhs_bv.size()));

if(expr.id()==ID_verilog_case_inequality)
return !bv_utils.equal(bv0, bv1);
return !bv_utils.equal(lhs_bv, rhs_bv);
else
return bv_utils.equal(bv0, bv1);
return bv_utils.equal(lhs_bv, rhs_bv);
}