diff options
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/passes/bv_gauss.cpp | 5 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_gauss.h | 3 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 23 | ||||
| -rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 2 |
4 files changed, 28 insertions, 5 deletions
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 683716410..b08f69b50 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -687,8 +687,9 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( return ret; } -BVGauss::BVGauss(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bv-gauss") +BVGauss::BVGauss(PreprocessingPassContext* preprocContext, + const std::string& name) + : PreprocessingPass(preprocContext, name) { } diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index 93d61be9e..7fb23814a 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -30,7 +30,8 @@ namespace passes { class BVGauss : public PreprocessingPass { public: - BVGauss(PreprocessingPassContext* preprocContext); + BVGauss(PreprocessingPassContext* preprocContext, + const std::string& name = "bv-gauss"); protected: /** 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: diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 7b8e61359..f1e9e39c5 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -169,7 +169,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::stringstream ssv; if (varCounter < 26) { - ssv << String::convertUnsignedIntToChar(varCounter + 32); + ssv << static_cast<char>(varCounter + 61); } else { |