src/cmuPort/cmuPortIter.c File Reference

#include "cmuPortInt.h"

Include dependency graph for cmuPortIter.c:

Go to the source code of this file.

Data Structures
struct	cmu_bdd_gen
Enumerations
enum	bdd_gen_type { bdd_gen_cubes, bdd_gen_nodes, bdd_gen_cubes, bdd_gen_nodes }
Functions
static void	pop_cube_stack (cmu_bdd_gen *gen)
static void	pop_node_stack (cmu_bdd_gen *gen)
static void	push_cube_stack (bdd_node *f, cmu_bdd_gen *gen)
static void	push_node_stack (bdd_node *f, cmu_bdd_gen *gen)
bdd_gen_status	bdd_gen_read_status (bdd_gen *gen)
bdd_gen *	bdd_first_cube (bdd_t *fn, array_t **cube)
boolean	bdd_next_cube (bdd_gen *gen_, array_t **cube)
bdd_gen *	bdd_first_disjoint_cube (bdd_t *fn, array_t **cube)
boolean	bdd_next_disjoint_cube (bdd_gen *gen_, array_t **cube)
bdd_gen *	bdd_first_node (bdd_t *fn, bdd_node **node)
boolean	bdd_next_node (bdd_gen *gen_, bdd_node **node)
int	bdd_gen_free (bdd_gen *gen_)

---

Enumeration Type Documentation

enum bdd_gen_type

CFile***********************************************************************

FileName [cmuPort.c]

PackageName [cmu_port]

Synopsis [Port routines for CMU package.]

Description [optional]

SeeAlso [optional]

Author [Thomas R. Shiple. Some changes by Rajeev K. Ranjan.]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id

cmuPortIter.c,v 1.4 2005/04/15 23:24:39 fabio Exp

]

Enumerator:

bdd_gen_cubes
bdd_gen_nodes
bdd_gen_cubes
bdd_gen_nodes

Definition at line 51 of file cmuPortIter.c.

             {
    bdd_gen_cubes,
    bdd_gen_nodes
} bdd_gen_type;

---

Function Documentation

bdd_gen* bdd_first_cube	(	bdd_t *	fn,
		array_t **	cube
	)

Definition at line 132 of file cmuPortIter.c.

{
    struct bdd_manager_ *manager;
    cmu_bdd_gen *gen;
    int i;
    long num_vars;
    bdd_node *f;

    if (fn == NIL(bdd_t)) {
        cmu_bdd_fatal("bdd_first_cube: invalid BDD");
    }

    manager = fn->mgr;

    /*
     *    Allocate a new generator structure and fill it in; the stack and the 
     *    cube will be used, but the visited table and the node will not be used.
     */
    gen = ALLOC(cmu_bdd_gen, 1);
    if (gen == NIL(cmu_bdd_gen)) {
        cmu_bdd_fatal("bdd_first_cube: failed on memory allocation, location 1");
    }

    /*
     *    first - init all the members to a rational value for cube iteration
     */
    gen->manager = manager;
    gen->status = bdd_EMPTY;
    gen->type = bdd_gen_cubes;
    gen->gen.cubes.cube = NIL(array_t);
    gen->stack.sp = 0;
    gen->stack.stack = NIL(bdd_node *);
    gen->node = NIL(bdd_node);

    num_vars = cmu_bdd_vars(manager);
    gen->gen.cubes.cube = array_alloc(bdd_literal, num_vars);
    if (gen->gen.cubes.cube == NIL(array_t)) {
        cmu_bdd_fatal("bdd_first_cube: failed on memory allocation, location 2");
    }
    
    /*
     * Initialize each literal to 2 (don't care).
     */
    for (i = 0; i < num_vars; i++) {
        array_insert(bdd_literal, gen->gen.cubes.cube, i, 2);
    }

    /*
     * The stack size will never exceed the number of variables in the BDD, since
     * the longest possible path from root to constant 1 is the number of variables 
     * in the BDD.
     */
    gen->stack.sp = 0;
    gen->stack.stack = ALLOC(bdd_node *, num_vars);
    if (gen->stack.stack == NIL(bdd_node *)) {
        cmu_bdd_fatal("bdd_first_cube: failed on memory allocation, location 3");
    }
    /*
     * Clear out the stack so that in bdd_gen_free, we can decrement the ref count
     * of those nodes still on the stack.
     */
    for (i = 0; i < num_vars; i++) {
        gen->stack.stack[i] = NIL(bdd_node);
    }

    if (bdd_is_tautology(fn, 0)) {
        /*
         *    All done, for this was but the zero constant ...
         *    We are enumerating the onset, (which is vacuous).
         *    gen->status initialized to bdd_EMPTY above, so this
         *    appears to be redundant.
         */
        gen->status = bdd_EMPTY;
    } else {
        /*
         *    Get to work enumerating the onset.  Get the first cube.  Note that
         *    if fn is just the constant 1, push_cube_stack will properly handle this.
         *    Get a new pointer to fn->node beforehand: this increments
         *    the reference count of fn->node; this is necessary, because when fn->node
         *    is popped from the stack at the very end, it's ref count is decremented.
         */
        gen->status = bdd_NONEMPTY;
        f = cmu_bdd_identity(manager, fn->node);
        push_cube_stack(f, gen);
    }

    *cube = gen->gen.cubes.cube;
    return (bdd_gen *)(gen);
}

