/**CFile**********************************************************************
FileName [dddmpStoreCnf.c]
PackageName [dddmp]
Synopsis [Functions to write out BDDs to file in a CNF format]
Description [Functions to write out BDDs to file in a CNF format.]
Author [Gianpiero Cabodi and Stefano Quer]
Copyright [
Copyright (c) 2004 by Politecnico di Torino.
All Rights Reserved. This software is for educational purposes only.
Permission is given to academic institutions to use, copy, and modify
this software and its documentation provided that this introductory
message is not removed, that this software and its documentation is
used for the institutions' internal research and educational purposes,
and that no monies are exchanged. No guarantee is expressed or implied
by the distribution of this code.
Send bug-reports and/or questions to:
{gianpiero.cabodi,stefano.quer}@polito.it.
]
******************************************************************************/
#include <limits.h>
#include "dddmpInt.h"
/*-------------------------------1--------------------------------------------*/
/* Stucture declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Type declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
#define DDDMP_DEBUG_CNF 0
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
#define GET_MAX(x,y) (x>y?x:y)
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
static int DddmpCuddBddArrayStoreCnf(DdManager *ddMgr, DdNode **f, int rootN, Dddmp_DecompCnfStoreType mode, int noHeader, char **varNames, int *bddIds, int *bddAuxIds, int *cnfIds, int idInitial, int edgeInTh, int pathLengthTh, char *fname, FILE *fp, int *clauseNPtr, int *varNewNPtr);
static int StoreCnfNodeByNode(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, FILE *fp, int *clauseN, int *varMax, int *rootStartLine);
static int StoreCnfNodeByNodeRecur(DdManager *ddMgr, DdNode *f, int *bddIds, int *cnfIds, FILE *fp, int *clauseN, int *varMax);
static int StoreCnfOneNode(DdNode *f, int idf, int vf, int idT, int idE, FILE *fp, int *clauseN, int *varMax);
static int StoreCnfMaxtermByMaxterm(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, int idInitial, FILE *fp, int *varMax, int *clauseN, int *rootStartLine);
static int StoreCnfBest(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, int idInitial, FILE *fp, int *varMax, int *clauseN, int *rootStartLine);
static void StoreCnfMaxtermByMaxtermRecur(DdManager *ddMgr, DdNode *node, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
static int StoreCnfBestNotSharedRecur(DdManager *ddMgr, DdNode *node, int idf, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
static int StoreCnfBestSharedRecur(DdManager *ddMgr, DdNode *node, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
static int printCubeCnf(DdManager *ddMgr, DdNode *node, int *cnfIds, FILE *fp, int *list, int *varMax);
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Writes a dump file representing the argument BDD in
a CNF format.
]
Description [Dumps the argument BDD to file.
This task is performed by calling the function
Dddmp_cuddBddArrayStoreCnf.
]
SideEffects [Nodes are temporarily removed from unique hash. They are
re-linked after the store operation in a modified order.
]
SeeAlso [Dddmp_cuddBddArrayStoreCnf]
******************************************************************************/
int
Dddmp_cuddBddStoreCnf (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *f /* IN: BDD root to be stored */,
Dddmp_DecompCnfStoreType mode /* IN: format selection */,
int noHeader /* IN: do not store header iff 1 */,
char **varNames /* IN: array of variable names (or NULL) */,
int *bddIds /* IN: array of var ids */,
int *bddAuxIds /* IN: array of BDD node Auxiliary Ids */,
int *cnfIds /* IN: array of CNF var ids */,
int idInitial /* IN: starting id for cutting variables */,
int edgeInTh /* IN: Max # Incoming Edges */,
int pathLengthTh /* IN: Max Path Length */,
char *fname /* IN: file name */,
FILE *fp /* IN: pointer to the store file */,
int *clauseNPtr /* OUT: number of clause stored */,
int *varNewNPtr /* OUT: number of new variable created */
)
{
int retValue;
DdNode *tmpArray[1];
tmpArray[0] = f;
retValue = Dddmp_cuddBddArrayStoreCnf (ddMgr, tmpArray, 1, mode,
noHeader, varNames, bddIds, bddAuxIds, cnfIds, idInitial, edgeInTh,
pathLengthTh, fname, fp, clauseNPtr, varNewNPtr);
Dddmp_CheckAndReturn (retValue==DDDMP_FAILURE, "Failure.");
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Writes a dump file representing the argument array of BDDs
in CNF format.
]
Description [Dumps the argument array of BDDs to file.]
SideEffects [Nodes are temporarily removed from the unique hash
table. They are re-linked after the store operation in a
modified order.
Three methods are allowed:
* NodeByNode method: Insert a cut-point for each BDD node (but the
terminal nodes)
* MaxtermByMaxterm method: Insert no cut-points, i.e. the off-set of
trhe function is stored
* Best method: Tradeoff between the previous two methods.
Auxiliary variables, i.e., cut points are inserted following these
criterias:
* edgeInTh
indicates the maximum number of incoming edges up to which
no cut point (auxiliary variable) is inserted.
If edgeInTh:
* is equal to -1 no cut point due to incoming edges are inserted
(MaxtermByMaxterm method.)
* is equal to 0 a cut point is inserted for each node with a single
incoming edge, i.e., each node, (NodeByNode method).
* is equal to n a cut point is inserted for each node with (n+1)
incoming edges.
* pathLengthTh
indicates the maximum length path up to which no cut points
(auxiliary variable) is inserted.
If the path length between two nodes exceeds this value, a cut point
is inserted.
If pathLengthTh:
* is equal to -1 no cut point due path length are inserted
(MaxtermByMaxterm method.)
* is equal to 0 a cut point is inserted for each node (NodeByNode
method).
* is equal to n a cut point is inserted on path whose length is
equal to (n+1).
Notice that the maximum number of literals in a clause is equal
to (pathLengthTh + 2), i.e., for each path we have to keep into
account a CNF variable for each node plus 2 added variables for
the bottom and top-path cut points.
The stored file can contain a file header or not depending on the
noHeader parameter (IFF 0, usual setting, the header is usually stored.
This option can be useful in storing multiple BDDs, as separate BDDs,
on the same file leaving the opening of the file to the caller.
]
SeeAlso []
******************************************************************************/
int
Dddmp_cuddBddArrayStoreCnf (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDD roots to be stored */,
int rootN /* IN: # output BDD roots to be stored */,
Dddmp_DecompCnfStoreType mode /* IN: format selection */,
int noHeader /* IN: do not store header iff 1 */,
char **varNames /* IN: array of variable names (or NULL) */,
int *bddIds /* IN: array of converted var IDs */,
int *bddAuxIds /* IN: array of BDD node Auxiliary Ids */,
int *cnfIds /* IN: array of converted var IDs */,
int idInitial /* IN: starting id for cutting variables */,
int edgeInTh /* IN: Max # Incoming Edges */,
int pathLengthTh /* IN: Max Path Length */,
char *fname /* IN: file name */,
FILE *fp /* IN: pointer to the store file */,
int *clauseNPtr /* OUT: number of clause stored */,
int *varNewNPtr /* OUT: number of new variable created */
)
{
int retValue2;
#if 0
#ifdef DDDMP_DEBUG
#ifndef __alpha__
int retValue1;
retValue1 = Cudd_DebugCheck (ddMgr);
Dddmp_CheckAndReturn (retValue1==1,
"Inconsistency Found During CNF Store.");
Dddmp_CheckAndReturn (retValue1==CUDD_OUT_OF_MEM,
"Out of Memory During CNF Store.");
#endif
#endif
#endif
retValue2 = DddmpCuddBddArrayStoreCnf (ddMgr, f, rootN, mode, noHeader,
varNames, bddIds, bddAuxIds, cnfIds, idInitial, edgeInTh, pathLengthTh,
fname, fp, clauseNPtr, varNewNPtr);
#if 0
#ifdef DDDMP_DEBUG
#ifndef __alpha__
retValue1 = Cudd_DebugCheck (ddMgr);
Dddmp_CheckAndReturn (retValue1==1,
"Inconsistency Found During CNF Store.");
Dddmp_CheckAndReturn (retValue1==CUDD_OUT_OF_MEM,
"Out of Memory During CNF Store.");
#endif
#endif
#endif
return (retValue2);
}
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Writes a dump file representing the argument Array of
BDDs in the CNF standard format.
]
Description [Dumps the argument array of BDDs/ADDs to file in CNF format.
The following arrays: varNames, bddIds, bddAuxIds, and cnfIds
fix the correspondence among variable names, BDD ids, BDD
auxiliary ids and the ids used to store the CNF problem.
All these arrays are automatically created iff NULL.
Auxiliary variable, iff necessary, are created starting from value
idInitial.
Iff idInitial is <= 0 its value is selected as the number of internal
CUDD variable + 2.
Auxiliary variables, i.e., cut points are inserted following these
criterias:
* edgeInTh
indicates the maximum number of incoming edges up to which
no cut point (auxiliary variable) is inserted.
If edgeInTh:
* is equal to -1 no cut point due to incoming edges are inserted
(MaxtermByMaxterm method.)
* is equal to 0 a cut point is inserted for each node with a single
incoming edge, i.e., each node, (NodeByNode method).
* is equal to n a cut point is inserted for each node with (n+1)
incoming edges.
* pathLengthTh
indicates the maximum length path up to which no cut points
(auxiliary variable) is inserted.
If the path length between two nodes exceeds this value, a cut point
is inserted.
If pathLengthTh:
* is equal to -1 no cut point due path length are inserted
(MaxtermByMaxterm method.)
* is equal to 0 a cut point is inserted for each node (NodeByNode
method).
* is equal to n a cut point is inserted on path whose length is
equal to (n+1).
Notice that the maximum number of literals in a clause is equal
to (pathLengthTh + 2), i.e., for each path we have to keep into
account a CNF variable for each node plus 2 added variables for
the bottom and top-path cut points.
]
SideEffects [Nodes are temporarily removed from the unique hash table.
They are re-linked after the store operation in a modified
order.
]
SeeAlso [Dddmp_cuddBddStore]
******************************************************************************/
static int
DddmpCuddBddArrayStoreCnf (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDD roots to be stored */,
int rootN /* IN: # of output BDD roots to be stored */,
Dddmp_DecompCnfStoreType mode /* IN: format selection */,
int noHeader /* IN: do not store header iff 1 */,
char **varNames /* IN: array of variable names (or NULL) */,
int *bddIds /* IN: array of BDD node Ids (or NULL) */,
int *bddAuxIds /* IN: array of BDD Aux Ids (or NULL) */,
int *cnfIds /* IN: array of CNF ids (or NULL) */,
int idInitial /* IN: starting id for cutting variables */,
int edgeInTh /* IN: Max # Incoming Edges */,
int pathLengthTh /* IN: Max Path Length */,
char *fname /* IN: file name */,
FILE *fp /* IN: pointer to the store file */,
int *clauseNPtr /* OUT: number of clause stored */,
int *varNewNPtr /* OUT: number of new variable created */
)
{
DdNode *support = NULL;
DdNode *scan = NULL;
int *bddIdsInSupport = NULL;
int *permIdsInSupport = NULL;
int *rootStartLine = NULL;
int nVar, nVarInSupport, retValue, i, j, fileToClose;
int varMax, clauseN, flagVar, intStringLength;
int bddIdsToFree = 0;
int bddAuxIdsToFree = 0;
int cnfIdsToFree = 0;
int varNamesToFree = 0;
char intString[DDDMP_MAXSTRLEN];
char tmpString[DDDMP_MAXSTRLEN];
fpos_t posFile1, posFile2;
/*---------------------------- Set Initial Values -------------------------*/
support = scan = NULL;
bddIdsInSupport = permIdsInSupport = rootStartLine = NULL;
nVar = ddMgr->size;
fileToClose = 0;
sprintf (intString, "%d", INT_MAX);
intStringLength = strlen (intString);
/*---------- Check if File needs to be opened in the proper mode ----------*/
if (fp == NULL) {
fp = fopen (fname, "w");
Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
failure);
fileToClose = 1;
}
/*--------- Generate Bdd LOCAL IDs and Perm IDs and count them ------------*/
/* BDD Ids */
bddIdsInSupport = DDDMP_ALLOC (int, nVar);
Dddmp_CheckAndGotoLabel (bddIdsInSupport==NULL, "Error allocating memory.",
failure);
/* BDD PermIds */
permIdsInSupport = DDDMP_ALLOC (int, nVar);
Dddmp_CheckAndGotoLabel (permIdsInSupport==NULL, "Error allocating memory.",
failure);
/* Support Size (Number of BDD Ids-PermIds */
nVarInSupport = 0;
for (i=0; i<nVar; i++) {
bddIdsInSupport[i] = permIdsInSupport[i] = (-1);
}
/*
* Take the union of the supports of each output function.
* Skip NULL functions.
*/
for (i=0; i<rootN; i++) {
if (f[i] == NULL) {
continue;
}
support = Cudd_Support (ddMgr, f[i]);
Dddmp_CheckAndGotoLabel (support==NULL, "NULL support returned.",
failure);
cuddRef (support);
scan = support;
while (!cuddIsConstant(scan)) {
/* Count Number of Variable in the Support */
nVarInSupport++;
/* Set Ids and Perm-Ids */
bddIdsInSupport[scan->index] = scan->index;
permIdsInSupport[scan->index] = ddMgr->perm[scan->index];
scan = cuddT (scan);
}
Cudd_RecursiveDeref (ddMgr, support);
}
/* so that we do not try to free it in case of failure */
support = NULL;
/*---------------------------- Start HEADER -------------------------------*/
if (noHeader==0) {
retValue = fprintf (fp,
"c # BDD stored by the DDDMP tool in CNF format\n");
Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing on file.",
failure);
fprintf (fp, "c #\n");
}
/*-------------------- Generate Bdd IDs IFF necessary ---------------------*/
if (bddIds == NULL) {
if (noHeader==0) {
fprintf (fp, "c # Warning: BDD IDs missing ... evaluating them.\n");
fprintf (fp, "c # \n");
fflush (fp);
}
bddIdsToFree = 1;
bddIds = DDDMP_ALLOC (int, nVar);
Dddmp_CheckAndGotoLabel (bddIds==NULL, "Error allocating memory.",
failure);
/* Get BDD-IDs Directly from Cudd Manager */
for (i=0; i<nVar; i++) {
bddIds[i] = i;
}
} /* end if bddIds == NULL */
/*------------------ Generate AUX BDD IDs IF necessary --------------------*/
if (bddAuxIds == NULL) {
if (noHeader==0) {
fprintf (fp, "c # Warning: AUX IDs missing ... equal to BDD IDs.\n");
fprintf (fp, "c #\n");
fflush (fp);
}
bddAuxIdsToFree = 1;
bddAuxIds = DDDMP_ALLOC (int, nVar);
Dddmp_CheckAndGotoLabel (bddAuxIds==NULL, "Error allocating memory.",
failure);
for (i=0; i<nVar; i++) {
bddAuxIds[i] = bddIds[i];
}
} /* end if cnfIds == NULL */
/*------------------- Generate CNF IDs IF necessary -----------------------*/
if (cnfIds == NULL) {
if (noHeader==0) {
fprintf (fp, "c # Warning: CNF IDs missing ... equal to BDD IDs.\n");
fprintf (fp, "c #\n");
fflush (fp);
}
cnfIdsToFree = 1;
cnfIds = DDDMP_ALLOC (int, nVar);
Dddmp_CheckAndGotoLabel (cnfIds==NULL, "Error allocating memory.",
failure);
for (i=0; i<nVar; i++) {
cnfIds[i] = bddIds[i] + 1;
}
} /* end if cnfIds == NULL */
/*------------------ Generate Var Names IF necessary ----------------------*/
flagVar = 0;
if (varNames == NULL) {
if (noHeader==0) {
fprintf (fp,
"c # Warning: null variable names ... create DUMMY names.\n");
fprintf (fp, "c #\n");
fflush (stderr);
}
varNamesToFree = 1;
varNames = DDDMP_ALLOC (char *, nVar);
for (i=0; i<nVar; i++) {
varNames[i] = NULL;
}
Dddmp_CheckAndGotoLabel (varNames==NULL, "Error allocating memory.",
failure);
flagVar = 1;
} else {
/* Protect the user also from partially loaded varNames array !!! */
for (i=0; i<nVar && flagVar==0; i++) {
if (varNames[i] == NULL) {
flagVar = 1;
}
}
}
if (flagVar == 1) {
for (i=0; i<nVar; i++) {
if (varNames[i] == NULL) {
sprintf (tmpString, "DUMMY%d", bddIds[i]);
varNames[i] = DDDMP_ALLOC (char, (strlen (tmpString)+1));
strcpy (varNames[i], tmpString);
}
}
}
/*----------------------- Set Initial ID IF necessary --------------------*/
if (idInitial <= 0) {
idInitial = nVar + 1;
}
/*--------------------------- Continue HEADER -----------------------------*/
if (noHeader==0) {
fprintf (fp, "c .ver %s\n", DDDMP_VERSION);
fprintf (fp, "c .nnodes %d\n", Cudd_SharingSize (f, rootN));
fprintf (fp, "c .nvars %d\n", nVar);
fprintf (fp, "c .nsuppvars %d\n", nVarInSupport);
/* Support Variable Names */
if (varNames != NULL) {
fprintf (fp, "c .suppvarnames");
for (i=0; i<nVar; i++) {
if (bddIdsInSupport[i] >= 0) {
fprintf (fp, " %s", varNames[i]);
}
}
fprintf (fp, "\n");
}
/* Ordered Variable Names */
if (varNames != NULL) {
fprintf (fp, "c .orderedvarnames");
for (i=0; i<nVar; i++) {
fprintf (fp, " %s", varNames[i]);
}
fprintf (fp, "\n");
}
/* BDD Variable Ids */
fprintf (fp, "c .ids ");
for (i=0; i<nVar; i++) {
if (bddIdsInSupport[i] >= 0) {
fprintf (fp, " %d", bddIdsInSupport[i]);
}
}
fprintf (fp, "\n");
/* BDD Variable Permutation Ids */
fprintf (fp, "c .permids ");
for (i=0; i<nVar; i++) {
if (bddIdsInSupport[i] >= 0) {
fprintf (fp, " %d", permIdsInSupport[i]);
}
}
fprintf (fp, "\n");
/* BDD Variable Auxiliary Ids */
fprintf (fp, "c .auxids ");
for (i=0; i<nVar; i++) {
if (bddIdsInSupport[i] >= 0) {
fprintf (fp, " %d", bddAuxIds[i]);
}
}
fprintf (fp, "\n");
/* CNF Ids */
fprintf (fp, "c .cnfids ");
for (i=0; i<nVar; i++) {
if (bddIdsInSupport[i] >= 0) {
fprintf (fp, " %d", cnfIds[i]);
}
}
fprintf (fp, "\n");
/* Number of Roots */
fprintf (fp, "c .nroots %d", rootN);
fprintf (fp, "\n");
/* Root Starting Line */
fgetpos (fp, &posFile1);
fprintf (fp, "c .rootids");
for (i=0; i<rootN; i++) {
for (j=0; j<intStringLength+1; j++) {
retValue = fprintf (fp, " ");
}
}
retValue = fprintf (fp, "\n");
fflush (fp);
} /* End of noHeader check */
/*------------ Select Mode and Print Number of Tmp Var Created ------------*/
switch (mode) {
case DDDMP_CNF_MODE_NODE:
*varNewNPtr = idInitial;
*varNewNPtr = DddmpNumberDdNodesCnf (ddMgr, f, rootN, cnfIds, idInitial)
- *varNewNPtr;
break;
case DDDMP_CNF_MODE_MAXTERM:
*varNewNPtr = 0;
break;
default:
Dddmp_Warning (1, "Wrong DDDMP Store Mode. Force DDDMP_MODE_BEST.");
case DDDMP_CNF_MODE_BEST:
*varNewNPtr = idInitial;
*varNewNPtr = DddmpDdNodesCountEdgesAndNumber (ddMgr, f, rootN,
edgeInTh, pathLengthTh, cnfIds, idInitial) - *varNewNPtr;
break;
}
/*------------ Print Space for Number of Variable and Clauses -------------*/
if (noHeader==0) {
fprintf (fp, "c .nAddedCnfVar %d\n", *varNewNPtr);
fprintf (fp, "c #\n");
fprintf (fp, "c # Init CNF Clauses\n");
fprintf (fp, "c #\n");
fgetpos (fp, &posFile2);
retValue = fprintf (fp, "p cnf");
for (j=0; j<2*(intStringLength+1); j++) {
retValue = fprintf (fp, " ");
}
retValue = fprintf (fp, "\n");
fflush (fp);
}
/*---------------------- Select Mode and Do the Job -----------------------*/
clauseN = 0;
varMax = -1;
rootStartLine = DDDMP_ALLOC (int, rootN);
Dddmp_CheckAndGotoLabel (rootStartLine==NULL, "Error allocating memory.",
failure);
for (i=0; i<rootN; i++) {
rootStartLine[i] = (-1);
}
switch (mode) {
case DDDMP_CNF_MODE_NODE:
StoreCnfNodeByNode (ddMgr, f, rootN, bddIds, cnfIds, fp, &clauseN,
&varMax, rootStartLine);
DddmpUnnumberDdNodesCnf (ddMgr, f, rootN);
break;
case DDDMP_CNF_MODE_MAXTERM:
StoreCnfMaxtermByMaxterm (ddMgr, f, rootN, bddIds, cnfIds, idInitial,
fp, &varMax, &clauseN, rootStartLine);
break;
default:
Dddmp_Warning (1, "Wrong DDDMP Store Mode. Force DDDMP_MODE_BEST.");
case DDDMP_CNF_MODE_BEST:
StoreCnfBest (ddMgr, f, rootN, bddIds, cnfIds, idInitial,
fp, &varMax, &clauseN, rootStartLine);
DddmpUnnumberDdNodesCnf (ddMgr, f, rootN);
break;
}
/*------------------------------ Write trailer ----------------------------*/
if (noHeader==0) {
retValue = fprintf (fp, "c # End of Cnf From dddmp-2.0\n");
Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
failure);
}
/*
* Write Root Starting Line
*/
if (noHeader==0) {
fsetpos (fp, &posFile1);
fprintf (fp, "c .rootids");
for (i=0; i<rootN; i++) {
Dddmp_Warning (rootStartLine[i]==(-1),
"Init Line for CNF file = (-1) {[(Stored one or zero BDD)]}.");
sprintf (tmpString, " %d", rootStartLine[i]);
for (j=strlen(tmpString); j<intStringLength+1; j++) {
strcat (tmpString, " ");
}
retValue = fprintf (fp, "%s", tmpString);
}
retValue = fprintf (fp, "\n");
fflush (fp);
}
/*
* Write Number of clauses and variable in the header
*/
*clauseNPtr = clauseN;
if (noHeader==0) {
fsetpos (fp, &posFile2);
retValue = fprintf (fp, "p cnf");
sprintf (tmpString, " %d %d", varMax, clauseN);
for (j=strlen(tmpString); j<2*(intStringLength+1); j++) {
strcat (tmpString, " ");
}
retValue = fprintf (fp, "%s\n", tmpString);
fflush (fp);
}
/*-------------------------- Close file and return ------------------------*/
if (fileToClose) {
fclose (fp);
}
DDDMP_FREE (bddIdsInSupport);
DDDMP_FREE (permIdsInSupport);
DDDMP_FREE (rootStartLine);
if (bddIdsToFree == 1) {
DDDMP_FREE (bddIds);
}
if (bddAuxIdsToFree == 1) {
DDDMP_FREE (bddAuxIds);
}
if (cnfIdsToFree == 1) {
DDDMP_FREE (cnfIds);
}
if (varNamesToFree == 1) {
for (i=0; i<nVar; i++) {
DDDMP_FREE (varNames[i]);
}
DDDMP_FREE (varNames);
}
return (DDDMP_SUCCESS);
failure:
if (support != NULL) {
Cudd_RecursiveDeref (ddMgr, support);
}
DDDMP_FREE (bddIdsInSupport);
DDDMP_FREE (permIdsInSupport);
DDDMP_FREE (rootStartLine);
if (bddIdsToFree == 1) {
DDDMP_FREE (bddIds);
}
if (bddAuxIdsToFree == 1) {
DDDMP_FREE (bddAuxIds);
}
if (cnfIdsToFree == 1) {
DDDMP_FREE (cnfIds);
}
if (varNamesToFree == 1) {
for (i=0; i<nVar; i++) {
DDDMP_FREE (varNames[i]);
}
DDDMP_FREE (varNames);
}
return (DDDMP_FAILURE);
}
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Store the BDD as CNF clauses.]
Description [Store the BDD as CNF clauses.
Use a multiplexer description for each BDD node.
]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
StoreCnfNodeByNode (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: BDD array to be stored */,
int rootN /* IN: number of BDDs in the array */,
int *bddIds /* IN: BDD ids for variables */,
int *cnfIds /* IN: CNF ids for variables */,
FILE *fp /* IN: store file */,
int *clauseN /* IN/OUT: number of clauses written in the CNF file */,
int *varMax /* IN/OUT: maximum value of id written in the CNF file */,
int *rootStartLine /* OUT: CNF line where root starts */
)
{
int retValue = 0;
int i, idf;
for (i=0; i<rootN; i++) {
if (f[i] != NULL) {
if (!cuddIsConstant(Cudd_Regular (f[i]))) {
/*
* Set Starting Line for this Root
*/
rootStartLine[i] = *clauseN + 1;
/*
* Store the BDD
*/
retValue = StoreCnfNodeByNodeRecur (ddMgr, Cudd_Regular(f[i]),
bddIds, cnfIds, fp, clauseN, varMax);
if (retValue == 0) {
(void) fprintf (stderr,
"DdStoreCnf: Error in recursive node store\n");
fflush (stderr);
}
/*
* Store CNF for the root if necessary
*/
idf = DddmpReadNodeIndexCnf (Cudd_Regular (f[i]));
#if DDDMP_DEBUG_CNF
retValue = fprintf (fp, "root %d --> \n", i);
#endif
if (Cudd_IsComplement (f[i])) {
retValue = fprintf (fp, "-%d 0\n", idf);
} else {
retValue = fprintf (fp, "%d 0\n", idf);
}
*varMax = GET_MAX (*varMax, idf);
*clauseN = *clauseN + 1;
if (retValue == EOF) {
(void) fprintf (stderr,
"DdStoreCnf: Error in recursive node store\n");
fflush (stderr);
}
}
}
}
return (retValue);
}
/**Function********************************************************************
Synopsis [Performs the recursive step of Dddmp_bddStore.]
Description [Performs the recursive step of Dddmp_bddStore.
Traverse the BDD and store a CNF formula for each "terminal" node.
]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
StoreCnfNodeByNodeRecur (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *f /* IN: BDD node to be stored */,
int *bddIds /* IN: BDD ids for variables */,
int *cnfIds /* IN: CNF ids for variables */,
FILE *fp /* IN: store file */,
int *clauseN /* OUT: number of clauses written in the CNF file */,
int *varMax /* OUT: maximum value of id written in the CNF file */
)
{
DdNode *T, *E;
int idf, idT, idE, vf;
int retValue;
#ifdef DDDMP_DEBUG
assert(!Cudd_IsComplement(f));
assert(f!=NULL);
#endif
/* If constant, nothing to do. */
if (Cudd_IsConstant(f)) {
return (1);
}
/* If already visited, nothing to do. */
if (DddmpVisitedCnf (f)) {
return (1);
}
/* Mark node as visited. */
DddmpSetVisitedCnf (f);
/*------------------ Non Terminal Node -------------------------------*/
#ifdef DDDMP_DEBUG
/* BDDs! Only one constant supported */
assert (!cuddIsConstant(f));
#endif
/*
* Recursive call for Then edge
*/
T = cuddT (f);
#ifdef DDDMP_DEBUG
/* ROBDDs! No complemented Then edge */
assert (!Cudd_IsComplement(T));
#endif
/* recur */
retValue = StoreCnfNodeByNodeRecur (ddMgr, T, bddIds, cnfIds, fp,
clauseN, varMax);
if (retValue != 1) {
return(retValue);
}
/*
* Recursive call for Else edge
*/
E = Cudd_Regular (cuddE (f));
retValue = StoreCnfNodeByNodeRecur (ddMgr, E, bddIds, cnfIds, fp,
clauseN, varMax);
if (retValue != 1) {
return (retValue);
}
/*
* Obtain nodeids and variable ids of f, T, E
*/
idf = DddmpReadNodeIndexCnf (f);
vf = f->index;
if (bddIds[vf] != vf) {
(void) fprintf (stderr, "DdStoreCnf: Error writing to file\n");
fflush (stderr);
return (0);
}
idT = DddmpReadNodeIndexCnf (T);
idE = DddmpReadNodeIndexCnf (E);
if (Cudd_IsComplement (cuddE (f))) {
idE = -idE;
}
retValue = StoreCnfOneNode (f, idf, cnfIds[vf], idT, idE, fp,
clauseN, varMax);
if (retValue == EOF) {
return (0);
} else {
return (1);
}
}
/**Function********************************************************************
Synopsis [Store One Single BDD Node.]
Description [Store One Single BDD Node translating it as a multiplexer.]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
StoreCnfOneNode (
DdNode *f /* IN: node to be stored */,
int idf /* IN: node CNF Index */,
int vf /* IN: node BDD Index */,
int idT /* IN: Then CNF Index with sign = inverted edge */,
int idE /* IN: Else CNF Index with sign = inverted edge */,
FILE *fp /* IN: store file */,
int *clauseN /* OUT: number of clauses */,
int *varMax /* OUT: maximun Index of variable stored */
)
{
int retValue = 0;
int idfAbs, idTAbs, idEAbs;
idfAbs = abs (idf);
idTAbs = abs (idT);
idEAbs = abs (idE);
/*----------------------------- Check for Constant ------------------------*/
assert(!Cudd_IsConstant(f));
/*------------------------- Check for terminal nodes ----------------------*/
if ((idTAbs==1) && (idEAbs==1)) {
return (1);
}
/*------------------------------ Internal Node ----------------------------*/
#if DDDMP_DEBUG_CNF
retValue = fprintf (fp, "id=%d var=%d idT=%d idE=%d\n",
idf, vf, idT, idE);
#endif
/*
* Then to terminal
*/
if ((idTAbs==1) && (idEAbs!=1)) {
#if DDDMP_DEBUG_CNF
retValue = fprintf (fp, "CASE 1 -->\n");
#endif
retValue = fprintf (fp, "%d %d 0\n",
idf, -vf);
retValue = fprintf (fp, "%d %d 0\n",
idf, -idE);
retValue = fprintf (fp, "%d %d %d 0\n",
-idf, vf, idE);
*clauseN = *clauseN + 3;
*varMax = GET_MAX (*varMax, idfAbs);
*varMax = GET_MAX (*varMax, vf);
*varMax = GET_MAX (*varMax, idEAbs);
}
/*
* Else to terminal
*/
if ((idTAbs!=1) && (idEAbs==1)) {
if (idE == 1) {
#if DDDMP_DEBUG_CNF
retValue = fprintf (fp, "CASE 2 -->\n");
#endif
retValue = fprintf (fp, "%d %d 0\n",
idf, vf);
retValue = fprintf (fp, "%d %d 0\n",
idf, -idT);
retValue = fprintf (fp, "%d %d %d 0\n",
-idf, -vf, idT);
} else {
#if DDDMP_DEBUG_CNF
retValue = fprintf (fp, "CASE 3 -->\n");
#endif
retValue = fprintf (fp, "%d %d 0\n",
-idf, vf);
retValue = fprintf (fp, "%d %d 0\n",
-idf, idT);
retValue = fprintf (fp, "%d %d %d 0\n",
idf, -vf, -idT);
}
*varMax = GET_MAX (*varMax, idfAbs);
*varMax = GET_MAX (*varMax, vf);
*varMax = GET_MAX (*varMax, idTAbs);
*clauseN = *clauseN + 3;
}
/*
* Nor Then or Else to terminal
*/
if ((idTAbs!=1) && (idEAbs!=1)) {
#if DDDMP_DEBUG_CNF
retValue = fprintf (fp, "CASE 4 -->\n");
#endif
retValue = fprintf (fp, "%d %d %d 0\n",
idf, vf, -idE);
retValue = fprintf (fp, "%d %d %d 0\n",
-idf, vf, idE);
retValue = fprintf (fp, "%d %d %d 0\n",
idf, -vf, -idT);
retValue = fprintf (fp, "%d %d %d 0\n",
-idf, -vf, idT);
*varMax = GET_MAX (*varMax, idfAbs);
*varMax = GET_MAX (*varMax, vf);
*varMax = GET_MAX (*varMax, idTAbs);
*varMax = GET_MAX (*varMax, idEAbs);
*clauseN = *clauseN + 4;
}
return (retValue);
}
/**Function********************************************************************
Synopsis [Prints a disjoint sum of products.]
Description [Prints a disjoint sum of product cover for the function
rooted at node. Each product corresponds to a path from node a
leaf node different from the logical zero, and different from
the background value. Uses the standard output. Returns 1 if
successful, 0 otherwise.
]
SideEffects [None]
SeeAlso [StoreCnfBest]
******************************************************************************/
static int
StoreCnfMaxtermByMaxterm (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDDs to store */,
int rootN /* IN: number of BDDs in the array */,
int *bddIds /* IN: BDD Identifiers */,
int *cnfIds /* IN: corresponding CNF Identifiers */,
int idInitial /* IN: initial value for numbering new CNF variables */,
FILE *fp /* IN: file pointer */,
int *varMax /* OUT: maximum identifier of the variables created */,
int *clauseN /* OUT: number of stored clauses */,
int *rootStartLine /* OUT: line where root starts */
)
{
int i, j, *list;
(void) idInitial; /* avoid warning */
list = DDDMP_ALLOC (int, ddMgr->size);
if (list == NULL) {
ddMgr->errorCode = CUDD_MEMORY_OUT;
return (DDDMP_FAILURE);
}
for (i=0; i<rootN; i++) {
if (f[i] != NULL) {
if (!cuddIsConstant(Cudd_Regular (f[i]))) {
for (j=0; j<ddMgr->size; j++) {
list[j] = 2;
}
/*
* Set Starting Line for this Root
*/
rootStartLine[i] = *clauseN + 1;
StoreCnfMaxtermByMaxtermRecur (ddMgr, f[i], bddIds, cnfIds, fp,
list, clauseN, varMax);
}
}
}
FREE (list);
return (1);
}
/**Function********************************************************************
Synopsis [Prints a disjoint sum of products with intermediate
cutting points.]
Description [Prints a disjoint sum of product cover for the function
rooted at node intorducing cutting points whenever necessary.
Each product corresponds to a path from node a leaf
node different from the logical zero, and different from the
background value. Uses the standard output. Returns 1 if
successful, 0 otherwise.
]
SideEffects [None]
SeeAlso [StoreCnfMaxtermByMaxterm]
******************************************************************************/
static int
StoreCnfBest (
DdManager *ddMgr /* IN: DD Manager */,
DdNode **f /* IN: array of BDDs to store */,
int rootN /* IN: number of BDD in the array */,
int *bddIds /* IN: BDD identifiers */,
int *cnfIds /* IN: corresponding CNF identifiers */,
int idInitial /* IN: initial value for numbering new CNF variables */,
FILE *fp /* IN: file pointer */,
int *varMax /* OUT: maximum identifier of the variables created */,
int *clauseN /* OUT: number of stored clauses */,
int *rootStartLine /* OUT: line where root starts */
)
{
int i, j, *list;
(void) idInitial; /* avoid warning */
list = DDDMP_ALLOC (int, ddMgr->size);
if (list == NULL) {
ddMgr->errorCode = CUDD_MEMORY_OUT;
return (DDDMP_FAILURE);
}
for (i=0; i<rootN; i++) {
if (f[i] != NULL) {
if (!cuddIsConstant(Cudd_Regular (f[i]))) {
for (j=0; j<ddMgr->size; j++) {
list[j] = 2;
}
/*
* Set Starting Line for this Root
*/
rootStartLine[i] = *clauseN + 1;
#if DDDMP_DEBUG_CNF
fprintf (fp, "root NOT shared BDDs %d --> \n", i);
#endif
StoreCnfBestNotSharedRecur (ddMgr, f[i], 0, bddIds, cnfIds, fp, list,
clauseN, varMax);
#if DDDMP_DEBUG_CNF
fprintf (fp, "root SHARED BDDs %d --> \n", i);
#endif
StoreCnfBestSharedRecur (ddMgr, Cudd_Regular (f[i]), bddIds, cnfIds,
fp, list, clauseN, varMax);
}
}
}
#if DDDMP_DEBUG_CNF
fprintf (stdout, "###---> BDDs After the Storing Process:\n");
DddmpPrintBddAndNext (ddMgr, f, rootN);
#endif
FREE (list);
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Performs the recursive step of Print Maxterm.]
Description [Performs the recursive step of Print Maxterm.
Traverse a BDD a print out a cube in CNF format each time a terminal
node is reached.
]
SideEffects [None]
SeeAlso []
******************************************************************************/
static void
StoreCnfMaxtermByMaxtermRecur (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *node /* IN: BDD to store */,
int *bddIds /* IN: BDD identifiers */,
int *cnfIds /* IN: corresponding CNF identifiers */,
FILE *fp /* IN: file pointer */,
int *list /* IN: temporary array to store cubes */,
int *clauseN /* OUT: number of stored clauses */,
int *varMax /* OUT: maximum identifier of the variables created */
)
{
DdNode *N, *Nv, *Nnv;
int retValue, index;
N = Cudd_Regular (node);
/*
* Terminal case: Print one cube based on the current recursion
*/
if (cuddIsConstant (N)) {
retValue = printCubeCnf (ddMgr, node, cnfIds, fp, list, varMax);
if (retValue == DDDMP_SUCCESS) {
fprintf (fp, "0\n");
*clauseN = *clauseN + 1;
}
return;
}
/*
* NON Terminal case: Recur
*/
Nv = cuddT (N);
Nnv = cuddE (N);
if (Cudd_IsComplement (node)) {
Nv = Cudd_Not (Nv);
Nnv = Cudd_Not (Nnv);
}
index = N->index;
/*
* StQ 06.05.2003
* Perform the optimization:
* f = (a + b)' = (a') ^ (a + b') = (a') ^ (b')
* i.e., if the THEN node is the constant ZERO then that variable
* can be forgotten (list[index] = 2) for subsequent ELSE cubes
*/
if (cuddIsConstant (Cudd_Regular (Nv)) && Nv != ddMgr->one) {
list[index] = 2;
} else {
list[index] = 0;
}
StoreCnfMaxtermByMaxtermRecur (ddMgr, Nnv, bddIds, cnfIds, fp, list,
clauseN, varMax);
/*
* StQ 06.05.2003
* Perform the optimization:
* f = a ^ b = (a) ^ (a' + b) = (a) ^ (b)
* i.e., if the ELSE node is the constant ZERO then that variable
* can be forgotten (list[index] = 2) for subsequent THEN cubes
*/
if (cuddIsConstant (Cudd_Regular (Nnv)) && Nnv != ddMgr->one) {
list[index] = 2;
} else {
list[index] = 1;
}
StoreCnfMaxtermByMaxtermRecur (ddMgr, Nv, bddIds, cnfIds, fp, list,
clauseN, varMax);
list[index] = 2;
return;
}
/**Function********************************************************************
Synopsis [Performs the recursive step of Print Best on Not Shared
sub-BDDs.]
Description [Performs the recursive step of Print Best on Not Shared
sub-BDDs, i.e., print out information for the nodes belonging to
BDDs not shared (whose root has just one incoming edge).
]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
StoreCnfBestNotSharedRecur (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *node /* IN: BDD to store */,
int idf /* IN: Id to store */,
int *bddIds /* IN: BDD identifiers */,
int *cnfIds /* IN: corresponding CNF identifiers */,
FILE *fp /* IN: file pointer */,
int *list /* IN: temporary array to store cubes */,
int *clauseN /* OUT: number of stored clauses */,
int *varMax /* OUT: maximum identifier of the variables created */
)
{
DdNode *N, *Nv, *Nnv;
int index, retValue;
N = Cudd_Regular (node);
/*
* Terminal case or Already Visited:
* Print one cube based on the current recursion
*/
if (cuddIsConstant (N)) {
retValue = printCubeCnf (ddMgr, node, cnfIds, fp, list, varMax);
if (retValue == DDDMP_SUCCESS) {
if (idf != 0) {
fprintf (fp, "%d ", idf);
}
fprintf (fp, "0\n");
*varMax = GET_MAX (*varMax, abs(idf));
*clauseN = *clauseN + 1;
}
return (DDDMP_SUCCESS);
}
/*
* Shared Sub-Tree: Print Cube
*/
index = DddmpReadNodeIndexCnf (N);
if (index > 0) {
if (idf != 0) {
fprintf (fp, "%d ", idf);
}
if (Cudd_IsComplement (node)) {
retValue = fprintf (fp, "-%d ", index);
} else {
retValue = fprintf (fp, "%d ", index);
}
retValue = printCubeCnf (ddMgr, node, cnfIds, fp, list, varMax);
fprintf (fp, "0\n");
*varMax = GET_MAX (*varMax, abs(index));
*clauseN = *clauseN + 1;
return (DDDMP_SUCCESS);
}
/*
* NON Terminal case: Recur
*/
Nv = cuddT (N);
Nnv = cuddE (N);
if (Cudd_IsComplement (node)) {
Nv = Cudd_Not (Nv);
Nnv = Cudd_Not (Nnv);
}
index = N->index;
/*
* StQ 06.05.2003
* Perform the optimization:
* f = (a + b)' = (a') ^ (a + b') = (a') ^ (b')
* i.e., if the THEN node is the constant ZERO then that variable
* can be forgotten (list[index] = 2) for subsequent ELSE cubes
*/
if (cuddIsConstant (Cudd_Regular (Nv)) && Nv != ddMgr->one) {
list[index] = 2;
} else {
list[index] = 0;
}
StoreCnfBestNotSharedRecur (ddMgr, Nnv, idf, bddIds, cnfIds, fp, list,
clauseN, varMax);
/*
* StQ 06.05.2003
* Perform the optimization:
* f = a ^ b = (a) ^ (a' + b) = (a) ^ (b)
* i.e., if the ELSE node is the constant ZERO then that variable
* can be forgotten (list[index] = 2) for subsequent THEN cubes
*/
if (cuddIsConstant (Cudd_Regular (Nnv)) && Nnv != ddMgr->one) {
list[index] = 2;
} else {
list[index] = 1;
}
StoreCnfBestNotSharedRecur (ddMgr, Nv, idf, bddIds, cnfIds, fp, list,
clauseN, varMax);
list[index] = 2;
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Performs the recursive step of Print Best on Shared
sub-BDDs.
]
Description [Performs the recursive step of Print Best on Not Shared
sub-BDDs, i.e., print out information for the nodes belonging to
BDDs not shared (whose root has just one incoming edge).
]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
StoreCnfBestSharedRecur (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *node /* IN: BDD to store */,
int *bddIds /* IN: BDD identifiers */,
int *cnfIds /* IN: corresponding CNF identifiers */,
FILE *fp /* IN: file pointer */,
int *list /* IN: temporary array to store cubes */,
int *clauseN /* OUT: number of stored clauses */,
int *varMax /* OUT: maximum identifier of the variables created */
)
{
DdNode *nodeThen, *nodeElse;
int i, idf;
Dddmp_Assert (node==Cudd_Regular(node),
"Inverted Edge during Shared Printing.");
/* If constant, nothing to do. */
if (cuddIsConstant (node)) {
return (DDDMP_SUCCESS);
}
/* If already visited, nothing to do. */
if (DddmpVisitedCnf (node)) {
return (DDDMP_SUCCESS);
}
/*
* Shared Sub-Tree: Print Cube
*/
idf = DddmpReadNodeIndexCnf (node);
if (idf > 0) {
/* Cheat the Recur Function about the Index of the Current Node */
DddmpWriteNodeIndexCnf (node, 0);
#if DDDMP_DEBUG_CNF
fprintf (fp, "Else of XNOR\n");
#endif
for (i=0; i<ddMgr->size; i++) {
list[i] = 2;
}
StoreCnfBestNotSharedRecur (ddMgr, Cudd_Not (node), idf, bddIds, cnfIds,
fp, list, clauseN, varMax);
#if DDDMP_DEBUG_CNF
fprintf (fp, "Then of XNOR\n");
#endif
for (i=0; i<ddMgr->size; i++) {
list[i] = 2;
}
StoreCnfBestNotSharedRecur (ddMgr, node, -idf, bddIds, cnfIds,
fp, list, clauseN, varMax);
/* Set Back Index of Current Node */
DddmpWriteNodeIndexCnf (node, idf);
}
/* Mark node as visited. */
DddmpSetVisitedCnf (node);
/*
* Recur
*/
nodeThen = cuddT (node);
nodeElse = cuddE (node);
StoreCnfBestSharedRecur (ddMgr, Cudd_Regular (nodeThen), bddIds, cnfIds,
fp, list, clauseN, varMax);
StoreCnfBestSharedRecur (ddMgr, Cudd_Regular (nodeElse), bddIds, cnfIds,
fp, list, clauseN, varMax);
return (DDDMP_SUCCESS);
}
/**Function********************************************************************
Synopsis [Print One Cube in CNF Format.]
Description [Print One Cube in CNF Format.
Return DDDMP_SUCCESS if something is printed out, DDDMP_FAILURE
is nothing is printed out.
]
SideEffects [None]
SeeAlso []
******************************************************************************/
static int
printCubeCnf (
DdManager *ddMgr /* IN: DD Manager */,
DdNode *node /* IN: BDD to store */,
int *cnfIds /* IN: CNF identifiers */,
FILE *fp /* IN: file pointer */,
int *list /* IN: temporary array to store cubes */,
int *varMax /* OUT: maximum identifier of the variables created */
)
{
int i, retValue;
DdNode *one;
retValue = DDDMP_FAILURE;
one = ddMgr->one;
if (node != one) {
for (i=0; i<ddMgr->size; i++) {
if (list[i] == 0) {
retValue = DDDMP_SUCCESS;
(void) fprintf (fp, "%d ", cnfIds[i]);
*varMax = GET_MAX(*varMax, cnfIds[i]);
} else {
if (list[i] == 1) {
retValue = DDDMP_SUCCESS;
(void) fprintf (fp, "-%d ", cnfIds[i]);
*varMax = GET_MAX(*varMax, cnfIds[i]);
}
}
}
}
return (retValue);
}