Skip to content

Commit 2a0c726

Browse files
tautschnigtautschnig
committed
Use propt::lcnf when cnf_handled_well is true
We can avoid Tseitin variables when using lcnf directly instead of using set_to_{true,false}.
1 parent bf58af8 commit 2a0c726

File tree

11 files changed

+263
-55
lines changed

11 files changed

+263
-55
lines changed

‎src/cprover/bv_pointers_wide.cpp

Lines changed: 32 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -629,9 +629,30 @@ bvt bv_pointers_widet::convert_bitvector(const exprt &expr)
629629
difference, element_size_bv, bv_utilst::representationt::SIGNED);
630630
}
631631

632-
prop.l_set_to_true(prop.limplies(
633-
prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
634-
bv_utils.equal(difference, bv)));
632+
if(prop.cnf_handled_well())
633+
{
634+
for(std::size_t i = 0; i < width; ++i)
635+
{
636+
prop.lcnf(
637+
{!same_object_lit,
638+
!lhs_in_bounds,
639+
!rhs_in_bounds,
640+
!difference[i],
641+
bv[i]});
642+
prop.lcnf(
643+
{!same_object_lit,
644+
!lhs_in_bounds,
645+
!rhs_in_bounds,
646+
difference[i],
647+
!bv[i]});
648+
}
649+
}
650+
else
651+
{
652+
prop.l_set_to_true(prop.limplies(
653+
prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
654+
bv_utils.equal(difference, bv)));
655+
}
635656
}
636657

637658
return bv;
@@ -892,7 +913,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
892913
if(!is_dynamic)
893914
l2 = !l2;
894915

895-
prop.l_set_to_true(prop.limplies(l1, l2));
916+
if(prop.cnf_handled_well())
917+
prop.lcnf({!l1, l2});
918+
else
919+
prop.l_set_to_true(prop.limplies(l1, l2));
896920
}
897921
}
898922
else if(
@@ -933,7 +957,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
933957
literalt l1 = bv_utils.equal(bv, saved_bv);
934958
literalt l2 = bv_utils.equal(postponed.bv, size_bv);
935959

936-
prop.l_set_to_true(prop.limplies(l1, l2));
960+
if(prop.cnf_handled_well())
961+
prop.lcnf({!l1, l2});
962+
else
963+
prop.l_set_to_true(prop.limplies(l1, l2));
937964
}
938965
}
939966
else

‎src/solvers/flattening/boolbv_bv_rel.cpp

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -73,10 +73,20 @@ literalt boolbvt::convert_bv_rel(const binary_relation_exprt &expr)
7373
{
7474
literalt equal_lit = equality(lhs, rhs);
7575
76-
if(or_equal)
77-
prop.l_set_to_true(prop.limplies(equal_lit, literal));
76+
if(prop.cnf_handled_well())
77+
{
78+
if(or_equal)
79+
prop.lcnf(!equal_lit, literal);
80+
else
81+
prop.lcnf(!equal_lit, !literal);
82+
}
7883
else
79-
prop.l_set_to_true(prop.limplies(equal_lit, !literal));
84+
{
85+
if(or_equal)
86+
prop.l_set_to_true(prop.limplies(equal_lit, literal));
87+
else
88+
prop.l_set_to_true(prop.limplies(equal_lit, !literal));
89+
}
8090
}
8191
}
8292

‎src/solvers/flattening/boolbv_byte_extract.cpp

Lines changed: 26 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -142,9 +142,32 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
142142
else
143143
equal_bv[j]=const_literal(true);
144144

145-
prop.l_set_to_true(prop.limplies(
146-
convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
147-
prop.land(equal_bv)));
145+
if(prop.cnf_handled_well())
146+
{
147+
literalt index_eq =
148+
convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
149+
150+
for(std::size_t j = 0; j < width; j++)
151+
{
152+
if(offset + j >= op_bv.size())
153+
break;
154+
155+
prop.lcnf({!index_eq, !bv[j], op_bv[offset + j]});
156+
prop.lcnf({!index_eq, bv[j], !op_bv[offset + j]});
157+
}
158+
}
159+
else
160+
{
161+
for(std::size_t j = 0; j < width; j++)
162+
if(offset + j < op_bv.size())
163+
equal_bv[j] = prop.lequal(bv[j], op_bv[offset + j]);
164+
else
165+
equal_bv[j] = const_literal(true);
166+
167+
prop.l_set_to_true(prop.limplies(
168+
convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
169+
prop.land(equal_bv)));
170+
}
148171
}
149172
}
150173
else

‎src/solvers/flattening/boolbv_case.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,8 +68,10 @@ bvt boolbvt::convert_case(const exprt &expr)
6868
{
6969
literalt value_literal=bv_utils.equal(bv, op);
7070

71-
prop.l_set_to_true(
72-
prop.limplies(compare_literal, value_literal));
71+
if(prop.cnf_handled_well())
72+
prop.lcnf({!compare_literal, value_literal});
73+
else
74+
prop.l_set_to_true(prop.limplies(compare_literal, value_literal));
7375
}
7476

7577
what=COMPARE;

‎src/solvers/flattening/boolbv_cond.cpp

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,9 +45,19 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
4545
{
4646
const bvt &op = convert_bv(operand, bv.size());
4747

48-
literalt value_literal=bv_utils.equal(bv, op);
49-
50-
prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
48+
if(prop.cnf_handled_well())
49+
{
50+
for(std::size_t i = 0; i < bv.size(); ++i)
51+
{
52+
prop.lcnf({!cond_literal, !bv[i], op[i]});
53+
prop.lcnf({!cond_literal, bv[i], !op[i]});
54+
}
55+
}
56+
else
57+
{
58+
literalt value_literal = bv_utils.equal(bv, op);
59+
prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
60+
}
5161
}
5262

