abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Macros | Typedefs | Functions | Variables
cuddEssent.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Data Structures

struct  DdTlcInfo
 
struct  TlClause
 

Macros

#define BPL   32
 
#define LOGBPL   5
 

Typedefs

typedef long BitVector
 
typedef struct TlClause TlClause
 

Functions

static DdNode * ddFindEssentialRecur (DdManager *dd, DdNode *f)
 
static DdTlcInfo * ddFindTwoLiteralClausesRecur (DdManager *dd, DdNode *f, st__table *table)
 
static DdTlcInfo * computeClauses (DdTlcInfo *Tres, DdTlcInfo *Eres, DdHalfWord label, int size)
 
static DdTlcInfo * computeClausesWithUniverse (DdTlcInfo *Cres, DdHalfWord label, short phase)
 
static DdTlcInfo * emptyClauseSet (void)
 
static int sentinelp (DdHalfWord var1, DdHalfWord var2)
 
static int equalp (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b)
 
static int beforep (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b)
 
static int oneliteralp (DdHalfWord var)
 
static int impliedp (DdHalfWord var1, short phase1, DdHalfWord var2, short phase2, BitVector *olv, BitVector *olp)
 
static BitVector * bitVectorAlloc (int size)
 
static DD_INLINE void bitVectorClear (BitVector *vector, int size)
 
static void bitVectorFree (BitVector *vector)
 
static DD_INLINE short bitVectorRead (BitVector *vector, int i)
 
static DD_INLINE void bitVectorSet (BitVector *vector, int i, short val)
 
static DdTlcInfo * tlcInfoAlloc (void)
 
DdNode * Cudd_FindEssential (DdManager *dd, DdNode *f)
 
int Cudd_bddIsVarEssential (DdManager *manager, DdNode *f, int id, int phase)
 
DdTlcInfo * Cudd_FindTwoLiteralClauses (DdManager *dd, DdNode *f)
 
int Cudd_ReadIthClause (DdTlcInfo *tlc, int i, DdHalfWord *var1, DdHalfWord *var2, int *phase1, int *phase2)
 
int Cudd_PrintTwoLiteralClauses (DdManager *dd, DdNode *f, char **names, FILE *fp)
 
void Cudd_tlcInfoFree (DdTlcInfo *t)
 

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddEssent.c,v 1.24 2009/02/21 18:24:10 fabio Exp $"
 
static BitVector * Tolv
 
static BitVector * Tolp
 
static BitVector * Eolv
 
static BitVector * Eolp
 

Macro Definition Documentation

#define BPL   32

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

FileName [cuddEssent.c]

PackageName [cudd]

Synopsis [Functions for the detection of essential variables.]

