From a47a14064c81eef054c378635b817f8103070614 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 10 Mar 2022 10:40:07 +0100 Subject: [PATCH 1/3] LASolver: Style update of Simplex::computeDelta --- src/tsolvers/lasolver/Simplex.cc | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/tsolvers/lasolver/Simplex.cc b/src/tsolvers/lasolver/Simplex.cc index d73914b04..94d1dfb40 100644 --- a/src/tsolvers/lasolver/Simplex.cc +++ b/src/tsolvers/lasolver/Simplex.cc @@ -412,7 +412,7 @@ Delta Simplex::getValuation(LVRef v) const { opensmt::Real Simplex::computeDelta() const { /* - Delta computation according to the Technical Report accompanying the Simple paper + Delta computation according to the Technical Report accompanying the Simplex paper https://yices.csl.sri.com/papers/sri-csl-06-01.pdf For a pair (c,k) \in Q_\delta representing Real value c + k * \delta if the inequality (c_1, k_1) <= (c_2, k_2) holds then there exists \delta_0 such that \forall 0 < \epsilon < \delta_0 the inequality c_1 + k_1 * \epsilon <= c_2 + k_2 * \epsilon holds. @@ -427,15 +427,14 @@ opensmt::Real Simplex::computeDelta() const { Delta delta_abst; bool deltaNotSet = true; - const LAVarStore& laVarStore = boundStore.getVarStore(); - for (LVRef v : laVarStore) - { - assert( !isModelOutOfBounds(v) ); + LAVarStore const & laVarStore = boundStore.getVarStore(); + for (LVRef v : laVarStore) { + assert(not isModelOutOfBounds(v)); - if (model->read(v).D() == 0) + auto const & val = model->read(v); + if (val.D().isZero()) continue; // If values are exact we do not need to consider them for delta computation - auto const & val = model->read(v); // Computing delta to satisfy lower bound if (model->hasLBound(v)) { auto const & lb = model->Lb(v); @@ -443,7 +442,7 @@ opensmt::Real Simplex::computeDelta() const { if (lb.R() < val.R() && lb.D() > val.D()) { Real valOfDelta = (val.R() - lb.R()) / (lb.D() - val.D()); assert(valOfDelta > 0); - if (deltaNotSet || delta_abst > valOfDelta) { + if (deltaNotSet or delta_abst > valOfDelta) { deltaNotSet = false; delta_abst = valOfDelta; } @@ -456,7 +455,7 @@ opensmt::Real Simplex::computeDelta() const { if (val.R() < ub.R() && val.D() > ub.D()) { Real valOfDelta = (ub.R() - val.R()) / (val.D() - ub.D()); assert(valOfDelta > 0); - if (deltaNotSet || delta_abst > valOfDelta) { + if (deltaNotSet or delta_abst > valOfDelta) { deltaNotSet = false; delta_abst = valOfDelta; } @@ -464,7 +463,7 @@ opensmt::Real Simplex::computeDelta() const { } } - if (deltaNotSet || delta_abst > 1) { + if (deltaNotSet or delta_abst > 1) { return 1; } return delta_abst.R()/2; From caea4f93dca084a4d1e708fd0e851de484cece24 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 10 Mar 2022 10:57:43 +0100 Subject: [PATCH 2/3] LASolver: Extract maxDelta value to a named constant --- src/tsolvers/lasolver/LASolver.cc | 5 +++-- src/tsolvers/lasolver/Simplex.cc | 7 +++++-- src/tsolvers/lasolver/Simplex.h | 1 + 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index af04fa7e3..14cb9f96a 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -1034,14 +1034,15 @@ vec LASolver::collectEqualitiesFor(vec const & vars, std::unordere } for (auto const & val : valuesWithDelta) { for (auto const & entry : eqClasses) { - // check if entry.first - val could be 0 for some value of delta, with 0 < delta <= 1 + // check if entry.first - val could be 0 for some value of delta, with 0 < delta <= maxDelta auto diff = entry.first - val; if (not diff.hasDelta()) { continue; } // MB: This takes care also of the case where val == entry.first if (isNonNegative(diff.R()) and isPositive(diff.D())) { continue; } if (isNonPositive(diff.R()) and isNegative(diff.D())) { continue; } auto ratio = diff.R() / diff.D(); assert(isNegative(ratio)); - if (ratio < FastRational(-1)) { continue; } // MB: ratio is -delta; hence -1 <= ratio < 0 + ratio.negate(); // MB: delta is the negated ratio + if (ratio > Simplex::maxDelta) { continue; } // No chance of collision // They could be equal for the right value of delta, add equalities for cross-product vec const & varsOfFirstVal = eqClasses.at(val); diff --git a/src/tsolvers/lasolver/Simplex.cc b/src/tsolvers/lasolver/Simplex.cc index 94d1dfb40..44d1a2ec7 100644 --- a/src/tsolvers/lasolver/Simplex.cc +++ b/src/tsolvers/lasolver/Simplex.cc @@ -409,6 +409,9 @@ Delta Simplex::getValuation(LVRef v) const { return val; } +// Definition of static member +const opensmt::Real Simplex::maxDelta {1}; + opensmt::Real Simplex::computeDelta() const { /* @@ -463,8 +466,8 @@ opensmt::Real Simplex::computeDelta() const { } } - if (deltaNotSet or delta_abst > 1) { - return 1; + if (deltaNotSet or delta_abst > maxDelta) { + return maxDelta; } return delta_abst.R()/2; } diff --git a/src/tsolvers/lasolver/Simplex.h b/src/tsolvers/lasolver/Simplex.h index 03d6ded58..f51b1e721 100644 --- a/src/tsolvers/lasolver/Simplex.h +++ b/src/tsolvers/lasolver/Simplex.h @@ -100,6 +100,7 @@ class Simplex { bool checkValueConsistency() const; bool invariantHolds() const; + static const opensmt::Real maxDelta; opensmt::Real computeDelta() const; Delta getValuation(LVRef) const; // Understands also variables deleted by gaussian elimination // Delta read(LVRef v) const { assert(!tableau.isQuasiBasic(v)); return model->read(v); } // ignores unsafely variables deleted by gaussian elimination From 69b8c924425dfd4a9d132a0c2ae8bf0e58cd6a87 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 10 Mar 2022 11:14:29 +0100 Subject: [PATCH 3/3] Simplex: Lower the maxDelta value for model computation In our current implementation of model-based theory combination, we need to make sure that two classes of interface variables do not collapse for our computed value of Simplex's delta. Lowering the max value should help to avoid deciding some pairs of classes explicitly. --- src/tsolvers/lasolver/Simplex.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tsolvers/lasolver/Simplex.cc b/src/tsolvers/lasolver/Simplex.cc index 44d1a2ec7..e1f2a01f1 100644 --- a/src/tsolvers/lasolver/Simplex.cc +++ b/src/tsolvers/lasolver/Simplex.cc @@ -409,8 +409,8 @@ Delta Simplex::getValuation(LVRef v) const { return val; } -// Definition of static member -const opensmt::Real Simplex::maxDelta {1}; +// Definition of static member: maxDelta = 1/2; +const opensmt::Real Simplex::maxDelta {1,2}; opensmt::Real Simplex::computeDelta() const {