Lookahead: checking wheter a bound propagates

This commit introduces a simple check whether a given linear inequality
would result in a propagation of another linear inequality.

Author: aehyvari

src/tsolvers/lasolver/LASolver.cc

@@ -623,13 +623,32 @@ bool LASolver::setStatus( LASolverStatus s )
     return getStatus( );
 }
 
-bool LASolver::wouldDeduce(LABoundRef br) const {
-    LABound const & bound = boundStore[br];
+bool LASolver::wouldDeduce(PtAsgn asgn) const {
+    assert(status != INIT);
+    assert(logic.isLeq(asgn.tr));
+    assert(not hasPolarity(asgn.tr));
+    LVRef v = getVarForLeq(asgn.tr);
+    LABoundRef boundRef = asgn.sgn == l_False ? getBoundRefPair(asgn.tr).neg : getBoundRefPair(asgn.tr).pos;
+    LABound const & bound = boundStore[boundRef];
+
+    auto searchForUnassignedBound = [this, &bound, &v](BoundT type) {
+        for (int it = bound.getIdx().x - 1; it >= 0; -- it) {
+            LABoundRef candidateRef = boundStore.getBoundByIdx(v, it);
+            LABound const & candidate = boundStore[candidateRef];
+            if (candidate.getType() != type) {
+                continue;
+            } else if (not hasPolarity(getAsgnByBound(candidateRef).tr)) {
+                return true;
+            }
+        }
+        return false;
+    };
+
     if (bound.getType() == bound_l) {
-       for (int it = bound.getIdx().x - 1; it >= 0; -- it) {
-          LABoundRef propagatedBoundRef = boundStore.getBoundByIdx(v, it)
-       }
+        return searchForUnassignedBound(bound_u);
     }
+    assert(bound.getType() == bound_u);
+    return searchForUnassignedBound(bound_l);
 }
 
 void LASolver::getSimpleDeductions(LVRef v, LABoundRef br)

src/tsolvers/lasolver/LASolver.h

@@ -160,6 +160,7 @@ class LASolver: public TSolver
     bool shouldTryCutFromProof() const;
 
     void getSuggestions( vec<PTRef>& dst, SolverId solver_id );                                   // find possible suggested atoms
+    bool wouldDeduce(PtAsgn pta) const; // Would setting this assignment deduce more bounds
     void getSimpleDeductions(LVRef v, LABoundRef);      // find deductions from actual bounds position
     unsigned getIteratorByPTRef( PTRef e, bool );                                                 // find bound iterator by the PTRef
     inline bool getStatus( );                               // Read the status of the solver in lbool