Skip to content

Commit

Permalink
Use propt::lcnf when cnf_handled_well is true
Browse files Browse the repository at this point in the history 
We can avoid Tseitin variables when using lcnf directly instead of using
set_to_{true,false}.
  • Loading branch information
@tautschnig
tautschnig committed Feb 23, 2023
1 parent d7099ae commit eb02254
Show file tree
Hide file tree
Showing 11 changed files with 255 additions and 52 deletions.
37 changes: 32 additions & 5 deletions src/cprover/bv_pointers_wide.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -627,9 +627,30 @@ bvt bv_pointers_widet::convert_bitvector(const exprt &expr)
difference, element_size_bv, bv_utilst::representationt::SIGNED);
}

prop.l_set_to_true(prop.limplies(
prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
bv_utils.equal(difference, bv)));
if(prop.cnf_handled_well())
{
for(std::size_t i = 0; i < width; ++i)
{
prop.lcnf(
{!same_object_lit,
!lhs_in_bounds,
!rhs_in_bounds,
!difference[i],
bv[i]});
prop.lcnf(
{!same_object_lit,
!lhs_in_bounds,
!rhs_in_bounds,
difference[i],
!bv[i]});
}
}
else
{
prop.l_set_to_true(prop.limplies(
prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
bv_utils.equal(difference, bv)));
}
}

return bv;
Expand Down Expand Up @@ -890,7 +911,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
if(!is_dynamic)
l2 = !l2;

prop.l_set_to_true(prop.limplies(l1, l2));
if(prop.cnf_handled_well())
prop.lcnf({!l1, l2});
else
prop.l_set_to_true(prop.limplies(l1, l2));
}
}
else if(
Expand Down Expand Up @@ -931,7 +955,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
literalt l1 = bv_utils.equal(bv, saved_bv);
literalt l2 = bv_utils.equal(postponed.bv, size_bv);

prop.l_set_to_true(prop.limplies(l1, l2));
if(prop.cnf_handled_well())
prop.lcnf({!l1, l2});
else
prop.l_set_to_true(prop.limplies(l1, l2));
}
}
else
Expand Down
16 changes: 13 additions & 3 deletions src/solvers/flattening/boolbv_bv_rel.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,10 +73,20 @@ literalt boolbvt::convert_bv_rel(const binary_relation_exprt &expr)
{
literalt equal_lit = equality(lhs, rhs);
if(or_equal)
prop.l_set_to_true(prop.limplies(equal_lit, literal));
if(prop.cnf_handled_well())
{
if(or_equal)
prop.lcnf(!equal_lit, literal);
else
prop.lcnf(!equal_lit, !literal);
}
else
prop.l_set_to_true(prop.limplies(equal_lit, !literal));
{
if(or_equal)
prop.l_set_to_true(prop.limplies(equal_lit, literal));
else
prop.l_set_to_true(prop.limplies(equal_lit, !literal));
}
}
}
Expand Down
29 changes: 26 additions & 3 deletions src/solvers/flattening/boolbv_byte_extract.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,9 +142,32 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
else
equal_bv[j]=const_literal(true);

prop.l_set_to_true(prop.limplies(
convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
prop.land(equal_bv)));
if(prop.cnf_handled_well())
{
literalt index_eq =
convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));

for(std::size_t j = 0; j < width; j++)
{
if(offset + j >= op_bv.size())
break;

prop.lcnf({!index_eq, !bv[j], op_bv[offset + j]});
prop.lcnf({!index_eq, bv[j], !op_bv[offset + j]});
}
}
else
{
for(std::size_t j = 0; j < width; j++)
if(offset + j < op_bv.size())
equal_bv[j] = prop.lequal(bv[j], op_bv[offset + j]);
else
equal_bv[j] = const_literal(true);

prop.l_set_to_true(prop.limplies(
convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
prop.land(equal_bv)));
}
}
}
else
Expand Down
6 changes: 4 additions & 2 deletions src/solvers/flattening/boolbv_case.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,10 @@ bvt boolbvt::convert_case(const exprt &expr)
{
literalt value_literal=bv_utils.equal(bv, op);

prop.l_set_to_true(
prop.limplies(compare_literal, value_literal));
if(prop.cnf_handled_well())
prop.lcnf({!compare_literal, value_literal});
else
prop.l_set_to_true(prop.limplies(compare_literal, value_literal));
}

