Lookahead: start working on linear arith [WiP]

Author: aehyvari

src/tsolvers/lasolver/LASolver.cc

@@ -623,6 +623,14 @@ bool LASolver::setStatus( LASolverStatus s )
     return getStatus( );
 }
 
+bool LASolver::wouldDeduce(LABoundRef br) const {
+    LABound const & bound = boundStore[br];
+    if (bound.getType() == bound_l) {
+       for (int it = bound.getIdx().x - 1; it >= 0; -- it) {
+          LABoundRef propagatedBoundRef = boundStore.getBoundByIdx(v, it)
+       }
+    }
+}
 
 void LASolver::getSimpleDeductions(LVRef v, LABoundRef br)
 {

src/tsolvers/lasolver/LASolver.h

@@ -181,9 +181,11 @@ class LASolver: public TSolver
 
     inline int     verbose                       ( ) const { return config.verbosity(); }
 
+    void deduce(LABoundRef bound_prop);
+    bool wouldDeduce(LABoundRef bound_prop) const;
+
     // Debug stuff
     void isProperLeq(PTRef tr);  // The Leq term conforms to the assumptions of its form.  Only asserts.
-    void deduce(LABoundRef bound_prop);
 };
 
 #endif