Description [External procedures included in this file:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 90 of file cuddEssent.c.

#define LOGBPL   5

Definition at line 91 of file cuddEssent.c.

Typedef Documentation

typedef long BitVector

Definition at line 142 of file cuddEssent.c.

typedef struct TlClause TlClause

Definition at line 143 of file cuddEssent.c.

Function Documentation

static int beforep ( DdHalfWord  var1a,
short  phase1a,
DdHalfWord  var1b,
short  phase1b,
DdHalfWord  var2a,
short  phase2a,
DdHalfWord  var2b,
short  phase2b 
)
static

Function********************************************************************

Synopsis [Returns true iff the first argument precedes the second in the clause order.]

Description [Returns true iff the first argument precedes the second in the clause order. A clause precedes another if its first lieral precedes the first literal of the other, or if the first literals are the same, and its second literal precedes the second literal of the other clause. A literal precedes another if it has a higher index, of if it has the same index, but it has lower phase. Phase 0 is the positive phase, and it is lower than Phase 1 (negative phase).]

SideEffects [None]

SeeAlso [equalp]

Definition at line 1233 of file cuddEssent.c.

1242 {
1243  return(var1a > var2a || (var1a == var2a &&
1244  (phase1a < phase2a || (phase1a == phase2a &&
1245  (var1b > var2b || (var1b == var2b && phase1b < phase2b))))));
1246 
1247 } /* end of beforep */
static BitVector * bitVectorAlloc ( int  size)
static

Function********************************************************************

Synopsis [Allocates a bit vector.]

Description [Allocates a bit vector. The parameter size gives the number of bits. This procedure allocates enough long's to hold the specified number of bits. Returns a pointer to the allocated vector if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [bitVectorClear bitVectorFree]

Definition at line 1319 of file cuddEssent.c.

1321 {
1322  int allocSize;
1323  BitVector *vector;
1324 
1325  /* Find out how many long's we need.
1326  ** There are sizeof(long) * 8 bits in a long.
1327  ** The ceiling of the ratio of two integers m and n is given
1328  ** by ((n-1)/m)+1. Putting all this together, we get... */
1329  allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1330  vector = ABC_ALLOC(BitVector, allocSize);
1331  if (vector == NULL) return(NULL);
1332  /* Clear the whole array. */
1333  (void) memset(vector, 0, allocSize * sizeof(BitVector));
1334  return(vector);
1335 
1336 } /* end of bitVectorAlloc */
memset
char * memset()
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
size
static int size
Definition: cuddSign.c:86
BitVector
long BitVector
Definition: cuddEssent.c:142
static DD_INLINE void bitVectorClear ( BitVector *  vector,
int  size 
)
static

Function********************************************************************

Synopsis [Clears a bit vector.]

Description [Clears a bit vector. The parameter size gives the number of bits.]

SideEffects [None]

SeeAlso [bitVectorAlloc]

Definition at line 1353 of file cuddEssent.c.

1356 {
1357  int allocSize;
1358 
1359  /* Find out how many long's we need.
1360  ** There are sizeof(long) * 8 bits in a long.
1361  ** The ceiling of the ratio of two integers m and n is given
1362  ** by ((n-1)/m)+1. Putting all this together, we get... */
1363  allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1364  /* Clear the whole array. */
1365  (void) memset(vector, 0, allocSize * sizeof(BitVector));
1366  return;
1367 
1368 } /* end of bitVectorClear */
memset
char * memset()
size
static int size
Definition: cuddSign.c:86
BitVector
long BitVector
Definition: cuddEssent.c:142
static void bitVectorFree ( BitVector *  vector)
static

Function********************************************************************

Synopsis [Frees a bit vector.]

Description [Frees a bit vector.]

SideEffects [None]

SeeAlso [bitVectorAlloc]

Definition at line 1383 of file cuddEssent.c.

1385 {
1386  ABC_FREE(vector);
1387 
1388 } /* end of bitVectorFree */
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
static DD_INLINE short bitVectorRead ( BitVector *  vector,
int  i 
)
static

Function********************************************************************

Synopsis [Returns the i-th entry of a bit vector.]

Description [Returns the i-th entry of a bit vector.]

SideEffects [None]

SeeAlso [bitVectorSet]

Definition at line 1404 of file cuddEssent.c.

1407 {
1408  int word, bit;
1409  short result;
1410 
1411  if (vector == NULL) return((short) 0);
1412 
1413  word = i >> LOGBPL;
1414  bit = i & (BPL - 1);
1415  result = (short) ((vector[word] >> bit) & 1L);
1416  return(result);
1417 
1418 } /* end of bitVectorRead */
LOGBPL
#define LOGBPL
Definition: cuddEssent.c:91
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
BPL
#define BPL
Definition: cuddEssent.c:90
result
static int result
Definition: cuddGenetic.c:125
static DD_INLINE void bitVectorSet ( BitVector *  vector,
int  i,
short  val 
)
static

Function********************************************************************

Synopsis [Sets the i-th entry of a bit vector to a value.]

Description [Sets the i-th entry of a bit vector to a value.]

SideEffects [None]

SeeAlso [bitVectorRead]

Definition at line 1434 of file cuddEssent.c.

1438 {
1439  int word, bit;
1440 
1441  word = i >> LOGBPL;
1442  bit = i & (BPL - 1);
1443  vector[word] &= ~(1L << bit);
1444  vector[word] |= (((long) val) << bit);
1445 
1446 } /* end of bitVectorSet */
LOGBPL
#define LOGBPL
Definition: cuddEssent.c:91
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
BPL
#define BPL
Definition: cuddEssent.c:90
static DdTlcInfo * computeClauses ( DdTlcInfo *  Tres,
DdTlcInfo *  Eres,
DdHalfWord  label,
int  size 
)
static

Function********************************************************************

Synopsis [Computes the two-literal clauses for a node.]

Description [Computes the two-literal clauses for a node given the clauses for its children and the label of the node. Returns a pointer to a TclInfo structure if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [computeClausesWithUniverse]

Definition at line 768 of file cuddEssent.c.

773 {
774  DdHalfWord *Tcv = Tres->vars; /* variables of clauses for the T child */
775  BitVector *Tcp = Tres->phases; /* phases of clauses for the T child */
776  DdHalfWord *Ecv = Eres->vars; /* variables of clauses for the E child */
777  BitVector *Ecp = Eres->phases; /* phases of clauses for the E child */
778  DdHalfWord *Vcv = NULL; /* pointer to variables of the clauses for v */
779  BitVector *Vcp = NULL; /* pointer to phases of the clauses for v */
780  DdTlcInfo *res = NULL; /* the set of clauses to be returned */
781  int pt = 0; /* index in the list of clauses of T */
782  int pe = 0; /* index in the list of clauses of E */
783  int cv = 0; /* counter of the clauses for this node */
784  TlClause *iclauses = NULL; /* list of inherited clauses */
785  TlClause *tclauses = NULL; /* list of 1-literal clauses of T */
786  TlClause *eclauses = NULL; /* list of 1-literal clauses of E */
787  TlClause *nclauses = NULL; /* list of new (non-inherited) clauses */
788  TlClause *lnclause = NULL; /* pointer to last new clause */
789  TlClause *newclause; /* temporary pointer to new clauses */
790 
791  /* Initialize sets of one-literal clauses. The one-literal clauses
792  ** are stored redundantly. These sets allow constant-time lookup, which
793  ** we need when we check for implication of a two-literal clause by a
794  ** one-literal clause. The linked lists allow fast sequential
795  ** processing. */
796  bitVectorClear(Tolv, size);
797  bitVectorClear(Tolp, size);
798  bitVectorClear(Eolv, size);
799  bitVectorClear(Eolp, size);
800 
801  /* Initialize result structure. */
802  res = tlcInfoAlloc();
803  if (res == NULL) goto cleanup;
804 
805  /* Scan the two input list. Extract inherited two-literal clauses
806  ** and set aside one-literal clauses from each list. The incoming lists
807  ** are sorted in the order defined by beforep. The three linked list
808  ** produced by this loop are sorted in the reverse order because we
809  ** always append to the front of the lists.
810  ** The inherited clauses are those clauses (both one- and two-literal)
811  ** that are common to both children; and the two-literal clauses of
812  ** one child that are implied by a one-literal clause of the other
813  ** child. */
814  while (!sentinelp(Tcv[pt], Tcv[pt+1]) || !sentinelp(Ecv[pe], Ecv[pe+1])) {
815  if (equalp(Tcv[pt], bitVectorRead(Tcp, pt),
816  Tcv[pt+1], bitVectorRead(Tcp, pt+1),
817  Ecv[pe], bitVectorRead(Ecp, pe),
818  Ecv[pe+1], bitVectorRead(Ecp, pe+1))) {
819  /* Add clause to inherited list. */
820  newclause = ABC_ALLOC(TlClause,1);
821  if (newclause == NULL) goto cleanup;
822  newclause->v1 = Tcv[pt];
823  newclause->v2 = Tcv[pt+1];
824  newclause->p1 = bitVectorRead(Tcp, pt);
825  newclause->p2 = bitVectorRead(Tcp, pt+1);
826  newclause->next = iclauses;
827  iclauses = newclause;
828  pt += 2; pe += 2; cv++;
829  } else if (beforep(Tcv[pt], bitVectorRead(Tcp, pt),
830  Tcv[pt+1], bitVectorRead(Tcp, pt+1),
831  Ecv[pe], bitVectorRead(Ecp, pe),
832  Ecv[pe+1], bitVectorRead(Ecp, pe+1))) {
833  if (oneliteralp(Tcv[pt+1])) {
834  /* Add this one-literal clause to the T set. */
835  newclause = ABC_ALLOC(TlClause,1);
836  if (newclause == NULL) goto cleanup;
837  newclause->v1 = Tcv[pt];
838  newclause->v2 = CUDD_MAXINDEX;
839  newclause->p1 = bitVectorRead(Tcp, pt);
840  newclause->p2 = 1;
841  newclause->next = tclauses;
842  tclauses = newclause;
843  bitVectorSet(Tolv, Tcv[pt], 1);
844  bitVectorSet(Tolp, Tcv[pt], bitVectorRead(Tcp, pt));
845  } else {
846  if (impliedp(Tcv[pt], bitVectorRead(Tcp, pt),
847  Tcv[pt+1], bitVectorRead(Tcp, pt+1),
848  Eolv, Eolp)) {
849  /* Add clause to inherited list. */
850  newclause = ABC_ALLOC(TlClause,1);
851  if (newclause == NULL) goto cleanup;
852  newclause->v1 = Tcv[pt];
853  newclause->v2 = Tcv[pt+1];
854  newclause->p1 = bitVectorRead(Tcp, pt);
855  newclause->p2 = bitVectorRead(Tcp, pt+1);
856  newclause->next = iclauses;
857  iclauses = newclause;
858  cv++;
859  }
860  }
861  pt += 2;
862  } else { /* !beforep() */
863  if (oneliteralp(Ecv[pe+1])) {
864  /* Add this one-literal clause to the E set. */
865  newclause = ABC_ALLOC(TlClause,1);
866  if (newclause == NULL) goto cleanup;
867  newclause->v1 = Ecv[pe];
868  newclause->v2 = CUDD_MAXINDEX;
869  newclause->p1 = bitVectorRead(Ecp, pe);
870  newclause->p2 = 1;
871  newclause->next = eclauses;
872  eclauses = newclause;
873  bitVectorSet(Eolv, Ecv[pe], 1);
874  bitVectorSet(Eolp, Ecv[pe], bitVectorRead(Ecp, pe));
875  } else {
876  if (impliedp(Ecv[pe], bitVectorRead(Ecp, pe),
877  Ecv[pe+1], bitVectorRead(Ecp, pe+1),
878  Tolv, Tolp)) {
879  /* Add clause to inherited list. */
880  newclause = ABC_ALLOC(TlClause,1);
881  if (newclause == NULL) goto cleanup;
882  newclause->v1 = Ecv[pe];
883  newclause->v2 = Ecv[pe+1];
884  newclause->p1 = bitVectorRead(Ecp, pe);
885  newclause->p2 = bitVectorRead(Ecp, pe+1);
886  newclause->next = iclauses;
887  iclauses = newclause;
888  cv++;
889  }
890  }
891  pe += 2;
892  }
893  }
894 
895  /* Add one-literal clauses for the label variable to the front of
896  ** the two lists. */
897  newclause = ABC_ALLOC(TlClause,1);
898  if (newclause == NULL) goto cleanup;
899  newclause->v1 = label;
900  newclause->v2 = CUDD_MAXINDEX;
901  newclause->p1 = 0;
902  newclause->p2 = 1;
903  newclause->next = tclauses;
904  tclauses = newclause;
905  newclause = ABC_ALLOC(TlClause,1);
906  if (newclause == NULL) goto cleanup;
907  newclause->v1 = label;
908  newclause->v2 = CUDD_MAXINDEX;
909  newclause->p1 = 1;
910  newclause->p2 = 1;
911  newclause->next = eclauses;
912  eclauses = newclause;
913 
914  /* Produce the non-inherited clauses. We preserve the "reverse"
915  ** order of the two input lists by appending to the end of the
916  ** list. In this way, iclauses and nclauses are consistent. */
917  while (tclauses != NULL && eclauses != NULL) {
918  if (beforep(eclauses->v1, eclauses->p1, eclauses->v2, eclauses->p2,
919  tclauses->v1, tclauses->p1, tclauses->v2, tclauses->p2)) {
920  TlClause *nextclause = tclauses->next;
921  TlClause *otherclauses = eclauses;
922  while (otherclauses != NULL) {
923  if (tclauses->v1 != otherclauses->v1) {
924  newclause = ABC_ALLOC(TlClause,1);
925  if (newclause == NULL) goto cleanup;
926  newclause->v1 = tclauses->v1;
927  newclause->v2 = otherclauses->v1;
928  newclause->p1 = tclauses->p1;
929  newclause->p2 = otherclauses->p1;
930  newclause->next = NULL;
931  if (nclauses == NULL) {
932  nclauses = newclause;
933  lnclause = newclause;
934  } else {
935  lnclause->next = newclause;
936  lnclause = newclause;
937  }
938  cv++;
939  }
940  otherclauses = otherclauses->next;
941  }
942  ABC_FREE(tclauses);
943  tclauses = nextclause;
944  } else {
945  TlClause *nextclause = eclauses->next;
946  TlClause *otherclauses = tclauses;
947  while (otherclauses != NULL) {
948  if (eclauses->v1 != otherclauses->v1) {
949  newclause = ABC_ALLOC(TlClause,1);
950  if (newclause == NULL) goto cleanup;
951  newclause->v1 = eclauses->v1;
952  newclause->v2 = otherclauses->v1;
953  newclause->p1 = eclauses->p1;
954  newclause->p2 = otherclauses->p1;
955  newclause->next = NULL;
956  if (nclauses == NULL) {
957  nclauses = newclause;
958  lnclause = newclause;
959  } else {
960  lnclause->next = newclause;
961  lnclause = newclause;
962  }
963  cv++;
964  }
965  otherclauses = otherclauses->next;
966  }
967  ABC_FREE(eclauses);
968  eclauses = nextclause;
969  }
970  }
971  while (tclauses != NULL) {
972  TlClause *nextclause = tclauses->next;
973  ABC_FREE(tclauses);
974  tclauses = nextclause;
975  }
976  while (eclauses != NULL) {
977  TlClause *nextclause = eclauses->next;
978  ABC_FREE(eclauses);
979  eclauses = nextclause;
980  }
981 
982  /* Merge inherited and non-inherited clauses. Now that we know the
983  ** total number, we allocate the arrays, and we fill them bottom-up
984  ** to restore the proper ordering. */
985  Vcv = ABC_ALLOC(DdHalfWord, 2*(cv+1));
986  if (Vcv == NULL) goto cleanup;
987  if (cv > 0) {
988  Vcp = bitVectorAlloc(2*cv);
989  if (Vcp == NULL) goto cleanup;
990  } else {
991  Vcp = NULL;
992  }
993  res->vars = Vcv;
994  res->phases = Vcp;
995  /* Add sentinel. */
996  Vcv[2*cv] = 0;
997  Vcv[2*cv+1] = 0;
998  while (iclauses != NULL || nclauses != NULL) {
999  TlClause *nextclause;
1000  cv--;
1001  if (nclauses == NULL || (iclauses != NULL &&
1002  beforep(nclauses->v1, nclauses->p1, nclauses->v2, nclauses->p2,
1003  iclauses->v1, iclauses->p1, iclauses->v2, iclauses->p2))) {
1004  Vcv[2*cv] = iclauses->v1;
1005  Vcv[2*cv+1] = iclauses->v2;
1006  bitVectorSet(Vcp, 2*cv, iclauses->p1);
1007  bitVectorSet(Vcp, 2*cv+1, iclauses->p2);
1008  nextclause = iclauses->next;
1009  ABC_FREE(iclauses);
1010  iclauses = nextclause;
1011  } else {
1012  Vcv[2*cv] = nclauses->v1;
1013  Vcv[2*cv+1] = nclauses->v2;
1014  bitVectorSet(Vcp, 2*cv, nclauses->p1);
1015  bitVectorSet(Vcp, 2*cv+1, nclauses->p2);
1016  nextclause = nclauses->next;
1017  ABC_FREE(nclauses);
1018  nclauses = nextclause;
1019  }
1020  }
1021  assert(cv == 0);
1022 
1023  return(res);
1024 
1025  cleanup:
1026  if (res != NULL) Cudd_tlcInfoFree(res);
1027  while (iclauses != NULL) {
1028  TlClause *nextclause = iclauses->next;
1029  ABC_FREE(iclauses);
1030  iclauses = nextclause;
1031  }
1032  while (nclauses != NULL) {
1033  TlClause *nextclause = nclauses->next;
1034  ABC_FREE(nclauses);
1035  nclauses = nextclause;
1036  }
1037  while (tclauses != NULL) {
1038  TlClause *nextclause = tclauses->next;
1039  ABC_FREE(tclauses);
1040  tclauses = nextclause;
1041  }
1042  while (eclauses != NULL) {
1043  TlClause *nextclause = eclauses->next;
1044  ABC_FREE(eclauses);
1045  eclauses = nextclause;
1046  }
1047 
1048  return(NULL);
1049 
1050 } /* end of computeClauses */
TlClause::p2
short p2
Definition: cuddEssent.c:134
DdHalfWord
unsigned short DdHalfWord
Definition: cudd.h:262
TlClause::v2
DdHalfWord v2
Definition: cuddEssent.c:133
bitVectorSet
static DD_INLINE void bitVectorSet(BitVector *vector, int i, short val)
Definition: cuddEssent.c:1434
TlClause::v1
DdHalfWord v1
Definition: cuddEssent.c:133
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
tlcInfoAlloc
static DdTlcInfo * tlcInfoAlloc(void)
Definition: cuddEssent.c:1462
impliedp
static int impliedp(DdHalfWord var1, short phase1, DdHalfWord var2, short phase2, BitVector *olv, BitVector *olp)
Definition: cuddEssent.c:1288
TlClause::p1
short p1
Definition: cuddEssent.c:134
Eolv
static BitVector * Eolv
Definition: cuddEssent.c:155
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
Tolp
static BitVector * Tolp
Definition: cuddEssent.c:154
Tolv
static BitVector * Tolv
Definition: cuddEssent.c:153
beforep
static int beforep(DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b)
Definition: cuddEssent.c:1233
size
static int size
Definition: cuddSign.c:86
Cudd_tlcInfoFree
void Cudd_tlcInfoFree(DdTlcInfo *t)
Definition: cuddEssent.c:455
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
TlClause::next
struct TlClause * next
Definition: cuddEssent.c:135
sentinelp
static int sentinelp(DdHalfWord var1, DdHalfWord var2)
Definition: cuddEssent.c:1174
bitVectorClear
static DD_INLINE void bitVectorClear(BitVector *vector, int size)
Definition: cuddEssent.c:1353
CUDD_MAXINDEX
#define CUDD_MAXINDEX
Definition: cudd.h:112
BitVector
long BitVector
Definition: cuddEssent.c:142
assert
#define assert(ex)
Definition: util_old.h:213
Eolp
static BitVector * Eolp
Definition: cuddEssent.c:156
equalp
static int equalp(DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b)
Definition: cuddEssent.c:1197
bitVectorRead
static DD_INLINE short bitVectorRead(BitVector *vector, int i)
Definition: cuddEssent.c:1404
bitVectorAlloc
static BitVector * bitVectorAlloc(int size)
Definition: cuddEssent.c:1319
oneliteralp
static int oneliteralp(DdHalfWord var)
Definition: cuddEssent.c:1265
static DdTlcInfo * computeClausesWithUniverse ( DdTlcInfo *  Cres,
DdHalfWord  label,
short  phase 
)
static

Function********************************************************************

Synopsis [Computes the two-literal clauses for a node.]

Description [Computes the two-literal clauses for a node with a zero child, given the clauses for its other child and the label of the node. Returns a pointer to a TclInfo structure if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [computeClauses]

Definition at line 1068 of file cuddEssent.c.

1072 {
1073  DdHalfWord *Ccv = Cres->vars; /* variables of clauses for child */
1074  BitVector *Ccp = Cres->phases; /* phases of clauses for child */
1075  DdHalfWord *Vcv = NULL; /* pointer to the variables of the clauses for v */
1076  BitVector *Vcp = NULL; /* pointer to the phases of the clauses for v */
1077  DdTlcInfo *res = NULL; /* the set of clauses to be returned */
1078  int i;
1079 
1080  /* Initialize result. */
1081  res = tlcInfoAlloc();
1082  if (res == NULL) goto cleanup;
1083  /* Count entries for new list and allocate accordingly. */
1084  for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2);
1085  /* At this point, i is twice the number of clauses in the child's
1086  ** list. We need four more entries for this node: 2 for the one-literal
1087  ** clause for the label, and 2 for the sentinel. */
1088  Vcv = ABC_ALLOC(DdHalfWord,i+4);
1089  if (Vcv == NULL) goto cleanup;
1090  Vcp = bitVectorAlloc(i+4);
1091  if (Vcp == NULL) goto cleanup;
1092  res->vars = Vcv;
1093  res->phases = Vcp;
1094  /* Copy old list into new. */
1095  for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2) {
1096  Vcv[i] = Ccv[i];
1097  Vcv[i+1] = Ccv[i+1];
1098  bitVectorSet(Vcp, i, bitVectorRead(Ccp, i));
1099  bitVectorSet(Vcp, i+1, bitVectorRead(Ccp, i+1));
1100  }
1101  /* Add clause corresponding to label. */
1102  Vcv[i] = label;
1103  bitVectorSet(Vcp, i, phase);
1104  i++;
1105  Vcv[i] = CUDD_MAXINDEX;
1106  bitVectorSet(Vcp, i, 1);
1107  i++;
1108  /* Add sentinel. */
1109  Vcv[i] = 0;
1110  Vcv[i+1] = 0;
1111  bitVectorSet(Vcp, i, 0);
1112  bitVectorSet(Vcp, i+1, 0);
1113 
1114  return(res);
1115 
1116  cleanup:
1117  /* Vcp is guaranteed to be NULL here. Hence, we do not try to free it. */
1118  if (Vcv != NULL) ABC_FREE(Vcv);
1119  if (res != NULL) Cudd_tlcInfoFree(res);
1120 
1121  return(NULL);
1122 
1123 } /* end of computeClausesWithUniverse */
DdHalfWord
unsigned short DdHalfWord
Definition: cudd.h:262
bitVectorSet
static DD_INLINE void bitVectorSet(BitVector *vector, int i, short val)
Definition: cuddEssent.c:1434
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
tlcInfoAlloc
static DdTlcInfo * tlcInfoAlloc(void)
Definition: cuddEssent.c:1462
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
Cudd_tlcInfoFree
void Cudd_tlcInfoFree(DdTlcInfo *t)
Definition: cuddEssent.c:455
phase
static pcube phase
Definition: cvrm.c:405
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
sentinelp
static int sentinelp(DdHalfWord var1, DdHalfWord var2)
Definition: cuddEssent.c:1174
CUDD_MAXINDEX
#define CUDD_MAXINDEX
Definition: cudd.h:112
BitVector
long BitVector
Definition: cuddEssent.c:142
bitVectorRead
static DD_INLINE short bitVectorRead(BitVector *vector, int i)
Definition: cuddEssent.c:1404
bitVectorAlloc
static BitVector * bitVectorAlloc(int size)
Definition: cuddEssent.c:1319
int Cudd_bddIsVarEssential ( DdManager *  manager,
DdNode *  f,
int  id,
int  phase 
)

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]

Definition at line 239 of file cuddEssent.c.

244 {
245  DdNode *var;
246  int res;
247 
248  var = Cudd_bddIthVar(manager, id);
249 
250  var = Cudd_NotCond(var,phase == 0);
251 
252  res = Cudd_bddLeq(manager, f, var);
253 
254  return(res);
255 
256 } /* end of Cudd_bddIsVarEssential */
DdNode
Definition: cudd.h:278
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
phase
static pcube phase
Definition: cvrm.c:405
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode* Cudd_FindEssential ( DdManager *  dd,
DdNode *  f 
)

AutomaticEnd 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]

