From 2c1c2491ee404660d4059dd687fed088c9ab3377 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 27 Feb 2025 21:58:48 +0100 Subject: [PATCH 1/2] LASolver: Small refactoring --- src/tsolvers/lasolver/LASolver.cc | 13 +++++-------- src/tsolvers/lasolver/LASolver.h | 2 +- src/tsolvers/lasolver/LAVarMapper.cc | 5 ++--- src/tsolvers/lasolver/LAVarMapper.h | 23 +++++++++++++---------- 4 files changed, 21 insertions(+), 22 deletions(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index ab718eeb9..23d2b7a47 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -29,7 +29,7 @@ void LASolver::addBound(PTRef leq_tr) { LABoundRefPair boundRefs = [this, leq_tr]() -> LABoundRefPair { auto [const_tr, sum_tr] = logic.leqToConstantAndTerm(leq_tr); assert(logic.isNumConst(const_tr) && logic.isLinearTerm(sum_tr)); - LVRef const v = laVarMapper.getVarByPTId(logic.getPterm(sum_tr).getId()); + LVRef const v = getVarForTerm(sum_tr); bool const isNegated = laVarMapper.isNegated(sum_tr); auto values = isNegated ? getBoundsValue(v, -logic.getNumConst(const_tr), false) : getBoundsValue(v, logic.getNumConst(const_tr), true); @@ -182,15 +182,12 @@ void LASolver::markVarAsInt(LVRef v) { LVRef LASolver::getVarForLeq(PTRef ref) const { assert(logic.isLeq(ref)); auto [constant, term] = logic.leqToConstantAndTerm(ref); - return laVarMapper.getVarByPTId(logic.getPterm(term).getId()); + return getVarForTerm(term); } LVRef LASolver::getLAVar_single(PTRef expr_in) { - assert(logic.isLinearTerm(expr_in)); - PTId id = logic.getPterm(expr_in).getId(); - - if (laVarMapper.hasVar(id)) { + if (laVarMapper.hasVar(expr_in)) { return getVarForTerm(expr_in); } @@ -877,7 +874,7 @@ TRes LASolver::cutFromProof() { } auto getVarValue = [this](PTRef var) { assert(this->logic.isVar(var)); - LVRef lvar = this->laVarMapper.getVarByPTId(logic.getPterm(var).getId()); + LVRef lvar = this->getVarForTerm(var); Delta val = this->simplex.getValuation(lvar); assert(not val.hasDelta()); return val.R(); @@ -912,7 +909,7 @@ vec LASolver::collectEqualitiesFor(vec const & vars, std::unordere if (not laVarMapper.hasVar(var)) { // LASolver does not have any constraints on this LA var continue; } - LVRef v = laVarMapper.getVarByPTId(logic.getPterm(var).getId()); + LVRef v = getVarForTerm(var); auto value = simplex.getValuation(v); eqClasses[value].push(var); } diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index 524623fc6..f78808636 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -118,7 +118,7 @@ class LASolver : public TSolver { LVRef getLAVar_single(PTRef term); // Initialize a new LA var if needed, otherwise return the old var LVRef getVarForLeq(PTRef ref) const; - LVRef getVarForTerm(PTRef ref) const { return laVarMapper.getVarByPTId(logic.getPterm(ref).getId()); } + LVRef getVarForTerm(PTRef ref) const { return laVarMapper.getVar(ref); } void notifyVar(LVRef); // Notify the solver of the existence of the var. This is so that LIA can add it to // integer vars list. diff --git a/src/tsolvers/lasolver/LAVarMapper.cc b/src/tsolvers/lasolver/LAVarMapper.cc index bcf3d95c5..c701ad2d1 100644 --- a/src/tsolvers/lasolver/LAVarMapper.cc +++ b/src/tsolvers/lasolver/LAVarMapper.cc @@ -31,7 +31,6 @@ void LAVarMapper::registerNewMapping(LVRef lv, PTRef e_orig) { PTId id_pos = logic.getPterm(e_orig).getId(); PTId id_neg = logic.getPterm(logic.mkNeg(e_orig)).getId(); - assert(!hasVar(id_pos)); int max_id = std::max(Idx(id_pos), Idx(id_neg)); if (max_id >= ptermToLavar.size()) { @@ -43,11 +42,11 @@ void LAVarMapper::registerNewMapping(LVRef lv, PTRef e_orig) { ptermToLavar[Idx(id_neg)] = lv; } -LVRef LAVarMapper::getVarByPTId(PTId i) const { return ptermToLavar[Idx(i)]; } +LVRef LAVarMapper::getVar(PTRef tr) const { return ptermToLavar[Idx(logic.getPterm(tr).getId())]; } bool LAVarMapper::hasVar(PTRef tr) const { return hasVar(logic.getPterm(tr).getId()); } -bool LAVarMapper::hasVar(PTId i) const { +bool LAVarMapper::hasVar(PTId i) const { return static_cast(ptermToLavar.size()) > Idx(i) && ptermToLavar[Idx(i)] != LVRef::Undef; } diff --git a/src/tsolvers/lasolver/LAVarMapper.h b/src/tsolvers/lasolver/LAVarMapper.h index 91b0672a1..6ba4d741d 100644 --- a/src/tsolvers/lasolver/LAVarMapper.h +++ b/src/tsolvers/lasolver/LAVarMapper.h @@ -28,22 +28,13 @@ class ArithLogic; * instead of forcing to isolate the term from the constant and normalize it. */ class LAVarMapper { -private: - /** Mapping of linear Pterms to LVRefs */ - vec ptermToLavar; - - /** The inverse of ptermToLavar, mapping LVRefs to PTRefs */ - vec laVarToPTRef; - - ArithLogic& logic; public: LAVarMapper(ArithLogic &logic) : logic(logic) {} void registerNewMapping(LVRef lv, PTRef e_orig); - LVRef getVarByPTId(PTId i) const; + LVRef getVar(PTRef tr) const; - bool hasVar(PTId i) const; bool hasVar(PTRef tr) const; inline PTRef getVarPTRef(LVRef ref) const { return laVarToPTRef[ref.x]; } @@ -51,6 +42,18 @@ class LAVarMapper { void clear(); bool isNegated(PTRef tr) const; + +private: + bool hasVar(PTId i) const; + + /** Mapping of linear Pterms to LVRefs */ + vec ptermToLavar; + + /** The inverse of ptermToLavar, mapping LVRefs to PTRefs */ + vec laVarToPTRef; + + ArithLogic& logic; + }; } From cbde920ef8b70722ed94dcc5013a74f3c7164527 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 27 Feb 2025 21:19:04 +0100 Subject: [PATCH 2/2] LASolver: Skip redundant check LASolver::updateBound was always called only on new inequalities, never on already seen ones. --- src/tsolvers/lasolver/LASolver.cc | 20 ++++---------------- src/tsolvers/lasolver/LASolver.h | 1 - 2 files changed, 4 insertions(+), 17 deletions(-) diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 23d2b7a47..61b7efb5d 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -38,6 +38,8 @@ void LASolver::addBound(PTRef leq_tr) { }(); int const tid = Idx(logic.getPterm(leq_tr).getId()); + // Must be a new inequality + assert(tid >= LeqToLABoundRefPair.size() or (LeqToLABoundRefPair[tid] == LABoundRefPair{LABoundRef_Undef, LABoundRef_Undef})); if (LeqToLABoundRefPair.size() <= tid) { LeqToLABoundRefPair.growTo(tid + 1); } @@ -52,18 +54,6 @@ void LASolver::addBound(PTRef leq_tr) { LABoundRefToLeqAsgn[br_neg_idx] = PtAsgn(leq_tr, l_False); } -void LASolver::updateBound(PTRef tr) -{ - // If the bound already exists, do nothing. - int id = Idx(logic.getPterm(tr).getId()); - - if ((LeqToLABoundRefPair.size() > id) && - !(LeqToLABoundRefPair[id] == LABoundRefPair{LABoundRef_Undef, LABoundRef_Undef})) { - return; - } - addBound(tr); -} - bool LASolver::isValid(PTRef tr) { return logic.isLeq(tr); // MB: LA solver expects only inequalities in LEQ form! @@ -278,12 +268,10 @@ void LASolver::declareAtom(PTRef leq_tr) if (status != INIT) { - // Treat the PTRef as it is pushed on-the-fly - // status = INCREMENT; - assert( status == SAT ); + assert(status == SAT); PTRef term = logic.getPterm(leq_tr)[1]; registerArithmeticTerm(term); - updateBound(leq_tr); + addBound(leq_tr); } // DEBUG check isProperLeq(leq_tr); diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index f78808636..2e65bde80 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -93,7 +93,6 @@ class LASolver : public TSolver { PTRef getVarPTRef(LVRef v) const { return laVarMapper.getVarPTRef(v); } void addBound(PTRef leq_tr); - void updateBound(PTRef leq_tr); LVRef registerArithmeticTerm(PTRef expr); // Ensures this term and all variables in it has corresponding LVAR. // Returns the LAVar for the term. void storeExplanation(Simplex::Explanation && explanationBounds);