bdd_gen* bdd_first_disjoint_cube	(	bdd_t *	fn,
		array_t **	cube
	)

Definition at line 239 of file cmuPortIter.c.

{
  return(bdd_first_cube(fn,cube));
}

bdd_gen* bdd_first_node	(	bdd_t *	fn,
		bdd_node **	node
	)

Definition at line 255 of file cmuPortIter.c.

{
    struct bdd_manager_ *manager;
    cmu_bdd_gen *gen;
    long num_vars;
    bdd_node *f;
    int i;

    if (fn == NIL(bdd_t)) {
        cmu_bdd_fatal("bdd_first_node: invalid BDD");
    }

    manager = fn->mgr;

    /*
     *    Allocate a new generator structure and fill it in; the
     *    visited table will be used, as will the stack, but the
     *    cube array will not be used.
     */
    gen = ALLOC(cmu_bdd_gen, 1);
    if (gen == NIL(bdd_gen)) {
        cmu_bdd_fatal("bdd_first_node: failed on memory allocation, location 1");
    }

    /*
     *    first - init all the members to a rational value for node iteration.
     */
    gen->manager = manager;
    gen->status = bdd_NONEMPTY;
    gen->type = bdd_gen_nodes;
    gen->gen.nodes.visited = NIL(st_table);
    gen->stack.sp = 0;
    gen->stack.stack = NIL(bdd_node *);
    gen->node = NIL(bdd_node);
  
    /* 
     * Set up the hash table for visited nodes.  Every time we visit a node,
     * we insert it into the table.
     */
    gen->gen.nodes.visited = st_init_table(st_ptrcmp, st_ptrhash);
    if (gen->gen.nodes.visited == NIL(st_table)) {
        cmu_bdd_fatal("bdd_first_node: failed on memory allocation, location 2");
    }

    /*
     * The stack size will never exceed the number of variables in the BDD, since
     * the longest possible path from root to constant 1 is the number of variables 
     * in the BDD.
     */
    gen->stack.sp = 0;
    num_vars = cmu_bdd_vars(manager);
    gen->stack.stack = ALLOC(bdd_node *, num_vars);
    if (gen->stack.stack == NIL(bdd_node *)) {
        cmu_bdd_fatal("bdd_first_node: failed on memory allocation, location 3");
    }
    /*
     * Clear out the stack so that in bdd_gen_free, we can decrement the ref count
     * of those nodes still on the stack.
     */
    for (i = 0; i < num_vars; i++) {
        gen->stack.stack[i] = NIL(bdd_node);
    }

    /*
     * Get the first node.  Get a new pointer to fn->node beforehand: this increments
     * the reference count of fn->node; this is necessary, because when fn->node
     * is popped from the stack at the very end, it's ref count is decremented.
     */
    f = cmu_bdd_identity(manager, fn->node);
    push_node_stack(f, gen);
    gen->status = bdd_NONEMPTY;

    *node = gen->node;  /* return the node */
    return (bdd_gen *) (gen);   /* and the new generator */
}

