updates for get_bounds_for_linexpr0

cwright7101 · Oct 1, 2019 · a67be60 · a67be60
1 parent 8328985
commit a67be60
Showing 1 changed file with 17 additions and 5 deletions.
diff --git a/fppoly/fppoly.c b/fppoly/fppoly.c
@@ -3633,8 +3633,12 @@ double get_lb_using_previous_layers(elina_manager_t *man, fppoly_t *fp,
   expr_t *lexpr = copy_expr(expr);
   fppoly_internal_t *pr =
       fppoly_init_from_manager(man, ELINA_FUNID_ASSIGN_LINEXPR_ARRAY);
-  k = layerno - 1;
-
+  if (fp->numlayers == layerno) {
+    k = layerno - 1;
+  } else {
+    k = fp->layers[layerno]->predecessors[0] - 1;
+  }
+  double res = -INFINITY;
   while (k >= 0) {
 
     if (fp->layers[k]->type == RESIDUAL) {
@@ -3693,10 +3697,11 @@ double get_lb_using_previous_layers(elina_manager_t *man, fppoly_t *fp,
 
       get_lb_using_predecessor_layer(pr, fp, &lexpr, k, use_area_heuristic);
       k = fp->layers[k]->predecessors[0] - 1;
+      res = fmax(res, compute_lb_from_expr(pr, lexpr, fp, k));
     }
   }
 
-  double res = compute_lb_from_expr(pr, lexpr, fp, -1);
+  res = fmax(res, compute_lb_from_expr(pr, lexpr, fp, -1));
   free_expr(lexpr);
   return res;
 }
@@ -3710,7 +3715,13 @@ double get_ub_using_previous_layers(elina_manager_t *man, fppoly_t *fp,
   expr_t *uexpr = copy_expr(expr);
   fppoly_internal_t *pr =
       fppoly_init_from_manager(man, ELINA_FUNID_ASSIGN_LINEXPR_ARRAY);
-  k = layerno - 1;
+
+  if (fp->numlayers == layerno) {
+    k = layerno - 1;
+  } else {
+    k = fp->layers[layerno]->predecessors[0] - 1;
+  }
+  double res = INFINITY;
   while (k >= 0) {
     if (fp->layers[k]->type == RESIDUAL) {
       if (fp->layers[k]->activation == RELU) {
@@ -3768,10 +3779,11 @@ double get_ub_using_previous_layers(elina_manager_t *man, fppoly_t *fp,
 
       get_ub_using_predecessor_layer(pr, fp, &uexpr, k, use_area_heuristic);
       k = fp->layers[k]->predecessors[0] - 1;
+      res = fmin(res, compute_ub_from_expr(pr, uexpr, fp, k));
     }
   }
 
-  double res = compute_ub_from_expr(pr, uexpr, fp, -1);
+  res = fmin(res, compute_ub_from_expr(pr, uexpr, fp, -1));
   free_expr(uexpr);
   return res;
 }