replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Use propt::l_set_to_{true,false} 

Avoids the lower-level l_set_to(..., {true,false}) and may then
highlight opportunities for further optimisation.
This commit is contained in:
Michael Tautschnig 2018-03-22 14:47:19 +00:00
parent 3a577d784c
commit 8c5303a2dd
2 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/solvers/flattening/bv_pointers.cpp
View File

@ -768,7 +768,7 @@ void bv_pointerst::do_postponed(
if(!is_dynamic)
l2=!l2;
prop.l_set_to(prop.limplies(l1, l2), true);
prop.l_set_to_true(prop.limplies(l1, l2));
}
}
else if(postponed.expr.id()==ID_object_size)
@ -814,7 +814,7 @@ void bv_pointerst::do_postponed(
literalt l1=bv_utils.equal(bv, saved_bv);
literalt l2=bv_utils.equal(postponed.bv, size_bv);
prop.l_set_to(prop.limplies(l1, l2), true);
prop.l_set_to_true(prop.limplies(l1, l2));
}
}
else

8
src/solvers/flattening/bv_utils.cpp
View File

@ -540,7 +540,7 @@ bvt bv_utilst::negate(const bvt &bv)
bvt bv_utilst::negate_no_overflow(const bvt &bv)
{
prop.l_set_to(overflow_negate(bv), false);
prop.l_set_to_false(overflow_negate(bv));
return negate(bv);
}
@ -780,9 +780,7 @@ bvt bv_utilst::absolute_value(const bvt &bv)
bvt bv_utilst::cond_negate_no_overflow(const bvt &bv, literalt cond)
{
prop.l_set_to(
prop.limplies(cond, !overflow_negate(bv)),
true);
prop.l_set_to_true(prop.limplies(cond, !overflow_negate(bv)));
return cond_negate(bv, cond);
}
@ -802,7 +800,7 @@ bvt bv_utilst::signed_multiplier_no_overflow(
bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
prop.l_set_to(result[result.size()-1], false);
prop.l_set_to_false(result[result.size() - 1]);
literalt result_sign=prop.lxor(sign0, sign1);