diff --git a/fppoly/fppoly.c b/fppoly/fppoly.c index a83c03c7..19cce503 100644 --- 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; }