Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

LRA: Use smaller value in delta computation #444

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

LRA: Use smaller value in delta computation #444

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a47a140
LASolver: Style update of Simplex::computeDelta
Mar 10, 2022
caea4f9
LASolver: Extract maxDelta value to a named constant
Mar 10, 2022
69b8c92
Simplex: Lower the maxDelta value for model computation
Mar 10, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/tsolvers/lasolver/LASolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1034,14 +1034,15 @@ vec<PTRef> LASolver::collectEqualitiesFor(vec<PTRef> 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<PTRef> const & varsOfFirstVal = eqClasses.at(val);
Expand Down
24 changes: 13 additions & 11 deletions src/tsolvers/lasolver/Simplex.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -409,10 +409,13 @@ Delta Simplex::getValuation(LVRef v) const {
return val;
}

// Definition of static member: maxDelta = 1/2;
const opensmt::Real Simplex::maxDelta {1,2};

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.
Expand All @@ -427,23 +430,22 @@ 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);
assert(lb.R() <= val.R());
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;
}
Expand All @@ -456,16 +458,16 @@ 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;
}
}
}
}

if (deltaNotSet || delta_abst > 1) {
return 1;
if (deltaNotSet or delta_abst > maxDelta) {
return maxDelta;
}
return delta_abst.R()/2;
}
Expand Down
1 change: 1 addition & 0 deletions src/tsolvers/lasolver/Simplex.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down