Merge pull request eth-sri#49 from ljlin/master

elina_zonotope bugfix
cwright7101 · Jun 21, 2019 · 1bc0d24 · 1bc0d24
2 parents e137b97 + ca67d1e
commit 1bc0d24
Show file tree

Hide file tree

Showing 3 changed files with 62 additions and 18 deletions.
diff --git a/elina_zonotope/elina_box_meetjoin.c b/elina_zonotope/elina_box_meetjoin.c
@@ -488,13 +488,31 @@ static bool elina_double_boxize_lincons0(double* res_inf, double * res_sup,
     elina_coeff_swap(tmp,coeff);
     double inf = 0.0;
     double sup = 0.0;
-
-    if (tmp->discr == ELINA_COEFF_SCALAR) {
-      inf = -tmp->val.scalar->val.dbl;
-      sup = tmp->val.scalar->val.dbl;
+    double d;
+
+    if (tmp->discr==ELINA_COEFF_SCALAR) {
+      if (tmp->discr == ELINA_SCALAR_DOUBLE) {
+        inf = -tmp->val.scalar->val.dbl;
+        sup = tmp->val.scalar->val.dbl;
+      } else {
+        elina_double_set_scalar(&d, tmp->val.scalar, GMP_RNDD);
+        inf = -d;
+        elina_double_set_scalar(&d, tmp->val.scalar, GMP_RNDU);
+        sup = d;
+      }
     } else {
-      inf = -tmp->val.interval->inf->val.dbl;
-      sup = tmp->val.interval->sup->val.dbl;
+        if (tmp->val.interval->inf->discr == ELINA_SCALAR_DOUBLE) {
+            inf = -tmp->val.interval->inf->val.dbl;
+        } else {
+            elina_double_set_scalar(&d,tmp->val.interval->inf,GMP_RNDD);
+            inf = -d;
+        }
+        if (tmp->val.interval->sup->discr == ELINA_SCALAR_DOUBLE) {
+            sup = tmp->val.interval->sup->val.dbl;
+        } else {
+            elina_double_set_scalar(&d,tmp->val.interval->inf,GMP_RNDU);
+            sup = d;
+        }
     }
     /* 2. evaluate e' */
     elina_double_interval_eval_elina_linexpr0(&itv_inf, & itv_sup, expr,env_inf, env_sup, discr);

diff --git a/elina_zonotope/zonotope_internal.c b/elina_zonotope/zonotope_internal.c
@@ -292,18 +292,44 @@ zonotope_aff_t * zonotope_aff_from_linexpr0(zonotope_internal_t* pr, elina_linex
     elina_coeff_t *coeff;
     zonotope_aff_t *res = zonotope_aff_alloc_init(pr);
     elina_coeff_t * cst = &(expr->cst);
-    if (cst->discr == ELINA_COEFF_SCALAR) {
-      res->c_inf = -cst->val.scalar->val.dbl;
-      res->c_sup = cst->val.scalar->val.dbl;
-      res->itv_inf = -cst->val.scalar->val.dbl;
-      res->itv_sup = cst->val.scalar->val.dbl;
+
+    if(cst->discr==ELINA_COEFF_SCALAR) {
+        if (cst->val.scalar->discr == ELINA_SCALAR_DOUBLE) {
+            res->c_inf = -cst->val.scalar->val.dbl;
+            res->c_sup = cst->val.scalar->val.dbl;
+            res->itv_inf = -cst->val.scalar->val.dbl;
+            res->itv_sup = cst->val.scalar->val.dbl;
+        } else {
+            double inf,sup;
+            elina_double_set_scalar(&inf,cst->val.scalar,GMP_RNDD);
+            elina_double_set_scalar(&sup,cst->val.scalar,GMP_RNDU);
+            res->c_inf = -inf;
+            res->c_sup = sup;
+            res->itv_inf = -inf;
+            res->itv_sup = sup;
+        }
     } else {
-      res->c_inf = -cst->val.interval->inf->val.dbl;
-      res->c_sup = cst->val.interval->sup->val.dbl;
-      res->itv_inf = -cst->val.interval->inf->val.dbl;
-      res->itv_sup = cst->val.interval->sup->val.dbl;
+        if (cst->val.interval->inf->discr == ELINA_SCALAR_DOUBLE) {
+            res->c_inf = -cst->val.interval->inf->val.dbl;
+            res->itv_inf = -cst->val.interval->inf->val.dbl;
+        } else {
+            double inf;
+            elina_double_set_scalar(&inf,cst->val.scalar,GMP_RNDD);
+            res->c_inf = -inf;
+            res->itv_inf = -inf;
+        }
+        if (cst->val.interval->sup->discr == ELINA_SCALAR_DOUBLE) {
+            res->c_sup = cst->val.interval->sup->val.dbl;
+            res->itv_sup = cst->val.interval->sup->val.dbl;
+        } else {
+            double sup;
+            elina_double_set_scalar(&sup,cst->val.scalar,GMP_RNDU);
+            res->c_sup = sup;
+            res->itv_sup = sup;
+        }
     }
-        //printf("size: %zu\n",expr->size);
+
+	//printf("size: %zu\n",expr->size);
 	//fflush(stdout);
     elina_linexpr0_ForeachLinterm(expr,i,dim,coeff) {
         zonotope_aff_t *aff = z->paf[dim];

diff --git a/elina_zonotope/zonotope_internal.h b/elina_zonotope/zonotope_internal.h
@@ -1435,8 +1435,8 @@ static inline zonotope_aff_t * zonotope_aff_join_constrained6(zonotope_internal_
 
         elina_scalar_sub(c0,dmax,dmin, ELINA_SCALAR_DOUBLE);
 	elina_scalar_div_2(c0, c0);
-        res->c_inf = c0->val.dbl;
-        res->c_sup = c0->val.dbl; 
+	res->c_inf = -c0->val.dbl;
+	res->c_sup = c0->val.dbl; 
 
 	if (elina_scalar_cmp(c1->inf,c2->inf) < 0) {
 	    elina_scalar_set(min, c1->inf);