You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
2315 lines
64 KiB
2315 lines
64 KiB
/**CFile***********************************************************************
|
|
|
|
FileName [ntrBddTest.c]
|
|
|
|
PackageName [ntr]
|
|
|
|
Synopsis [BDD test functions for the nanotrav program.]
|
|
|
|
Description []
|
|
|
|
SeeAlso []
|
|
|
|
Author [Fabio Somenzi]
|
|
|
|
Copyright [Copyright (c) 1995-2012, 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.]
|
|
|
|
******************************************************************************/
|
|
|
|
#include "ntr.h"
|
|
#include "cuddInt.h"
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Constant declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Stucture declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Type declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Variable declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
#ifndef lint
|
|
static char rcsid[] UTIL_UNUSED = "$Id: ntrBddTest.c,v 1.22 2012/02/05 01:53:01 fabio Exp fabio $";
|
|
#endif
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Macro declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/**AutomaticStart*************************************************************/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Static function prototypes */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
static int ntrTestMinimizationAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *name, DdNode *c, char *cname, NtrOptions *option);
|
|
static int ntrTestDensityAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *name, NtrOptions *option);
|
|
static int ntrTestDecompAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *name, NtrOptions *option);
|
|
static int ntrTestCofEstAux (DdManager * dd, BnetNetwork * net, DdNode * f, char * name, NtrOptions * option);
|
|
static int ntrTestClippingAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *name, DdNode *g, char *gname, NtrOptions *option);
|
|
static int ntrTestEquivAndContainAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *fname, DdNode *g, char *gname, DdNode *d, char *dname, NtrOptions *option);
|
|
static int ntrTestClosestCubeAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *fname, DdNode *g, char *gname, DdNode **vars, NtrOptions *option);
|
|
static int ntrTestCharToVect(DdManager * dd, DdNode * f, NtrOptions *option);
|
|
#if 0
|
|
static DdNode * ntrCompress1 (DdManager *dd, DdNode *f, int nvars, int threshold);
|
|
#endif
|
|
static DdNode * ntrCompress2 (DdManager *dd, DdNode *f, int nvars, int threshold);
|
|
static BnetNode * ntrNodeIsBuffer (BnetNode *nd, st_table *hash);
|
|
|
|
/**AutomaticEnd***************************************************************/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Definition of exported functions */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests BDD minimization functions.]
|
|
|
|
Description [Tests BDD minimization functions, including
|
|
leaf-identifying compaction, squeezing, and restrict. This function
|
|
uses as constraint the first output of net2 and computes positive
|
|
and negative cofactors of all the outputs of net1. For each
|
|
cofactor, it checks whether compaction was safe (cofactor not larger
|
|
than original function) and that the expansion based on each
|
|
minimization function (used as a generalized cofactor) equals the
|
|
original function. Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestMinimization(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
BnetNetwork * net2,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f;
|
|
DdNode *c = NULL;
|
|
char *cname = NULL;
|
|
BnetNode *node;
|
|
int i;
|
|
int result;
|
|
int nsize, csize;
|
|
|
|
if (option->second == FALSE) return(1);
|
|
|
|
(void) printf("Testing BDD minimization algorithms\n");
|
|
/* Use largest output of second network as constraint. */
|
|
csize = -1;
|
|
for (i = 0; i < net2->noutputs; i++) {
|
|
if (!st_lookup(net2->hash,net2->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
nsize = Cudd_DagSize(node->dd);
|
|
if (nsize > csize) {
|
|
c = node->dd;
|
|
cname = node->name;
|
|
csize = nsize;
|
|
}
|
|
}
|
|
if (c == NULL || cname == NULL) return(0);
|
|
(void) printf("TEST-MINI: Constrain (%s) %d nodes\n",
|
|
cname, Cudd_DagSize(c));
|
|
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestMinimizationAux(dd,net1,f,node->name,c,cname,
|
|
option);
|
|
if (result == 0) return(0);
|
|
}
|
|
} else {
|
|
if (!st_lookup(net1->hash,option->node,&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestMinimizationAux(dd,net1,f,option->node,c,cname,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
|
|
return(1);
|
|
|
|
} /* end of Ntr_TestMinimization */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests BDD density-related functions.]
|
|
|
|
Description [Tests BDD density-related functions.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestDensity(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f;
|
|
BnetNode *node;
|
|
int i;
|
|
int result;
|
|
|
|
if (option->density == FALSE) return(1);
|
|
|
|
(void) printf("Testing BDD density-related algorithms\n");
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestDensityAux(dd,net1,f,node->name,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
} else {
|
|
if (!st_lookup(net1->hash,option->node,&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestDensityAux(dd,net1,f,option->node,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
|
|
return(1);
|
|
|
|
} /* end of Ntr_TestDensity */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests BDD decomposition functions.]
|
|
|
|
Description [Tests BDD decomposition functions.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestDecomp(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f;
|
|
BnetNode *node;
|
|
int i;
|
|
int result;
|
|
|
|
if (option->decomp == FALSE) return(1);
|
|
|
|
(void) printf("Testing BDD decomposition algorithms\n");
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestDecompAux(dd,net1,f,node->name,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
} else {
|
|
if (!st_lookup(net1->hash,option->node,&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestDecompAux(dd,net1,f,option->node,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
|
|
return(1);
|
|
|
|
} /* end of ntrTestDecomp */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Verify equivalence of combinational networks.]
|
|
|
|
Description [Verify equivalence of combinational networks.
|
|
Returns 1 if successful and if the networks are equivalent; -1 if
|
|
successful, but the networks are not equivalent; 0 otherwise.
|
|
The two networks are supposed to have the same names for inputs and
|
|
outputs. The only exception is that the second network may miss
|
|
output buffers that are present in the first network. This function tries
|
|
to match both the output and the input of the buffer.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_VerifyEquivalence(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
BnetNetwork * net2,
|
|
NtrOptions * option)
|
|
{
|
|
BnetNode *node;
|
|
char *oname;
|
|
DdNode *odd1, *odd2;
|
|
int i;
|
|
int pr;
|
|
|
|
(void) printf("Testing equivalence\n");
|
|
if (net2->noutputs != net1->noutputs) {
|
|
(void) printf("The two networks have different number of outputs\n");
|
|
(void) printf(" %s has %d outputs\n %s has %d outputs\n",
|
|
net1->name, net1->noutputs, net2->name, net2->noutputs);
|
|
return(-1);
|
|
}
|
|
if (net2->nlatches != net1->nlatches) {
|
|
(void) printf("The two networks have different number of latches\n");
|
|
(void) printf(" %s has %d latches\n %s has %d latches\n",
|
|
net1->name, net1->nlatches, net2->name, net2->nlatches);
|
|
return(-1);
|
|
}
|
|
|
|
pr = option->verb;
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
oname = net1->outputs[i];
|
|
if (!st_lookup(net1->hash,oname,&node)) {
|
|
return(0);
|
|
}
|
|
odd1 = node->dd;
|
|
(void) printf("%s", oname);
|
|
Cudd_PrintDebug(dd, node->dd, Cudd_ReadSize(dd), pr);
|
|
if (!st_lookup(net2->hash,oname,&node)) {
|
|
BnetNode *inpnd;
|
|
if ((inpnd = ntrNodeIsBuffer(node,net1->hash)) == NULL ||
|
|
!st_lookup(net2->hash,inpnd->name,&node)) {
|
|
(void) printf("Output %s missing from network %s\n",
|
|
oname, net2->name);
|
|
return(-1);
|
|
} else {
|
|
odd2 = inpnd->dd;
|
|
}
|
|
} else {
|
|
odd2 = node->dd;
|
|
}
|
|
if (odd1 != odd2) {
|
|
(void) printf("Output %s is not equivalent\n", oname);
|
|
return(-1);
|
|
}
|
|
}
|
|
return(1);
|
|
|
|
} /* end of Ntr_VerifyEquivalence */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests BDD cofactor estimate functions.]
|
|
|
|
Description [Tests BDD cofactor estimate functions.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestCofactorEstimate(
|
|
DdManager * dd,
|
|
BnetNetwork * net,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f;
|
|
BnetNode *node;
|
|
int i;
|
|
int result;
|
|
|
|
if (option->cofest == FALSE) return(1);
|
|
|
|
(void) printf("Testing BDD cofactor estimation algorithms\n");
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net->noutputs; i++) {
|
|
if (!st_lookup(net->hash,net->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestCofEstAux(dd,net,f,node->name,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
} else {
|
|
if (!st_lookup(net->hash,option->node,&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestCofEstAux(dd,net,f,option->node,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
|
|
return(1);
|
|
|
|
} /* end of Ntr_TestCofactorEstimate */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests BDD clipping functions.]
|
|
|
|
Description [Tests BDD clipping functions.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestClipping(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
BnetNetwork * net2,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f;
|
|
DdNode *g = NULL;
|
|
char *gname = NULL;
|
|
BnetNode *node;
|
|
int i;
|
|
int result;
|
|
int nsize, gsize;
|
|
|
|
if (option->clip < 0.0) return(1);
|
|
|
|
(void) printf("Testing BDD clipping algorithms\n");
|
|
/* Use largest output of second network as second operand. */
|
|
gsize = -1;
|
|
for (i = 0; i < net2->noutputs; i++) {
|
|
if (!st_lookup(net2->hash,net2->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
nsize = Cudd_DagSize(node->dd);
|
|
if (nsize > gsize) {
|
|
g = node->dd;
|
|
gname = node->name;
|
|
gsize = nsize;
|
|
}
|
|
}
|
|
if (g == NULL || gname == NULL) return(0);
|
|
(void) printf("TEST-CLIP: Second operand (%s) %d nodes\n",
|
|
gname, Cudd_DagSize(g));
|
|
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestClippingAux(dd,net1,f,node->name,g,gname,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
} else {
|
|
if (!st_lookup(net1->hash,option->node,&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestClippingAux(dd,net1,f,option->node,g,gname,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
|
|
return(1);
|
|
|
|
} /* end of Ntr_TestClipping */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests BDD equivalence and containment with don't cares.]
|
|
|
|
Description [Tests functions for BDD equivalence and containment
|
|
with don't cares, including Cudd_EquivDC and Cudd_bddLeqUnless. This
|
|
function uses as care set the first output of net2 and checkes
|
|
equivalence and containment for of all the output pairs of net1.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestEquivAndContain(
|
|
DdManager *dd,
|
|
BnetNetwork *net1,
|
|
BnetNetwork *net2,
|
|
NtrOptions *option)
|
|
{
|
|
DdNode *f, *g;
|
|
DdNode *d = NULL;
|
|
char *dname = NULL;
|
|
BnetNode *node1, *node2;
|
|
int i, j;
|
|
int result;
|
|
int nsize, dsize;
|
|
|
|
if (option->dontcares == FALSE) return(1);
|
|
|
|
(void) printf("Testing BDD equivalence and containment algorithms\n");
|
|
/* Use largest output of second network as constraint. */
|
|
dsize = -1;
|
|
for (i = 0; i < net2->noutputs; i++) {
|
|
if (!st_lookup(net2->hash,net2->outputs[i],&node1)) {
|
|
return(0);
|
|
}
|
|
nsize = Cudd_DagSize(node1->dd);
|
|
if (nsize > dsize) {
|
|
d = node1->dd;
|
|
dname = node1->name;
|
|
dsize = nsize;
|
|
}
|
|
}
|
|
if (d == NULL || dname == NULL) return(0);
|
|
(void) printf("TEST-DC: Don't care set (%s) %d nodes\n",
|
|
dname, Cudd_DagSize(d));
|
|
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[i],&node1)) {
|
|
return(0);
|
|
}
|
|
f = node1->dd;
|
|
if (f == NULL) return(0);
|
|
for (j = 0; j < net1->noutputs; j++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[j],&node2)) {
|
|
return(0);
|
|
}
|
|
g = node2->dd;
|
|
if (g == NULL) return(0);
|
|
result = ntrTestEquivAndContainAux(dd,net1,f,node1->name,g,
|
|
node2->name,d,dname,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
}
|
|
} else {
|
|
if (!st_lookup(net1->hash,option->node,&node1)) {
|
|
return(0);
|
|
}
|
|
f = node1->dd;
|
|
if (f == NULL) return(0);
|
|
for (j = 0; j < net1->noutputs; j++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[j],&node2)) {
|
|
return(0);
|
|
}
|
|
g = node2->dd;
|
|
if (g == NULL) return(0);
|
|
result = ntrTestEquivAndContainAux(dd,net1,f,option->node,
|
|
g,node2->name,d,dname,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
}
|
|
|
|
return(1);
|
|
|
|
} /* end of Ntr_TestEquivAndContain */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests the Cudd_bddClosestCube function.]
|
|
|
|
Description [Tests the Cudd_bddClosestCube function.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestClosestCube(
|
|
DdManager * dd,
|
|
BnetNetwork * net,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f, *g;
|
|
BnetNode *node1, *node2;
|
|
int i, j, nvars;
|
|
int result;
|
|
DdNode **vars;
|
|
double calls;
|
|
|
|
if (option->closestCube == FALSE) return(1);
|
|
|
|
(void) printf("Testing Cudd_bddClosestCube\n");
|
|
nvars = Cudd_ReadSize(dd);
|
|
vars = ALLOC(DdNode *, nvars);
|
|
if (vars == NULL) return(0);
|
|
for (i = 0; i < nvars; i++) {
|
|
vars[i] = Cudd_bddIthVar(dd,i);
|
|
}
|
|
calls = Cudd_ReadRecursiveCalls(dd);
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net->noutputs; i++) {
|
|
if (!st_lookup(net->hash,net->outputs[i],&node1)) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
f = node1->dd;
|
|
if (f == NULL) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
for (j = 0; j < net->noutputs; j++) {
|
|
if (!st_lookup(net->hash,net->outputs[j],&node2)) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
g = node2->dd;
|
|
if (g == NULL) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
result = ntrTestClosestCubeAux(dd,net,f,node1->name,g,
|
|
node2->name,vars,option);
|
|
if (result == 0) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
}
|
|
}
|
|
} else {
|
|
if (!st_lookup(net->hash,option->node,&node1)) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
f = node1->dd;
|
|
if (f == NULL) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
for (j = 0; j < net->noutputs; j++) {
|
|
if (!st_lookup(net->hash,net->outputs[j],&node2)) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
g = node2->dd;
|
|
if (g == NULL) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
result = ntrTestClosestCubeAux(dd,net,f,option->node,g,
|
|
node2->name,vars,option);
|
|
if (result == 0) {
|
|
FREE(vars);
|
|
return(0);
|
|
}
|
|
}
|
|
}
|
|
(void) printf("End of test. Performed %.0f recursive calls.\n",
|
|
Cudd_ReadRecursiveCalls(dd) - calls);
|
|
FREE(vars);
|
|
return(1);
|
|
|
|
} /* end of Ntr_TestClosestCube */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Tests extraction of two-literal clauses.]
|
|
|
|
Description [Tests extraction of two-literal clauses.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestTwoLiteralClauses(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f;
|
|
BnetNode *node;
|
|
int result;
|
|
char **inames = NULL;
|
|
int i;
|
|
|
|
if (option->clauses == FALSE) return(1);
|
|
|
|
/* Initialize data structures. */
|
|
inames = ALLOC(char *,Cudd_ReadSize(dd));
|
|
if (inames == NULL) return(0);
|
|
for (i = 0; i < Cudd_ReadSize(dd); i++) {
|
|
inames[i] = NULL;
|
|
}
|
|
|
|
/* Find the input names. */
|
|
for (i = 0; i < net1->ninputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->inputs[i],&node)) {
|
|
FREE(inames);
|
|
return(0);
|
|
}
|
|
inames[node->var] = net1->inputs[i];
|
|
}
|
|
for (i = 0; i < net1->nlatches; i++) {
|
|
if (!st_lookup(net1->hash,net1->latches[i][1],&node)) {
|
|
FREE(inames);
|
|
return(0);
|
|
}
|
|
inames[node->var] = net1->latches[i][1];
|
|
}
|
|
|
|
(void) printf("Testing extraction of two literal clauses\n");
|
|
if (option->node == NULL) {
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) {
|
|
FREE(inames);
|
|
return(0);
|
|
}
|
|
(void) printf("*** %s ***\n", net1->outputs[i]);
|
|
result = Cudd_PrintTwoLiteralClauses(dd, f, inames, NULL);
|
|
if (result == 0) {
|
|
FREE(inames);
|
|
return(0);
|
|
}
|
|
}
|
|
} else {
|
|
if (!st_lookup(net1->hash,option->node,&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) {
|
|
FREE(inames);
|
|
return(0);
|
|
}
|
|
(void) printf("*** %s ***\n", option->node);
|
|
result = Cudd_PrintTwoLiteralClauses(dd, f, inames, NULL);
|
|
if (result == 0) {
|
|
FREE(inames);
|
|
return(0);
|
|
}
|
|
}
|
|
|
|
FREE(inames);
|
|
return(1);
|
|
|
|
} /* end of Ntr_TestTwoLiteralClauses */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Test char-to-vect conversion.]
|
|
|
|
Description [Test char-to-vect conversion. Returns 1 if successful;
|
|
0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
int
|
|
Ntr_TestCharToVect(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *f;
|
|
int result;
|
|
BnetNode *node;
|
|
int i;
|
|
|
|
if (option->char2vect == FALSE) return(1);
|
|
|
|
(void) printf("Testing char-to-vect\n");
|
|
if (net1->nlatches > 0) {
|
|
NtrPartTR *T;
|
|
T = Ntr_buildTR(dd,net1,option,NTR_IMAGE_MONO);
|
|
result = ntrTestCharToVect(dd,T->part[0],option);
|
|
Ntr_freeTR(dd,T);
|
|
} else if (option->node == NULL) {
|
|
result = 1;
|
|
for (i = 0; i < net1->noutputs; i++) {
|
|
if (!st_lookup(net1->hash,net1->outputs[i],&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
(void) printf("*** %s ***\n", net1->outputs[i]);
|
|
result = ntrTestCharToVect(dd,f,option);
|
|
if (result == 0) return(0);
|
|
}
|
|
} else {
|
|
if (!st_lookup(net1->hash,option->node,&node)) {
|
|
return(0);
|
|
}
|
|
f = node->dd;
|
|
if (f == NULL) return(0);
|
|
result = ntrTestCharToVect(dd,f,option);
|
|
}
|
|
return(result);
|
|
|
|
} /* end of Ntr_TestCharToVect */
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Definition of internal functions */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Definition of static functions */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one BDD for Ntr_TestMinimization.]
|
|
|
|
Description [Processes one BDD for Ntr_TestMinimization.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [Ntr_TestMinimization]
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestMinimizationAux(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
DdNode * f,
|
|
char * name,
|
|
DdNode * c,
|
|
char * cname,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *com1, *com0, *min1, *min0, *sq1, *sq0;
|
|
DdNode *rs1, *rs0, *cs1, *cs0, *na1, *na0, *a1, *a0;
|
|
DdNode *g, *u1, *l1, *u0, *l0;
|
|
int pr, nvars;
|
|
int sizeF, sizeMin1, sizeMin0, sizeSq1, sizeSq0, sizeCom1, sizeCom0;
|
|
int sizeRs1, sizeRs0, sizeCs1, sizeCs0, sizeNa1, sizeNa0, sizeA1, sizeA0;
|
|
static char *onames[11];
|
|
DdNode *outputs[11];
|
|
DdNode *fc[2];
|
|
|
|
pr = option->verb;
|
|
fc[0] = f; fc[1] = c;
|
|
nvars = Cudd_VectorSupportSize(dd,fc,2);
|
|
if (nvars == CUDD_OUT_OF_MEM) return(0);
|
|
(void) printf("TEST-MINI:: %s\n", name);
|
|
(void) printf("T-M ");
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
sizeF = Cudd_DagSize(f);
|
|
|
|
/* Compute positive generalized cofactor. */
|
|
com1 = Cudd_bddLICompaction(dd, f, c);
|
|
if (com1 == NULL) {
|
|
(void) printf("TEST-MINI: LI-compaction failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(com1);
|
|
(void) printf("T-M L1 ");
|
|
Cudd_PrintDebug(dd, com1, nvars, pr);
|
|
sizeCom1 = Cudd_DagSize(com1);
|
|
if (sizeCom1 > sizeF) {
|
|
(void) printf("TEST-MINI: LI-compaction not safe (1).\n");
|
|
return(0);
|
|
}
|
|
min1 = Cudd_bddMinimize(dd, f, c);
|
|
if (min1 == NULL) {
|
|
(void) printf("TEST-MINI: minimize failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(min1);
|
|
(void) printf("T-M M1 ");
|
|
Cudd_PrintDebug(dd, min1, nvars, pr);
|
|
sizeMin1 = Cudd_DagSize(min1);
|
|
if (sizeMin1 > sizeF) {
|
|
(void) printf("TEST-MINI: minimize not safe (1).\n");
|
|
return(0);
|
|
}
|
|
rs1 = Cudd_bddRestrict(dd, f, c);
|
|
if (rs1 == NULL) {
|
|
(void) printf("TEST-MINI: restrict failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(rs1);
|
|
(void) printf("T-M R1 ");
|
|
Cudd_PrintDebug(dd, rs1, nvars, pr);
|
|
sizeRs1 = Cudd_DagSize(rs1);
|
|
cs1 = Cudd_bddConstrain(dd, f, c);
|
|
if (cs1 == NULL) {
|
|
(void) printf("TEST-MINI: constrain failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(cs1);
|
|
(void) printf("T-M C1 ");
|
|
Cudd_PrintDebug(dd, cs1, nvars, pr);
|
|
sizeCs1 = Cudd_DagSize(cs1);
|
|
l1 = Cudd_bddAnd(dd, f, c);
|
|
if (l1 == NULL) {
|
|
(void) printf("TEST-MINI: lower bound failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(l1);
|
|
u1 = Cudd_bddOr(dd, f, Cudd_Not(c));
|
|
if (u1 == NULL) {
|
|
(void) printf("TEST-MINI: upper bound failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(u1);
|
|
(void) printf("TEST-MINI: (lb,ub) : (%d,%d) nodes\n",
|
|
Cudd_DagSize(l1), Cudd_DagSize(u1));
|
|
sq1 = Cudd_bddSqueeze(dd, l1, u1);
|
|
if (sq1 == NULL) {
|
|
(void) printf("TEST-MINI: squeezing failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(sq1);
|
|
sizeSq1 = Cudd_DagSize(sq1);
|
|
if (sizeSq1 > sizeF) {
|
|
Cudd_RecursiveDeref(dd,sq1);
|
|
sq1 = f;
|
|
Cudd_Ref(sq1);
|
|
sizeSq1 = sizeF;
|
|
}
|
|
(void) printf("T-M S1 ");
|
|
Cudd_PrintDebug(dd, sq1, nvars, pr);
|
|
na1 = Cudd_bddNPAnd(dd, f, c);
|
|
if (na1 == NULL) {
|
|
(void) printf("TEST-MINI: NPand failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(na1);
|
|
(void) printf("T-M N1 ");
|
|
Cudd_PrintDebug(dd, na1, nvars, pr);
|
|
sizeNa1 = Cudd_DagSize(na1);
|
|
a1 = Cudd_bddAnd(dd, f, c);
|
|
if (a1 == NULL) {
|
|
(void) printf("TEST-MINI: and failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(a1);
|
|
(void) printf("T-M A1 ");
|
|
Cudd_PrintDebug(dd, a1, nvars, pr);
|
|
sizeA1 = Cudd_DagSize(a1);
|
|
(void) printf("TEST-MINI: f %d comp %d mini %d rest %d cons %d sque %d na %d and %d\n",
|
|
sizeF, sizeCom1, sizeMin1, sizeRs1, sizeCs1, sizeSq1, sizeNa1, sizeA1);
|
|
if (option->bdddump) {
|
|
onames[0] = name; outputs[0] = f;
|
|
onames[1] = cname; outputs[1] = c;
|
|
onames[2] = (char *) "cons"; outputs[2] = cs1;
|
|
onames[3] = (char *) "rest"; outputs[3] = rs1;
|
|
onames[4] = (char *) "comp"; outputs[4] = com1;
|
|
onames[5] = (char *) "mini"; outputs[5] = min1;
|
|
onames[6] = (char *) "sqee"; outputs[6] = sq1;
|
|
onames[7] = (char *) "lb"; outputs[7] = l1;
|
|
onames[8] = (char *) "ub"; outputs[8] = u1;
|
|
onames[9] = (char *) "na"; outputs[9] = na1;
|
|
onames[10] = (char *) "and"; outputs[10] = a1;
|
|
if (!Bnet_bddArrayDump(dd, net1, option->dumpfile, outputs, onames,
|
|
11, option->dumpFmt))
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,l1);
|
|
Cudd_RecursiveDeref(dd,u1);
|
|
|
|
/* Compute negative generalized cofactor. */
|
|
(void) printf("TEST-MINI:: %s\n", name);
|
|
(void) printf("T-M ");
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
|
|
com0 = Cudd_bddLICompaction(dd, f, Cudd_Not(c));
|
|
if (com0 == NULL) {
|
|
(void) printf("TEST-MINI: LI-compaction failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(com0);
|
|
(void) printf("T-M L0 ");
|
|
Cudd_PrintDebug(dd, com0, nvars, pr);
|
|
sizeCom0 = Cudd_DagSize(com0);
|
|
if (sizeCom0 > sizeF) {
|
|
(void) printf("TEST-MINI: LI-compaction not safe (2).\n");
|
|
return(0);
|
|
}
|
|
min0 = Cudd_bddMinimize(dd, f, Cudd_Not(c));
|
|
if (min0 == NULL) {
|
|
(void) printf("TEST-MINI: minimize failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(min0);
|
|
(void) printf("T-M M0 ");
|
|
Cudd_PrintDebug(dd, min0, nvars, pr);
|
|
sizeMin0 = Cudd_DagSize(min0);
|
|
if (sizeMin0 > sizeF) {
|
|
(void) printf("TEST-MINI: minimize not safe (2).\n");
|
|
return(0);
|
|
}
|
|
rs0 = Cudd_bddRestrict(dd, f, Cudd_Not(c));
|
|
if (rs0 == NULL) {
|
|
(void) printf("TEST-MINI: restrict failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(rs0);
|
|
(void) printf("T-M R0 ");
|
|
Cudd_PrintDebug(dd, rs0, nvars, pr);
|
|
sizeRs0 = Cudd_DagSize(rs0);
|
|
cs0 = Cudd_bddConstrain(dd, f, Cudd_Not(c));
|
|
if (cs0 == NULL) {
|
|
(void) printf("TEST-MINI: constrain failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(cs0);
|
|
(void) printf("T-M C0 ");
|
|
Cudd_PrintDebug(dd, cs0, nvars, pr);
|
|
sizeCs0 = Cudd_DagSize(cs0);
|
|
|
|
l0 = Cudd_bddAnd(dd, f, Cudd_Not(c));
|
|
if (l0 == NULL) {
|
|
(void) printf("TEST-MINI: lower bound failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(l0);
|
|
u0 = Cudd_bddOr(dd, f, c);
|
|
if (u0 == NULL) {
|
|
(void) printf("TEST-MINI: upper bound failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(u0);
|
|
(void) printf("TEST-MINI: (lb,ub) : (%d,%d) nodes\n",
|
|
Cudd_DagSize(l0), Cudd_DagSize(u0));
|
|
sq0 = Cudd_bddSqueeze(dd, l0, u0);
|
|
if (sq0 == NULL) {
|
|
(void) printf("TEST-MINI: squeezing failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(sq0);
|
|
Cudd_RecursiveDeref(dd,l0);
|
|
Cudd_RecursiveDeref(dd,u0);
|
|
sizeSq0 = Cudd_DagSize(sq0);
|
|
if (sizeSq0 > sizeF) {
|
|
Cudd_RecursiveDeref(dd,sq0);
|
|
sq0 = f;
|
|
Cudd_Ref(sq0);
|
|
sizeSq0 = sizeF;
|
|
}
|
|
(void) printf("T-M S0 ");
|
|
Cudd_PrintDebug(dd, sq0, nvars, pr);
|
|
na0 = Cudd_bddNPAnd(dd, f, Cudd_Not(c));
|
|
if (na0 == NULL) {
|
|
(void) printf("TEST-MINI: NPand failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(na0);
|
|
(void) printf("T-M N0 ");
|
|
Cudd_PrintDebug(dd, na0, nvars, pr);
|
|
sizeNa0 = Cudd_DagSize(na0);
|
|
a0 = Cudd_bddAnd(dd, f, Cudd_Not(c));
|
|
if (a0 == NULL) {
|
|
(void) printf("TEST-MINI: and failed (2).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(a0);
|
|
(void) printf("T-M A0 ");
|
|
Cudd_PrintDebug(dd, a0, nvars, pr);
|
|
sizeA0 = Cudd_DagSize(a0);
|
|
(void) printf("TEST-MINI: f %d comp %d mini %d rest %d cons %d sque %d na %d, and %d\n",
|
|
sizeF, sizeCom0, sizeMin0, sizeRs0, sizeCs0, sizeSq0, sizeNa0, sizeA0);
|
|
|
|
/* Check fundamental identity. */
|
|
g = Cudd_bddIte(dd,c,com1,com0);
|
|
if (g == NULL) {
|
|
(void) printf("TEST-MINI: LI-compaction failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(g);
|
|
if (g != f) {
|
|
(void) printf("TEST-MINI: LI-compaction failed (4).\n");
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,com1);
|
|
Cudd_RecursiveDeref(dd,com0);
|
|
Cudd_RecursiveDeref(dd,g);
|
|
g = Cudd_bddIte(dd,c,min1,min0);
|
|
if (g == NULL) {
|
|
(void) printf("TEST-MINI: minimize failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(g);
|
|
if (g != f) {
|
|
(void) printf("TEST-MINI: minimize failed (4).\n");
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,min1);
|
|
Cudd_RecursiveDeref(dd,min0);
|
|
Cudd_RecursiveDeref(dd,g);
|
|
g = Cudd_bddIte(dd,c,sq1,sq0);
|
|
if (g == NULL) {
|
|
(void) printf("TEST-MINI: squeezing failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(g);
|
|
if (g != f) {
|
|
(void) printf("TEST-MINI: squeezing failed (4).\n");
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,sq1);
|
|
Cudd_RecursiveDeref(dd,sq0);
|
|
Cudd_RecursiveDeref(dd,g);
|
|
g = Cudd_bddIte(dd,c,rs1,rs0);
|
|
if (g == NULL) {
|
|
(void) printf("TEST-MINI: restrict failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(g);
|
|
if (g != f) {
|
|
(void) printf("TEST-MINI: restrict failed (4).\n");
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,rs1);
|
|
Cudd_RecursiveDeref(dd,rs0);
|
|
Cudd_RecursiveDeref(dd,g);
|
|
g = Cudd_bddIte(dd,c,cs1,cs0);
|
|
if (g == NULL) {
|
|
(void) printf("TEST-MINI: constrain failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(g);
|
|
if (g != f) {
|
|
(void) printf("TEST-MINI: constrain failed (4).\n");
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,cs1);
|
|
Cudd_RecursiveDeref(dd,cs0);
|
|
Cudd_RecursiveDeref(dd,g);
|
|
g = Cudd_bddIte(dd,c,na1,na0);
|
|
if (g == NULL) {
|
|
(void) printf("TEST-MINI: NPand failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(g);
|
|
if (g != f) {
|
|
(void) printf("TEST-MINI: NPand failed (4).\n");
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,na1);
|
|
Cudd_RecursiveDeref(dd,na0);
|
|
Cudd_RecursiveDeref(dd,g);
|
|
g = Cudd_bddIte(dd,c,a1,a0);
|
|
if (g == NULL) {
|
|
(void) printf("TEST-MINI: and failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(g);
|
|
if (g != f) {
|
|
(void) printf("TEST-MINI: and failed (4).\n");
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,a1);
|
|
Cudd_RecursiveDeref(dd,a0);
|
|
Cudd_RecursiveDeref(dd,g);
|
|
|
|
return(1);
|
|
|
|
} /* end of ntrTestMinimizationAux */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one BDD for Ntr_TestDensity.]
|
|
|
|
Description [Processes one BDD for Ntr_TestDensity. Returns 1 if
|
|
successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [Ntr_TestDensity ntrCompress1]
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestDensityAux(
|
|
DdManager * dd,
|
|
BnetNetwork * net,
|
|
DdNode * f,
|
|
char * name,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *s, *b, *hb, *sp, *ua, *c1, *c2;
|
|
int pr;
|
|
int result;
|
|
int nvars;
|
|
int size, sizeS;
|
|
double densityF, densityB, densityS, densityHB, densitySP, densityUA;
|
|
double densityC1, densityC2;
|
|
char *onames[8];
|
|
DdNode *outputs[8];
|
|
|
|
result = 1;
|
|
pr = option->verb;
|
|
nvars = Cudd_SupportSize(dd,f);
|
|
if (nvars == CUDD_OUT_OF_MEM) return(0);
|
|
densityF = Cudd_Density(dd,f,nvars);
|
|
(void) printf("TEST-DENSITY:: %s (%d variables)\n", name, nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D (%g)", densityF);
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
(void) printf("T-D APA ");
|
|
if (!Cudd_ApaPrintMinterm(stdout, dd, f, nvars))
|
|
result = 0;
|
|
}
|
|
/* Test remapping underapproximation. */
|
|
/* s = Cudd_SubsetRemap(dd,f); */
|
|
s = Cudd_RemapUnderApprox(dd,f,nvars,0,option->quality);
|
|
if (s == NULL) {
|
|
(void) printf("TEST-DENSITY: computation failed\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(s);
|
|
sizeS = Cudd_DagSize(s);
|
|
densityS = Cudd_Density(dd,s,nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D ID (%g)", densityS);
|
|
Cudd_PrintDebug(dd, s, nvars, pr);
|
|
}
|
|
if (!Cudd_bddLeq(dd,s,f)) {
|
|
(void) printf("TEST-DENSITY: result not a subset\n");
|
|
result = 0;
|
|
}
|
|
if (densityF > densityS) {
|
|
(void) printf("TEST-DENSITY: result less dense\n");
|
|
/* result = 0; */
|
|
}
|
|
size = sizeS;
|
|
/* Test biased underapproximation. */
|
|
b = Cudd_BiasedUnderApprox(dd,f,Cudd_Not(s),nvars,0,
|
|
option->quality*1.1,option->quality*0.5);
|
|
if (b == NULL) {
|
|
(void) printf("TEST-DENSITY: computation failed\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(b);
|
|
densityB = Cudd_Density(dd,b,nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D BU (%g)", densityB);
|
|
Cudd_PrintDebug(dd, b, nvars, pr);
|
|
}
|
|
if (!Cudd_bddLeq(dd,b,f)) {
|
|
(void) printf("TEST-DENSITY: result not a subset\n");
|
|
result = 0;
|
|
}
|
|
if (densityF > densityB) {
|
|
(void) printf("TEST-DENSITY: result less dense\n");
|
|
/* result = 0; */
|
|
}
|
|
/* Test heavy-branch subsetting. */
|
|
hb = Cudd_SubsetHeavyBranch(dd, f, nvars, size);
|
|
if (hb == NULL) {
|
|
(void) printf("TEST-DENSITY: HB computation failed\n");
|
|
Cudd_RecursiveDeref(dd,s);
|
|
return(0);
|
|
}
|
|
Cudd_Ref(hb);
|
|
densityHB = Cudd_Density(dd,hb,nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D HB (%g)", densityHB);
|
|
Cudd_PrintDebug(dd, hb, nvars, pr);
|
|
}
|
|
if (!Cudd_bddLeq(dd,hb,f)) {
|
|
(void) printf("TEST-DENSITY: HB not a subset\n");
|
|
result = 0;
|
|
}
|
|
/* Test short paths subsetting. */
|
|
sp = Cudd_SubsetShortPaths(dd, f, nvars, size, 0);
|
|
if (sp == NULL) {
|
|
(void) printf("TEST-DENSITY: SP computation failed\n");
|
|
Cudd_RecursiveDeref(dd,s);
|
|
Cudd_RecursiveDeref(dd,hb);
|
|
return(0);
|
|
}
|
|
Cudd_Ref(sp);
|
|
densitySP = Cudd_Density(dd,sp,nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D SP (%g)", densitySP);
|
|
Cudd_PrintDebug(dd, sp, nvars, pr);
|
|
}
|
|
if (!Cudd_bddLeq(dd,sp,f)) {
|
|
(void) printf("TEST-DENSITY: SP not a subset\n");
|
|
result = 0;
|
|
}
|
|
/* Test underapproximation. */
|
|
ua = Cudd_UnderApprox(dd,f,nvars,0,FALSE,option->quality);
|
|
if (ua == NULL) {
|
|
(void) printf("TEST-DENSITY: computation failed\n");
|
|
Cudd_RecursiveDeref(dd,s);
|
|
Cudd_RecursiveDeref(dd,hb);
|
|
Cudd_RecursiveDeref(dd,sp);
|
|
return(0);
|
|
}
|
|
Cudd_Ref(ua);
|
|
densityUA = Cudd_Density(dd,ua,nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D UA (%g)", densityUA);
|
|
Cudd_PrintDebug(dd, ua, nvars, pr);
|
|
}
|
|
if (!Cudd_bddLeq(dd,ua,f)) {
|
|
(void) printf("TEST-DENSITY: result not a subset\n");
|
|
result = 0;
|
|
}
|
|
if (densityF > densityUA) {
|
|
(void) printf("TEST-DENSITY: result less dense\n");
|
|
}
|
|
/* Test compress 2 method. */
|
|
c1 = ntrCompress2(dd, f, nvars, size);
|
|
if (c1 == NULL) {
|
|
(void) printf("TEST-DENSITY: C1 computation failed\n");
|
|
Cudd_RecursiveDeref(dd,s);
|
|
Cudd_RecursiveDeref(dd,hb);
|
|
Cudd_RecursiveDeref(dd,sp);
|
|
Cudd_RecursiveDeref(dd,ua);
|
|
return(0);
|
|
}
|
|
densityC1 = Cudd_Density(dd,c1,nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D C1 (%g)", densityC1);
|
|
Cudd_PrintDebug(dd, c1, nvars, pr);
|
|
}
|
|
if (!Cudd_bddLeq(dd,c1,f)) {
|
|
(void) printf("TEST-DENSITY: C1 not a subset\n");
|
|
result = 0;
|
|
}
|
|
/* Test compress subsetting. */
|
|
c2 = Cudd_SubsetCompress(dd, f, nvars, size);
|
|
if (c2 == NULL) {
|
|
(void) printf("TEST-DENSITY: C2 computation failed\n");
|
|
Cudd_RecursiveDeref(dd,s);
|
|
Cudd_RecursiveDeref(dd,hb);
|
|
Cudd_RecursiveDeref(dd,sp);
|
|
Cudd_RecursiveDeref(dd,ua);
|
|
Cudd_RecursiveDeref(dd,c1);
|
|
return(0);
|
|
}
|
|
Cudd_Ref(c2);
|
|
densityC2 = Cudd_Density(dd,c2,nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-D C2 (%g)", densityC2);
|
|
Cudd_PrintDebug(dd, c2, nvars, pr);
|
|
}
|
|
if (!Cudd_bddLeq(dd,c2,f)) {
|
|
(void) printf("TEST-DENSITY: C2 not a subset\n");
|
|
result = 0;
|
|
}
|
|
/* Dump results if so requested. */
|
|
if (option->bdddump) {
|
|
onames[0] = name; outputs[0] = f;
|
|
onames[1] = (char *) "id"; outputs[1] = s;
|
|
onames[2] = (char *) "bu"; outputs[2] = b;
|
|
onames[3] = (char *) "hb"; outputs[3] = hb;
|
|
onames[4] = (char *) "sp"; outputs[4] = sp;
|
|
onames[5] = (char *) "ua"; outputs[5] = ua;
|
|
onames[6] = (char *) "c1"; outputs[6] = c1;
|
|
onames[7] = (char *) "c2"; outputs[7] = c2;
|
|
result &= Bnet_bddArrayDump(dd, net, option->dumpfile, outputs,
|
|
onames, 8, option->dumpFmt);
|
|
}
|
|
|
|
Cudd_RecursiveDeref(dd,s);
|
|
Cudd_RecursiveDeref(dd,b);
|
|
Cudd_RecursiveDeref(dd,hb);
|
|
Cudd_RecursiveDeref(dd,sp);
|
|
Cudd_RecursiveDeref(dd,ua);
|
|
Cudd_RecursiveDeref(dd,c1);
|
|
Cudd_RecursiveDeref(dd,c2);
|
|
|
|
return(result);
|
|
|
|
} /* end of ntrTestDensityAux */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one BDD for Ntr_TestDecomp.]
|
|
|
|
Description [Processes one BDD for Ntr_TestDecomp. Returns 1 if
|
|
successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [Ntr_TestDecomp]
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestDecompAux(
|
|
DdManager * dd,
|
|
BnetNetwork * net,
|
|
DdNode * f,
|
|
char * name,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *one, *g, *h, *product;
|
|
DdNode **A, **I, **G, **V;
|
|
int pr;
|
|
int i, result;
|
|
int nA, nI, nG, nV;
|
|
int nvars;
|
|
int sizeSa;
|
|
int sizeSi, sizeSg, sizeSv;
|
|
char *onames[9];
|
|
DdNode *outputs[9];
|
|
|
|
result = 1;
|
|
pr = option->verb;
|
|
nvars = Cudd_SupportSize(dd,f);
|
|
if (nvars == CUDD_OUT_OF_MEM) return(0);
|
|
(void) printf("TEST-DECOMP:: %s (%d variables)\n", name, nvars);
|
|
if (pr > 0) {
|
|
(void) printf("T-d ");
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
}
|
|
one = Cudd_ReadOne(dd);
|
|
|
|
/* Test Cudd_bddApproxConjDecomp */
|
|
nA = Cudd_bddApproxConjDecomp(dd,f,&A);
|
|
if (nA == 0) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
g = A[0];
|
|
h = (nA == 2) ? A[1] : one;
|
|
sizeSa = Cudd_SharingSize(A,nA);
|
|
if (pr > 0) {
|
|
(void) printf("T-d SS : %d nodes\n", sizeSa);
|
|
(void) printf("T-d GS ");
|
|
Cudd_PrintDebug(dd, g, nvars, pr);
|
|
(void) printf("T-d HS ");
|
|
Cudd_PrintDebug(dd, h, nvars, pr);
|
|
}
|
|
product = Cudd_bddAnd(dd,g,h);
|
|
if (product == NULL) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(product);
|
|
if (product != f) {
|
|
(void) printf("TEST-DECOMP: result not a decomposition\n");
|
|
result = 0;
|
|
}
|
|
Cudd_RecursiveDeref(dd,product);
|
|
|
|
/* Test Cudd_bddIterConjDecomp */
|
|
nI = Cudd_bddIterConjDecomp(dd,f,&I);
|
|
if (nI == 0) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
g = I[0];
|
|
h = (nI == 2) ? I[1] : one;
|
|
sizeSi = Cudd_SharingSize(I,nI);
|
|
if (pr > 0) {
|
|
(void) printf("T-d SI : %d nodes\n", sizeSi);
|
|
(void) printf("T-d GI ");
|
|
Cudd_PrintDebug(dd, g, nvars, pr);
|
|
(void) printf("T-d HI ");
|
|
Cudd_PrintDebug(dd, h, nvars, pr);
|
|
}
|
|
product = Cudd_bddAnd(dd,g,h);
|
|
if (product == NULL) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(product);
|
|
if (product != f) {
|
|
(void) printf("TEST-DECOMP: result not a decomposition\n");
|
|
result = 0;
|
|
}
|
|
Cudd_RecursiveDeref(dd,product);
|
|
|
|
/* Test Cudd_bddGenConjDecomp */
|
|
nG = Cudd_bddGenConjDecomp(dd,f,&G);
|
|
if (nG == 0) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
g = G[0];
|
|
h = (nG == 2) ? G[1] : one;
|
|
sizeSg = Cudd_SharingSize(G,nG);
|
|
if (pr > 0) {
|
|
(void) printf("T-d SD : %d nodes\n", sizeSg);
|
|
(void) printf("T-d GD ");
|
|
Cudd_PrintDebug(dd, g, nvars, pr);
|
|
(void) printf("T-d HD ");
|
|
Cudd_PrintDebug(dd, h, nvars, pr);
|
|
}
|
|
product = Cudd_bddAnd(dd,g,h);
|
|
if (product == NULL) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(product);
|
|
if (product != f) {
|
|
(void) printf("TEST-DECOMP: result not a decomposition\n");
|
|
result = 0;
|
|
}
|
|
Cudd_RecursiveDeref(dd,product);
|
|
|
|
/* Test Cudd_bddVarConjDecomp */
|
|
nV = Cudd_bddVarConjDecomp(dd,f,&V);
|
|
if (nV == 0) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
g = V[0];
|
|
h = (nV == 2) ? V[1] : one;
|
|
sizeSv = Cudd_SharingSize(V,nV);
|
|
if (pr > 0) {
|
|
(void) printf("T-d SQ : %d nodes\n", sizeSv);
|
|
(void) printf("T-d GQ ");
|
|
Cudd_PrintDebug(dd, g, nvars, pr);
|
|
(void) printf("T-d HQ ");
|
|
Cudd_PrintDebug(dd, h, nvars, pr);
|
|
}
|
|
product = Cudd_bddAnd(dd,g,h);
|
|
if (product == NULL) {
|
|
(void) printf("TEST-DECOMP: computation failed\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(product);
|
|
if (product != f) {
|
|
(void) printf("TEST-DECOMP: result not a decomposition\n");
|
|
result = 0;
|
|
}
|
|
Cudd_RecursiveDeref(dd,product);
|
|
|
|
/* Dump to file if requested. */
|
|
if (option->bdddump) {
|
|
onames[0] = name; outputs[0] = f;
|
|
onames[1] = (char *) "ga"; outputs[1] = A[0];
|
|
onames[2] = (char *) "ha"; outputs[2] = (nA == 2) ? A[1] : one;
|
|
onames[3] = (char *) "gi"; outputs[3] = I[0];
|
|
onames[4] = (char *) "hi"; outputs[4] = (nI == 2) ? I[1] : one;
|
|
onames[5] = (char *) "gg"; outputs[5] = G[0];
|
|
onames[6] = (char *) "hg"; outputs[6] = (nG == 2) ? G[1] : one;
|
|
onames[7] = (char *) "gv"; outputs[7] = V[0];
|
|
onames[8] = (char *) "hv"; outputs[8] = (nV == 2) ? V[1] : one;
|
|
result &= Bnet_bddArrayDump(dd, net, option->dumpfile, outputs,
|
|
onames, 9, option->dumpFmt);
|
|
}
|
|
|
|
/* Clean up. */
|
|
for (i = 0; i < nA; i++) {
|
|
Cudd_RecursiveDeref(dd,A[i]);
|
|
}
|
|
for (i = 0; i < nI; i++) {
|
|
Cudd_RecursiveDeref(dd,I[i]);
|
|
}
|
|
for (i = 0; i < nG; i++) {
|
|
Cudd_RecursiveDeref(dd,G[i]);
|
|
}
|
|
for (i = 0; i < nV; i++) {
|
|
Cudd_RecursiveDeref(dd,V[i]);
|
|
}
|
|
FREE(A);
|
|
FREE(I);
|
|
FREE(G);
|
|
FREE(V);
|
|
|
|
return(result);
|
|
|
|
} /* end of ntrTestDecompAux */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one BDD for Ntr_TestCofactorEstimate.]
|
|
|
|
Description [Processes one BDD for Ntr_TestCofactorEstimate. Returns 1 if
|
|
successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestCofEstAux(
|
|
DdManager * dd,
|
|
BnetNetwork * net,
|
|
DdNode * f,
|
|
char * name,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *support, *scan, *cof;
|
|
int pr;
|
|
int nvars;
|
|
int exactSize, estimate, estimateS;
|
|
int totalExactSize = 0;
|
|
int totalEstimate = 0;
|
|
int totalEstimateS = 0;
|
|
int largestError = -1;
|
|
int largestErrorS = -1;
|
|
DdNode *errorVar = NULL;
|
|
|
|
pr = option->verb;
|
|
support = Cudd_Support(dd,f);
|
|
if (support == NULL) return(0);
|
|
Cudd_Ref(support);
|
|
nvars = Cudd_DagSize(support) - 1;
|
|
scan = support;
|
|
while (!Cudd_IsConstant(scan)) {
|
|
DdNode *var = Cudd_bddIthVar(dd,scan->index);
|
|
cof = Cudd_Cofactor(dd,f,var);
|
|
if (cof == NULL) return(0);
|
|
Cudd_Ref(cof);
|
|
exactSize = Cudd_DagSize(cof);
|
|
totalExactSize += exactSize;
|
|
estimate = Cudd_EstimateCofactor(dd,f,scan->index,1);
|
|
totalEstimate += estimate;
|
|
if (estimate < exactSize)
|
|
(void) printf("Optimistic estimate!\n");
|
|
if (estimate - exactSize > largestError) {
|
|
largestError = estimate - exactSize;
|
|
errorVar = var;
|
|
}
|
|
estimateS = Cudd_EstimateCofactorSimple(f,scan->index);
|
|
totalEstimateS += estimateS;
|
|
if (estimateS < exactSize)
|
|
(void) printf("Optimistic estimateS!\n");
|
|
if (estimateS - exactSize > largestErrorS)
|
|
largestErrorS = estimateS - exactSize;
|
|
Cudd_RecursiveDeref(dd,cof);
|
|
scan = cuddT(scan);
|
|
}
|
|
Cudd_RecursiveDeref(dd,support);
|
|
(void) printf("TEST-COF:: %s (%d vars)", name, nvars);
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
(void) printf("T-c : %d\n", totalExactSize);
|
|
(void) printf("T-c E : %d %d\n", totalEstimate, largestError);
|
|
(void) printf("T-c S : %d %d\n", totalEstimateS, largestErrorS);
|
|
|
|
/* Dump to file if requested. */
|
|
if (option->bdddump) {
|
|
char *onames[3];
|
|
DdNode *outputs[3];
|
|
int result;
|
|
cof = Cudd_Cofactor(dd,f,errorVar);
|
|
if (cof == NULL) return(0);
|
|
Cudd_Ref(cof);
|
|
onames[0] = name; outputs[0] = f;
|
|
onames[1] = (char *) "var"; outputs[1] = errorVar;
|
|
onames[2] = (char *) "cof"; outputs[2] = cof;
|
|
result = Bnet_bddArrayDump(dd, net, option->dumpfile, outputs,
|
|
onames, 3, option->dumpFmt);
|
|
Cudd_RecursiveDeref(dd,cof);
|
|
if (result == 0) return(0);
|
|
}
|
|
|
|
return(1);
|
|
|
|
} /* end of ntrTestCofEstAux */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one BDD for Ntr_TestClipping.]
|
|
|
|
Description [Processes one BDD for Ntr_TestClipping. It checks whether
|
|
clipping was correct. Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [Ntr_TestClipping]
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestClippingAux(
|
|
DdManager * dd,
|
|
BnetNetwork * net1,
|
|
DdNode * f,
|
|
char * name,
|
|
DdNode * g,
|
|
char * gname,
|
|
NtrOptions * option)
|
|
{
|
|
DdNode *prod, *sub, *sup;
|
|
DdNode *subF, *subG, *psub;
|
|
DdNode *supF, *supG, *psup;
|
|
int pr, nvars, depth;
|
|
int sizeProd, sizeSub, sizeSup;
|
|
static char *onames[7];
|
|
DdNode *outputs[7];
|
|
DdNode *operands[2];
|
|
int retval = 1;
|
|
int threshold = (option->threshold < 0) ? 0 : option->threshold;
|
|
|
|
pr = option->verb;
|
|
operands[0] = f; operands[1] = g;
|
|
nvars = Cudd_VectorSupportSize(dd,operands,2);
|
|
if (nvars == CUDD_OUT_OF_MEM) return(0);
|
|
depth = (int) ((double) nvars * option->clip);
|
|
(void) printf("TEST-CLIP:: %s depth = %d\n", name, depth);
|
|
(void) printf("T-C ");
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
|
|
/* Compute product. */
|
|
prod = Cudd_bddAnd(dd, f, g);
|
|
if (prod == NULL) {
|
|
(void) printf("TEST-CLIP: product failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(prod);
|
|
(void) printf("T-C P= ");
|
|
Cudd_PrintDebug(dd, prod, nvars, pr);
|
|
sizeProd = Cudd_DagSize(prod);
|
|
|
|
/* Compute subset of product. */
|
|
sub = Cudd_bddClippingAnd(dd, f, g, depth, 0);
|
|
if (sub == NULL) {
|
|
(void) printf("TEST-CLIP: subsetting product failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(sub);
|
|
(void) printf("T-C P- ");
|
|
Cudd_PrintDebug(dd, sub, nvars, pr);
|
|
sizeSub = Cudd_DagSize(sub);
|
|
if (sizeSub > sizeProd) {
|
|
(void) printf("TEST-CLIP: subsetting product not safe.\n");
|
|
}
|
|
|
|
/* Compute product of subsets. */
|
|
subF = Cudd_RemapUnderApprox(dd,f,nvars,threshold,option->quality);
|
|
if (subF == NULL) {
|
|
(void) printf("TEST-CLIP: subsetting of f failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(subF);
|
|
subG = Cudd_RemapUnderApprox(dd,g,nvars,threshold,option->quality);
|
|
if (subF == NULL) {
|
|
(void) printf("TEST-CLIP: subsetting of g failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(subG);
|
|
psub = Cudd_bddAnd(dd,subF,subG);
|
|
if (psub == NULL) {
|
|
(void) printf("TEST-CLIP: product of subsets failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(psub);
|
|
Cudd_RecursiveDeref(dd,subF);
|
|
Cudd_RecursiveDeref(dd,subG);
|
|
(void) printf("T-C P< ");
|
|
Cudd_PrintDebug(dd, psub, nvars, pr);
|
|
|
|
/* Compute superset of product. */
|
|
sup = Cudd_bddClippingAnd(dd, f, g, depth, 1);
|
|
if (sup == NULL) {
|
|
(void) printf("TEST-CLIP: supersetting product failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(sup);
|
|
(void) printf("T-C P+ ");
|
|
Cudd_PrintDebug(dd, sup, nvars, pr);
|
|
sizeSup = Cudd_DagSize(sup);
|
|
if (sizeSup > sizeProd) {
|
|
(void) printf("TEST-CLIP: supersetting product not safe.\n");
|
|
}
|
|
|
|
/* Compute product of supersets. */
|
|
supF = Cudd_RemapOverApprox(dd,f,nvars,threshold,option->quality);
|
|
if (supF == NULL) {
|
|
(void) printf("TEST-CLIP: supersetting of f failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(supF);
|
|
supG = Cudd_RemapOverApprox(dd,g,nvars,threshold,option->quality);
|
|
if (supF == NULL) {
|
|
(void) printf("TEST-CLIP: supersetting of g failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(supG);
|
|
psup = Cudd_bddAnd(dd,supF,supG);
|
|
if (psup == NULL) {
|
|
(void) printf("TEST-CLIP: product of supersets failed.\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(psup);
|
|
Cudd_RecursiveDeref(dd,supF);
|
|
Cudd_RecursiveDeref(dd,supG);
|
|
(void) printf("T-C P> ");
|
|
Cudd_PrintDebug(dd, psup, nvars, pr);
|
|
|
|
if (option->bdddump) {
|
|
onames[0] = name; outputs[0] = f;
|
|
onames[1] = gname; outputs[1] = g;
|
|
onames[2] = (char *) "prod"; outputs[2] = prod;
|
|
onames[3] = (char *) "sub"; outputs[3] = sub;
|
|
onames[4] = (char *) "sup"; outputs[4] = sup;
|
|
onames[5] = (char *) "psub"; outputs[5] = psub;
|
|
onames[6] = (char *) "psup"; outputs[6] = psup;
|
|
retval &= Bnet_bddArrayDump(dd, net1, option->dumpfile, outputs,
|
|
onames, 7, option->dumpFmt);
|
|
}
|
|
|
|
/* Check correctness. */
|
|
if (!Cudd_bddLeq(dd,sub,prod)) {
|
|
(void) printf("TEST-CLIP: subsetting product not a subset.\n");
|
|
return(0);
|
|
}
|
|
if (!Cudd_bddLeq(dd,prod,sup)) {
|
|
(void) printf("TEST-CLIP: supersetting product not a superset.\n");
|
|
return(0);
|
|
}
|
|
if (!Cudd_bddLeq(dd,psub,prod)) {
|
|
(void) printf("TEST-CLIP: product of subsets not a subset.\n");
|
|
return(0);
|
|
}
|
|
if (!Cudd_bddLeq(dd,prod,psup)) {
|
|
(void) printf("TEST-CLIP: product of supersets not a superset.\n");
|
|
return(0);
|
|
}
|
|
|
|
Cudd_RecursiveDeref(dd,prod);
|
|
Cudd_RecursiveDeref(dd,sub);
|
|
Cudd_RecursiveDeref(dd,sup);
|
|
Cudd_RecursiveDeref(dd,psub);
|
|
Cudd_RecursiveDeref(dd,psup);
|
|
|
|
return(retval);
|
|
|
|
} /* end of ntrTestClippingAux */
|
|
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one triplet of BDDs for Ntr_TestEquivAndContain.]
|
|
|
|
Description [Processes one triplet of BDDs for Ntr_TestEquivAndContain.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [Ntr_TestEquivAndContain]
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestEquivAndContainAux(
|
|
DdManager *dd,
|
|
BnetNetwork *net1,
|
|
DdNode *f,
|
|
char *fname,
|
|
DdNode *g,
|
|
char *gname,
|
|
DdNode *d,
|
|
char *dname,
|
|
NtrOptions *option)
|
|
{
|
|
DdNode *xor_, *diff, *ndiff;
|
|
int pr, nvars;
|
|
int equiv, implies;
|
|
static char *onames[6];
|
|
DdNode *outputs[6];
|
|
DdNode *fgd[3];
|
|
|
|
pr = option->verb;
|
|
fgd[0] = f; fgd[1] = g; fgd[2] = d;
|
|
nvars = Cudd_VectorSupportSize(dd,fgd,3);
|
|
if (nvars == CUDD_OUT_OF_MEM) return(0);
|
|
(void) printf("TEST-DC:: %s [=<]= %s unless %s\n", fname, gname, dname);
|
|
(void) printf("T-F ");
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
(void) printf("T-G ");
|
|
Cudd_PrintDebug(dd, g, nvars, pr);
|
|
(void) printf("T-D ");
|
|
Cudd_PrintDebug(dd, d, nvars, pr);
|
|
|
|
/* Check equivalence unless don't cares. */
|
|
xor_ = Cudd_bddXor(dd, f, g);
|
|
if (xor_ == NULL) {
|
|
(void) printf("TEST-DC: XOR computation failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(xor_);
|
|
equiv = Cudd_EquivDC(dd, f, g, d);
|
|
if (equiv != Cudd_bddLeq(dd,xor_,d)) {
|
|
(void) printf("TEST-DC: EquivDC computation incorrect (1).\n");
|
|
(void) printf(" EquivDC states that %s and %s are %s\n",
|
|
fname, gname, equiv ? "equivalent" : "not equivalent");
|
|
(void) printf("T-X ");
|
|
Cudd_PrintDebug(dd, xor_, nvars, pr);
|
|
return(0);
|
|
}
|
|
equiv = Cudd_EquivDC(dd, f, g, Cudd_Not(d));
|
|
if (equiv != Cudd_bddLeq(dd,xor_,Cudd_Not(d))) {
|
|
(void) printf("TEST-DC: EquivDC computation incorrect (2).\n");
|
|
(void) printf(" EquivDC states that %s and %s are %s\n",
|
|
fname, gname, equiv ? "equivalent" : "not equivalent");
|
|
(void) printf("T-X ");
|
|
Cudd_PrintDebug(dd, xor_, nvars, pr);
|
|
return(0);
|
|
}
|
|
equiv = Cudd_EquivDC(dd, f, Cudd_Not(g), d);
|
|
if (equiv != Cudd_bddLeq(dd,Cudd_Not(xor_),d)) {
|
|
(void) printf("TEST-DC: EquivDC computation incorrect (3).\n");
|
|
(void) printf(" EquivDC states that %s and not %s are %s\n",
|
|
fname, gname, equiv ? "equivalent" : "not equivalent");
|
|
(void) printf("T-X ");
|
|
Cudd_PrintDebug(dd, Cudd_Not(xor_), nvars, pr);
|
|
return(0);
|
|
}
|
|
equiv = Cudd_EquivDC(dd, f, Cudd_Not(g), Cudd_Not(d));
|
|
if (equiv != Cudd_bddLeq(dd,d,xor_)) {
|
|
(void) printf("TEST-DC: EquivDC computation incorrect (4).\n");
|
|
(void) printf(" EquivDC states that %s and not %s are %s\n",
|
|
fname, gname, equiv ? "equivalent" : "not equivalent");
|
|
(void) printf("T-X ");
|
|
Cudd_PrintDebug(dd, Cudd_Not(xor_), nvars, pr);
|
|
return(0);
|
|
}
|
|
|
|
/* Check containment unless don't cares. */
|
|
diff = Cudd_bddAnd(dd, f, Cudd_Not(g));
|
|
if (diff == NULL) {
|
|
(void) printf("TEST-DC: AND/NOT computation failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(diff);
|
|
implies = Cudd_bddLeqUnless(dd, f, g, d);
|
|
if (implies != Cudd_bddLeq(dd,diff,d)) {
|
|
(void) printf("TEST-DC: LeqUnless computation incorrect (1).\n");
|
|
(void) printf(" LeqUnless states that %s %s %s\n",
|
|
fname, implies ? "implies" : "does not imply", gname);
|
|
(void) printf("T-I ");
|
|
Cudd_PrintDebug(dd, diff, nvars, pr);
|
|
return(0);
|
|
}
|
|
implies = Cudd_bddLeqUnless(dd, f, g, Cudd_Not(d));
|
|
if (implies != Cudd_bddLeq(dd,diff,Cudd_Not(d))) {
|
|
(void) printf("TEST-DC: LeqUnless computation incorrect (2).\n");
|
|
(void) printf(" LeqUnless states that %s %s %s\n",
|
|
fname, implies ? "implies" : "does not imply", gname);
|
|
(void) printf("T-I ");
|
|
Cudd_PrintDebug(dd, diff, nvars, pr);
|
|
return(0);
|
|
}
|
|
ndiff = Cudd_bddAnd(dd, f, g);
|
|
if (ndiff == NULL) {
|
|
(void) printf("TEST-DC: AND computation failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(ndiff);
|
|
implies = Cudd_bddLeqUnless(dd, f, Cudd_Not(g), d);
|
|
if (implies != Cudd_bddLeq(dd,ndiff,d)) {
|
|
(void) printf("TEST-DC: LeqUnless computation incorrect (3).\n");
|
|
(void) printf(" LeqUnless states that %s %s not(%s)\n",
|
|
fname, implies ? "implies" : "does not imply", gname);
|
|
(void) printf("T-I ");
|
|
Cudd_PrintDebug(dd, ndiff, nvars, pr);
|
|
return(0);
|
|
}
|
|
implies = Cudd_bddLeqUnless(dd, f, Cudd_Not(g), Cudd_Not(d));
|
|
if (implies != Cudd_bddLeq(dd,ndiff,Cudd_Not(d))) {
|
|
(void) printf("TEST-DC: LeqUnless computation incorrect (3).\n");
|
|
(void) printf(" LeqUnless states that %s %s not(%s)\n",
|
|
fname, implies ? "implies" : "does not imply", gname);
|
|
(void) printf("T-I ");
|
|
Cudd_PrintDebug(dd, ndiff, nvars, pr);
|
|
return(0);
|
|
}
|
|
if (option->bdddump) {
|
|
onames[0] = fname; outputs[0] = f;
|
|
onames[1] = gname; outputs[1] = g;
|
|
onames[2] = dname; outputs[2] = d;
|
|
onames[3] = (char *) "xor"; outputs[3] = xor_;
|
|
onames[4] = (char *) "diff"; outputs[4] = diff;
|
|
onames[5] = (char *) "ndiff"; outputs[5] = ndiff;
|
|
if (!Bnet_bddArrayDump(dd, net1, option->dumpfile, outputs, onames,
|
|
6, option->dumpFmt))
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,xor_);
|
|
Cudd_RecursiveDeref(dd,diff);
|
|
Cudd_RecursiveDeref(dd,ndiff);
|
|
|
|
return(1);
|
|
|
|
} /* end of ntrTestEquivAndContainAux */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one pair of BDDs for Ntr_TestClosestCube.]
|
|
|
|
Description [Processes one pair of BDDs for Ntr_TestClosestCube.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [Ntr_TestClosestCube]
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestClosestCubeAux(
|
|
DdManager *dd,
|
|
BnetNetwork *net,
|
|
DdNode *f,
|
|
char *fname,
|
|
DdNode *g,
|
|
char *gname,
|
|
DdNode **vars,
|
|
NtrOptions *option)
|
|
{
|
|
DdNode *cube, *cubeN;
|
|
int distance, pr, nvars;
|
|
DdNode *fg[2];
|
|
static char *onames[4];
|
|
DdNode *outputs[4];
|
|
|
|
pr = option->verb;
|
|
fg[0] = f; fg[1] = g;
|
|
nvars = Cudd_VectorSupportSize(dd,fg,2);
|
|
if (nvars == CUDD_OUT_OF_MEM) return(0);
|
|
(void) printf("TEST-CC:: H(%s, %s)\n", fname, gname);
|
|
(void) printf("T-F ");
|
|
Cudd_PrintDebug(dd, f, nvars, pr);
|
|
(void) printf("T-G ");
|
|
Cudd_PrintDebug(dd, g, nvars, pr);
|
|
|
|
cube = Cudd_bddClosestCube(dd, f, g, &distance);
|
|
if (cube == NULL) {
|
|
(void) printf("TEST-CC: computation failed (1).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(cube);
|
|
(void) printf("T-C (%d) ", distance);
|
|
Cudd_PrintDebug(dd, cube, nvars, pr);
|
|
if (distance == 0) {
|
|
if (!Cudd_bddLeq(dd,cube,g)) {
|
|
(void) printf("TEST-CC: distance-0 cube not in g (2).\n");
|
|
return(0);
|
|
}
|
|
}
|
|
|
|
(void) printf("T-GN ");
|
|
Cudd_PrintDebug(dd, Cudd_Not(g), nvars, pr);
|
|
cubeN = Cudd_bddClosestCube(dd, f, Cudd_Not(g), &distance);
|
|
if (cubeN == NULL) {
|
|
(void) printf("TEST-CC: computation failed (3).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(cubeN);
|
|
(void) printf("T-N (%d) ", distance);
|
|
Cudd_PrintDebug(dd, cubeN, nvars, pr);
|
|
if (distance == 0) {
|
|
if (!Cudd_bddLeq(dd,cubeN,Cudd_Not(g))) {
|
|
(void) printf("TEST-CC: distance-0 cube not in not(g) (4).\n");
|
|
return(0);
|
|
}
|
|
} else {
|
|
int d, *minterm;
|
|
int numvars = Cudd_ReadSize(dd);
|
|
DdNode *scan, *zero;
|
|
DdNode *minBdd = Cudd_bddPickOneMinterm(dd,cubeN,vars,numvars);
|
|
if (minBdd == NULL) {
|
|
(void) printf("TEST-CC: minterm selection failed (5).\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(minBdd);
|
|
minterm = ALLOC(int,numvars);
|
|
if (minterm == NULL) {
|
|
(void) printf("TEST-CC: allocation failed (6).\n");
|
|
Cudd_RecursiveDeref(dd,minBdd);
|
|
return(0);
|
|
}
|
|
scan = minBdd;
|
|
zero = Cudd_Not(DD_ONE(dd));
|
|
while (!Cudd_IsConstant(scan)) {
|
|
DdNode *R = Cudd_Regular(scan);
|
|
DdNode *T = Cudd_T(R);
|
|
DdNode *E = Cudd_E(R);
|
|
if (R != scan) {
|
|
T = Cudd_Not(T);
|
|
E = Cudd_Not(E);
|
|
}
|
|
if (T == zero) {
|
|
minterm[Cudd_NodeReadIndex(R)] = 0;
|
|
scan = E;
|
|
} else {
|
|
minterm[Cudd_NodeReadIndex(R)] = 1;
|
|
scan = T;
|
|
}
|
|
}
|
|
Cudd_RecursiveDeref(dd,minBdd);
|
|
d = Cudd_MinHammingDist(dd,Cudd_Not(g),minterm,numvars);
|
|
FREE(minterm);
|
|
if (d != distance) {
|
|
(void) printf("TEST-CC: distance disagreement (7).\n");
|
|
return(0);
|
|
}
|
|
}
|
|
|
|
if (option->bdddump) {
|
|
onames[0] = fname; outputs[0] = f;
|
|
onames[1] = gname; outputs[1] = g;
|
|
onames[2] = (char *) "cube"; outputs[2] = cube;
|
|
onames[3] = (char *) "cubeN"; outputs[3] = cubeN;
|
|
if (!Bnet_bddArrayDump(dd, net, option->dumpfile, outputs, onames,
|
|
4, option->dumpFmt))
|
|
return(0);
|
|
}
|
|
Cudd_RecursiveDeref(dd,cube);
|
|
Cudd_RecursiveDeref(dd,cubeN);
|
|
|
|
return(1);
|
|
|
|
} /* end of ntrTestClosestCubeAux */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Processes one BDDs for Ntr_TestCharToVect.]
|
|
|
|
Description [Processes one BDD for Ntr_TestCharToVect.
|
|
Returns 1 if successful; 0 otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [Ntr_TestCharToVect]
|
|
|
|
******************************************************************************/
|
|
static int
|
|
ntrTestCharToVect(
|
|
DdManager * dd,
|
|
DdNode * f,
|
|
NtrOptions *option)
|
|
{
|
|
DdNode **vector;
|
|
int sharingSize;
|
|
DdNode *verify;
|
|
int pr = option->verb;
|
|
int i;
|
|
|
|
(void) fprintf(stdout,"f");
|
|
Cudd_PrintDebug(dd, f, Cudd_ReadSize(dd), 1);
|
|
if (pr > 1) {
|
|
Cudd_bddPrintCover(dd, f, f);
|
|
}
|
|
vector = Cudd_bddCharToVect(dd,f);
|
|
if (vector == NULL) return(0);
|
|
sharingSize = Cudd_SharingSize(vector, Cudd_ReadSize(dd));
|
|
(void) fprintf(stdout, "Vector Size: %d components %d nodes\n",
|
|
Cudd_ReadSize(dd), sharingSize);
|
|
for (i = 0; i < Cudd_ReadSize(dd); i++) {
|
|
(void) fprintf(stdout,"v[%d]",i);
|
|
Cudd_PrintDebug(dd, vector[i], Cudd_ReadSize(dd), 1);
|
|
if (pr > 1) {
|
|
Cudd_bddPrintCover(dd, vector[i], vector[i]);
|
|
}
|
|
}
|
|
verify = Cudd_bddVectorCompose(dd,f,vector);
|
|
if (verify != Cudd_ReadOne(dd)) {
|
|
(void) fprintf(stdout, "Verification failed!\n");
|
|
return(0);
|
|
}
|
|
Cudd_Ref(verify);
|
|
Cudd_IterDerefBdd(dd, verify);
|
|
for (i = 0; i < Cudd_ReadSize(dd); i++) {
|
|
Cudd_IterDerefBdd(dd, vector[i]);
|
|
}
|
|
FREE(vector);
|
|
return(1);
|
|
|
|
} /* end of ntrTestCharToVect */
|
|
|
|
|
|
#if 0
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Try hard to squeeze a BDD.]
|
|
|
|
Description [Try hard to squeeze a BDD.
|
|
Returns a pointer to the squeezed BDD if successful; NULL otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [ntrTestDensityAux Cudd_SubsetCompress]
|
|
|
|
******************************************************************************/
|
|
static DdNode *
|
|
ntrCompress1(
|
|
DdManager * dd,
|
|
DdNode * f,
|
|
int nvars,
|
|
int threshold)
|
|
{
|
|
DdNode *res, *tmp1, *tmp2;
|
|
int sizeI, size;
|
|
|
|
tmp1 = Cudd_RemapUnderApprox(dd,f,nvars,0,1.0);
|
|
if (tmp1 == NULL) return(NULL);
|
|
Cudd_Ref(tmp1);
|
|
sizeI = Cudd_DagSize(tmp1);
|
|
size = (sizeI < threshold) ? sizeI : threshold;
|
|
tmp2 = Cudd_SubsetShortPaths(dd, tmp1, nvars, size, 0);
|
|
if (tmp2 == NULL) {
|
|
Cudd_RecursiveDeref(dd,tmp1);
|
|
return(NULL);
|
|
}
|
|
Cudd_Ref(tmp2);
|
|
Cudd_RecursiveDeref(dd,tmp1);
|
|
res = Cudd_bddSqueeze(dd,tmp2,f);
|
|
if (res == NULL) {
|
|
Cudd_RecursiveDeref(dd,tmp2);
|
|
return(NULL);
|
|
}
|
|
Cudd_Ref(res);
|
|
Cudd_RecursiveDeref(dd,tmp2);
|
|
return(res);
|
|
|
|
} /* end of ntrCompress1 */
|
|
#endif
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Try hard to squeeze a BDD.]
|
|
|
|
Description [Try hard to squeeze a BDD.
|
|
Returns a pointer to the squeezed BDD if successful; NULL otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [ntrTestDensityAux Cudd_SubsetCompress]
|
|
|
|
******************************************************************************/
|
|
static DdNode *
|
|
ntrCompress2(
|
|
DdManager * dd,
|
|
DdNode * f,
|
|
int nvars,
|
|
int threshold)
|
|
{
|
|
DdNode *res, *tmp1, *tmp2;
|
|
int sizeI;
|
|
|
|
tmp1 = Cudd_RemapUnderApprox(dd,f,nvars,0,1.0);
|
|
if (tmp1 == NULL) return(NULL);
|
|
Cudd_Ref(tmp1);
|
|
sizeI = Cudd_DagSize(tmp1);
|
|
if (sizeI > threshold) {
|
|
tmp2 = Cudd_SubsetShortPaths(dd, tmp1, nvars, threshold, 0);
|
|
if (tmp2 == NULL) {
|
|
Cudd_RecursiveDeref(dd,tmp1);
|
|
return(NULL);
|
|
}
|
|
Cudd_Ref(tmp2);
|
|
Cudd_RecursiveDeref(dd,tmp1);
|
|
} else {
|
|
tmp2 = tmp1;
|
|
}
|
|
res = Cudd_bddSqueeze(dd,tmp2,f);
|
|
if (res == NULL) {
|
|
Cudd_RecursiveDeref(dd,tmp2);
|
|
return(NULL);
|
|
}
|
|
Cudd_Ref(res);
|
|
if (Cudd_Density(dd,res,nvars) < Cudd_Density(dd,tmp2,nvars)) {
|
|
Cudd_RecursiveDeref(dd,res);
|
|
return(tmp2);
|
|
} else {
|
|
Cudd_RecursiveDeref(dd,tmp2);
|
|
return(res);
|
|
}
|
|
|
|
} /* end of ntrCompress2 */
|
|
|
|
|
|
/**Function********************************************************************
|
|
|
|
Synopsis [Checks whether node is a buffer.]
|
|
|
|
Description [Checks whether node is a buffer. Returns a pointer to the
|
|
input node if nd is a buffer; NULL otherwise.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
static BnetNode *
|
|
ntrNodeIsBuffer(
|
|
BnetNode *nd,
|
|
st_table *hash)
|
|
{
|
|
BnetNode *inpnd;
|
|
|
|
if (nd->ninp != 1) return(0);
|
|
if (!st_lookup(hash, nd->inputs[0], &inpnd)) return(0);
|
|
|
|
return(nd->dd == inpnd->dd ? inpnd : NULL);
|
|
|
|
} /* end of ntrNodeIsBuffer */
|