Definition at line 209 of file cuddEssent.c.

212 {
213  DdNode *res;
214 
215  do {
216  dd->reordered = 0;
217  res = ddFindEssentialRecur(dd,f);
218  } while (dd->reordered == 1);
219  return(res);
220 
221 } /* end of Cudd_FindEssential */
DdNode
Definition: cudd.h:278
DdManager::reordered
int reordered
Definition: cuddInt.h:409
ddFindEssentialRecur
static DdNode * ddFindEssentialRecur(DdManager *dd, DdNode *f)
Definition: cuddEssent.c:486
DdTlcInfo* Cudd_FindTwoLiteralClauses ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Finds the two literal clauses of a DD.]

Description [Returns the one- and two-literal clauses of a DD. Returns a pointer to the structure holding the clauses if successful; NULL otherwise. For a constant DD, the empty set of clauses is returned. This is obviously correct for a non-zero constant. For the constant zero, it is based on the assumption that only those clauses containing variables in the support of the function are considered. Since the support of a constant function is empty, no clauses are returned.]

SideEffects [None]

SeeAlso [Cudd_FindEssential]

Definition at line 277 of file cuddEssent.c.

280 {
281  DdTlcInfo *res;
282  st__table *table;
283  st__generator *gen;
284  DdTlcInfo *tlc;
285  DdNode *node;
286  int size = dd->size;
287 
288  if (Cudd_IsConstant(f)) {
289  res = emptyClauseSet();
290  return(res);
291  }
292  table = st__init_table( st__ptrcmp, st__ptrhash);
293  if (table == NULL) return(NULL);
294  Tolv = bitVectorAlloc(size);
295  if (Tolv == NULL) {
296  st__free_table(table);
297  return(NULL);
298  }
299  Tolp = bitVectorAlloc(size);
300  if (Tolp == NULL) {
301  st__free_table(table);
302  bitVectorFree(Tolv);
303  return(NULL);
304  }
305  Eolv = bitVectorAlloc(size);
306  if (Eolv == NULL) {
307  st__free_table(table);
308  bitVectorFree(Tolv);
309  bitVectorFree(Tolp);
310  return(NULL);
311  }
312  Eolp = bitVectorAlloc(size);
313  if (Eolp == NULL) {
314  st__free_table(table);
315  bitVectorFree(Tolv);
316  bitVectorFree(Tolp);
317  bitVectorFree(Eolv);
318  return(NULL);
319  }
320 
321  res = ddFindTwoLiteralClausesRecur(dd,f,table);
322  /* Dispose of table contents and free table. */
323  st__foreach_item(table, gen, (const char **)&node, (char **)&tlc) {
324  if (node != f) {
325  Cudd_tlcInfoFree(tlc);
326  }
327  }
328  st__free_table(table);
329  bitVectorFree(Tolv);
330  bitVectorFree(Tolp);
331  bitVectorFree(Eolv);
332  bitVectorFree(Eolp);
333 
334  if (res != NULL) {
335  int i;
336  for (i = 0; !sentinelp(res->vars[i], res->vars[i+1]); i += 2);
337  res->cnt = i >> 1;
338  }
339 
340  return(res);
341 
342 } /* end of Cudd_FindTwoLiteralClauses */
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
DdNode
Definition: cudd.h:278
DdManager::size
int size
Definition: cuddInt.h:361
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
Eolv
static BitVector * Eolv
Definition: cuddEssent.c:155
Tolp
static BitVector * Tolp
Definition: cuddEssent.c:154
st__table
Definition: st.h:52
emptyClauseSet
static DdTlcInfo * emptyClauseSet(void)
Definition: cuddEssent.c:1140
Tolv
static BitVector * Tolv
Definition: cuddEssent.c:153
size
static int size
Definition: cuddSign.c:86
ddFindTwoLiteralClausesRecur
static DdTlcInfo * ddFindTwoLiteralClausesRecur(DdManager *dd, DdNode *f, st__table *table)
Definition: cuddEssent.c:620
Cudd_tlcInfoFree
void Cudd_tlcInfoFree(DdTlcInfo *t)
Definition: cuddEssent.c:455
bitVectorFree
static void bitVectorFree(BitVector *vector)
Definition: cuddEssent.c:1383
DdTlcInfo::cnt
DdHalfWord cnt
Definition: cuddEssent.c:125
sentinelp
static int sentinelp(DdHalfWord var1, DdHalfWord var2)
Definition: cuddEssent.c:1174
st__foreach_item
#define st__foreach_item(table, gen, key, value)
Definition: st.h:107
Eolp
static BitVector * Eolp
Definition: cuddEssent.c:156
bitVectorAlloc
static BitVector * bitVectorAlloc(int size)
Definition: cuddEssent.c:1319
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468
st__generator
Definition: st.h:64
int Cudd_PrintTwoLiteralClauses ( DdManager *  dd,
DdNode *  f,
char **  names,
FILE *  fp 
)

