source: vis_dev/glu-2.3/src/mdd/mdd_cofactor.c @ 13

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

library glu 2.3
File size: 3.3 KB
Line 
1#include "mdd.h"
2
3/*
4 * MDD Package
5 *
6 * $Id: mdd_cofactor.c,v 1.10 2009/01/07 17:14:47 fabio Exp $
7 *
8 * Author: Timothy Kam
9 *
10 * Copyright 1992 by the Regents of the University of California.
11 *
12 * All rights reserved.  Permission to use, copy, modify and distribute
13 * this software is hereby granted, provided that the above copyright
14 * notice and this permission notice appear in all copies.  This software
15 * is made available as is, with no warranties.
16 */
17
18
19
20/*---------------------------------------------------------------------------*/
21/* Static function prototypes                                                */
22/*---------------------------------------------------------------------------*/
23
24static void mdd_traverse(mdd_manager *mgr, bdd_t *top, boolean *mvar_present);
25static array_t * mvars_extract(mdd_manager *mgr, mdd_t *fn);
26
27/*---------------------------------------------------------------------------*/
28/* Definition of exported functions                                          */
29/*---------------------------------------------------------------------------*/
30
31mdd_t *
32mdd_cofactor(
33  mdd_manager *mgr,
34  mdd_t *fn,
35  mdd_t *cube)
36{
37    array_t *mvars;
38    mdd_t *top;
39
40    mvars = mvars_extract(mgr, cube);
41    top = mdd_and_smooth(mgr, fn, cube, mvars);
42    array_free(mvars);
43    return top;
44}
45
46/*---------------------------------------------------------------------------*/
47/* Definition of static functions                                            */
48/*---------------------------------------------------------------------------*/
49
50static void
51mdd_traverse(
52  mdd_manager *mgr,
53  bdd_t *top,
54  boolean *mvar_present)
55{
56    bvar_type bv;
57    array_t *bvar_list = mdd_ret_bvar_list(mgr);
58    int is_complemented;
59    bdd_t *uncomp_top, *child, *temp_child;
60
61    if (bdd_is_tautology(top,1)) {
62        return;
63    }
64    if (bdd_is_tautology(top,0)) {
65        return;
66    }
67
68    (void)bdd_get_node(top,&is_complemented);
69
70    bv = array_fetch(bvar_type, bvar_list, bdd_top_var_id(top));
71    mvar_present[bv.mvar_id] = 1;
72
73    if (is_complemented) uncomp_top = bdd_not(top);
74    else uncomp_top = mdd_dup(top);
75
76    child = bdd_then(uncomp_top);
77    (void) bdd_get_node(child,&is_complemented);
78    if (is_complemented) {
79        temp_child = child;
80        child = bdd_not(temp_child);
81        mdd_free(temp_child);
82    }
83   
84    mdd_traverse(mgr, child , mvar_present);
85    mdd_free(child);
86
87    child = bdd_else(uncomp_top);
88    (void) bdd_get_node(child,&is_complemented);
89    if (is_complemented) {
90        temp_child = child;
91        child = bdd_not(temp_child);
92        mdd_free(temp_child);
93    }
94
95    mdd_traverse(mgr, child, mvar_present);
96   
97 
98    mdd_free(child);
99    mdd_free(uncomp_top);
100    return;   
101}
102
103
104static array_t *
105mvars_extract(
106  mdd_manager *mgr,
107  mdd_t *fn)
108{
109    int i, no_mvar;
110    boolean *mvar_present;
111    array_t *mvar_list = mdd_ret_mvar_list(mgr);
112    array_t *mvars;
113                                                                         
114
115    mvars = array_alloc(int, 0);
116    no_mvar = array_n(mvar_list);
117    mvar_present = ALLOC(boolean, no_mvar);
118    for (i=0; i<no_mvar; i++) mvar_present[i] = 0;
119    mdd_traverse(mgr, fn, mvar_present);
120    for (i=0; i<no_mvar; i++) 
121        if (mvar_present[i] == 1) array_insert_last(int, mvars, i);
122    FREE(mvar_present);
123    return mvars;
124}
Note: See TracBrowser for help on using the repository browser.