summaryrefslogtreecommitdiffstats
path: root/abc70930/src/bdd/cudd/cuddEssent.c
diff options
context:
space:
mode:
Diffstat (limited to 'abc70930/src/bdd/cudd/cuddEssent.c')
-rw-r--r--abc70930/src/bdd/cudd/cuddEssent.c279
1 files changed, 279 insertions, 0 deletions
diff --git a/abc70930/src/bdd/cudd/cuddEssent.c b/abc70930/src/bdd/cudd/cuddEssent.c
new file mode 100644
index 00000000..db4b8b49
--- /dev/null
+++ b/abc70930/src/bdd/cudd/cuddEssent.c
@@ -0,0 +1,279 @@
+/**CFile***********************************************************************
+
+ FileName [cuddEssent.c]
+
+ PackageName [cudd]
+
+ Synopsis [Functions for the detection of essential variables.]
+
+ Description [External procedures included in this file:
+ <ul>
+ <li> Cudd_FindEssential()
+ <li> Cudd_bddIsVarEssential()
+ </ul>
+ Static procedures included in this module:
+ <ul>
+ <li> ddFindEssentialRecur()
+ </ul>]
+
+ Author [Fabio Somenzi]
+
+ Copyright [This file was created at the University of Colorado at
+ Boulder. The University of Colorado at Boulder makes no warranty
+ about the suitability of this software for any purpose. It is
+ presented on an AS IS basis.]
+
+******************************************************************************/
+
+#include "util_hack.h"
+#include "cuddInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] DD_UNUSED = "$Id: cuddEssent.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+static DdNode * ddFindEssentialRecur ARGS((DdManager *dd, DdNode *f));
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Finds the essential variables of a DD.]
+
+ Description [Returns the cube of the essential variables. A positive
+ literal means that the variable must be set to 1 for the function to be
+ 1. A negative literal means that the variable must be set to 0 for the
+ function to be 1. Returns a pointer to the cube BDD if successful;
+ NULL otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_bddIsVarEssential]
+
+******************************************************************************/
+DdNode *
+Cudd_FindEssential(
+ DdManager * dd,
+ DdNode * f)
+{
+ DdNode *res;
+
+ do {
+ dd->reordered = 0;
+ res = ddFindEssentialRecur(dd,f);
+ } while (dd->reordered == 1);
+ return(res);
+
+} /* end of Cudd_FindEssential */
+
+
+/**Function********************************************************************
+
+ Synopsis [Determines whether a given variable is essential with a
+ given phase in a BDD.]
+
+ Description [Determines whether a given variable is essential with a
+ given phase in a BDD. Uses Cudd_bddIteConstant. Returns 1 if phase == 1
+ and f-->x_id, or if phase == 0 and f-->x_id'.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_FindEssential]
+
+******************************************************************************/
+int
+Cudd_bddIsVarEssential(
+ DdManager * manager,
+ DdNode * f,
+ int id,
+ int phase)
+{
+ DdNode *var;
+ int res;
+ DdNode *one, *zero;
+
+ one = DD_ONE(manager);
+ zero = Cudd_Not(one);
+
+ var = cuddUniqueInter(manager, id, one, zero);
+
+ var = Cudd_NotCond(var,phase == 0);
+
+ res = Cudd_bddIteConstant(manager, Cudd_Not(f), one, var) == one;
+
+ return(res);
+
+} /* end of Cudd_bddIsVarEssential */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Implements the recursive step of Cudd_FindEssential.]
+
+ Description [Implements the recursive step of Cudd_FindEssential.
+ Returns a pointer to the cube BDD if successful; NULL otherwise.]
+
+ SideEffects [None]
+
+******************************************************************************/
+static DdNode *
+ddFindEssentialRecur(
+ DdManager * dd,
+ DdNode * f)
+{
+ DdNode *T, *E, *F;
+ DdNode *essT, *essE, *res;
+ int index;
+ DdNode *one, *lzero, *azero;
+
+ one = DD_ONE(dd);
+ F = Cudd_Regular(f);
+ /* If f is constant the set of essential variables is empty. */
+ if (cuddIsConstant(F)) return(one);
+
+ res = cuddCacheLookup1(dd,Cudd_FindEssential,f);
+ if (res != NULL) {
+ return(res);
+ }
+
+ lzero = Cudd_Not(one);
+ azero = DD_ZERO(dd);
+ /* Find cofactors: here f is non-constant. */
+ T = cuddT(F);
+ E = cuddE(F);
+ if (Cudd_IsComplement(f)) {
+ T = Cudd_Not(T); E = Cudd_Not(E);
+ }
+
+ index = F->index;
+ if (Cudd_IsConstant(T) && T != lzero && T != azero) {
+ /* if E is zero, index is essential, otherwise there are no
+ ** essentials, because index is not essential and no other variable
+ ** can be, since setting index = 1 makes the function constant and
+ ** different from 0.
+ */
+ if (E == lzero || E == azero) {
+ res = dd->vars[index];
+ } else {
+ res = one;
+ }
+ } else if (T == lzero || T == azero) {
+ if (Cudd_IsConstant(E)) { /* E cannot be zero here */
+ res = Cudd_Not(dd->vars[index]);
+ } else { /* E == non-constant */
+ /* find essentials in the else branch */
+ essE = ddFindEssentialRecur(dd,E);
+ if (essE == NULL) {
+ return(NULL);
+ }
+ cuddRef(essE);
+
+ /* add index to the set with negative phase */
+ res = cuddUniqueInter(dd,index,one,Cudd_Not(essE));
+ if (res == NULL) {
+ Cudd_RecursiveDeref(dd,essE);
+ return(NULL);
+ }
+ res = Cudd_Not(res);
+ cuddDeref(essE);
+ }
+ } else { /* T == non-const */
+ if (E == lzero || E == azero) {
+ /* find essentials in the then branch */
+ essT = ddFindEssentialRecur(dd,T);
+ if (essT == NULL) {
+ return(NULL);
+ }
+ cuddRef(essT);
+
+ /* add index to the set with positive phase */
+ /* use And because essT may be complemented */
+ res = cuddBddAndRecur(dd,dd->vars[index],essT);
+ if (res == NULL) {
+ Cudd_RecursiveDeref(dd,essT);
+ return(NULL);
+ }
+ cuddDeref(essT);
+ } else if (!Cudd_IsConstant(E)) {
+ /* if E is a non-zero constant there are no essentials
+ ** because T is non-constant.
+ */
+ essT = ddFindEssentialRecur(dd,T);
+ if (essT == NULL) {
+ return(NULL);
+ }
+ if (essT == one) {
+ res = one;
+ } else {
+ cuddRef(essT);
+ essE = ddFindEssentialRecur(dd,E);
+ if (essE == NULL) {
+ Cudd_RecursiveDeref(dd,essT);
+ return(NULL);
+ }
+ cuddRef(essE);
+
+ /* res = intersection(essT, essE) */
+ res = cuddBddLiteralSetIntersectionRecur(dd,essT,essE);
+ if (res == NULL) {
+ Cudd_RecursiveDeref(dd,essT);
+ Cudd_RecursiveDeref(dd,essE);
+ return(NULL);
+ }
+ cuddRef(res);
+ Cudd_RecursiveDeref(dd,essT);
+ Cudd_RecursiveDeref(dd,essE);
+ cuddDeref(res);
+ }
+ } else { /* E is a non-zero constant */
+ res = one;
+ }
+ }
+
+ cuddCacheInsert1(dd,Cudd_FindEssential, f, res);
+ return(res);
+
+} /* end of ddFindEssentialRecur */
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 00:00:54 +0000