LASolver: Skip redundant check

LASolver::updateBound was always called only on new inequalities, never
on already seen ones.

Author: blishko

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);

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);