what=COMPARE;
Expand Down
16 changes: 13 additions & 3 deletions src/solvers/flattening/boolbv_cond.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,9 +45,19 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
{
const bvt &op = convert_bv(operand, bv.size());

literalt value_literal=bv_utils.equal(bv, op);

prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
if(prop.cnf_handled_well())
{
for(std::size_t i = 0; i < bv.size(); ++i)
{
prop.lcnf({!cond_literal, !bv[i], op[i]});
prop.lcnf({!cond_literal, bv[i], !op[i]});
}
}
else
{
literalt value_literal = bv_utils.equal(bv, op);
prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
}
}

condition=!condition;
Expand Down
13 changes: 11 additions & 2 deletions src/solvers/flattening/boolbv_extractbit.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,17 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
for(std::size_t i = 0; i < src_bv.size(); i++)
{
equality.rhs()=from_integer(i, index_type);
literalt equal = prop.lequal(literal, src_bv[i]);
prop.l_set_to_true(prop.limplies(convert(equality), equal));
if(prop.cnf_handled_well())
{
literalt index_eq = convert(equality);
prop.lcnf({!index_eq, !literal, src_bv[i]});
prop.lcnf({!index_eq, literal, !src_bv[i]});
}
else
{
literalt equal = prop.lequal(literal, src_bv[i]);
prop.l_set_to_true(prop.limplies(convert(equality), equal));
}
}

return literal;
Expand Down
47 changes: 38 additions & 9 deletions src/solvers/flattening/boolbv_index.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -186,9 +186,18 @@ bvt boolbvt::convert_index(const index_exprt &expr)
"past the array's end");

// Cache comparisons and equalities
prop.l_set_to_true(convert(implies_exprt(
equal_exprt(index, from_integer(i, index.type())),
equal_exprt(result, *it++))));
if(prop.cnf_handled_well())
{
prop.lcnf(
{!convert(equal_exprt(index, from_integer(i, index.type()))),
convert(equal_exprt(result, *it++))});
}
else
{
prop.l_set_to_true(convert(implies_exprt(
equal_exprt(index, from_integer(i, index.type())),
equal_exprt(result, *it++))));
}
}

return bv;
Expand Down Expand Up @@ -229,13 +238,33 @@ bvt boolbvt::convert_index(const index_exprt &expr)
{
mp_integer offset=i*width;

for(std::size_t j=0; j<width; j++)
equal_bv[j] = prop.lequal(
bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
if(prop.cnf_handled_well())
{
literalt index_eq =
convert(equal_exprt(index, from_integer(i, index.type())));

for(std::size_t j = 0; j < width; j++)
{
prop.lcnf(
{!index_eq,
!bv[j],
array_bv[numeric_cast_v<std::size_t>(offset + j)]});
prop.lcnf(
{!index_eq,
bv[j],
!array_bv[numeric_cast_v<std::size_t>(offset + j)]});
}
}
else
{
for(std::size_t j = 0; j < width; j++)
equal_bv[j] = prop.lequal(
bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);

prop.l_set_to_true(prop.limplies(
convert(equal_exprt(index, from_integer(i, index.type()))),
prop.land(equal_bv)));
prop.l_set_to_true(prop.limplies(
convert(equal_exprt(index, from_integer(i, index.type()))),
prop.land(equal_bv)));
}
}
}
else
Expand Down
26 changes: 22 additions & 4 deletions src/solvers/flattening/bv_pointers.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -669,8 +669,20 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
}

prop.l_set_to_true(prop.limplies(
prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
if(prop.cnf_handled_well())
{
for(std::size_t i = 0; i < width; ++i)
{
prop.lcnf({!same_object_lit, !in_bounds, !difference[i], bv[i]});
prop.lcnf({!same_object_lit, !in_bounds, difference[i], !bv[i]});
}
}
else
{
prop.l_set_to_true(prop.limplies(
prop.land(same_object_lit, in_bounds),
bv_utils.equal(difference, bv)));
}
}

return bv;
Expand Down Expand Up @@ -929,7 +941,10 @@ void bv_pointerst::do_postponed(
if(!is_dynamic)
l2=!l2;

prop.l_set_to_true(prop.limplies(l1, l2));
if(prop.cnf_handled_well())
prop.lcnf({!l1, l2});
else
prop.l_set_to_true(prop.limplies(l1, l2));
}
}
else if(
Expand Down Expand Up @@ -980,7 +995,10 @@ void bv_pointerst::do_postponed(
#ifndef COMPACT_OBJECT_SIZE_EQ
literalt l2=bv_utils.equal(postponed.bv, size_bv);

prop.l_set_to_true(prop.limplies(l1, l2));
if(prop.cnf_handled_well())
prop.lcnf({!l1, l2});
else
prop.l_set_to_true(prop.limplies(l1, l2));
#else
for(std::size_t i = 0; i < postponed.bv.size(); ++i)
{
Expand Down
Loading

0 comments on commit eb02254

Please sign in to comment.