source: vis_dev/glu-2.3/src/cmuPort/cmuPort.c

Last change on this file was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 51.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cmuPort.c]
4
5  PackageName [cmu_port]
6
7  Synopsis    [Port routines for CMU package.]
8
9  Description [optional]
10
11  SeeAlso     [optional]
12
13  Author      [Thomas R. Shiple. Some changes by Rajeev K. Ranjan.]
14
15  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
16  All rights reserved.
17
18  Permission is hereby granted, without written agreement and without license
19  or royalty fees, to use, copy, modify, and distribute this software and its
20  documentation for any purpose, provided that the above copyright notice and
21  the following two paragraphs appear in all copies of this software.
22
23  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
24  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
25  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
26  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27
28  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
29  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
30  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
31  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
32  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33
34  Revision    [$Id: cmuPort.c,v 1.80 2009/04/11 16:13:17 fabio Exp $]
35
36******************************************************************************/
37
38#include "cmuPortInt.h"
39#ifndef EPD_MAX_BIN
40#include "epd.h"
41#endif
42
43/*---------------------------------------------------------------------------*/
44/* Constant declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47
48/*---------------------------------------------------------------------------*/
49/* Type declarations                                                         */
50/*---------------------------------------------------------------------------*/
51
52
53/*---------------------------------------------------------------------------*/
54/* Structure declarations                                                    */
55/*---------------------------------------------------------------------------*/
56
57
58/*---------------------------------------------------------------------------*/
59/* Variable declarations                                                     */
60/*---------------------------------------------------------------------------*/
61
62
63/*---------------------------------------------------------------------------*/
64/* Macro declarations                                                        */
65/*---------------------------------------------------------------------------*/
66
67
68/**AutomaticStart*************************************************************/
69
70/*---------------------------------------------------------------------------*/
71/* Static function prototypes                                                */
72/*---------------------------------------------------------------------------*/
73
74/**AutomaticEnd***************************************************************/
75
76
77/*---------------------------------------------------------------------------*/
78/* Definition of exported functions                                          */
79/*---------------------------------------------------------------------------*/
80
81/**Function********************************************************************
82
83  Synopsis    [Builds the bdd_t structure.]
84
85  Description [Builds the bdd_t structure from manager and node.
86  Assumes that the reference count of the node has already been
87  increased.]
88
89  SideEffects []
90
91******************************************************************************/
92bdd_t *
93bdd_construct_bdd_t(bdd_manager *manager, bdd_node *func)
94{
95    bdd_t *result;
96    cmu_bdd_manager mgr = (cmu_bdd_manager)manager;
97    bdd fn = (bdd)func;
98
99    if (fn == (struct bdd_ *) 0) {
100        cmu_bdd_fatal("bdd_construct_bdd_t: possible memory overflow");
101    }
102
103    result = ALLOC(bdd_t, 1);
104    result->mgr = mgr;
105    result->node = fn;
106    result->free = FALSE;
107    return result;
108}
109
110/**Function********************************************************************
111  Synopsis           [required]
112
113  Description        [optional]
114
115  SideEffects        [required]
116
117  SeeAlso            [optional]
118******************************************************************************/
119bdd_package_type_t
120bdd_get_package_name(void)
121{
122  return CMU;
123}
124
125/*
126BDD Manager Allocation And Destruction ----------------------------------------
127*/
128void
129bdd_end(bdd_manager *manager)
130{
131    bdd_external_hooks *hooks;
132    cmu_bdd_manager mgr = (cmu_bdd_manager)manager;
133    hooks = (bdd_external_hooks *) mgr->hooks;
134    FREE(hooks); 
135    cmu_bdd_quit(mgr);
136}
137
138
139bdd_manager *
140bdd_start(int nvariables)
141{
142    struct bdd_manager_ *mgr;
143    int i;
144    bdd_external_hooks *hooks;
145   
146    mgr = cmu_bdd_init();    /*no args*/
147
148    /*
149     * Calls to UCB bdd_get_variable are translated into cmu_bdd_var_with_id calls.  However,
150     * cmu_bdd_var_with_id assumes that single variable BDDs have already been created for
151     * all the variables that we wish to access.  Thus, following, we explicitly create n
152     * variables.  We do not care about the return value of cmu_bdd_new_var_last; in the
153     * CMU package, the single variable BDDs are NEVER garbage collected.
154     */
155    for (i = 0; i < nvariables; i++) {
156        (void) cmu_bdd_new_var_last(mgr);
157    }
158
159    hooks = ALLOC(bdd_external_hooks, 1);
160    hooks->mdd = hooks->network = hooks->undef1 = (char *) 0;
161    mgr->hooks = (char *) hooks;  /* new field added to CMU manager */
162
163    return (bdd_manager *) mgr;
164}
165
166/*
167BDD Variable Allocation -------------------------------------------------------
168*/
169
170bdd_t *
171bdd_create_variable(bdd_manager *manager)
172{
173  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
174  return bdd_construct_bdd_t(mgr, cmu_bdd_new_var_last(mgr));
175}
176
177bdd_t *
178bdd_create_variable_after(bdd_manager *manager, bdd_variableId after_id)
179{
180  struct bdd_ *after_var;
181  bdd_t         *result;
182  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
183
184  after_var = cmu_bdd_var_with_id(mgr, (long)after_id + 1);
185 
186  result =  bdd_construct_bdd_t(mgr, cmu_bdd_new_var_after(mgr, after_var));
187 
188  /* No need to free after_var, since single variable BDDs are never garbage collected */
189 
190  return result;
191}
192
193
194
195bdd_t *
196bdd_get_variable(bdd_manager *manager, bdd_variableId variable_ID)
197{
198  struct bdd_ *fn;
199  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
200  fn = cmu_bdd_var_with_id(mgr, (long) (variable_ID + 1));
201
202  if (fn == (struct bdd_ *) 0) {
203    int i;
204    for (i=cmu_bdd_vars(mgr); i < variable_ID + 1; i++) {
205      fn = cmu_bdd_new_var_last(mgr);
206    }
207  }
208 
209  return bdd_construct_bdd_t(mgr, fn);
210}
211
212/*
213BDD Formula Management --------------------------------------------------------
214*/
215
216bdd_t *
217bdd_dup(bdd_t *f)
218{
219  return bdd_construct_bdd_t(f->mgr, cmu_bdd_identity(f->mgr, f->node));
220}
221
222void
223bdd_free(bdd_t *f)
224{
225  if (f == NIL(bdd_t)) {
226        fail("bdd_free: trying to free a NIL bdd_t");                   
227  }
228 
229  if (f->free == TRUE) {
230        fail("bdd_free: trying to free a freed bdd_t");                 
231  }     
232 
233  cmu_bdd_free(f->mgr, f->node);
234 
235  /*
236   * In case the user tries to free this bdd_t again, set the free field to TRUE,
237     * and NIL out the other fields.  Then free the bdd_t structure itself.
238     */
239  f->free = TRUE;
240  f->node = NIL(struct bdd_);
241  f->mgr = NIL(struct bdd_manager_);
242  FREE(f); 
243}
244
245/*
246  Operations on BDD Formulas ----------------------------------------------------
247  */
248
249bdd_t *
250bdd_and(
251  bdd_t *f,
252  bdd_t *g,
253  boolean f_phase,
254  boolean g_phase)
255{
256  struct bdd_ *temp1, *temp2;
257  bdd_t *result;
258  struct bdd_manager_ *mgr;
259 
260  mgr = f->mgr;
261  temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
262  temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
263  result = bdd_construct_bdd_t(mgr, cmu_bdd_and(mgr, temp1, temp2));
264  cmu_bdd_free(mgr, temp1);
265  cmu_bdd_free(mgr, temp2);
266  return result;
267}
268
269bdd_t *
270bdd_and_with_limit(
271  bdd_t *f,
272  bdd_t *g,
273  boolean f_phase,
274  boolean g_phase,
275  unsigned int limit)
276{
277  /* Unsupported: fall back on standard AND. */
278  return bdd_and(f, g, f_phase, g_phase);
279}
280
281bdd_t *
282bdd_and_array(
283  bdd_t *f,
284  array_t *g_array,
285  boolean f_phase,
286  boolean g_phase)
287{
288  struct bdd_ *temp1, *temp2, *result;
289  bdd_t *g;
290  struct bdd_manager_ *mgr;
291  int i;
292
293  mgr = f->mgr;
294  result = ((f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) :
295            cmu_bdd_not(mgr, f->node)); 
296
297  for (i = 0; i < array_n(g_array); i++) {
298    g = array_fetch(bdd_t *, g_array, i);
299    temp1 = result;
300    temp2 = ((g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) :
301             cmu_bdd_not(mgr, g->node));
302    result = cmu_bdd_and(mgr, temp1, temp2);
303    cmu_bdd_free(mgr, temp1);
304    cmu_bdd_free(mgr, temp2);
305    if (result == NULL)
306      return(NULL);
307  }
308
309  return(bdd_construct_bdd_t(mgr, result));
310}
311
312bdd_t *
313bdd_multiway_and(bdd_manager *manager, array_t *bddArray)
314{
315  int i;
316  bdd temp, result;
317  bdd_t *operand;
318  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
319  result = cmu_bdd_one(mgr);
320  for (i=0; i<array_n(bddArray); i++){
321    operand = array_fetch(bdd_t *, bddArray, i);
322    temp = cmu_bdd_and(mgr, result, operand->node);
323    cmu_bdd_free(mgr, result);
324    result = temp;
325  }
326  return bdd_construct_bdd_t(mgr, result);
327}
328
329bdd_t *
330bdd_multiway_or(bdd_manager *manager, array_t *bddArray)
331{
332  int i;
333  bdd temp, result;
334  bdd_t *operand;
335  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
336  result = cmu_bdd_zero(mgr);
337  for (i=0; i<array_n(bddArray); i++){
338    operand = array_fetch(bdd_t *, bddArray, i);
339    temp = cmu_bdd_or(mgr, result, operand->node);
340    cmu_bdd_free(mgr, result);
341    result = temp;
342  }
343  return bdd_construct_bdd_t(mgr, result);
344}
345
346bdd_t *
347bdd_multiway_xor(bdd_manager *manager, array_t *bddArray)
348{
349  int i;
350  bdd temp, result;
351  bdd_t *operand;
352  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
353  result = cmu_bdd_zero(mgr);
354  for (i=0; i<array_n(bddArray); i++){
355    operand = array_fetch(bdd_t *, bddArray, i);
356    temp = cmu_bdd_xor(mgr, result, operand->node);
357    cmu_bdd_free(mgr, result);
358    result = temp;
359  }
360  return bdd_construct_bdd_t(mgr, result);
361}
362
363array_t *
364bdd_pairwise_or(bdd_manager *manager, array_t *bddArray1, array_t
365                *bddArray2) 
366{
367  int i;
368  bdd_t *operand1, *operand2;
369  array_t *resultArray;
370  bdd result;
371  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
372  if (array_n(bddArray1) != array_n(bddArray2)){
373    fprintf(stderr, "bdd_pairwise_or: Arrays of different lengths.\n");
374    return NIL(array_t);
375  }
376  resultArray = array_alloc(bdd_t *, 0);
377  for (i=0; i<array_n(bddArray1); i++){
378    operand1 = array_fetch(bdd_t *, bddArray1, i);
379    operand2 = array_fetch(bdd_t *, bddArray2, i);
380    result = cmu_bdd_or(mgr, operand1->node, operand2->node);
381    array_insert_last(bdd_t*, resultArray,
382                      bdd_construct_bdd_t(mgr, result)); 
383  }
384  return resultArray;
385}
386
387array_t *
388bdd_pairwise_and(bdd_manager *manager, array_t *bddArray1, array_t
389                 *bddArray2) 
390{
391  int i;
392  bdd_t *operand1, *operand2;
393  array_t *resultArray;
394  bdd result;
395  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
396  if (array_n(bddArray1) != array_n(bddArray2)){
397    fprintf(stderr, "bdd_pairwise_and: Arrays of different lengths.\n");
398    return NIL(array_t);
399  }
400  resultArray = array_alloc(bdd_t *, 0);
401  for (i=0; i<array_n(bddArray1); i++){
402    operand1 = array_fetch(bdd_t *, bddArray1, i);
403    operand2 = array_fetch(bdd_t *, bddArray2, i);
404    result = cmu_bdd_and(mgr, operand1->node, operand2->node);
405    array_insert_last(bdd_t*, resultArray,
406                      bdd_construct_bdd_t(mgr, result)); 
407  }
408  return resultArray;
409}
410
411array_t *
412bdd_pairwise_xor(bdd_manager *manager, array_t *bddArray1, array_t
413                 *bddArray2) 
414{
415  int i;
416  bdd_t *operand1, *operand2;
417  array_t *resultArray;
418  bdd result;
419  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
420  if (array_n(bddArray1) != array_n(bddArray2)){
421    fprintf(stderr, "bdd_pairwise_xor: Arrays of different lengths.\n");
422    return NIL(array_t);
423  }
424  resultArray = array_alloc(bdd_t *, 0);
425  for (i=0; i<array_n(bddArray1); i++){
426    operand1 = array_fetch(bdd_t *, bddArray1, i);
427    operand2 = array_fetch(bdd_t *, bddArray2, i);
428    result = cmu_bdd_xor(mgr, operand1->node, operand2->node);
429    array_insert_last(bdd_t*, resultArray,
430                      bdd_construct_bdd_t(mgr, result)); 
431  }
432  return resultArray;
433}
434
435bdd_t *
436bdd_and_smooth(
437  bdd_t *f,
438  bdd_t *g,
439  array_t *smoothing_vars /* of bdd_t *'s */)
440{
441  int num_vars, i;
442  bdd_t *fn, *result;
443  struct bdd_ **assoc;
444  struct bdd_manager_ *mgr;
445 
446  num_vars = array_n(smoothing_vars);
447  if (num_vars <= 0) {
448        cmu_bdd_fatal("bdd_and_smooth: no smoothing variables");
449  }
450 
451  assoc = ALLOC(struct bdd_ *, num_vars+1);
452 
453  for (i = 0; i < num_vars; i++) {
454        fn = array_fetch(bdd_t *, smoothing_vars, i);
455        assoc[i] = fn->node;
456  }
457  assoc[num_vars] = (struct bdd_ *) 0;
458 
459  mgr = f->mgr;
460  cmu_bdd_temp_assoc(mgr, assoc, 0);
461  (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
462 
463  result = bdd_construct_bdd_t(mgr, cmu_bdd_rel_prod(mgr, f->node, g->node));
464  FREE(assoc);
465  return result;
466}
467
468bdd_t *
469bdd_and_smooth_with_limit(
470  bdd_t *f,
471  bdd_t *g,
472  array_t *smoothing_vars /* of bdd_t *'s */,
473  unsigned int limit)
474{
475  /* Unsupported: fall back to standard and_smooth */
476  return bdd_and_smooth(f, g, smoothing_vars);
477}
478
479bdd_t *
480bdd_between(bdd_t *f_min, bdd_t *f_max)
481{
482  bdd_t *temp, *ret;
483  long size1, size2, size3; 
484  temp = bdd_or(f_min, f_max, 1, 0);
485  ret = bdd_minimize(f_min, temp);
486  bdd_free(temp);
487  size1 = bdd_size(f_min);
488  size2 = bdd_size(f_max);
489  size3 = bdd_size(ret);
490  if (size3 < size1) {
491        if (size3 < size2){
492      return ret;
493    }
494    else {
495      bdd_free(ret);
496      return bdd_dup(f_max);
497    }
498  }
499  else {
500    bdd_free(ret);
501    if (size1 < size2){
502      return bdd_dup(f_min);
503    }
504    else {
505      return bdd_dup(f_max);
506    }
507  }
508}
509
510bdd_t *
511bdd_cofactor(bdd_t *f, bdd_t *g)
512{
513  return bdd_construct_bdd_t(f->mgr, cmu_bdd_cofactor(f->mgr, f->node, g->node));
514}
515
516bdd_t *
517bdd_cofactor_array(bdd_t *f, array_t *bddArray)
518{
519  bdd_t *operand;
520  struct bdd_ *result, *temp;
521  int i;
522
523  result = cmu_bdd_identity(f->mgr, f->node);
524
525  for (i = 0; i < array_n(bddArray); i++) {
526    operand = array_fetch(bdd_t *, bddArray, i);
527    temp = cmu_bdd_cofactor(f->mgr, result, operand->node);
528    if (temp == NULL) {
529      cmu_bdd_free(f->mgr, result);
530      return(NULL);
531    }
532    cmu_bdd_free(f->mgr, result);
533    result = temp;
534  }
535
536  return(bdd_construct_bdd_t(f->mgr, result));
537}
538
539bdd_t *
540bdd_compose(
541  bdd_t *f,
542  bdd_t *v,
543  bdd_t *g)
544{
545  return bdd_construct_bdd_t(f->mgr, cmu_bdd_compose(f->mgr, f->node, v->node, g->node));
546}
547
548bdd_t *
549bdd_consensus(
550  bdd_t *f,
551  array_t *quantifying_vars /* of bdd_t *'s */)
552{
553  int num_vars, i;
554  bdd_t *fn, *result;
555  struct bdd_ **assoc;
556  struct bdd_manager_ *mgr;
557 
558  num_vars = array_n(quantifying_vars);
559  if (num_vars <= 0) {
560        cmu_bdd_fatal("bdd_consensus: no quantifying variables");
561  }
562 
563  assoc = ALLOC(struct bdd_ *, num_vars+1);
564 
565  for (i = 0; i < num_vars; i++) {
566        fn = array_fetch(bdd_t *, quantifying_vars, i);
567        assoc[i] = fn->node;
568  }
569  assoc[num_vars] = (struct bdd_ *) 0;
570 
571  mgr = f->mgr;
572  cmu_bdd_temp_assoc(mgr, assoc, 0);
573  (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
574 
575  result = bdd_construct_bdd_t(mgr, cmu_bdd_forall(mgr, f->node));
576  FREE(assoc);
577  return result;
578}
579
580
581bdd_t *
582bdd_cproject(
583  bdd_t *f,
584  array_t *quantifying_vars /* of bdd_t* */)
585{
586  int num_vars, i;
587  bdd_t *fn, *result;
588  struct bdd_ **assoc;
589  struct bdd_manager_ *mgr;
590 
591  if (f == NIL(bdd_t)) fail ("bdd_cproject: invalid BDD");
592 
593  num_vars = array_n(quantifying_vars);
594  if (num_vars <= 0) {
595    printf("Warning: bdd_cproject: no projection variables\n");
596    result = bdd_dup(f);
597  }
598  else {
599    assoc = ALLOC(struct bdd_ *, num_vars+1);
600    for (i = 0; i < num_vars; i++) {
601      fn = array_fetch(bdd_t *, quantifying_vars, i);
602      assoc[i] = fn->node;
603    }
604    assoc[num_vars] = (struct bdd_ *) 0;
605    mgr = f->mgr;
606    cmu_bdd_temp_assoc(mgr, assoc, 0);
607    (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current a
608                                       ssociation */
609   
610    result = bdd_construct_bdd_t(mgr, cmu_bdd_project(mgr, f->node));
611    FREE(assoc);
612  }
613  return result;
614}
615
616
617bdd_t *
618bdd_else(bdd_t *f)
619{
620  return bdd_construct_bdd_t(f->mgr, cmu_bdd_else(f->mgr, f->node));
621}
622
623
624bdd_t *
625bdd_ite(
626  bdd_t *i,
627  bdd_t *t,
628  bdd_t *e,
629  boolean i_phase,
630  boolean t_phase,
631  boolean e_phase)
632{
633  struct bdd_ *temp1, *temp2, *temp3;
634  bdd_t *result;
635  struct bdd_manager_ *mgr;
636 
637  mgr = i->mgr;
638  temp1 = ( (i_phase == TRUE) ? cmu_bdd_identity(mgr, i->node) : cmu_bdd_not(mgr, i->node));
639  temp2 = ( (t_phase == TRUE) ? cmu_bdd_identity(mgr, t->node) : cmu_bdd_not(mgr, t->node));
640  temp3 = ( (e_phase == TRUE) ? cmu_bdd_identity(mgr, e->node) : cmu_bdd_not(mgr, e->node));
641  result = bdd_construct_bdd_t(mgr, cmu_bdd_ite(mgr, temp1, temp2, temp3));
642  cmu_bdd_free(mgr, temp1);
643  cmu_bdd_free(mgr, temp2);
644  cmu_bdd_free(mgr, temp3);
645  return result;
646}
647
648bdd_t *
649bdd_minimize(bdd_t *f, bdd_t *c)
650{
651  bdd_t *result = bdd_construct_bdd_t(f->mgr, cmu_bdd_reduce(f->mgr,
652                                                             f->node,
653                                                             c->node)); 
654  if (bdd_size(result) < bdd_size(f)){
655    return result;
656  }
657  else{
658    bdd_free(result);
659    return bdd_dup(f);
660  }
661}
662
663bdd_t *
664bdd_minimize_array(bdd_t *f, array_t *bddArray)
665{
666  bdd_t *operand;
667  struct bdd_ *result, *temp;
668  bdd_t *final;
669  int i;
670
671  result = cmu_bdd_identity(f->mgr, f->node);
672  for (i = 0; i < array_n(bddArray); i++) {
673    operand = array_fetch(bdd_t *, bddArray, i);
674    temp = cmu_bdd_reduce(f->mgr, result, operand->node);
675    if (temp == NULL) {
676      cmu_bdd_free(f->mgr, result);
677      return(NULL);
678    }
679    cmu_bdd_free(f->mgr, result);
680    result = temp;
681  }
682
683  final = bdd_construct_bdd_t(f->mgr, result);
684
685  if (bdd_size(final) < bdd_size(f)){
686    return final;
687  }
688  else{
689    bdd_free(final);
690    return bdd_dup(f);
691  }
692}
693
694
695bdd_t *
696bdd_not(bdd_t *f)
697{
698  return bdd_construct_bdd_t(f->mgr, cmu_bdd_not(f->mgr, f->node));
699}
700
701bdd_t *
702bdd_one(bdd_manager *manager)
703{
704  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
705  return bdd_construct_bdd_t(mgr, cmu_bdd_one(mgr));
706}
707
708bdd_t *
709bdd_or(
710  bdd_t *f,
711  bdd_t *g,
712  boolean f_phase,
713  boolean g_phase)
714{
715  struct bdd_ *temp1, *temp2;
716  bdd_t *result;
717  struct bdd_manager_ *mgr;
718 
719  mgr = f->mgr;
720  temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
721  temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
722  result = bdd_construct_bdd_t(mgr, cmu_bdd_or(mgr, temp1, temp2));
723  cmu_bdd_free(mgr, temp1);
724  cmu_bdd_free(mgr, temp2);
725  return result;
726}
727
728bdd_t *
729bdd_smooth(
730  bdd_t *f,
731  array_t *smoothing_vars /* of bdd_t *'s */)
732{
733  int num_vars, i;
734  bdd_t *fn, *result;
735  struct bdd_ **assoc;
736  struct bdd_manager_ *mgr;
737 
738  num_vars = array_n(smoothing_vars);
739  if (num_vars <= 0) {
740        cmu_bdd_fatal("bdd_smooth: no smoothing variables");
741  }
742 
743  assoc = ALLOC(struct bdd_ *, num_vars+1);
744 
745  for (i = 0; i < num_vars; i++) {
746        fn = array_fetch(bdd_t *, smoothing_vars, i);
747        assoc[i] = fn->node;
748  }
749  assoc[num_vars] = (struct bdd_ *) 0;
750 
751  mgr = f->mgr;
752  cmu_bdd_temp_assoc(mgr, assoc, 0);
753  (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
754 
755  result = bdd_construct_bdd_t(mgr, cmu_bdd_exists(mgr, f->node));
756  FREE(assoc);
757  return result;
758}
759
760bdd_t *
761bdd_substitute(
762  bdd_t *f,
763  array_t *old_array /* of bdd_t *'s */,
764  array_t *new_array /* of bdd_t *'s */)
765{
766    int num_old_vars, num_new_vars, i;
767    bdd_t *fn_old, *fn_new, *result;
768    struct bdd_ **assoc;
769    struct bdd_manager_ *mgr;
770
771    num_old_vars = array_n(old_array);
772    num_new_vars = array_n(new_array);
773    if (num_old_vars != num_new_vars) {
774        cmu_bdd_fatal("bdd_substitute: mismatch of number of new and old variables");
775    }
776
777    assoc = ALLOC(struct bdd_ *, 2*(num_old_vars+1));
778
779    for (i = 0; i < num_old_vars; i++) {
780        fn_old = array_fetch(bdd_t *, old_array, i);
781        fn_new = array_fetch(bdd_t *, new_array, i);
782        assoc[2*i]   = fn_old->node;
783        assoc[2*i+1] = fn_new->node;
784    }
785    assoc[2*num_old_vars]   = (struct bdd_ *) 0;
786    assoc[2*num_old_vars+1] = (struct bdd_ *) 0;  /* not sure if we need this second 0 */
787
788    mgr = f->mgr;
789    cmu_bdd_temp_assoc(mgr, assoc, 1);
790    (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
791
792    result = bdd_construct_bdd_t(mgr, cmu_bdd_substitute(mgr, f->node));
793    FREE(assoc);
794    return result;
795}
796
797array_t *
798bdd_substitute_array(
799  array_t *f_array,
800  array_t *old_array /* of bdd_t *'s */,
801  array_t *new_array /* of bdd_t *'s */)
802{
803  int   i;
804  bdd_t *f, *new_;
805  array_t *substitute_array = array_alloc(bdd_t *, 0);
806
807  arrayForEachItem(bdd_t *, f_array, i, f) {
808    new_ = bdd_substitute(f, old_array, new_array);
809    array_insert_last(bdd_t *, substitute_array, new_);
810  }
811  return(substitute_array);
812}
813
814void *
815bdd_pointer(bdd_t *f)
816{
817    return((void *)f->node);
818}
819
820bdd_t *
821bdd_then(bdd_t *f)
822{
823    return bdd_construct_bdd_t(f->mgr, cmu_bdd_then(f->mgr, f->node));
824}
825
826bdd_t *
827bdd_top_var(bdd_t *f)
828{
829    return bdd_construct_bdd_t(f->mgr, cmu_bdd_if(f->mgr, f->node));
830}
831
832bdd_t *
833bdd_xnor(bdd_t *f, bdd_t *g)
834{
835    return bdd_construct_bdd_t(f->mgr, cmu_bdd_xnor(f->mgr, f->node, g->node));
836}
837
838bdd_t *
839bdd_xor(bdd_t *f, bdd_t *g)
840{
841    return bdd_construct_bdd_t(f->mgr, cmu_bdd_xor(f->mgr, f->node, g->node));
842}
843
844bdd_t *
845bdd_zero(bdd_manager *manager)
846{
847  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
848  return bdd_construct_bdd_t(mgr, cmu_bdd_zero(mgr));
849}
850
851/*
852Queries about BDD Formulas ----------------------------------------------------
853*/
854
855boolean
856bdd_equal(bdd_t *f, bdd_t *g)
857{
858    return (f->node == g->node);
859}
860
861boolean
862bdd_equal_mod_care_set(bdd_t *f, bdd_t *g, bdd_t *CareSet)
863{
864  bdd_t *diffBdd;
865  boolean result;
866
867  if (bdd_equal(f, g))
868    return 1;
869
870  diffBdd = bdd_xor(f, g);
871
872  result = bdd_leq(diffBdd, CareSet, 1, 0);
873  bdd_free(diffBdd);
874
875  return(result);
876}
877
878bdd_t *
879bdd_intersects(bdd_t *f, bdd_t *g)
880{
881    return bdd_construct_bdd_t(f->mgr, cmu_bdd_intersects(f->mgr, f->node, g->node));
882}
883
884bdd_t *
885bdd_closest_cube(bdd_t *f, bdd_t *g, int *dist)
886{
887    return (NULL);
888}
889
890boolean
891bdd_is_tautology(bdd_t *f, boolean phase)
892{
893    return ((phase == TRUE) ? (f->node == cmu_bdd_one(f->mgr)) : (f->node == cmu_bdd_zero(f->mgr)));
894}
895
896boolean
897bdd_leq(
898  bdd_t *f,
899  bdd_t *g,
900  boolean f_phase,
901  boolean g_phase)
902{
903    struct bdd_ *temp1, *temp2, *implies_fn;
904    struct bdd_manager_ *mgr;
905    boolean result_value;
906
907    mgr = f->mgr;
908    temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
909    temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
910    implies_fn = cmu_bdd_implies(mgr, temp1, temp2); /* returns a minterm of temp1*!temp2 */
911    result_value = (implies_fn == cmu_bdd_zero(mgr));
912    cmu_bdd_free(mgr, temp1);
913    cmu_bdd_free(mgr, temp2);
914    cmu_bdd_free(mgr, implies_fn);
915    return result_value;
916}
917
918boolean
919bdd_lequal_mod_care_set(
920  bdd_t *f,
921  bdd_t *g,
922  boolean f_phase,
923  boolean g_phase,
924  bdd_t *careSet)
925{
926  bdd_t *temp;
927  boolean result;
928
929  if (bdd_leq(f, g, f_phase, g_phase))
930    return 1;
931
932  temp = bdd_and(f, careSet, f_phase, 1);
933
934  result = bdd_leq(temp, g, 1, g_phase);
935  bdd_free(temp);
936
937  return(result);
938}
939
940boolean
941bdd_leq_array(
942  bdd_t *f,
943  array_t *g_array,
944  boolean f_phase,
945  boolean g_phase)
946{
947  int   i;
948  bdd_t *g;
949  boolean result;
950
951  arrayForEachItem(bdd_t *, g_array, i, g) {
952    result = bdd_leq(f, g, f_phase, g_phase);
953    if (g_phase) {
954      if (!result)
955        return(0);
956    } else {
957      if (result)
958        return(1);
959    }
960  }
961  if (g_phase)
962    return(1);
963  else
964    return(0);
965}
966
967/*
968Statistics and Other Queries --------------------------------------------------
969*/
970
971double 
972bdd_count_onset(
973  bdd_t *f,
974  array_t *var_array /* of bdd_t *'s */)
975{
976    int num_vars;
977    double fraction;
978
979    num_vars = array_n(var_array);
980    fraction = cmu_bdd_satisfying_fraction(f->mgr, f->node); /* cannot give support vars */
981    return (fraction * pow((double) 2, (double) num_vars));
982}
983
984/**Function********************************************************************
985
986  Synopsis    [Counts the number of minterms in the on set.]
987
988  SideEffects []
989
990******************************************************************************/
991int
992bdd_epd_count_onset(
993  bdd_t *f,
994  array_t *var_array /* of bdd_t *'s */,
995  EpDouble *epd)
996{
997  double nMinterms;
998
999  nMinterms = bdd_count_onset(f, var_array);
1000  EpdConvert(nMinterms, epd);
1001  return 0;
1002} /* end of bdd_epd_count_onset */
1003
1004int
1005bdd_get_free(bdd_t *f)
1006{
1007    return (f->free);
1008}
1009
1010bdd_manager *
1011bdd_get_manager(bdd_t *f)
1012{
1013    return (bdd_manager *) (f->mgr);
1014}
1015
1016bdd_node *
1017bdd_get_node(
1018  bdd_t *f,
1019  boolean *is_complemented /* return */)
1020{
1021    *is_complemented = (boolean) TAG0(f->node);  /* using bddint.h */
1022    return ((bdd_node *) BDD_POINTER(f->node));  /* using bddint.h */
1023}
1024
1025var_set_t *
1026bdd_get_support(bdd_t *f)
1027{
1028    struct bdd_ **support, *var;
1029    struct bdd_manager_ *mgr;
1030    long num_vars;
1031    var_set_t *result;
1032    int id, i;
1033
1034    mgr = f->mgr;
1035    num_vars = cmu_bdd_vars(mgr);
1036
1037    result = var_set_new((int) num_vars);
1038    support = (struct bdd_ **) mem_get_block((num_vars+1) * sizeof(struct bdd_ *));
1039    (void) cmu_bdd_support(mgr, f->node, support);
1040
1041    for (i = 0; i < num_vars; ++i) {  /* can never have more than num_var non-zero entries in array */
1042        var = support[i]; 
1043        if (var == (struct bdd_ *) 0) {
1044            break;  /* have reach end of null-terminated array */
1045        }
1046        id = (int) (cmu_bdd_if_id(mgr, var) - 1);  /* a variable is never garbage collected, so no need to free */
1047        var_set_set_elt(result, id);
1048    }
1049
1050    mem_free_block((pointer)support);
1051
1052    return result;
1053}
1054
1055int
1056bdd_is_support_var(bdd_t *f, bdd_t *var)
1057{
1058    return(bdd_is_support_var_id(f, bdd_top_var_id(var)));
1059}
1060
1061int
1062bdd_is_support_var_id(bdd_t *f, int index)
1063{
1064    struct bdd_ **support, *var;
1065    struct bdd_manager_ *mgr;
1066    long num_vars;
1067    int id, i;
1068
1069    mgr = f->mgr;
1070    num_vars = cmu_bdd_vars(mgr);
1071
1072    support = (struct bdd_ **) mem_get_block((num_vars+1) * sizeof(struct bdd_ *));
1073    (void) cmu_bdd_support(mgr, f->node, support);
1074
1075    for (i = 0; i < num_vars; ++i) {  /* can never have more than num_var non-zero entries in array */
1076        var = support[i]; 
1077        if (var == (struct bdd_ *) 0) {
1078            break;  /* have reach end of null-terminated array */
1079        }
1080        id = (int) (cmu_bdd_if_id(mgr, var) - 1);  /* a variable is never garbage collected, so no need to free */
1081        if (id == index) {
1082            mem_free_block((pointer)support);
1083            return 1;
1084        }
1085    }
1086
1087    mem_free_block((pointer)support);
1088
1089    return 0;
1090}
1091
1092array_t *
1093bdd_get_varids(array_t *var_array)
1094{
1095  int i;
1096  bdd_t *var;
1097  array_t *result;
1098 
1099  result = array_alloc(bdd_variableId, 0);
1100  for (i = 0; i < array_n(var_array); i++) {
1101    var = array_fetch(bdd_t *, var_array, i);
1102    array_insert_last(bdd_variableId, result, bdd_top_var_id(var));
1103  }
1104  return result;
1105}
1106
1107unsigned int 
1108bdd_num_vars(bdd_manager *manager)
1109{
1110  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
1111  return (cmu_bdd_vars(mgr));
1112}
1113
1114void
1115bdd_print(bdd_t *f)
1116{
1117    cmu_bdd_print_bdd(f->mgr, f->node, bdd_naming_fn_none, bdd_terminal_id_fn_none, (pointer) 0, stdout);
1118}
1119
1120void
1121bdd_print_stats(bdd_manager *manager, FILE *file)
1122{
1123  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
1124  cmu_bdd_stats(mgr, file);
1125}
1126
1127/**Function********************************************************************
1128
1129  Synopsis [Sets the internal parameters of the package to the given values.]
1130
1131  SideEffects []
1132
1133******************************************************************************/
1134int
1135bdd_set_parameters(
1136  bdd_manager *mgr,
1137  avl_tree *valueTable,
1138  FILE *file)
1139{
1140  (void) fprintf(file, "Functionality not supported yet in the CMU package\n");
1141  return 1;
1142} /* End of bdd_set_parameters */
1143
1144int
1145bdd_size(bdd_t *f)
1146{
1147    return ((int) cmu_bdd_size(f->mgr, f->node, 1));
1148}
1149
1150int
1151bdd_node_size(bdd_node *f)
1152{
1153  return(0);
1154}
1155
1156long
1157bdd_size_multiple(array_t *bdd_array)
1158{
1159    long result;
1160    struct bdd_ **vector_bdd;
1161    bdd_t *f;
1162    int i;
1163    struct bdd_manager_ *mgr;
1164
1165    if ((bdd_array == NIL(array_t)) || (array_n(bdd_array) == 0))
1166        return 0;
1167
1168    f = array_fetch(bdd_t*, bdd_array, 0);
1169    mgr = f->mgr;
1170
1171    vector_bdd = (struct bdd_ **)
1172                        malloc((array_n(bdd_array)+1)*sizeof(struct bdd_ *));
1173
1174    for(i=0; i<array_n(bdd_array);i++){
1175        f = array_fetch(bdd_t*, bdd_array, i);
1176        vector_bdd[i] = f->node;
1177    }
1178    vector_bdd[array_n(bdd_array)] = 0;
1179    result =  cmu_bdd_size_multiple(mgr, vector_bdd,1);
1180    FREE(vector_bdd);
1181    return result;
1182}
1183
1184bdd_variableId
1185bdd_top_var_id(bdd_t *f)
1186{
1187    return ((bdd_variableId) (cmu_bdd_if_id(f->mgr, f->node) - 1));
1188}
1189
1190/*
1191Miscellaneous -----------------------------------------------------------------
1192*/
1193
1194bdd_external_hooks *
1195bdd_get_external_hooks(bdd_manager *manager)
1196{
1197  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
1198  return ((bdd_external_hooks *) mgr->hooks);
1199}
1200
1201
1202void
1203bdd_set_gc_mode(bdd_manager *manager, boolean no_gc)
1204{
1205  cmu_bdd_warning("bdd_set_gc_mode: translated to no-op in CMU package");
1206}
1207
1208void 
1209bdd_dynamic_reordering(bdd_manager *manager, bdd_reorder_type_t
1210                       algorithm_type, bdd_reorder_verbosity_t verbosity) 
1211{
1212  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
1213    switch(algorithm_type) {
1214    case BDD_REORDER_SIFT:
1215        cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_sift);
1216        break;
1217    case BDD_REORDER_WINDOW:
1218        cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_stable_window3);
1219        break;
1220    case BDD_REORDER_NONE:
1221        cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_none);
1222        break;
1223    default:
1224      fprintf(stderr,"CMU: bdd_dynamic_reordering: unknown algorithm type\n");
1225      fprintf(stderr,"Using SIFT method instead\n");
1226      cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_sift);
1227    }
1228}
1229
1230void 
1231bdd_dynamic_reordering_zdd(bdd_manager *manager, bdd_reorder_type_t
1232                       algorithm_type, bdd_reorder_verbosity_t verbosity) 
1233{
1234    return;
1235}
1236
1237void 
1238bdd_reorder(bdd_manager *manager)
1239{
1240  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
1241  cmu_bdd_reorder(mgr);
1242}
1243
1244bdd_variableId
1245bdd_get_id_from_level(bdd_manager *manager, long level)
1246{
1247  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
1248  struct bdd_ *fn;
1249
1250  fn = cmu_bdd_var_with_index(mgr, level);
1251 
1252  if (fn == (struct bdd_ *) 0) {
1253    /* variable should always be found, since they are created at bdd_start */
1254    cmu_bdd_fatal("bdd_get_id_from_level: assumption violated");
1255  }
1256 
1257  return ((bdd_variableId)(cmu_bdd_if_id(mgr, fn) - 1 ));
1258 
1259}
1260
1261long
1262bdd_top_var_level(bdd_manager *manager, bdd_t *fn)
1263{
1264  cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
1265  return cmu_bdd_if_index(mgr, fn->node);
1266}
1267
1268/*
1269 * Return TRUE if f is a cube, else return FALSE.
1270 */
1271boolean
1272bdd_is_cube(bdd_t *f)
1273{
1274  struct bdd_manager_ *manager;
1275
1276  if (f == NIL(bdd_t)) {
1277        fail("bdd_is_cube: invalid BDD");
1278  }
1279  if(  f->free ) fail ("Freed Bdd passed to bdd_is_cube");
1280  manager = f->mgr;
1281  return ((boolean)cmu_bdd_is_cube(manager, f->node));
1282}
1283
1284bdd_block *
1285bdd_new_var_block(bdd_t *f, long length)
1286{
1287  struct bdd_manager_ *manager;
1288  if (f == NIL(bdd_t)) {
1289        fail("bdd_new_var_block: invalid BDD");
1290  }
1291  manager = f->mgr;
1292  return (bdd_block *)cmu_bdd_new_var_block(manager, f->node, length);
1293}
1294
1295bdd_t *
1296bdd_var_with_index(bdd_manager *manager, int index)
1297{
1298  return bdd_construct_bdd_t(manager, 
1299                            cmu_bdd_var_with_index((cmu_bdd_manager) manager,
1300                                                   index));
1301}
1302
1303bdd_t *
1304bdd_compact(bdd_t *f, bdd_t *g)
1305{
1306    return (NULL);
1307}
1308
1309
1310bdd_t *
1311bdd_squeeze(bdd_t *f, bdd_t *g)
1312{
1313    return (NULL);
1314}
1315
1316double
1317bdd_correlation(bdd_t *f, bdd_t *g)
1318{
1319    return (0.0);
1320}
1321
1322/**Function********************************************************************
1323
1324  Synopsis    [Dummy functions defined in bdd.h]
1325
1326  SideEffects []
1327
1328******************************************************************************/
1329int
1330bdd_reordering_status(
1331  bdd_manager *mgr,
1332  bdd_reorder_type_t *method)
1333{
1334  return 0;
1335}
1336
1337/**Function********************************************************************
1338
1339  Synopsis    [Dummy functions defined in bdd.h]
1340
1341  SideEffects []
1342
1343******************************************************************************/
1344
1345bdd_t *
1346bdd_compute_cube(
1347  bdd_manager *mgr,
1348  array_t *vars)
1349{
1350  return NIL(bdd_t);
1351}
1352
1353bdd_t *
1354bdd_compute_cube_with_phase(
1355  bdd_manager *mgr,
1356  array_t *vars,
1357  array_t *phase)
1358{
1359  return NIL(bdd_t);
1360}
1361
1362bdd_t *
1363bdd_clipping_and_smooth(
1364  bdd_t *f,
1365  bdd_t *g,
1366  array_t *smoothing_vars /* of bdd_t *'s */,
1367  int maxDepth,
1368  int over)
1369{
1370  return NIL(bdd_t);
1371}
1372
1373bdd_t *
1374bdd_approx_hb(
1375  bdd_t *f,
1376  bdd_approx_dir_t approxDir,
1377  int numVars,
1378  int threshold)
1379{
1380  return NIL(bdd_t);
1381}
1382
1383bdd_t *
1384bdd_approx_sp(
1385  bdd_t *f,
1386  bdd_approx_dir_t approxDir,
1387  int numVars,
1388  int threshold,
1389  int hardlimit)
1390{
1391  return NIL(bdd_t);
1392}
1393
1394bdd_t *
1395bdd_approx_ua(
1396  bdd_t *f,
1397  bdd_approx_dir_t approxDir,
1398  int numVars,
1399  int threshold,
1400  int safe,
1401  double quality)
1402{
1403  return NIL(bdd_t);
1404}
1405
1406bdd_t *
1407bdd_approx_remap_ua(
1408  bdd_t *f,
1409  bdd_approx_dir_t approxDir,
1410  int numVars,
1411  int threshold,
1412  double quality)
1413{
1414  return NIL(bdd_t);
1415}
1416
1417bdd_t *
1418bdd_approx_biased_rua(
1419  bdd_t *f,
1420  bdd_approx_dir_t approxDir,
1421  bdd_t *bias,
1422  int numVars,
1423  int threshold,
1424  double quality,
1425  double quality1)
1426{
1427  return NIL(bdd_t);
1428}
1429
1430bdd_t *
1431bdd_approx_compress(
1432  bdd_t *f,
1433  bdd_approx_dir_t approxDir,
1434  int numVars,
1435  int threshold)
1436{
1437  return NIL(bdd_t);
1438}
1439
1440int
1441bdd_gen_decomp(
1442  bdd_t *f,
1443  bdd_partition_type_t partType,
1444  bdd_t ***conjArray)
1445{
1446  return 0;
1447}
1448
1449int
1450bdd_var_decomp(
1451  bdd_t *f,
1452  bdd_partition_type_t partType,
1453  bdd_t ***conjArray)
1454{
1455  return 0;
1456}
1457
1458int 
1459bdd_approx_decomp(
1460  bdd_t *f,
1461  bdd_partition_type_t partType,
1462  bdd_t ***conjArray)
1463{
1464  return 0;
1465}
1466
1467int
1468bdd_iter_decomp(
1469  bdd_t *f,
1470  bdd_partition_type_t partType,
1471  bdd_t  ***conjArray)
1472{
1473  return 0;
1474}
1475
1476bdd_t *
1477bdd_solve_eqn(
1478  bdd_t *f,
1479  array_t *g,
1480  array_t *unknowns)
1481{
1482  return NIL(bdd_t);
1483}
1484
1485int
1486bdd_add_hook(
1487  bdd_manager *mgr,
1488  int (*procedure)(bdd_manager *, char *, void *),
1489  bdd_hook_type_t whichHook)
1490{
1491  return 0;
1492}
1493
1494int
1495bdd_remove_hook(
1496  bdd_manager *mgr,
1497  int (*procedure)(bdd_manager *, char *, void *),
1498  bdd_hook_type_t whichHook)
1499{
1500  return 0;
1501}
1502
1503int
1504bdd_enable_reordering_reporting(bdd_manager *mgr)
1505{
1506  return 0;
1507}
1508
1509int
1510bdd_disable_reordering_reporting(bdd_manager *mgr)
1511{
1512  return 0;
1513}
1514
1515bdd_reorder_verbosity_t
1516bdd_reordering_reporting(bdd_manager *mgr)
1517{
1518  return BDD_REORDER_VERBOSITY_DEFAULT;
1519}
1520
1521int 
1522bdd_print_apa_minterm(
1523  FILE *fp,
1524  bdd_t *f,
1525  int nvars,
1526  int precision)
1527{
1528  return 0;
1529}
1530
1531int 
1532bdd_apa_compare_ratios(
1533  int nvars,
1534  bdd_t *f1,
1535  bdd_t *f2,
1536  int f1Num,
1537  int f2Num)
1538{
1539  return 0;
1540}
1541
1542int
1543bdd_read_node_count(bdd_manager *mgr)
1544{
1545  return 0;
1546}
1547
1548
1549int
1550bdd_reordering_zdd_status(
1551  bdd_manager *mgr,
1552  bdd_reorder_type_t *method)
1553{
1554  return 0;
1555}
1556
1557
1558bdd_node *
1559bdd_bdd_to_add(
1560  bdd_manager *mgr,
1561  bdd_node *fn)
1562{
1563  return NIL(bdd_node);
1564}
1565
1566bdd_node *
1567bdd_add_permute(
1568  bdd_manager *mgr,
1569  bdd_node *fn,
1570  int *permut)
1571{
1572  return NIL(bdd_node);
1573}
1574
1575bdd_node *
1576bdd_bdd_permute(
1577  bdd_manager *mgr,
1578  bdd_node *fn,
1579  int *permut)
1580{
1581  return NIL(bdd_node);
1582}
1583
1584void
1585bdd_ref(bdd_node *fn)
1586{
1587  return ;
1588}
1589
1590
1591void
1592bdd_recursive_deref(bdd_manager *mgr, bdd_node *f)
1593{
1594  return;
1595}
1596
1597
1598bdd_node *
1599bdd_add_exist_abstract(
1600  bdd_manager *mgr,
1601  bdd_node *fn,
1602  bdd_node *vars)
1603{
1604  return NIL(bdd_node);
1605}
1606
1607
1608bdd_node *
1609bdd_add_apply(
1610  bdd_manager *mgr,
1611  bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **),
1612  bdd_node *fn1,
1613  bdd_node *fn2)
1614{
1615  return NIL(bdd_node);
1616}
1617
1618
1619bdd_node *
1620bdd_add_nonsim_compose(
1621  bdd_manager *mgr,
1622  bdd_node *fn,
1623  bdd_node **vector)
1624{
1625  return NIL(bdd_node);
1626}
1627
1628
1629bdd_node *
1630bdd_add_residue(
1631  bdd_manager *mgr,
1632  int n,
1633  int m,
1634  int options,
1635  int top)
1636{
1637  return NIL(bdd_node);
1638}
1639
1640
1641bdd_node *
1642bdd_add_vector_compose(
1643  bdd_manager *mgr,
1644  bdd_node *fn,
1645  bdd_node **vector)
1646{
1647  return NIL(bdd_node);
1648}
1649
1650
1651bdd_node *
1652bdd_add_times(
1653  bdd_manager *mgr,
1654  bdd_node **fn1,
1655  bdd_node **fn2)
1656{
1657  return NIL(bdd_node);
1658}
1659 
1660
1661int
1662bdd_check_zero_ref(bdd_manager *mgr)
1663{
1664  return 0;
1665}
1666
1667
1668void
1669bdd_dynamic_reordering_disable(bdd_manager *mgr)
1670{
1671  return;
1672}
1673
1674void
1675bdd_dynamic_reordering_zdd_disable(bdd_manager *mgr)
1676{
1677  return;
1678}
1679
1680
1681bdd_node *
1682bdd_add_xnor(
1683  bdd_manager *mgr,
1684  bdd_node **fn1,
1685  bdd_node **fn2)
1686{
1687  return NIL(bdd_node);
1688}
1689
1690
1691int
1692bdd_shuffle_heap(
1693  bdd_manager *mgr,
1694  int *permut)
1695{
1696  return 0;
1697}
1698
1699
1700bdd_node *
1701bdd_add_compose(
1702  bdd_manager *mgr,
1703  bdd_node *fn1,
1704  bdd_node *fn2,
1705  int var)
1706{
1707  return NIL(bdd_node);
1708}
1709
1710
1711bdd_node *
1712bdd_add_ith_var(
1713  bdd_manager *mgr,
1714  int i)
1715{
1716  return NIL(bdd_node);
1717}
1718
1719
1720int
1721bdd_get_level_from_id(
1722  bdd_manager *mgr,
1723  int id)
1724{
1725  return 0;
1726}
1727
1728
1729bdd_node *
1730bdd_bdd_exist_abstract(
1731  bdd_manager *mgr,
1732  bdd_node *fn,
1733  bdd_node *cube)
1734{
1735  return NIL(bdd_node);
1736}
1737
1738
1739int
1740bdd_equal_sup_norm(
1741  bdd_manager *mgr,
1742  bdd_node *fn,
1743  bdd_node *gn,
1744  BDD_VALUE_TYPE tolerance,
1745  int pr)
1746{
1747  return 0;
1748}
1749
1750
1751bdd_node *
1752bdd_read_logic_zero(bdd_manager *mgr)
1753{
1754    return NIL(bdd_node);
1755}
1756
1757
1758bdd_node *
1759bdd_bdd_ith_var(bdd_manager *mgr, int i)
1760{
1761    return NIL(bdd_node);
1762}
1763
1764
1765bdd_node *
1766bdd_add_divide(
1767  bdd_manager *mgr,
1768  bdd_node **fn1,
1769  bdd_node **fn2)
1770{
1771  return NIL(bdd_node);
1772}
1773
1774
1775bdd_node *
1776bdd_bdd_constrain(
1777  bdd_manager *mgr,
1778  bdd_node *f,
1779  bdd_node *c)
1780{
1781    return NIL(bdd_node);
1782}
1783
1784bdd_node *
1785bdd_bdd_restrict(
1786  bdd_manager *mgr,
1787  bdd_node *f,
1788  bdd_node *c)
1789{
1790    return NIL(bdd_node);
1791}
1792
1793
1794bdd_node *
1795bdd_add_hamming(
1796  bdd_manager *mgr,
1797  bdd_node **xVars,
1798  bdd_node **yVars,
1799  int nVars)
1800{
1801    return NIL(bdd_node);
1802}
1803
1804
1805bdd_node *
1806bdd_add_ite(
1807  bdd_manager *mgr,
1808  bdd_node *f,
1809  bdd_node *g,
1810  bdd_node *h)
1811{
1812    return NIL(bdd_node);
1813}
1814
1815
1816bdd_node *
1817bdd_add_find_max(
1818  bdd_manager *mgr,
1819  bdd_node *f)
1820{
1821    return NIL(bdd_node);
1822}
1823
1824
1825int
1826bdd_bdd_pick_one_cube(
1827  bdd_manager *mgr,
1828  bdd_node *node,
1829  char *string)
1830{
1831    return 0;
1832}
1833
1834
1835bdd_node *
1836bdd_add_swap_variables(
1837  bdd_manager *mgr,
1838  bdd_node *f,
1839  bdd_node **x,
1840  bdd_node **y,
1841  int n)
1842{
1843    return NIL(bdd_node);
1844}
1845
1846bdd_node *
1847bdd_bdd_swap_variables(
1848  bdd_manager *mgr,
1849  bdd_node *f,
1850  bdd_node **x,
1851  bdd_node **y,
1852  int n)
1853{
1854    return NIL(bdd_node);
1855}
1856
1857
1858bdd_node *
1859bdd_bdd_or(
1860  bdd_manager *mgr,
1861  bdd_node *f,
1862  bdd_node *g)
1863{
1864    return NIL(bdd_node);
1865}
1866
1867
1868bdd_node *
1869bdd_bdd_compute_cube(
1870  bdd_manager *mgr,
1871  bdd_node **vars,
1872  int *phase,
1873  int n)
1874{
1875    return NIL(bdd_node);
1876}
1877
1878
1879bdd_node *
1880bdd_indices_to_cube(
1881  bdd_manager *mgr,
1882  int *idArray,
1883  int n)
1884{
1885    return NIL(bdd_node);
1886}
1887
1888bdd_node *
1889bdd_bdd_and(
1890  bdd_manager *mgr,
1891  bdd_node *f,
1892  bdd_node *g)
1893{
1894    return NIL(bdd_node);
1895}
1896
1897
1898bdd_node *
1899bdd_add_matrix_multiply(
1900  bdd_manager *mgr,
1901  bdd_node *A,
1902  bdd_node *B,
1903  bdd_node **z,
1904  int nz)
1905{
1906    return NIL(bdd_node);
1907}
1908
1909
1910bdd_node *
1911bdd_add_compute_cube(
1912  bdd_manager *mgr,
1913  bdd_node **vars,
1914  int *phase,
1915  int n)
1916{
1917    return NIL(bdd_node);
1918}
1919
1920
1921bdd_node *
1922bdd_add_const(
1923  bdd_manager *mgr,
1924  BDD_VALUE_TYPE c)
1925{
1926    return NIL(bdd_node);
1927}
1928
1929
1930double
1931bdd_count_minterm(
1932  bdd_manager *mgr,
1933  bdd_node *f,
1934  int n)
1935{
1936    return 0;
1937}
1938
1939
1940bdd_node *
1941bdd_add_bdd_threshold(
1942  bdd_manager *mgr,
1943  bdd_node *f,
1944  BDD_VALUE_TYPE value)
1945{
1946    return NIL(bdd_node);
1947}
1948
1949
1950bdd_node *
1951bdd_add_bdd_strict_threshold(
1952  bdd_manager *mgr,
1953  bdd_node *f,
1954  BDD_VALUE_TYPE value)
1955{
1956    return NIL(bdd_node);
1957}
1958
1959BDD_VALUE_TYPE
1960bdd_read_epsilon(bdd_manager *mgr)
1961{
1962    return 0;
1963}
1964
1965bdd_node *
1966bdd_read_one(bdd_manager *mgr)
1967{
1968    return NIL(bdd_node);
1969}
1970
1971
1972bdd_node *
1973bdd_bdd_pick_one_minterm(
1974  bdd_manager *mgr,
1975  bdd_node *f,
1976  bdd_node **vars,
1977  int n)
1978{
1979    return NIL(bdd_node);
1980}
1981
1982
1983bdd_t *
1984bdd_pick_one_minterm(
1985  bdd_t *f,
1986  array_t *varsArray)
1987{
1988    return NIL(bdd_t);
1989}
1990
1991
1992array_t *
1993bdd_bdd_pick_arbitrary_minterms(
1994  bdd_t *f,
1995  array_t *varsArray,
1996  int n,
1997  int k)
1998{
1999    return NIL(array_t);
2000}
2001
2002bdd_node *
2003bdd_read_zero(bdd_manager *mgr)
2004{
2005    return NIL(bdd_node);
2006}
2007
2008
2009bdd_node *
2010bdd_bdd_new_var(bdd_manager *mgr)
2011{
2012    return NIL(bdd_node);
2013}
2014
2015
2016bdd_node *
2017bdd_bdd_and_abstract(
2018  bdd_manager *mgr,
2019  bdd_node *f,
2020  bdd_node *g,
2021  bdd_node *cube)
2022{
2023    return NIL(bdd_node);
2024}
2025
2026void
2027bdd_deref(bdd_node *f)
2028{
2029}
2030
2031bdd_node *
2032bdd_add_plus(
2033  bdd_manager *mgr,
2034  bdd_node **fn1,
2035  bdd_node **fn2)
2036{
2037  return NIL(bdd_node);
2038}
2039
2040
2041int
2042bdd_read_reorderings(bdd_manager *mgr)
2043{
2044    return 0;
2045}
2046
2047int
2048bdd_read_next_reordering(bdd_manager *mgr)
2049{
2050    return 0;
2051}
2052
2053void
2054bdd_set_next_reordering(bdd_manager *mgr, int next)
2055{
2056}
2057
2058
2059bdd_node *
2060bdd_bdd_xnor(
2061  bdd_manager *mgr,
2062  bdd_node *f,
2063  bdd_node *g)
2064{
2065    return NIL(bdd_node);
2066}
2067
2068bdd_node *
2069bdd_bdd_vector_compose(
2070  bdd_manager *mgr,
2071  bdd_node *f,
2072  bdd_node **vector)
2073{
2074    return NIL(bdd_node);
2075}
2076
2077bdd_node *
2078bdd_extract_node_as_is(bdd_t *fn)
2079{
2080  return NIL(bdd_node);
2081}
2082
2083
2084bdd_node *
2085bdd_zdd_get_node(
2086  bdd_manager *mgr,
2087  int id,
2088  bdd_node *g,
2089  bdd_node *h)
2090{
2091    return NIL(bdd_node);
2092}
2093
2094bdd_node *
2095bdd_zdd_product(
2096  bdd_manager *mgr,
2097  bdd_node *f,
2098  bdd_node *g)
2099{
2100    return NIL(bdd_node);
2101}
2102
2103bdd_node *
2104bdd_zdd_product_recur(
2105  bdd_manager *mgr,
2106  bdd_node *f,
2107  bdd_node *g)
2108{
2109    return NIL(bdd_node);
2110}
2111
2112
2113bdd_node *
2114bdd_zdd_union(
2115  bdd_manager *mgr,
2116  bdd_node *f,
2117  bdd_node *g)
2118{
2119  return NIL(bdd_node);
2120}
2121
2122
2123bdd_node *
2124bdd_zdd_weak_div(
2125  bdd_manager *mgr,
2126  bdd_node *f,
2127  bdd_node *g)
2128{
2129    return NIL(bdd_node);
2130}
2131
2132bdd_node *
2133bdd_zdd_weak_div_recur(
2134  bdd_manager *mgr,
2135  bdd_node *f,
2136  bdd_node *g)
2137{
2138    return NIL(bdd_node);
2139}
2140
2141bdd_node *
2142bdd_zdd_isop_recur(
2143  bdd_manager *mgr,
2144  bdd_node *L,
2145  bdd_node *U,
2146  bdd_node **zdd_I)
2147{
2148    return NIL(bdd_node);
2149}
2150
2151
2152bdd_node *
2153bdd_zdd_isop(
2154  bdd_manager *mgr,
2155  bdd_node *L,
2156  bdd_node *U,
2157  bdd_node **zdd_I)
2158{
2159    return NIL(bdd_node);
2160}
2161
2162int
2163bdd_zdd_get_cofactors3(
2164  bdd_manager *mgr,
2165  bdd_node *f,
2166  int v,
2167  bdd_node **f1,
2168  bdd_node **f0,
2169  bdd_node **fd)
2170{
2171    return 0;
2172}
2173
2174bdd_node *
2175bdd_bdd_and_recur(
2176  bdd_manager *mgr,
2177  bdd_node *f,
2178  bdd_node *g)
2179{
2180     return NIL(bdd_node);
2181}
2182
2183bdd_node *
2184bdd_unique_inter(
2185  bdd_manager *mgr,
2186  int v,
2187  bdd_node *f,
2188  bdd_node *g)
2189{
2190     return NIL(bdd_node);
2191}
2192
2193bdd_node *
2194bdd_unique_inter_ivo(
2195  bdd_manager *mgr,
2196  int v,
2197  bdd_node *f,
2198  bdd_node *g)
2199{
2200     return NIL(bdd_node);
2201}
2202
2203
2204bdd_node *
2205bdd_zdd_diff(
2206  bdd_manager *mgr,
2207  bdd_node *f,
2208  bdd_node *g)
2209{
2210    return NIL(bdd_node);
2211} 
2212
2213bdd_node *
2214bdd_zdd_diff_recur(
2215  bdd_manager *mgr,
2216  bdd_node *f,
2217  bdd_node *g)
2218{
2219    return NIL(bdd_node);
2220} 
2221
2222int
2223bdd_num_zdd_vars(bdd_manager *mgr)
2224{
2225    return -1;
2226}
2227
2228bdd_node *
2229bdd_regular(bdd_node *f)
2230{
2231    return NIL(bdd_node);
2232}
2233
2234int
2235bdd_is_constant(bdd_node *f)
2236{
2237    return 0;
2238}
2239
2240int
2241bdd_is_complement(bdd_node *f)
2242{
2243    return 0;
2244}
2245
2246bdd_node *
2247bdd_bdd_T(bdd_node *f)
2248{
2249    return NIL(bdd_node);
2250}
2251
2252bdd_node *
2253bdd_bdd_E(bdd_node *f)
2254{
2255    return NIL(bdd_node);
2256}
2257
2258bdd_node *
2259bdd_not_bdd_node(bdd_node *f)
2260{
2261    return NIL(bdd_node);
2262} 
2263
2264void
2265bdd_recursive_deref_zdd(bdd_manager *mgr, bdd_node *f)
2266{
2267    return;
2268} 
2269
2270int
2271bdd_zdd_count(bdd_manager *mgr, bdd_node *f)
2272{
2273    return 0;
2274}
2275
2276int
2277bdd_read_zdd_level(bdd_manager *mgr, int index)
2278{
2279    return -1;
2280} 
2281
2282int
2283bdd_zdd_vars_from_bdd_vars(bdd_manager *mgr, int multiplicity)
2284{
2285   return 0;
2286} 
2287
2288void
2289bdd_zdd_realign_enable(bdd_manager *mgr)
2290{
2291    return;
2292} 
2293
2294void
2295bdd_zdd_realign_disable(bdd_manager *mgr)
2296{
2297    return;
2298} 
2299
2300int
2301bdd_zdd_realignment_enabled(bdd_manager *mgr)
2302{
2303    return 0;
2304} 
2305
2306void
2307bdd_realign_enable(bdd_manager *mgr)
2308{
2309    return;
2310} 
2311
2312void
2313bdd_realign_disable(bdd_manager *mgr)
2314{
2315    return;
2316} 
2317
2318int
2319bdd_realignment_enabled(bdd_manager *mgr)
2320{
2321    return 0;
2322} 
2323
2324int
2325bdd_node_read_index(bdd_node *f)
2326{
2327    return -1;
2328}
2329
2330bdd_node *
2331bdd_read_next(bdd_node *f)
2332{
2333    return NIL(bdd_node);
2334}
2335
2336
2337void
2338bdd_set_next(bdd_node *f, bdd_node *g)
2339{
2340    return;
2341}
2342
2343
2344int
2345bdd_read_reordered_field(bdd_manager *mgr)
2346{
2347    return -1;
2348}
2349
2350void
2351bdd_set_reordered_field(bdd_manager *mgr, int n)
2352{
2353    return;
2354}
2355
2356bdd_node *
2357bdd_add_apply_recur(
2358  bdd_manager *mgr,
2359  bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **),
2360  bdd_node *fn1,
2361  bdd_node *fn2)
2362{
2363    return NIL(bdd_node);
2364}
2365
2366BDD_VALUE_TYPE
2367bdd_add_value(bdd_node *f)
2368{
2369    return 0.0; 
2370}
2371
2372int
2373bdd_print_minterm(bdd_t *f)
2374{
2375  return 0;
2376}
2377
2378int
2379bdd_print_cover(bdd_t *f)
2380{
2381  return 0;
2382}
2383
2384bdd_t *
2385bdd_xor_smooth(
2386  bdd_t *f,
2387  bdd_t *g,
2388  array_t *smoothing_vars)
2389{
2390    return NIL(bdd_t);
2391}
2392
2393
2394bdd_node *
2395bdd_read_plus_infinity(bdd_manager *mgr)
2396{
2397    return NIL(bdd_node);
2398
2399} /* end of bdd_read_plus_infinity */
2400
2401
2402bdd_node *
2403bdd_priority_select(
2404  bdd_manager *mgr,
2405  bdd_node *R,
2406  bdd_node **x,
2407  bdd_node **y,
2408  bdd_node **z,
2409  bdd_node *Pi,
2410  int n,
2411  bdd_node *(*Pifunc)(bdd_manager *, int, bdd_node **, bdd_node **, bdd_node **))
2412{
2413    return NIL(bdd_node);
2414
2415} /* end of bdd_priority_select */
2416
2417
2418void
2419bdd_set_background(
2420  bdd_manager *mgr,
2421  bdd_node *f)
2422{
2423    return;
2424 
2425} /* end of bdd_set_background */
2426
2427
2428bdd_node *
2429bdd_read_background(bdd_manager *mgr)
2430{
2431  return NIL(bdd_node);
2432
2433} /* end of bdd_read_background */
2434
2435
2436bdd_node *
2437bdd_bdd_cofactor(
2438  bdd_manager *mgr,
2439  bdd_node *f,
2440  bdd_node *g)
2441{
2442    return NIL(bdd_node);
2443
2444} /* end of bdd_bdd_cofactor */
2445
2446
2447bdd_node *
2448bdd_bdd_ite(
2449  bdd_manager *mgr,
2450  bdd_node *f,
2451  bdd_node *g,
2452  bdd_node *h)
2453{
2454    return NIL(bdd_node);
2455
2456} /* end of bdd_bdd_ite */
2457
2458
2459bdd_node *
2460bdd_add_minus(
2461  bdd_manager *mgr,
2462  bdd_node **fn1,
2463  bdd_node **fn2)
2464{
2465    return NIL(bdd_node);
2466
2467} /* end of bdd_add_plus */
2468
2469
2470bdd_node *
2471bdd_dxygtdxz(
2472  bdd_manager *mgr,
2473  int N,
2474  bdd_node **x,
2475  bdd_node **y,
2476  bdd_node **z)
2477{
2478    return NIL(bdd_node);
2479
2480} /* end of bdd_dxygtdxz */
2481
2482
2483bdd_node *
2484bdd_bdd_univ_abstract(
2485  bdd_manager *mgr,
2486  bdd_node *fn,
2487  bdd_node *vars)
2488{
2489    return NIL(bdd_node);
2490
2491} /* end of bdd_bdd_univ_abstract */
2492
2493
2494bdd_node *
2495bdd_bdd_cprojection(
2496  bdd_manager *mgr,
2497  bdd_node *R,
2498  bdd_node *Y)
2499{
2500    return NIL(bdd_node);
2501
2502} /* end of bdd_bdd_cprojection */
2503
2504bdd_node *
2505bdd_xeqy(
2506  bdd_manager *mgr,
2507  int N,
2508  bdd_node **x,
2509  bdd_node **y)
2510{
2511  return NIL(bdd_node);
2512
2513} /* end of bdd_xeqy */
2514
2515bdd_node *
2516bdd_add_roundoff(
2517  bdd_manager *mgr,
2518  bdd_node *f,
2519  int N)
2520{
2521  return NIL(bdd_node);
2522
2523} /* end of bdd_add_roundoff */
2524
2525bdd_node *
2526bdd_xgty(
2527  bdd_manager *mgr,
2528  int N,
2529  bdd_node **x,
2530  bdd_node **y)
2531{
2532  return NIL(bdd_node);
2533
2534} /* end of bdd_xgty */
2535
2536bdd_node *
2537bdd_add_cmpl(
2538  bdd_manager *mgr,
2539  bdd_node *f)
2540{
2541  return NIL(bdd_node);
2542
2543} /* end of bdd_add_cmpl */
2544
2545bdd_node *
2546bdd_split_set(
2547  bdd_manager *mgr,
2548  bdd_node *f,
2549  bdd_node **x,
2550  int n,
2551  double m)
2552{
2553  return NIL(bdd_node);
2554
2555} /* end of bdd_split_set */
2556
2557
2558int
2559bdd_debug_check(bdd_manager *mgr)
2560{
2561    return (-1);
2562
2563} /* end of bdd_debug_check */
2564
2565bdd_node *
2566bdd_bdd_xor(
2567  bdd_manager *mgr,
2568  bdd_node *f,
2569  bdd_node *g)
2570{
2571    return NIL(bdd_node);
2572}
2573
2574void 
2575bdd_dump_blif(
2576  bdd_manager *mgr,
2577  int nBdds,
2578  bdd_node **bdds,
2579  char **inames,
2580  char **onames,
2581  char *model,
2582  FILE *fp)
2583{
2584  return;
2585}
2586
2587void 
2588bdd_dump_blif_body(
2589  bdd_manager *mgr,
2590  int nBdds,
2591  bdd_node **bdds,
2592  char **inames,
2593  char **onames,
2594  FILE *fp)
2595{
2596  return;
2597}
2598
2599void 
2600bdd_dump_dot(
2601  bdd_manager *mgr,
2602  int nBdds,
2603  bdd_node **bdds,
2604  char **inames,
2605  char **onames,
2606  FILE *fp)
2607{
2608  return;
2609}
2610
2611bdd_node *
2612bdd_make_bdd_from_zdd_cover(bdd_manager *mgr, bdd_node *node)
2613{
2614    return(NIL(bdd_node));
2615}
2616
2617bdd_node *
2618bdd_zdd_complement(bdd_manager *mgr, bdd_node *node)
2619{
2620    return(NIL(bdd_node));
2621}
2622
2623bdd_node *
2624bdd_bdd_vector_support(
2625  bdd_manager *mgr,
2626  bdd_node **F,
2627  int n)
2628{
2629  return NIL(bdd_node);
2630}
2631
2632int
2633bdd_bdd_vector_support_size(
2634  bdd_manager *mgr,
2635  bdd_node **F,
2636  int n)
2637{
2638  return -1;
2639}
2640
2641int
2642bdd_bdd_support_size(
2643  bdd_manager *mgr,
2644  bdd_node *F)
2645{
2646  return -1;
2647}
2648
2649bdd_node *
2650bdd_bdd_support(
2651  bdd_manager *mgr,
2652  bdd_node *F)
2653{
2654  return NIL(bdd_node);
2655}
2656
2657bdd_node *
2658bdd_add_general_vector_compose(
2659  bdd_manager *mgr,
2660  bdd_node *f,
2661  bdd_node **vectorOn,
2662  bdd_node **vectorOff)
2663{
2664  return NIL(bdd_node);
2665}
2666
2667int
2668bdd_bdd_leq(
2669  bdd_manager *mgr,
2670  bdd_node *f,
2671  bdd_node *g)
2672{
2673  return -1;
2674} 
2675
2676bdd_node *
2677bdd_bdd_boolean_diff(
2678  bdd_manager *mgr,
2679  bdd_node *f,
2680  int x)
2681{
2682  return NIL(bdd_node);
2683}
2684
2685/**Function********************************************************************
2686
2687  Synopsis    [Compares two bdds are same.]
2688
2689  SideEffects []
2690
2691******************************************************************************/
2692int
2693bdd_ptrcmp(bdd_t *f, bdd_t *g)
2694{
2695  if (f->node == g->node)
2696    return(0);
2697  else
2698    return(1);
2699}
2700
2701
2702/**Function********************************************************************
2703
2704  Synopsis    [Returns the hash value of a bdd.]
2705
2706  SideEffects []
2707
2708******************************************************************************/
2709int
2710bdd_ptrhash(bdd_t *f, int size)
2711{
2712  int hash;
2713
2714  hash = (int)((unsigned long)f->node >> 2) % size;
2715  return(hash);
2716}
2717
2718bdd_t *
2719bdd_subset_with_mask_vars(
2720  bdd_t *f,
2721  array_t *varsArray,
2722  array_t *maskVarsArray)
2723{
2724  return NIL(bdd_t);
2725}
2726
2727bdd_t *
2728bdd_and_smooth_with_cube(
2729  bdd_t *f,
2730  bdd_t *g,
2731  bdd_t *cube)
2732{
2733  return NIL(bdd_t);
2734}
2735
2736bdd_t *
2737bdd_smooth_with_cube(bdd_t *f, bdd_t *cube)
2738{
2739  int i;
2740  bdd_t *var, *res;
2741  array_t *smoothingVars;
2742  var_set_t *supportVarSet;
2743
2744  smoothingVars = array_alloc(bdd_t *, 0);
2745  supportVarSet = bdd_get_support(f);
2746  for (i = 0; i < supportVarSet->n_elts; i++) {
2747    if (var_set_get_elt(supportVarSet, i) == 1) {
2748      var = bdd_var_with_index(f->mgr, i);
2749      array_insert_last(bdd_t *, smoothingVars, var);
2750    }
2751  }
2752  var_set_free(supportVarSet);
2753
2754  res = bdd_smooth(f, smoothingVars);
2755
2756  for (i = 0; i < array_n(smoothingVars); i++) {
2757    var = array_fetch(bdd_t *, smoothingVars, i);
2758    bdd_free(var);
2759  }
2760  array_free(smoothingVars);
2761  return res;
2762}
2763
2764bdd_t *
2765bdd_substitute_with_permut(bdd_t *f, int *permut)
2766{
2767  return NIL(bdd_t);
2768}
2769
2770array_t *
2771bdd_substitute_array_with_permut(
2772  array_t *f_array,
2773  int *permut)
2774{
2775  return NIL(array_t);
2776}
2777
2778bdd_t *
2779bdd_vector_compose(
2780  bdd_t *f,
2781  array_t *varArray,
2782  array_t *funcArray)
2783{
2784  return NIL(bdd_t);
2785}
2786
2787double *
2788bdd_cof_minterm(bdd_t *f)
2789{
2790  return(NIL(double));
2791}
2792
2793int
2794bdd_var_is_dependent(bdd_t *f, bdd_t *var)
2795{
2796  return(0);
2797}
2798
2799array_t *
2800bdd_find_essential(bdd_t *f)
2801{
2802  return(NIL(array_t));
2803}
2804
2805bdd_t *
2806bdd_find_essential_cube(bdd_t *f)
2807{
2808  return(NIL(bdd_t));
2809}
2810
2811int
2812bdd_estimate_cofactor(bdd_t *f, bdd_t *var, int phase)
2813{
2814  return(0);
2815}
2816
2817long
2818bdd_read_peak_memory(bdd_manager *mgr)
2819{
2820  return(0);
2821}
2822
2823int
2824bdd_read_peak_live_node(bdd_manager *mgr)
2825{
2826  return(0);
2827}
2828
2829int
2830bdd_set_pi_var(bdd_manager *mgr, int index)
2831{
2832    return(0);
2833}
2834
2835int
2836bdd_set_ps_var(bdd_manager *mgr, int index)
2837{
2838    return(0);
2839}
2840
2841int
2842bdd_set_ns_var(bdd_manager *mgr, int index)
2843{
2844    return(0);
2845}
2846
2847int
2848bdd_is_pi_var(bdd_manager *mgr, int index)
2849{
2850    return(0);
2851}
2852
2853int
2854bdd_is_ps_var(bdd_manager *mgr, int index)
2855{
2856    return(0);
2857}
2858
2859int
2860bdd_is_ns_var(bdd_manager *mgr, int index)
2861{
2862    return(0);
2863}
2864
2865int
2866bdd_set_pair_index(bdd_manager *mgr, int index, int pairIndex)
2867{
2868    return(0);
2869}
2870
2871int
2872bdd_read_pair_index(bdd_manager *mgr, int index)
2873{
2874    return(0);
2875}
2876
2877int
2878bdd_set_var_to_be_grouped(bdd_manager *mgr, int index)
2879{
2880    return(0);
2881}
2882
2883int
2884bdd_set_var_hard_group(bdd_manager *mgr, int index)
2885{
2886    return(0);
2887}
2888
2889int
2890bdd_reset_var_to_be_grouped(bdd_manager *mgr, int index)
2891{
2892    return(0);
2893}
2894
2895int
2896bdd_is_var_to_be_grouped(bdd_manager *mgr, int index)
2897{
2898    return(0);
2899}
2900
2901int
2902bdd_is_var_hard_group(bdd_manager *mgr, int index)
2903{
2904    return(0);
2905}
2906
2907int
2908bdd_is_var_to_be_ungrouped(bdd_manager *mgr, int index)
2909{
2910    return(0);
2911}
2912
2913int
2914bdd_set_var_to_be_ungrouped(bdd_manager *mgr, int index)
2915{
2916    return(0);
2917}
2918
2919int
2920bdd_bind_var(bdd_manager *mgr, int index)
2921{
2922    return(0);
2923}
2924
2925int
2926bdd_unbind_var(bdd_manager *mgr, int index)
2927{
2928    return(0);
2929}
2930
2931int
2932bdd_is_lazy_sift(bdd_manager *mgr)
2933{
2934    return(0);
2935}
2936
2937void
2938bdd_discard_all_var_groups(bdd_manager *mgr)
2939{
2940    return;
2941}
2942
2943/*---------------------------------------------------------------------------*/
2944/* Definition of internal functions                                          */
2945/*---------------------------------------------------------------------------*/
2946
2947
2948/*---------------------------------------------------------------------------*/
2949/* Definition of static functions                                            */
2950/*---------------------------------------------------------------------------*/
2951
2952
2953
Note: See TracBrowser for help on using the repository browser.