int bdd_gen_free

(

bdd_gen *

gen_

)

Definition at line 354 of file cmuPortIter.c.

{
    long num_vars;
    int i;
    struct bdd_manager_ *mgr;
    bdd_node *f;
    st_table *visited_table;
    st_generator *visited_gen;
    cmu_bdd_gen *gen = (cmu_bdd_gen *) gen_;

    mgr = gen->manager;

    switch (gen->type) {
    case bdd_gen_cubes:
        array_free(gen->gen.cubes.cube);
        gen->gen.cubes.cube = NIL(array_t);
        break;
    case bdd_gen_nodes:
        visited_table = gen->gen.nodes.visited;
        st_foreach_item(visited_table, visited_gen, &f, NIL(refany)) {
            cmu_bdd_free(mgr, (bdd) f);
        }
        st_free_table(visited_table);
        visited_table = NIL(st_table);
        break;
    }

    /*
     * Free the data associated with this generator.  If there are any nodes remaining
     * on the stack, we must free them, to get their ref counts back to what they were before.
     */
    num_vars = cmu_bdd_vars(mgr);
    for (i = 0; i < num_vars; i++) {
        f = gen->stack.stack[i];
        if (f != NIL(bdd_node)) {
            cmu_bdd_free(mgr, (bdd) f);
        }
    }
    FREE(gen->stack.stack);

    FREE(gen);

    return (0); /* make it return some sort of an int */
}

bdd_gen_status bdd_gen_read_status

(

bdd_gen *

gen

)

AutomaticEnd

Definition at line 110 of file cmuPortIter.c.

{
  return ((cmu_bdd_gen *)gen)->status;
}

boolean bdd_next_cube	(	bdd_gen *	gen_,
		array_t **	cube
	)

Definition at line 227 of file cmuPortIter.c.

{
  cmu_bdd_gen *gen = (cmu_bdd_gen *) gen_;
  pop_cube_stack(gen);
  if (gen->status == bdd_EMPTY) {
    return (FALSE);
  }
  *cube = gen->gen.cubes.cube;
  return (TRUE);
}

boolean bdd_next_disjoint_cube	(	bdd_gen *	gen_,
		array_t **	cube
	)

Definition at line 245 of file cmuPortIter.c.

{
  return(bdd_next_cube(gen_,cube));
}

boolean bdd_next_node	(	bdd_gen *	gen_,
		bdd_node **	node
	)

Definition at line 336 of file cmuPortIter.c.

{
  cmu_bdd_gen *gen = (cmu_bdd_gen *) gen_;
  
    pop_node_stack(gen);
    if (gen->status == bdd_EMPTY) {
        return (FALSE);
    }
    *node = gen->node;
    return (TRUE);
}

static void pop_cube_stack

(

cmu_bdd_gen *

gen

)

[static]

AutomaticStart

Definition at line 486 of file cmuPortIter.c.