Function********************************************************************

Synopsis [Prints the two literal clauses of a DD.]

Description [Prints the one- and two-literal clauses. Returns 1 if successful; 0 otherwise. The argument "names" can be NULL, in which case the variable indices are printed.]

SideEffects [None]

SeeAlso [Cudd_FindTwoLiteralClauses]

Definition at line 393 of file cuddEssent.c.

398 {
399  DdHalfWord *vars;
400  BitVector *phases;
401  int i;
402  DdTlcInfo *res = Cudd_FindTwoLiteralClauses(dd, f);
403  FILE *ifp = fp == NULL ? dd->out : fp;
404 
405  if (res == NULL) return(0);
406  vars = res->vars;
407  phases = res->phases;
408  for (i = 0; !sentinelp(vars[i], vars[i+1]); i += 2) {
409  if (names != NULL) {
410  if (vars[i+1] == CUDD_MAXINDEX) {
411  (void) fprintf(ifp, "%s%s\n",
412  bitVectorRead(phases, i) ? "~" : " ",
413  names[vars[i]]);
414  } else {
415  (void) fprintf(ifp, "%s%s | %s%s\n",
416  bitVectorRead(phases, i) ? "~" : " ",
417  names[vars[i]],
418  bitVectorRead(phases, i+1) ? "~" : " ",
419  names[vars[i+1]]);
420  }
421  } else {
422  if (vars[i+1] == CUDD_MAXINDEX) {
423  (void) fprintf(ifp, "%s%d\n",
424  bitVectorRead(phases, i) ? "~" : " ",
425  (int) vars[i]);
426  } else {
427  (void) fprintf(ifp, "%s%d | %s%d\n",
428  bitVectorRead(phases, i) ? "~" : " ",
429  (int) vars[i],
430  bitVectorRead(phases, i+1) ? "~" : " ",
431  (int) vars[i+1]);
432  }
433  }
434  }
435  Cudd_tlcInfoFree(res);
436 
437  return(1);
438 
439 } /* end of Cudd_PrintTwoLiteralClauses */
DdHalfWord
unsigned short DdHalfWord
Definition: cudd.h:262
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
Cudd_FindTwoLiteralClauses
DdTlcInfo * Cudd_FindTwoLiteralClauses(DdManager *dd, DdNode *f)
Definition: cuddEssent.c:277
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
DdManager::out
FILE * out
Definition: cuddInt.h:441
Cudd_tlcInfoFree
void Cudd_tlcInfoFree(DdTlcInfo *t)
Definition: cuddEssent.c:455
sentinelp
static int sentinelp(DdHalfWord var1, DdHalfWord var2)
Definition: cuddEssent.c:1174
CUDD_MAXINDEX
#define CUDD_MAXINDEX
Definition: cudd.h:112
BitVector
long BitVector
Definition: cuddEssent.c:142
bitVectorRead
static DD_INLINE short bitVectorRead(BitVector *vector, int i)
Definition: cuddEssent.c:1404
int Cudd_ReadIthClause ( DdTlcInfo *  tlc,
int  i,
DdHalfWord *  var1,
DdHalfWord *  var2,
int *  phase1,
int *  phase2 
)

