Skip to content

Commit e73c451

Browse files
tautschnigtautschnig
committed
Improve bv_utilst less-than-or-less-or-equals
1. Duplicate some code to specialise it for signed/unsigned and, thereby, add clarity. 2. De-duplicate code to handle all cases directly in lt_or_le. 3. Make sure we constant-propagate whatever is possible in unsigned comparison to avoid introducing unnecessary fresh literals. Previously, we would create fresh literals even when comparing constant values.
1 parent 46f9d54 commit e73c451

File tree

1 file changed

+113
-62
lines changed

1 file changed

+113
-62
lines changed

‎src/solvers/flattening/bv_utils.cpp‎

Lines changed: 113 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -1415,11 +1415,6 @@ literalt bv_utilst::lt_or_le(
14151415
#ifdef COMPACT_LT_OR_LE
14161416
if(prop.has_set_to() && prop.cnf_handled_well())
14171417
{
1418-
bvt compareBelow; // 1 if a compare is needed below this bit
1419-
literalt result;
1420-
size_t start;
1421-
size_t i;
1422-
14231418
if(rep == representationt::SIGNED)
14241419
{
14251420
if(top0.is_false() && top1.is_true())
@@ -1429,8 +1424,9 @@ literalt bv_utilst::lt_or_le(
14291424

14301425
INVARIANT(
14311426
bv0.size() >= 2, "signed bitvectors should have at least two bits");
1432-
compareBelow = prop.new_variables(bv0.size() - 1);
1433-
start = compareBelow.size() - 1;
1427+
// 1 if a compare is needed below this bit
1428+
bvt compareBelow = prop.new_variables(bv0.size() - 1);
1429+
size_t start = compareBelow.size() - 1;
14341430

14351431
literalt &firstComp = compareBelow[start];
14361432
if(top0.is_false())
@@ -1442,7 +1438,7 @@ literalt bv_utilst::lt_or_le(
14421438
else if(top1.is_true())
14431439
firstComp = top0;
14441440

1445-
result = prop.new_variable();
1441+
literalt result = prop.new_variable();
14461442

14471443
// When comparing signs we are comparing the top bit
14481444
// Four cases...
@@ -1454,70 +1450,130 @@ literalt bv_utilst::lt_or_le(
14541450
#ifdef INCLUDE_REDUNDANT_CLAUSES
14551451
prop.lcnf(top0, !top1, !firstComp);
14561452
prop.lcnf(!top0, top1, !firstComp);
1457-
#endif
1458-
}
1459-
else
1460-
{
1461-
// Unsigned is much easier
1462-
compareBelow = prop.new_variables(bv0.size() - 1);
1463-
compareBelow.push_back(const_literal(true));
1464-
start = compareBelow.size() - 1;
1465-
result = prop.new_variable();
1466-
}
1453+
# endif
14671454

1468-
// Determine the output
1469-
// \forall i . cb[i] & -a[i] & b[i] => result
1470-
// \forall i . cb[i] & a[i] & -b[i] => -result
1471-
i = start;
1472-
do
1473-
{
1474-
if(compareBelow[i].is_false())
1475-
continue;
1476-
else if(compareBelow[i].is_true())
1455+
// Determine the output
1456+
// \forall i . cb[i] & -a[i] & b[i] => result
1457+
// \forall i . cb[i] & a[i] & -b[i] => -result
1458+
size_t i = start;
1459+
do
14771460
{
1478-
if(bv0[i].is_false() && bv1[i].is_true())
1479-
return const_literal(true);
1480-
else if(bv0[i].is_true() && bv1[i].is_false())
1481-
return const_literal(false);
1461+
if(compareBelow[i].is_false())
1462+
continue;
1463+
1464+
prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1465+
prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1466+
} while(i-- != 0);
1467+
1468+
// Chain the comparison bit
1469+
// \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1470+
// \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1471+
for(i = start; i > 0; i--)
1472+
{
1473+
prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i - 1]);
1474+
prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i - 1]);
14821475
}
14831476

1484-
prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1485-
prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1486-
}
1487-
while(i-- != 0);
1477+
# ifdef INCLUDE_REDUNDANT_CLAUSES
1478+
// Optional zeroing of the comparison bit when not needed
1479+
// \forall i != 0 . -c[i] => -c[i-1]
1480+
// \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1481+
// \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1482+
for(i = start; i > 0; i--)
1483+
{
1484+
prop.lcnf(compareBelow[i], !compareBelow[i - 1]);
1485+
prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i - 1]);
1486+
prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i - 1]);
1487+
}
1488+
# endif
14881489