{
    bdd_variableId topf_id, level_i_id;
    bdd_node *branch_f;
    bdd_node *f1;
    int i;
    long topf_level;
    struct bdd_manager_ *mgr;
    struct bdd_ *var_bdd;

    mgr = gen->manager;

    if (gen->stack.sp == 0) {
        /*
         * Stack is empty.  Have already explored both the 0 and 1 branches of 
         * the root of the BDD.
         */
        gen->status = bdd_EMPTY;
    } else {
        /*
         * Explore the 1 branch of the node at the top of the stack (since it is
         * on the stack, this means we have already explored the 0 branch).  We 
         * permanently pop the top node, and bdd_free it, since there are no more edges left to 
         * explore. 
         */
        branch_f = gen->stack.stack[--gen->stack.sp];
        gen->stack.stack[gen->stack.sp] = NIL(bdd_node); /* overwrite with NIL */
        topf_id = (bdd_variableId) (cmu_bdd_if_id(mgr, (bdd) branch_f) - 1);
        array_insert(bdd_literal, gen->gen.cubes.cube, topf_id, 1);

        /* 
         * We must set the variables with levels greater than the level of branch_f,
         * back to 2 (don't care).  This is because these variables are not
         * on the current path, and thus there values are don't care.
         *
         * Note the following correspondence:
         *   CMU          UCB
         *  index         level   (both start at zero)
         *  indexindex    id      (CMU has id 0 for constant, thus really start numbering at 1;
         *                                           UCB starts numbering at 0)
         */
        topf_level = cmu_bdd_if_index(mgr, (bdd) branch_f);
        for (i = topf_level + 1; i < array_n(gen->gen.cubes.cube); i++) {
            var_bdd = cmu_bdd_var_with_index(mgr, i);
            level_i_id = (bdd_variableId) (cmu_bdd_if_id(mgr, var_bdd) - 1);
            /*
             * No need to free var_bdd, since single variable BDDs are never garbage collected.
             * Note that level_i_id is just (mgr->indexindexes[i] - 1); however, wanted
             * to avoid using CMU internals.
             */
            array_insert(bdd_literal, gen->gen.cubes.cube, level_i_id, 2);
        }
        f1 = cmu_bdd_then(mgr, (bdd) branch_f);
        push_cube_stack(f1, gen);
        cmu_bdd_free(mgr, (bdd) branch_f);
    }
}

static void pop_node_stack

(

cmu_bdd_gen *

gen

)

[static]

Definition at line 630 of file cmuPortIter.c.

{
    bdd_node *branch_f;

    if (gen->stack.sp == 0) {
        gen->status = bdd_EMPTY;
    } else {
        branch_f = gen->stack.stack[--gen->stack.sp];  /* overwrite with NIL */
        gen->stack.stack[gen->stack.sp] = NIL(bdd_node);
        push_node_stack(branch_f, gen);
    }
}

static void push_cube_stack	(	bdd_node *	f,
		cmu_bdd_gen *	gen
	)			[static]

Definition at line 428 of file cmuPortIter.c.

{
    bdd_variableId topf_id;
    bdd_node *f0, *f1;
    struct bdd_manager_ *mgr;

    mgr = gen->manager;

    if (f == cmu_bdd_one(mgr)) {
        return;
    }

    topf_id = (bdd_variableId) (cmu_bdd_if_id(mgr, (bdd) f) - 1);

    /* 
     * Get the then and else branches of f. Note that cmu_bdd_then and cmu_bdd_else 
     * automatically take care of inverted pointers.  
     */
    f0 = cmu_bdd_else(mgr, (bdd) f);
    f1 = cmu_bdd_then(mgr, (bdd) f);

    if (f1 == cmu_bdd_zero(mgr)) {
        /*
         *    No choice: take the 0 branch.  Since there is only one branch to 
         *    explore from f, there is no need to push f onto the stack, because
         *    after exploring this branch we are done with f.  A consequence of 
         *    this is that there will be no f to pop either.  Same goes for the
         *    next case.  Decrement the ref count of f and of the branch leading
         *    to zero, since we will no longer need to access these nodes.
         */
        array_insert(bdd_literal, gen->gen.cubes.cube, topf_id, 0);
        push_cube_stack(f0, gen);
        cmu_bdd_free(mgr, (bdd) f1);
        cmu_bdd_free(mgr, (bdd) f);
    } else if (f0 == cmu_bdd_zero(mgr)) {
        /*
         *    No choice: take the 1 branch
         */
        array_insert(bdd_literal, gen->gen.cubes.cube, topf_id, 1);
        push_cube_stack(f1, gen);
        cmu_bdd_free(mgr, (bdd) f0);
        cmu_bdd_free(mgr, (bdd) f);
    } else {
        /*
         * In this case, we must explore both branches of f.  We always choose
         * to explore the 0 branch first.  We must push f on the stack, so that
         * we can later pop it and explore its 1 branch. Decrement the ref count 
         * of f1 since we will no longer need to access this node.  Note that 
         * the parent of f1 was bdd_freed above or in pop_cube_stack.
         */
        gen->stack.stack[gen->stack.sp++] = f;
        array_insert(bdd_literal, gen->gen.cubes.cube, topf_id, 0);
        push_cube_stack(f0, gen);
        cmu_bdd_free(mgr, (bdd) f1);
    }
}