Function********************************************************************

Synopsis [Accesses the i-th clause of a DD.]

Description [Accesses the i-th clause of a DD given the clause set which must be already computed. Returns 1 if successful; 0 if i is out of range, or in case of error.]

SideEffects [the four components of a clause are returned as side effects.]

SeeAlso [Cudd_FindTwoLiteralClauses]

Definition at line 359 of file cuddEssent.c.

366 {
367  if (tlc == NULL) return(0);
368  if (tlc->vars == NULL || tlc->phases == NULL) return(0);
369  if (i < 0 || (unsigned) i >= tlc->cnt) return(0);
370  *var1 = tlc->vars[2*i];
371  *var2 = tlc->vars[2*i+1];
372  *phase1 = (int) bitVectorRead(tlc->phases, 2*i);
373  *phase2 = (int) bitVectorRead(tlc->phases, 2*i+1);
374  return(1);
375 
376 } /* end of Cudd_ReadIthClause */
var1
static const int var1
Definition: satSolver.c:77
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
DdTlcInfo::cnt
DdHalfWord cnt
Definition: cuddEssent.c:125
bitVectorRead
static DD_INLINE short bitVectorRead(BitVector *vector, int i)
Definition: cuddEssent.c:1404
void Cudd_tlcInfoFree ( DdTlcInfo *  t)

