src/mdd/mdd_substit.c

Go to the documentation of this file.

#include "mdd.h"

/*
 * MDD Package
 *
 * $Id: mdd_substit.c,v 1.10 2002/08/24 21:48:15 fabio Exp $
 * 
 * Author: Timothy Kam
 *
 * Copyright 1992 by the Regents of the University of California.
 *
 * All rights reserved.  Permission to use, copy, modify and distribute
 * this software is hereby granted, provided that the above copyright
 * notice and this permission notice appear in all copies.  This software
 * is made available as is, with no warranties.
 */

array_t *
mdd_substitute_array(
  mdd_manager   *mgr,
  array_t       *fn_array,
  array_t       *old_mvars,
  array_t       *new_mvars)
{
    array_t     *new_fn_array;
    mdd_t       *new_fn, *fn;
    int         i;

    new_fn_array = array_alloc(mdd_t *, 0);
    arrayForEachItem(mdd_t *, fn_array, i, fn) {
        new_fn = mdd_substitute(mgr, fn, old_mvars, new_mvars);
        array_insert(mdd_t *, new_fn_array, i, new_fn);
    }

    return(new_fn_array);
}

mdd_t *
mdd_substitute(
  mdd_manager   *mgr,
  mdd_t         *fn,
  array_t       *old_mvars,
  array_t       *new_mvars)
{
    array_t             *old_bdd_vars, *new_bdd_vars;
    int                 i, j, old_mv_no, new_mv_no, no_mvar;
    mvar_type           old_mv, new_mv;
    mdd_t               *top;
    array_t             *mvar_list = mdd_ret_mvar_list(mgr);
    bdd_t               *varBdd;

    old_bdd_vars = array_alloc( bdd_t *, 0);
    new_bdd_vars = array_alloc( bdd_t *, 0);

    no_mvar = array_n(old_mvars);
    if (no_mvar != array_n(new_mvars)) 
        fail("mdd_substitute: arrays contains different no. of mvars.\n");

    for (i=0; i<no_mvar; i++) {
        old_mv_no = array_fetch(int, old_mvars, i);
        old_mv = array_fetch(mvar_type, mvar_list, old_mv_no);
        if (old_mv.status == MDD_BUNDLED) {
                (void) fprintf(stderr, 
                   "\nmdd_substitute: bundled variable %s used\n",old_mv.name);
                fail("");
        }

        new_mv_no = array_fetch(int, new_mvars, i);
        new_mv = array_fetch(mvar_type, mvar_list, new_mv_no);
        if (new_mv.status == MDD_BUNDLED) {
                (void) fprintf(stderr, 
                   "\nmdd_substitute: bundled variable %s used\n",new_mv.name);
                fail("");
        }

        if (old_mv.values != new_mv.values) 
            fail("mdd_substitute: mvars have different no. of values\n");

        for (j=0; j<old_mv.encode_length; j++) {        
            varBdd = bdd_get_variable( mgr, mdd_ret_bvar_id(&old_mv,j) );
            array_insert_last( bdd_t *, old_bdd_vars, varBdd );

            varBdd = bdd_get_variable( mgr, mdd_ret_bvar_id(&new_mv, j) );
            array_insert_last( bdd_t *, new_bdd_vars, varBdd);
        }
    }
    top = bdd_substitute(fn, old_bdd_vars, new_bdd_vars);

    for(j=0; j<array_n(old_bdd_vars); j++) {
        varBdd = array_fetch(bdd_t*,old_bdd_vars,j);
        bdd_free(varBdd);
    }
    array_free(old_bdd_vars);
    for(j=0; j<array_n(new_bdd_vars); j++) {
        varBdd = array_fetch(bdd_t*,new_bdd_vars,j);
        bdd_free(varBdd);
    }
    array_free(new_bdd_vars);

    return top;
}

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

---