1489-
// Chain the comparison bit
1490-
// \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1491-
// \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1492-
for(i = start; i > 0; i--)
1493-
{
1494-
prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]);
1495-
prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]);
1496-
}
1490+
// The 'base case' of the induction is the case when they are equal
1491+
prop.lcnf(
1492+
!compareBelow[0], !bv0[0], !bv1[0], (or_equal) ? result : !result);
1493+
prop.lcnf(
1494+
!compareBelow[0], bv0[0], bv1[0], (or_equal) ? result : !result);
14971495

1496+
return result;
1497+
}
1498+
else
1499+
{
1500+
// Unsigned is much easier
1501+
// 1 if a compare is needed below this bit
1502+
bvt compareBelow;
1503+
literalt result;
1504+
size_t start = bv0.size() - 1;
1505+
1506+
// Determine the output
1507+
// \forall i . cb[i] & -a[i] & b[i] => result
1508+
// \forall i . cb[i] & a[i] & -b[i] => -result
1509+
bool same_prefix = true;
1510+
size_t i = start;
1511+
do
1512+
{
1513+
if(same_prefix)
1514+
{
1515+
if(i == 0)
1516+
{
1517+
if(or_equal)
1518+
return prop.lor(!bv0[0], bv1[0]);
1519+
else
1520+
return prop.land(!bv0[0], bv1[0]);
1521+
}
1522+
else if(bv0[i] == bv1[i])
1523+
continue;
1524+
else if(bv0[i].is_false() && bv1[i].is_true())
1525+
return const_literal(true);
1526+
else if(bv0[i].is_true() && bv1[i].is_false())
1527+
return const_literal(false);
1528+
else
1529+
{
1530+
same_prefix = false;
1531+
start = i;
1532+
compareBelow = prop.new_variables(i);
1533+
compareBelow.push_back(const_literal(true));
1534+
result = prop.new_variable();
1535+
}
1536+
}
1537+
1538+
prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result);
1539+
prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result);
1540+
} while(i-- != 0);
1541+
1542+
// Chain the comparison bit
1543+
// \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1]
1544+
// \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1]
1545+
for(i = start; i > 0; i--)
1546+
{
1547+
prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i - 1]);
1548+
prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i - 1]);
1549+
}
14981550

14991551
#ifdef INCLUDE_REDUNDANT_CLAUSES
1500-
// Optional zeroing of the comparison bit when not needed
1501-
// \forall i != 0 . -c[i] => -c[i-1]
1502-
// \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1503-
// \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1504-
for(i = start; i > 0; i--)
1505-
{
1506-
prop.lcnf(compareBelow[i], !compareBelow[i-1]);
1507-
prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]);
1508-
prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]);
1509-
}
1552+
// Optional zeroing of the comparison bit when not needed
1553+
// \forall i != 0 . -c[i] => -c[i-1]
1554+
// \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1]
1555+
// \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1]
1556+
for(i = start; i > 0; i--)
1557+
{
1558+
prop.lcnf(compareBelow[i], !compareBelow[i - 1]);
1559+
prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i - 1]);
1560+
prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i - 1]);
1561+
}
15101562
#endif
15111563

1512-
// The 'base case' of the induction is the case when they are equal
1513-
prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result);
1514-
prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result);
1564+
// The 'base case' of the induction is the case when they are equal
1565+
prop.lcnf(
1566+
!compareBelow[0], !bv0[0], !bv1[0], (or_equal) ? result : !result);
1567+
prop.lcnf(
1568+
!compareBelow[0], bv0[0], bv1[0], (or_equal) ? result : !result);
15151569

1516-
return result;
1570+
return result;
1571+
}
15171572
}
15181573
else
15191574
#endif
15201575
{
1576+
// A <= B iff there is an overflow on A-B
15211577
literalt carry=
15221578
carry_out(bv0, inverted(bv1), const_literal(true));
15231579

@@ -1544,12 +1600,7 @@ literalt bv_utilst::unsigned_less_than(
15441600
const bvt &op0,
15451601
const bvt &op1)
15461602
{
1547-
#ifdef COMPACT_LT_OR_LE
15481603
return lt_or_le(false, op0, op1, representationt::UNSIGNED);
1549-
#else
1550-
// A <= B iff there is an overflow on A-B
1551-
return !carry_out(op0, inverted(op1), const_literal(true));
1552-
#endif
15531604
}
15541605

15551606
literalt bv_utilst::signed_less_than(

0 commit comments

Comments
 (0)