diff options
| author | Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | 2020-03-25 09:37:57 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-25 11:37:57 -0500 |
| commit | 34a0e4420960a2f6a34d02e53636fecd63b5c4de (patch) | |
| tree | 969319b0e4a83b1c019c777187efbb5d0d94129a | |
| parent | b71f00097394c5f292abb002e31f49a07aff0b58 (diff) | |
bv2int : linear mult opt (#4142)
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index cb78b0897..0e4bc41c0 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -401,7 +401,28 @@ Node BVToInt::bvToInt(Node n) d_nm->mkNode(kind::MINUS, mult, multSig); d_rangeAssertions.insert( mkRangeConstraint(d_bvToIntCache[current], bvsize)); - d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize)); + if (translated_children[0].isConst() + || translated_children[1].isConst()) + { + /* + * based on equation (23), section 3.2.3 of: + * Bozzano et al. + * Encoding RTL Constructs for MathSAT: a Preliminary Report. + */ + // this is an optimization when one of the children is constant + Node c = translated_children[0].isConst() + ? translated_children[0] + : translated_children[1]; + d_rangeAssertions.insert( + d_nm->mkNode(kind::LEQ, d_zero, sigma)); + // the value of sigma is bounded by (c - 1) + // where c is the constant multiplicand + d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c)); + } + else + { + d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize)); + } break; } case kind::BITVECTOR_UDIV_TOTAL: |