From e73c451011ceae6b9653c2332fe1d8a33b108522 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Jul 2025 10:42:47 +0000 Subject: [PATCH] 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. --- src/solvers/flattening/bv_utils.cpp | 175 ++++++++++++++++++---------- 1 file changed, 113 insertions(+), 62 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 31dd12fea20..5ea86851c15 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -1415,11 +1415,6 @@ literalt bv_utilst::lt_or_le( #ifdef COMPACT_LT_OR_LE if(prop.has_set_to() && prop.cnf_handled_well()) { - bvt compareBelow; // 1 if a compare is needed below this bit - literalt result; - size_t start; - size_t i; - if(rep == representationt::SIGNED) { if(top0.is_false() && top1.is_true()) @@ -1429,8 +1424,9 @@ literalt bv_utilst::lt_or_le( INVARIANT( bv0.size() >= 2, "signed bitvectors should have at least two bits"); - compareBelow = prop.new_variables(bv0.size() - 1); - start = compareBelow.size() - 1; + // 1 if a compare is needed below this bit + bvt compareBelow = prop.new_variables(bv0.size() - 1); + size_t start = compareBelow.size() - 1; literalt &firstComp = compareBelow[start]; if(top0.is_false()) @@ -1442,7 +1438,7 @@ literalt bv_utilst::lt_or_le( else if(top1.is_true()) firstComp = top0; - result = prop.new_variable(); + literalt result = prop.new_variable(); // When comparing signs we are comparing the top bit // Four cases... @@ -1454,70 +1450,130 @@ literalt bv_utilst::lt_or_le( #ifdef INCLUDE_REDUNDANT_CLAUSES prop.lcnf(top0, !top1, !firstComp); prop.lcnf(!top0, top1, !firstComp); -#endif - } - else - { - // Unsigned is much easier - compareBelow = prop.new_variables(bv0.size() - 1); - compareBelow.push_back(const_literal(true)); - start = compareBelow.size() - 1; - result = prop.new_variable(); - } +# endif - // Determine the output - // \forall i . cb[i] & -a[i] & b[i] => result - // \forall i . cb[i] & a[i] & -b[i] => -result - i = start; - do - { - if(compareBelow[i].is_false()) - continue; - else if(compareBelow[i].is_true()) + // Determine the output + // \forall i . cb[i] & -a[i] & b[i] => result + // \forall i . cb[i] & a[i] & -b[i] => -result + size_t i = start; + do { - if(bv0[i].is_false() && bv1[i].is_true()) - return const_literal(true); - else if(bv0[i].is_true() && bv1[i].is_false()) - return const_literal(false); + if(compareBelow[i].is_false()) + continue; + + prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result); + prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result); + } while(i-- != 0); + + // Chain the comparison bit + // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1] + // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1] + for(i = start; i > 0; i--) + { + prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i - 1]); + prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i - 1]); } - prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result); - prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result); - } - while(i-- != 0); +# ifdef INCLUDE_REDUNDANT_CLAUSES + // Optional zeroing of the comparison bit when not needed + // \forall i != 0 . -c[i] => -c[i-1] + // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1] + // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1] + for(i = start; i > 0; i--) + { + prop.lcnf(compareBelow[i], !compareBelow[i - 1]); + prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i - 1]); + prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i - 1]); + } +# endif - // Chain the comparison bit - // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1] - // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1] - for(i = start; i > 0; i--) - { - prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i-1]); - prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i-1]); - } + // The 'base case' of the induction is the case when they are equal + prop.lcnf( + !compareBelow[0], !bv0[0], !bv1[0], (or_equal) ? result : !result); + prop.lcnf( + !compareBelow[0], bv0[0], bv1[0], (or_equal) ? result : !result); + return result; + } + else + { + // Unsigned is much easier + // 1 if a compare is needed below this bit + bvt compareBelow; + literalt result; + size_t start = bv0.size() - 1; + + // Determine the output + // \forall i . cb[i] & -a[i] & b[i] => result + // \forall i . cb[i] & a[i] & -b[i] => -result + bool same_prefix = true; + size_t i = start; + do + { + if(same_prefix) + { + if(i == 0) + { + if(or_equal) + return prop.lor(!bv0[0], bv1[0]); + else + return prop.land(!bv0[0], bv1[0]); + } + else if(bv0[i] == bv1[i]) + continue; + else if(bv0[i].is_false() && bv1[i].is_true()) + return const_literal(true); + else if(bv0[i].is_true() && bv1[i].is_false()) + return const_literal(false); + else + { + same_prefix = false; + start = i; + compareBelow = prop.new_variables(i); + compareBelow.push_back(const_literal(true)); + result = prop.new_variable(); + } + } + + prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], result); + prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !result); + } while(i-- != 0); + + // Chain the comparison bit + // \forall i != 0 . cb[i] & a[i] & b[i] => cb[i-1] + // \forall i != 0 . cb[i] & -a[i] & -b[i] => cb[i-1] + for(i = start; i > 0; i--) + { + prop.lcnf(!compareBelow[i], !bv0[i], !bv1[i], compareBelow[i - 1]); + prop.lcnf(!compareBelow[i], bv0[i], bv1[i], compareBelow[i - 1]); + } #ifdef INCLUDE_REDUNDANT_CLAUSES - // Optional zeroing of the comparison bit when not needed - // \forall i != 0 . -c[i] => -c[i-1] - // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1] - // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1] - for(i = start; i > 0; i--) - { - prop.lcnf(compareBelow[i], !compareBelow[i-1]); - prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i-1]); - prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i-1]); - } + // Optional zeroing of the comparison bit when not needed + // \forall i != 0 . -c[i] => -c[i-1] + // \forall i != 0 . c[i] & -a[i] & b[i] => -c[i-1] + // \forall i != 0 . c[i] & a[i] & -b[i] => -c[i-1] + for(i = start; i > 0; i--) + { + prop.lcnf(compareBelow[i], !compareBelow[i - 1]); + prop.lcnf(!compareBelow[i], bv0[i], !bv1[i], !compareBelow[i - 1]); + prop.lcnf(!compareBelow[i], !bv0[i], bv1[i], !compareBelow[i - 1]); + } #endif - // The 'base case' of the induction is the case when they are equal - prop.lcnf(!compareBelow[0], !bv0[0], !bv1[0], (or_equal)?result:!result); - prop.lcnf(!compareBelow[0], bv0[0], bv1[0], (or_equal)?result:!result); + // The 'base case' of the induction is the case when they are equal + prop.lcnf( + !compareBelow[0], !bv0[0], !bv1[0], (or_equal) ? result : !result); + prop.lcnf( + !compareBelow[0], bv0[0], bv1[0], (or_equal) ? result : !result); - return result; + return result; + } } else #endif { + // A <= B iff there is an overflow on A-B literalt carry= carry_out(bv0, inverted(bv1), const_literal(true)); @@ -1544,12 +1600,7 @@ literalt bv_utilst::unsigned_less_than( const bvt &op0, const bvt &op1) { -#ifdef COMPACT_LT_OR_LE return lt_or_le(false, op0, op1, representationt::UNSIGNED); -#else - // A <= B iff there is an overflow on A-B - return !carry_out(op0, inverted(op1), const_literal(true)); -#endif } literalt bv_utilst::signed_less_than(