Skip to content

Commit 6c49935

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 81f1fb6 commit 6c49935

File tree

11 files changed

+255
-52
lines changed

11 files changed

+255
-52
lines changed

‎src/cprover/bv_pointers_wide.cpp

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

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

635656
return bv;
@@ -890,7 +911,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
890911
if(!is_dynamic)
891912
l2 = !l2;
892913

893-
prop.l_set_to_true(prop.limplies(l1, l2));
914+
if(prop.cnf_handled_well())
915+
prop.lcnf({!l1, l2});
916+
else
917+
prop.l_set_to_true(prop.limplies(l1, l2));
894918
}
895919
}
896920
else if(
@@ -931,7 +955,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
931955
literalt l1 = bv_utils.equal(bv, saved_bv);
932956
literalt l2 = bv_utils.equal(postponed.bv, size_bv);
933957

934-
prop.l_set_to_true(prop.limplies(l1, l2));
958+
if(prop.cnf_handled_well())
959+
prop.lcnf({!l1, l2});
960+
else
961+
prop.l_set_to_true(prop.limplies(l1, l2));
935962
}
936963
}
937964
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
equality.rhs()=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: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -669,8 +669,20 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
669669
prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
670670
}
671671

672-
prop.l_set_to_true(prop.limplies(
673-
prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
672+
if(prop.cnf_handled_well())
673+
{
674+
for(std::size_t i = 0; i < width; ++i)
675+
{
676+
prop.lcnf({!same_object_lit, !in_bounds, !difference[i], bv[i]});
677+
prop.lcnf({!same_object_lit, !in_bounds, difference[i], !bv[i]});
678+
}
679+
}
680+
else
681+
{
682+
prop.l_set_to_true(prop.limplies(
683+
prop.land(same_object_lit, in_bounds),
684+
bv_utils.equal(difference, bv)));
685+
}
674686
}
675687

676688
return bv;
@@ -929,7 +941,10 @@ void bv_pointerst::do_postponed(
929941
if(!is_dynamic)
930942
l2=!l2;
931943

932-
prop.l_set_to_true(prop.limplies(l1, l2));
944+
if(prop.cnf_handled_well())
945+
prop.lcnf({!l1, l2});
946+
else
947+
prop.l_set_to_true(prop.limplies(l1, l2));
933948
}
934949
}
935950
else if(
@@ -980,7 +995,10 @@ void bv_pointerst::do_postponed(
980995
#ifndef COMPACT_OBJECT_SIZE_EQ
981996
literalt l2=bv_utils.equal(postponed.bv, size_bv);
982997

983-
prop.l_set_to_true(prop.limplies(l1, l2));
998+
if(prop.cnf_handled_well())
999+
prop.lcnf({!l1, l2});
1000+
else
1001+
prop.l_set_to_true(prop.limplies(l1, l2));
9841002
#else
9851003
for(std::size_t i = 0; i < postponed.bv.size(); ++i)
9861004
{

0 commit comments

Comments
 (0)