Function********************************************************************

Synopsis [Frees a DdTlcInfo Structure.]

Description [Frees a DdTlcInfo Structure as well as the memory pointed by it.]

SideEffects [None]

SeeAlso []

Definition at line 455 of file cuddEssent.c.

457 {
458  if (t->vars != NULL) ABC_FREE(t->vars);
459  if (t->phases != NULL) ABC_FREE(t->phases);
460  ABC_FREE(t);
461 
462 } /* end of Cudd_tlcInfoFree */
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
static DdNode * ddFindEssentialRecur ( DdManager *  dd,
DdNode *  f 
)
static

AutomaticStart

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]

Definition at line 486 of file cuddEssent.c.

489 {
490  DdNode *T, *E, *F;
491  DdNode *essT, *essE, *res;
492  int index;
493  DdNode *one, *lzero, *azero;
494 
495  one = DD_ONE(dd);
496  F = Cudd_Regular(f);
497  /* If f is constant the set of essential variables is empty. */
498  if (cuddIsConstant(F)) return(one);
499 
500  res = cuddCacheLookup1(dd,Cudd_FindEssential,f);
501  if (res != NULL) {
502  return(res);
503  }
504 
505  lzero = Cudd_Not(one);
506  azero = DD_ZERO(dd);
507  /* Find cofactors: here f is non-constant. */
508  T = cuddT(F);
509  E = cuddE(F);
510  if (Cudd_IsComplement(f)) {
511  T = Cudd_Not(T); E = Cudd_Not(E);
512  }
513 
514  index = F->index;
515  if (Cudd_IsConstant(T) && T != lzero && T != azero) {
516  /* if E is zero, index is essential, otherwise there are no
517  ** essentials, because index is not essential and no other variable
518  ** can be, since setting index = 1 makes the function constant and
519  ** different from 0.
520  */
521  if (E == lzero || E == azero) {
522  res = dd->vars[index];
523  } else {
524  res = one;
525  }
526  } else if (T == lzero || T == azero) {
527  if (Cudd_IsConstant(E)) { /* E cannot be zero here */
528  res = Cudd_Not(dd->vars[index]);
529  } else { /* E == non-constant */
530  /* find essentials in the else branch */
531  essE = ddFindEssentialRecur(dd,E);
532  if (essE == NULL) {
533  return(NULL);
534  }
535  cuddRef(essE);
536 
537  /* add index to the set with negative phase */
538  res = cuddUniqueInter(dd,index,one,Cudd_Not(essE));
539  if (res == NULL) {
540  Cudd_RecursiveDeref(dd,essE);
541  return(NULL);
542  }
543  res = Cudd_Not(res);
544  cuddDeref(essE);
545  }
546  } else { /* T == non-const */
547  if (E == lzero || E == azero) {
548  /* find essentials in the then branch */
549  essT = ddFindEssentialRecur(dd,T);
550  if (essT == NULL) {
551  return(NULL);
552  }
553  cuddRef(essT);
554 
555  /* add index to the set with positive phase */
556  /* use And because essT may be complemented */
557  res = cuddBddAndRecur(dd,dd->vars[index],essT);
558  if (res == NULL) {
559  Cudd_RecursiveDeref(dd,essT);
560  return(NULL);
561  }
562  cuddDeref(essT);
563  } else if (!Cudd_IsConstant(E)) {
564  /* if E is a non-zero constant there are no essentials
565  ** because T is non-constant.
566  */
567  essT = ddFindEssentialRecur(dd,T);
568  if (essT == NULL) {
569  return(NULL);
570  }
571  if (essT == one) {
572  res = one;
573  } else {
574  cuddRef(essT);
575  essE = ddFindEssentialRecur(dd,E);
576  if (essE == NULL) {
577  Cudd_RecursiveDeref(dd,essT);
578  return(NULL);
579  }
580  cuddRef(essE);
581 
582  /* res = intersection(essT, essE) */
583  res = cuddBddLiteralSetIntersectionRecur(dd,essT,essE);
584  if (res == NULL) {
585  Cudd_RecursiveDeref(dd,essT);
586  Cudd_RecursiveDeref(dd,essE);
587  return(NULL);
588  }
589  cuddRef(res);
590  Cudd_RecursiveDeref(dd,essT);
591  Cudd_RecursiveDeref(dd,essE);
592  cuddDeref(res);
593  }
594  } else { /* E is a non-zero constant */
595  res = one;
596  }
597  }
598 
599  cuddCacheInsert1(dd,Cudd_FindEssential, f, res);
600  return(res);
601 
602 } /* end of ddFindEssentialRecur */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
ddFindEssentialRecur
static DdNode * ddFindEssentialRecur(DdManager *dd, DdNode *f)
Definition: cuddEssent.c:486
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
cuddBddLiteralSetIntersectionRecur
DdNode * cuddBddLiteralSetIntersectionRecur(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddLiteral.c:153
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:556
one
static DdNode * one
Definition: cuddDecomp.c:112
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdNode::index
DdHalfWord index
Definition: cudd.h:279
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Cudd_FindEssential
DdNode * Cudd_FindEssential(DdManager *dd, DdNode *f)
Definition: cuddEssent.c:209
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
static DdTlcInfo * ddFindTwoLiteralClausesRecur ( DdManager *  dd,
DdNode *  f,
st__table *  table 
)
static

Function********************************************************************

Synopsis [Implements the recursive step of Cudd_FindTwoLiteralClauses.]

Description [Implements the recursive step of Cudd_FindTwoLiteralClauses. The DD node is assumed to be not constant. Returns a pointer to a set of clauses if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_FindTwoLiteralClauses]

Definition at line 620 of file cuddEssent.c.

624 {
625  DdNode *T, *E, *F;
626  DdNode *one, *lzero, *azero;
627  DdTlcInfo *res, *Tres, *Eres;
628  DdHalfWord index;
629 
630  F = Cudd_Regular(f);
631 
632  assert(!cuddIsConstant(F));
633 
634  /* Check computed table. Separate entries are necessary for
635  ** a node and its complement. We should update the counter here. */
636  if ( st__lookup(table, (const char *)f, (char **)&res)) {
637  return(res);
638  }
639 
640  /* Easy access to the constants for BDDs and ADDs. */
641  one = DD_ONE(dd);
642  lzero = Cudd_Not(one);
643  azero = DD_ZERO(dd);
644 
645  /* Find cofactors and variable labeling the top node. */
646  T = cuddT(F); E = cuddE(F);
647  if (Cudd_IsComplement(f)) {
648  T = Cudd_Not(T); E = Cudd_Not(E);
649  }
650  index = F->index;
651 
652  if (Cudd_IsConstant(T) && T != lzero && T != azero) {
653  /* T is a non-zero constant. If E is zero, then this node's index
654  ** is a one-literal clause. Otherwise, if E is a non-zero
655  ** constant, there are no clauses for this node. Finally,
656  ** if E is not constant, we recursively compute its clauses, and then
657  ** merge using the empty set for T. */
658  if (E == lzero || E == azero) {
659  /* Create the clause (index + 0). */
660  res = tlcInfoAlloc();
661  if (res == NULL) return(NULL);
662  res->vars = ABC_ALLOC(DdHalfWord,4);
663  if (res->vars == NULL) {
664  ABC_FREE(res);
665  return(NULL);
666  }
667  res->phases = bitVectorAlloc(2);
668  if (res->phases == NULL) {
669  ABC_FREE(res->vars);
670  ABC_FREE(res);
671  return(NULL);
672  }
673  res->vars[0] = index;
674  res->vars[1] = CUDD_MAXINDEX;
675  res->vars[2] = 0;
676  res->vars[3] = 0;
677  bitVectorSet(res->phases, 0, 0); /* positive phase */
678  bitVectorSet(res->phases, 1, 1); /* negative phase */
679  } else if (Cudd_IsConstant(E)) {
680  /* If E is a non-zero constant, no clauses. */
681  res = emptyClauseSet();
682  } else {
683  /* E is non-constant */
684  Tres = emptyClauseSet();
685  if (Tres == NULL) return(NULL);
686  Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
687  if (Eres == NULL) {
688  Cudd_tlcInfoFree(Tres);
689  return(NULL);
690  }
691  res = computeClauses(Tres, Eres, index, dd->size);
692  Cudd_tlcInfoFree(Tres);
693  }
694  } else if (T == lzero || T == azero) {
695  /* T is zero. If E is a non-zero constant, then the
696  ** complement of this node's index is a one-literal clause.
697  ** Otherwise, if E is not constant, we recursively compute its
698  ** clauses, and then merge using the universal set for T. */
699  if (Cudd_IsConstant(E)) { /* E cannot be zero here */
700  /* Create the clause (!index + 0). */
701  res = tlcInfoAlloc();
702  if (res == NULL) return(NULL);
703  res->vars = ABC_ALLOC(DdHalfWord,4);
704  if (res->vars == NULL) {
705  ABC_FREE(res);
706  return(NULL);
707  }
708  res->phases = bitVectorAlloc(2);
709  if (res->phases == NULL) {
710  ABC_FREE(res->vars);
711  ABC_FREE(res);
712  return(NULL);
713  }
714  res->vars[0] = index;
715  res->vars[1] = CUDD_MAXINDEX;
716  res->vars[2] = 0;
717  res->vars[3] = 0;
718  bitVectorSet(res->phases, 0, 1); /* negative phase */
719  bitVectorSet(res->phases, 1, 1); /* negative phase */
720  } else { /* E == non-constant */
721  Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
722  if (Eres == NULL) return(NULL);
723  res = computeClausesWithUniverse(Eres, index, 1);
724  }
725  } else { /* T == non-const */
726  Tres = ddFindTwoLiteralClausesRecur(dd, T, table);
727  if (Tres == NULL) return(NULL);
728  if (Cudd_IsConstant(E)) {
729  if (E == lzero || E == azero) {
730  res = computeClausesWithUniverse(Tres, index, 0);
731  } else {
732  Eres = emptyClauseSet();
733  if (Eres == NULL) return(NULL);
734  res = computeClauses(Tres, Eres, index, dd->size);
735  Cudd_tlcInfoFree(Eres);
736  }
737  } else {
738  Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
739  if (Eres == NULL) return(NULL);
740  res = computeClauses(Tres, Eres, index, dd->size);
741  }
742  }
743 
744  /* Cache results. */
745  if ( st__add_direct(table, (char *)f, (char *)res) == st__OUT_OF_MEM) {
746  ABC_FREE(res);
747  return(NULL);
748  }
749  return(res);
750 
751 } /* end of ddFindTwoLiteralClausesRecur */
computeClausesWithUniverse
static DdTlcInfo * computeClausesWithUniverse(DdTlcInfo *Cres, DdHalfWord label, short phase)
Definition: cuddEssent.c:1068
DdHalfWord
unsigned short DdHalfWord
Definition: cudd.h:262
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
DdManager::size
int size
Definition: cuddInt.h:361
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
bitVectorSet
static DD_INLINE void bitVectorSet(BitVector *vector, int i, short val)
Definition: cuddEssent.c:1434
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
tlcInfoAlloc
static DdTlcInfo * tlcInfoAlloc(void)
Definition: cuddEssent.c:1462
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
one
static DdNode * one
Definition: cuddDecomp.c:112
emptyClauseSet
static DdTlcInfo * emptyClauseSet(void)
Definition: cuddEssent.c:1140
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
ddFindTwoLiteralClausesRecur
static DdTlcInfo * ddFindTwoLiteralClausesRecur(DdManager *dd, DdNode *f, st__table *table)
Definition: cuddEssent.c:620
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
st__OUT_OF_MEM
#define st__OUT_OF_MEM
Definition: st.h:113
Cudd_tlcInfoFree
void Cudd_tlcInfoFree(DdTlcInfo *t)
Definition: cuddEssent.c:455
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
CUDD_MAXINDEX
#define CUDD_MAXINDEX
Definition: cudd.h:112
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
st__add_direct
int st__add_direct(st__table *table, char *key, char *value)
Definition: st.c:205
assert
#define assert(ex)
Definition: util_old.h:213
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
computeClauses
static DdTlcInfo * computeClauses(DdTlcInfo *Tres, DdTlcInfo *Eres, DdHalfWord label, int size)
Definition: cuddEssent.c:768
bitVectorAlloc
static BitVector * bitVectorAlloc(int size)
Definition: cuddEssent.c:1319
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
static DdTlcInfo * emptyClauseSet ( void  )
static

Function********************************************************************

Synopsis [Returns an enpty set of clauses.]

Description [Returns a pointer to an empty set of clauses if successful; NULL otherwise. No bit vector for the phases is allocated.]

SideEffects [None]

SeeAlso []

Definition at line 1140 of file cuddEssent.c.

1141 {
1142  DdTlcInfo *eset;
1143 
1144  eset = ABC_ALLOC(DdTlcInfo,1);
1145  if (eset == NULL) return(NULL);
1146  eset->vars = ABC_ALLOC(DdHalfWord,2);
1147  if (eset->vars == NULL) {
1148  ABC_FREE(eset);
1149  return(NULL);
1150  }
1151  /* Sentinel */
1152  eset->vars[0] = 0;
1153  eset->vars[1] = 0;
1154  eset->phases = NULL; /* does not matter */
1155  eset->cnt = 0;
1156  return(eset);
1157 
1158 } /* end of emptyClauseSet */
DdHalfWord
unsigned short DdHalfWord
Definition: cudd.h:262
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdTlcInfo::cnt
DdHalfWord cnt
Definition: cuddEssent.c:125
static int equalp ( DdHalfWord  var1a,
short  phase1a,
DdHalfWord  var1b,
short  phase1b,
DdHalfWord  var2a,
short  phase2a,
DdHalfWord  var2b,
short  phase2b 
)
static

Function********************************************************************

Synopsis [Returns true iff the two arguments are identical clauses.]

Description [Returns true iff the two arguments are identical clauses. Since literals are sorted, we only need to compare literals in the same position.]

SideEffects [None]

SeeAlso [beforep]

Definition at line 1197 of file cuddEssent.c.

1206 {
1207  return(var1a == var2a && phase1a == phase2a &&
1208  var1b == var2b && phase1b == phase2b);
1209 
1210 } /* end of equalp */
static int impliedp ( DdHalfWord  var1,
short  phase1,
DdHalfWord  var2,
short  phase2,
BitVector *  olv,
BitVector *  olp 
)
static

Function********************************************************************

Synopsis [Returns true iff either literal of a clause is in a set of literals.]

Description [Returns true iff either literal of a clause is in a set of literals. The first four arguments specify the clause. The remaining two arguments specify the literal set.]

SideEffects [None]

SeeAlso []

Definition at line 1288 of file cuddEssent.c.

1295 {
1296  return((bitVectorRead(olv, var1) &&
1297  bitVectorRead(olp, var1) == phase1) ||
1298  (bitVectorRead(olv, var2) &&
1299  bitVectorRead(olp, var2) == phase2));
1300 
1301 } /* end of impliedp */
var1
static const int var1
Definition: satSolver.c:77
bitVectorRead
static DD_INLINE short bitVectorRead(BitVector *vector, int i)
Definition: cuddEssent.c:1404
static int oneliteralp ( DdHalfWord  var)
static

Function********************************************************************

Synopsis [Returns true iff the argument is a one-literal clause.]

Description [Returns true iff the argument is a one-literal clause. A one-litaral clause has the constant FALSE as second literal. Since the constant TRUE is never used, it is sufficient to test for a constant.]

SideEffects [None]

SeeAlso []

Definition at line 1265 of file cuddEssent.c.

1267 {
1268  return(var == CUDD_MAXINDEX);
1269 
1270 } /* end of oneliteralp */
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
CUDD_MAXINDEX
#define CUDD_MAXINDEX
Definition: cudd.h:112
static int sentinelp ( DdHalfWord  var1,
DdHalfWord  var2 
)
static

Function********************************************************************

Synopsis [Returns true iff the argument is the sentinel clause.]

Description [Returns true iff the argument is the sentinel clause. A sentinel clause has both variables equal to 0.]

SideEffects [None]

SeeAlso []

Definition at line 1174 of file cuddEssent.c.

1177 {
1178  return(var1 == 0 && var2 == 0);
1179 
1180 } /* end of sentinelp */
var1
static const int var1
Definition: satSolver.c:77
static DdTlcInfo * tlcInfoAlloc ( void  )
static

Function********************************************************************

Synopsis [Allocates a DdTlcInfo Structure.]

Description [Returns a pointer to a DdTlcInfo Structure if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_tlcInfoFree]

Definition at line 1462 of file cuddEssent.c.

1463 {
1464  DdTlcInfo *res = ABC_ALLOC(DdTlcInfo,1);
1465  if (res == NULL) return(NULL);
1466  res->vars = NULL;
1467  res->phases = NULL;
1468  res->cnt = 0;
1469  return(res);
1470 
1471 } /* end of tlcInfoAlloc */
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
DdTlcInfo::phases
long * phases
Definition: cuddEssent.c:124
DdTlcInfo::cnt
DdHalfWord cnt
Definition: cuddEssent.c:125

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddEssent.c,v 1.24 2009/02/21 18:24:10 fabio Exp $"
static

Definition at line 150 of file cuddEssent.c.

BitVector* Eolp
static

Definition at line 156 of file cuddEssent.c.

BitVector* Eolv
static

Definition at line 155 of file cuddEssent.c.

BitVector* Tolp
static

Definition at line 154 of file cuddEssent.c.

BitVector* Tolv
static

Definition at line 153 of file cuddEssent.c.