static void push_node_stack	(	bdd_node *	f,
		cmu_bdd_gen *	gen
	)			[static]

Definition at line 560 of file cmuPortIter.c.

{
    bdd_node *f0, *f1;
    bdd_node *reg_f, *reg_f0, *reg_f1;
    struct bdd_manager_ *mgr;

    mgr = gen->manager;

    reg_f = (bdd_node *) BDD_POINTER(f);  /* use of bddint.h */
    if (st_lookup(gen->gen.nodes.visited, (refany) reg_f, NIL(refany))) {
        /* 
         * Already been visited.
         */
        return;
    }

    if (f == cmu_bdd_one(mgr) || f == cmu_bdd_zero(mgr)) {
        /*
         * If f is the constant node and it has not been visited yet, then put it in the visited table
         * and set the gen->node pointer.  There is no need to put it in the stack because
         * the constant node does not have any branches, and there is no need to free f because 
         * constant nodes have a saturated reference count.
         */
        st_insert(gen->gen.nodes.visited, (refany) reg_f, NIL(any));
        gen->node = reg_f;
    } else {
        /*
         * f has not been marked as visited.  We don't know yet if any of its branches 
         * remain to be explored.  First get its branches.  Note that cmu_bdd_then and 
         * cmu_bdd_else automatically take care of inverted pointers.  
         */
        f0 = cmu_bdd_else(mgr, (bdd) f);
        f1 = cmu_bdd_then(mgr, (bdd) f);

        reg_f0 = (bdd_node *) BDD_POINTER(f0);  /* use of bddint.h */
        reg_f1 = (bdd_node *) BDD_POINTER(f1);
        if (! st_lookup(gen->gen.nodes.visited, (refany) reg_f0, NIL(refany))) {
            /* 
             * The 0 child has not been visited, so explore the 0 branch.  First push f on 
             * the stack.  Bdd_free f1 since we will not need to access this exact pointer
             * any more.
             */
            gen->stack.stack[gen->stack.sp++] = f;
            push_node_stack(f0, gen);
            cmu_bdd_free(mgr, (bdd) f1);
        } else if (! st_lookup(gen->gen.nodes.visited, (refany) reg_f1, NIL(refany))) {
            /* 
             * The 0 child has been visited, but the 1 child has not been visited, so 
             * explore the 1 branch.  First push f on the stack. We are done with f0, 
             * so bdd_free it.
             */
            gen->stack.stack[gen->stack.sp++] = f;
            push_node_stack(f1, gen);
            cmu_bdd_free(mgr, (bdd) f0);
        } else {
            /*
             * Both the 0 and 1 children have been visited. Thus we are done exploring from f.  
             * Mark f as visited (put it in the visited table), and set the gen->node pointer.
             * We will no longer need to refer to f0 and f1, so bdd_free them.  f will be
             * bdd_freed when the visited table is freed.
             */
            st_insert(gen->gen.nodes.visited, (refany) reg_f, NIL(any));
            gen->node = reg_f;
            cmu_bdd_free(mgr, (bdd) f0);
            cmu_bdd_free(mgr, (bdd) f1);
        }
    }
}