forked from eth-sri/ELINA
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathzonotope_otherops.c
64 lines (60 loc) · 2.17 KB
/
zonotope_otherops.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
/*
*
* This source file is part of ELINA (ETH LIbrary for Numerical Analysis).
* ELINA is Copyright © 2021 Department of Computer Science, ETH Zurich
* This software is distributed under GNU Lesser General Public License Version 3.0.
* For more information, see the ELINA project website at:
* http://elina.ethz.ch
*
* THE SOFTWARE IS PROVIDED "AS-IS" WITHOUT ANY WARRANTY OF ANY KIND, EITHER
* EXPRESS, IMPLIED OR STATUTORY, INCLUDING BUT NOT LIMITED TO ANY WARRANTY
* THAT THE SOFTWARE WILL CONFORM TO SPECIFICATIONS OR BE ERROR-FREE AND ANY
* IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE,
* TITLE, OR NON-INFRINGEMENT. IN NO EVENT SHALL ETH ZURICH BE LIABLE FOR ANY
* DAMAGES, INCLUDING BUT NOT LIMITED TO DIRECT, INDIRECT,
* SPECIAL OR CONSEQUENTIAL DAMAGES, ARISING OUT OF, RESULTING FROM, OR IN
* ANY WAY CONNECTED WITH THIS SOFTWARE (WHETHER OR NOT BASED UPON WARRANTY,
* CONTRACT, TORT OR OTHERWISE).
*
*/
#include "zonotope_otherops.h"
zonotope_t* zonotope_forget_array(elina_manager_t* man,
bool destructive, zonotope_t* z,
elina_dim_t* tdim, size_t size,
bool project)
{
start_timing();
zonotope_internal_t* pr = zonotope_init_from_manager(man, ELINA_FUNID_FORGET_ARRAY);
zonotope_t* res;
size_t i;
//printf("forget input %d\n",tdim[0]);
//zonotope_fprint(stdout,man,z,NULL);
//fflush(stdout);
man->result.flag_best = true;
man->result.flag_exact = true;
res = destructive ? z : zonotope_copy(man,z);
if (project){
for (i=0;i<size;i++){
zonotope_aff_check_free(pr, res->paf[tdim[i]]);
res->paf[tdim[i]] = zonotope_aff_alloc_init(pr);
res->paf[tdim[i]]->pby++;
res->box_inf[tdim[i]] = 0.0;
res->box_sup[tdim[i]] = 0.0;
}
}
else {
for (i=0;i<size;i++){
zonotope_aff_check_free(pr, res->paf[tdim[i]]);
res->paf[tdim[i]] = pr->top;
res->paf[tdim[i]]->pby++;
res->box_inf[tdim[i]]=INFINITY;
res->box_sup[tdim[i]]=INFINITY;
}
}
//printf("forget output %d\n", res->paf[tdim[0]] == pr->top);
//zonotope_fprint(stdout,man,res,NULL);
//fflush(stdout);
record_timing(zonotope_forget_array_time);
return res;
//not_implemented();
}