5363
condition=!condition;

‎src/solvers/flattening/boolbv_extractbit.cpp

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -65,8 +65,17 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
6565
for(std::size_t i = 0; i < src_bv.size(); i++)
6666
{
6767
equal_exprt equality(index_casted, from_integer(i, index_type));
68-
literalt equal = prop.lequal(literal, src_bv[i]);
69-
prop.l_set_to_true(prop.limplies(convert(equality), equal));
68+
if(prop.cnf_handled_well())
69+
{
70+
literalt index_eq = convert(equality);
71+
prop.lcnf({!index_eq, !literal, src_bv[i]});
72+
prop.lcnf({!index_eq, literal, !src_bv[i]});
73+
}
74+
else
75+
{
76+
literalt equal = prop.lequal(literal, src_bv[i]);
77+
prop.l_set_to_true(prop.limplies(convert(equality), equal));
78+
}
7079
}
7180

7281
return literal;

‎src/solvers/flattening/boolbv_index.cpp

Lines changed: 38 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -186,9 +186,18 @@ bvt boolbvt::convert_index(const index_exprt &expr)
186186
"past the array's end");
187187

188188
// Cache comparisons and equalities
189-
prop.l_set_to_true(convert(implies_exprt(
190-
equal_exprt(index, from_integer(i, index.type())),
191-
equal_exprt(result, *it++))));
189+
if(prop.cnf_handled_well())
190+
{
191+
prop.lcnf(
192+
{!convert(equal_exprt(index, from_integer(i, index.type()))),
193+
convert(equal_exprt(result, *it++))});
194+
}
195+
else
196+
{
197+
prop.l_set_to_true(convert(implies_exprt(
198+
equal_exprt(index, from_integer(i, index.type())),
199+
equal_exprt(result, *it++))));
200+
}
192201
}
193202

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

232-
for(std::size_t j=0; j<width; j++)
233-
equal_bv[j] = prop.lequal(
234-
bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
241+
if(prop.cnf_handled_well())
242+
{
243+
literalt index_eq =
244+
convert(equal_exprt(index, from_integer(i, index.type())));
245+
246+
for(std::size_t j = 0; j < width; j++)
247+
{
248+
prop.lcnf(
249+
{!index_eq,
250+
!bv[j],
251+
array_bv[numeric_cast_v<std::size_t>(offset + j)]});
252+
prop.lcnf(
253+
{!index_eq,
254+
bv[j],
255+
!array_bv[numeric_cast_v<std::size_t>(offset + j)]});
256+
}
257+
}
258+
else
259+
{
260+
for(std::size_t j = 0; j < width; j++)
261+
equal_bv[j] = prop.lequal(
262+
bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
235263

236-
prop.l_set_to_true(prop.limplies(
237-
convert(equal_exprt(index, from_integer(i, index.type()))),
238-
prop.land(equal_bv)));
264+
prop.l_set_to_true(prop.limplies(
265+
convert(equal_exprt(index, from_integer(i, index.type()))),
266+
prop.land(equal_bv)));
267+
}
239268
}
240269
}
241270
else

‎src/solvers/flattening/bv_pointers.cpp

Lines changed: 30 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -697,8 +697,20 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
697697
prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
698698
}
699699

700-
prop.l_set_to_true(prop.limplies(
701-
prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
700+
if(prop.cnf_handled_well())
701+
{
702+
for(std::size_t i = 0; i < width; ++i)
703+
{
704+
prop.lcnf({!same_object_lit, !in_bounds, !difference[i], bv[i]});
705+
prop.lcnf({!same_object_lit, !in_bounds, difference[i], !bv[i]});
706+
}
707+
}
708+
else
709+
{
710+
prop.l_set_to_true(prop.limplies(
711+
prop.land(same_object_lit, in_bounds),
712+
bv_utils.equal(difference, bv)));
713+
}
702714
}
703715

704716
return bv;
@@ -1071,10 +1083,18 @@ void bv_pointerst::finish_eager_conversion()
10711083
replace_expr(replacements, is_not_dyn);
10721084

10731085
PRECONDITION(postponed.bv.size() == 1);
1074-
prop.l_set_to_true(
1075-
prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
1076-
prop.l_set_to_true(
1077-
prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
1086+
if(prop.cnf_handled_well())
1087+
{
1088+
prop.lcnf({!convert_bv(is_dyn)[0], postponed.bv.front()});
1089+
prop.lcnf({!convert_bv(is_not_dyn)[0], !postponed.bv.front()});
1090+
}
1091+
else
1092+
{
1093+
prop.l_set_to_true(
1094+
prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
1095+
prop.l_set_to_true(
1096+
prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
1097+
}
10781098
}
10791099
else if(
10801100
const auto postponed_object_size =
@@ -1121,7 +1141,10 @@ void bv_pointerst::finish_eager_conversion()
11211141
#ifndef COMPACT_OBJECT_SIZE_EQ
11221142
literalt l2 = bv_utils.equal(postponed.bv, size_bv);
11231143

1124-
prop.l_set_to_true(prop.limplies(l1, l2));
1144+
if(prop.cnf_handled_well())
1145+
prop.lcnf({!l1, l2});
1146+
else
1147+
prop.l_set_to_true(prop.limplies(l1, l2));
11251148
#else
11261149
for(std::size_t i = 0; i < postponed.bv.size(); ++i)
11271150
{

0 commit comments

Comments
 (0)