buddy/src/fdd.c

33   DESCR: Finite domain extensions to BDD package
49 /*       and in index zero of the domain tables                         */
54    int realsize;   /* The specified domain (0...N-1) */
55    int binsize;    /* The number of BDD variables representing the domain */
67 static Domain *domain;            /* Table of domain sizes */
77    domain = NULL;
87    if (domain != NULL)
90 	 Domain_done(&domain[n]);
91       free(domain);
94    domain = NULL;
101 SHORT   {* adds another set of finite domain blocks *}
103 DESCR   {* Extends the set of finite domain blocks with the {\tt num}
106 	   finite domain which later on can be used for finite state machine
107 	   traversal and other operations on finte domains. Each domain
110 	   call to {\tt bdd\_extdomain}. This means that assuming domain
111 	   $D_0$ needs 2 BDD variables $x_1$ and $x_2$, and another domain
114 	   domain in {\tt dom} is returned. The index of the other domains
117 	   The BDD variables needed to encode the domain are created for the
120 RETURN  {* The index of the first domain or a negative error code. *}
133       /* Build domain table */
134    if (domain == NULL)  /* First time */
137       if ((domain=(Domain*)malloc(sizeof(Domain)*num)) == NULL)
146 	 domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
147 	 if (domain == NULL)
155       Domain_allocate(&domain[n+fdvarnum], dom[n]);
156       extravars += domain[n+fdvarnum].binsize;
169 	 if (bn < domain[n+fdvarnum].binsize)
172 	    domain[n+fdvarnum].ivar[bn] = binoffset++;
178       domain[n+fdvarnum].var = bdd_makeset(domain[n+fdvarnum].ivar,
179 					   domain[n+fdvarnum].binsize);
180       bdd_addref(domain[n+fdvarnum].var);
198 	   a_n$ and has a domain of $[0,N_1]$, and {\tt v2} is encoded using
199 	   $b_1, \ldots, b_n$ and has a domain of $[0,N_2]$, then the result
201 	   \ldots, b_n$ and have the domain $[0,N_1*N_2]$. The use of this
204 RETURN  {* The index of the finite domain block *}
222       domain = (Domain*)realloc(domain, sizeof(Domain)*fdvaralloc);
223       if (domain == NULL)
227    d = &domain[fdvarnum];
228    d->realsize = domain[v1].realsize * domain[v2].realsize;
229    d->binsize = domain[v1].binsize + domain[v2].binsize;
232    for (n=0 ; n<domain[v1].binsize ; n++)
233       d->ivar[n] = domain[v1].ivar[n];
234    for (n=0 ; n<domain[v2].binsize ; n++)
235       d->ivar[domain[v1].binsize+n] = domain[v2].ivar[n];
249 DESCR   {* Removes all defined finite domain blocks defined by
266 SHORT   {* number of defined finite domain blocks *}
268 DESCR   {* Returns the number of finite domain blocks define by calls to
270 RETURN  {* The number of defined finite domain blocks
286 SHORT   {* real size of a finite domain block *}
288 DESCR   {* Returns the size of the domain for the finite domain
300    return domain[v].realsize;
307 SHORT   {* binary size of a finite domain block *}
309 DESCR   {* Returns the number of BDD variables used for the finite domain
321    return domain[v].binsize;
328 SHORT   {* all BDD variables associated with a finite domain block *}
331            define the finite domain block {\tt var}. The size of the array
332 	   is the number of variables used to define the finite domain block.
353    return domain[v].ivar;
368            finite domain block {\tt var}. The encoding places the
394    if (val < 0  ||  val >= domain[var].realsize)
400    for (n=0 ; n<domain[var].binsize ; n++)
405 	 tmp = bdd_apply(bdd_ithvar(domain[var].ivar[n]), v, bddop_and);
407 	 tmp = bdd_apply(bdd_nithvar(domain[var].ivar[n]), v, bddop_and);
498       for (m=domain[n].binsize-1 ; m>=0 ; m--)
499 	 if ( store[domain[n].ivar[m]] )
515 SHORT   {* the variable set for the i'th finite domain block *}
518            define the finite domain block {\tt var}. *}
536    return domain[var].var;
542 SHORT   {* BDD encoding of the domain of a FDD variable *}
548 	   for all values in the domain of {\tt var}. *}
549 RETURN  {* The encoding of the domain*}
569       /* Encode V<=X-1. V is the variables in 'var' and X is the domain size */
571    dom = &domain[var];
622    if (domain[left].realsize != domain[right].realsize)
628    for (n=0 ; n<domain[left].binsize ; n++)
630       tmp1 = bdd_addref( bdd_apply(bdd_ithvar(domain[left].ivar[n]),
631 				   bdd_ithvar(domain[right].ivar[n]),
686 SHORT   {* prints a BDD for a finite domain block *}
690            {\tt bdd\_printset} but with the index of the finite domain blocks
754 	 for (m=0 ; m<domain[n].binsize ; m++)
755 	    if (set[domain[n].ivar[m]] != 0)
769 	    var = domain[n].ivar;
771 	    for (m=0 ; m<(1<<domain[n].binsize) ; m++)
776 	       for (i=0 ; i<domain[n].binsize && ok ; i++)
842       for (m=0 ; m<domain[n].binsize && !found ; m++)
845 	    if (domain[n].ivar[m] == fv[i])
860       for (m=0 ; m<domain[n].binsize && !found ; m++)
863 	    if (domain[n].ivar[m] == fv[i])
882 SHORT   {* creates a variable set for N finite domain blocks *}
911       tmp = bdd_apply(domain[varset[n]].var, res, bddop_and);
945       tmp = bdd_apply(domain[n].var, res, bddop_and);
960 SHORT   {* defines a pair for two finite domain blocks *}
962 DESCR   {* Defines each variable in the finite domain block {\tt p1} to
979    if (domain[p1].binsize != domain[p2].binsize)
982    for (n=0 ; n<domain[p1].binsize ; n++)
983       if ((e=bdd_setpair(pair, domain[p1].ivar[n], domain[p2].ivar[n])) < 0)
993 SHORT   {* defines N pairs for finite domain blocks *}
995 DESCR   {* Defines each variable in all the finite domain blocks listed in
1062    res = (int *)malloc(sizeof(int)*domain[var].binsize);
1063    memset(res, 0, sizeof(int)*domain[var].binsize);