src/mdd/mdd_func2.c File Reference

#include "mdd.h"

Include dependency graph for mdd_func2.c:

Go to the source code of this file.

Functions
mdd_t *	mdd_func2 (mdd_manager *mgr, int mvar1, int mvar2, boolean(*func2)(int, int))
boolean	eq2 (int x, int y)
boolean	geq2 (int x, int y)
boolean	gt2 (int x, int y)
boolean	leq2 (int x, int y)
boolean	lt2 (int x, int y)
boolean	neq2 (int x, int y)
boolean	unary_minus2 (int x, int y)

---

Function Documentation

boolean eq2	(	int	x,
		int	y
	)

Definition at line 74 of file mdd_func2.c.

{
    return (x == y);
}

boolean geq2	(	int	x,
		int	y
	)

Definition at line 80 of file mdd_func2.c.

{
    return (x >= y);
}

boolean gt2	(	int	x,
		int	y
	)

Definition at line 86 of file mdd_func2.c.

{
    return (x > y);
}

boolean leq2	(	int	x,
		int	y
	)

Definition at line 92 of file mdd_func2.c.

{
    return (x <= y);
}

boolean lt2	(	int	x,
		int	y
	)

Definition at line 98 of file mdd_func2.c.

{
    return (x < y);
}

mdd_t* mdd_func2	(	mdd_manager *	mgr,
		int	mvar1,
		int	mvar2,
		boolean(*)(int, int)	func2
	)

Definition at line 19 of file mdd_func2.c.

{
    mvar_type x, y;
    array_t *child_list_x, *child_list_y;
    int i, j;
    mdd_t *tx, *ty;
    array_t *mvar_list = mdd_ret_mvar_list(mgr);
    mdd_t *one, *zero;

    one = mdd_one(mgr);
    zero = mdd_zero(mgr);

    x = array_fetch(mvar_type, mvar_list, mvar1);
    y = array_fetch(mvar_type, mvar_list, mvar2);

    if (x.status == MDD_BUNDLED) {
        (void) fprintf(stderr, 
                "\nWarning: mdd_func2, bundled variable %s is used\n", x.name);
        fail("");
    }

    if (y.status == MDD_BUNDLED) {
        (void) fprintf(stderr,
                "\nWarning: mdd_func2 bundled variable %s is used\n", y.name);
        fail("");
    }

    child_list_x = array_alloc(mdd_t *, 0);
    for (i=0; i<x.values; i++) {
        child_list_y = array_alloc(mdd_t *, 0);
        for (j=0; j<y.values; j++) {
            if (func2(i,j))
                array_insert_last(mdd_t *, child_list_y, one);
            else
                array_insert_last(mdd_t *, child_list_y, zero);
        }
        ty = mdd_case(mgr, mvar2, child_list_y);
        array_insert_last(mdd_t *, child_list_x, ty);
        array_free(child_list_y);
    }
    tx = mdd_case(mgr, mvar1, child_list_x);
    array_free(child_list_x);
    mdd_free(one);
    mdd_free(zero);
    return tx;
}

boolean neq2	(	int	x,
		int	y
	)

Definition at line 104 of file mdd_func2.c.

{
    return (x != y);
}

boolean unary_minus2	(	int	x,
		int	y
	)

Definition at line 110 of file mdd_func2.c.

{
    return (x+y == 0);
}