Skip to content
Projects
Groups
Snippets
Help
This project
Loading...
Sign in / Register
Toggle navigation
A
abc
Overview
Overview
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
lvzhengyang
abc
Commits
f26ea1ea
Commit
f26ea1ea
authored
Nov 27, 2021
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Changes to make compiler happy.
parent
96bdcd2b
Show whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
231 additions
and
1 deletions
+231
-1
src/base/abci/abcNtbdd.c
+2
-1
src/bdd/cudd/cuddAddIte.c
+25
-0
src/bdd/cudd/cuddAddNeg.c
+20
-0
src/bdd/cudd/cuddBddAbs.c
+19
-0
src/bdd/cudd/cuddBddIte.c
+24
-0
src/bdd/cudd/cuddClip.c
+32
-0
src/bdd/cudd/cuddMatMult.c
+21
-0
src/bdd/cudd/cuddPriority.c
+24
-0
src/bdd/cudd/cuddSat.c
+44
-0
src/bdd/cudd/cuddZddIsop.c
+20
-0
No files found.
src/base/abci/abcNtbdd.c
View file @
f26ea1ea
...
@@ -237,7 +237,8 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
...
@@ -237,7 +237,8 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
{
{
Abc_Obj_t
*
pNodeNew
,
*
pNodeNew0
,
*
pNodeNew1
,
*
pNodeNewC
;
Abc_Obj_t
*
pNodeNew
,
*
pNodeNew0
,
*
pNodeNew1
,
*
pNodeNewC
;
assert
(
!
Cudd_IsComplement
(
bFunc
)
);
assert
(
!
Cudd_IsComplement
(
bFunc
)
);
if
(
bFunc
==
b1
||
bFunc
==
a1
)
assert
(
b1
==
a1
);
if
(
bFunc
==
a1
)
return
Abc_NtkCreateNodeConst1
(
pNtkNew
);
return
Abc_NtkCreateNodeConst1
(
pNtkNew
);
if
(
bFunc
==
a0
)
if
(
bFunc
==
a0
)
return
Abc_NtkCreateNodeConst0
(
pNtkNew
);
return
Abc_NtkCreateNodeConst0
(
pNtkNew
);
...
...
src/bdd/cudd/cuddAddIte.c
View file @
f26ea1ea
...
@@ -359,6 +359,22 @@ Cudd_addCmpl(
...
@@ -359,6 +359,22 @@ Cudd_addCmpl(
}
/* end of Cudd_addCmpl */
}
/* end of Cudd_addCmpl */
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 as a key
that can be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
Cudd_addLeq_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
g
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Determines whether f is less than or equal to g.]
Synopsis [Determines whether f is less than or equal to g.]
...
@@ -394,7 +410,11 @@ Cudd_addLeq(
...
@@ -394,7 +410,11 @@ Cudd_addLeq(
if
(
g
==
DD_MINUS_INFINITY
(
dd
))
return
(
0
);
/* since f != g */
if
(
g
==
DD_MINUS_INFINITY
(
dd
))
return
(
0
);
/* since f != g */
/* Check cache. */
/* Check cache. */
#ifdef USE_CASH_DUMMY
tmp
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_addLeq_dummy
,
f
,
g
);
#else
tmp
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_addLeq
,
f
,
g
);
tmp
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_addLeq
,
f
,
g
);
#endif
if
(
tmp
!=
NULL
)
{
if
(
tmp
!=
NULL
)
{
return
(
tmp
==
DD_ONE
(
dd
));
return
(
tmp
==
DD_ONE
(
dd
));
}
}
...
@@ -416,8 +436,13 @@ Cudd_addLeq(
...
@@ -416,8 +436,13 @@ Cudd_addLeq(
res
=
Cudd_addLeq
(
dd
,
fvn
,
gvn
)
&&
Cudd_addLeq
(
dd
,
fv
,
gv
);
res
=
Cudd_addLeq
(
dd
,
fvn
,
gvn
)
&&
Cudd_addLeq
(
dd
,
fv
,
gv
);
/* Store result in cache and return. */
/* Store result in cache and return. */
#ifdef USE_CASH_DUMMY
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_addLeq_dummy
,
f
,
g
,
Cudd_NotCond
(
DD_ONE
(
dd
),
res
==
0
));
#else
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_addLeq
,
f
,
g
,
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_addLeq
,
f
,
g
,
Cudd_NotCond
(
DD_ONE
(
dd
),
res
==
0
));
Cudd_NotCond
(
DD_ONE
(
dd
),
res
==
0
));
#endif
return
(
res
);
return
(
res
);
}
/* end of Cudd_addLeq */
}
/* end of Cudd_addLeq */
...
...
src/bdd/cudd/cuddAddNeg.c
View file @
f26ea1ea
...
@@ -226,6 +226,22 @@ cuddAddNegateRecur(
...
@@ -226,6 +226,22 @@ cuddAddNegateRecur(
}
/* end of cuddAddNegateRecur */
}
/* end of cuddAddNegateRecur */
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup1 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
Cudd_addRoundOff_dummy
(
DdManager
*
dd
,
DdNode
*
f
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addRoundOff.]
Synopsis [Implements the recursive step of Cudd_addRoundOff.]
...
@@ -253,7 +269,11 @@ cuddAddRoundOffRecur(
...
@@ -253,7 +269,11 @@ cuddAddRoundOffRecur(
res
=
cuddUniqueConst
(
dd
,
n
);
res
=
cuddUniqueConst
(
dd
,
n
);
return
(
res
);
return
(
res
);
}
}
#ifdef USE_CASH_DUMMY
cacheOp
=
(
DD_CTFP1
)
Cudd_addRoundOff_dummy
;
#else
cacheOp
=
(
DD_CTFP1
)
Cudd_addRoundOff
;
cacheOp
=
(
DD_CTFP1
)
Cudd_addRoundOff
;
#endif
res
=
cuddCacheLookup1
(
dd
,
cacheOp
,
f
);
res
=
cuddCacheLookup1
(
dd
,
cacheOp
,
f
);
if
(
res
!=
NULL
)
{
if
(
res
!=
NULL
)
{
return
(
res
);
return
(
res
);
...
...
src/bdd/cudd/cuddBddAbs.c
View file @
f26ea1ea
...
@@ -266,6 +266,21 @@ Cudd_bddBooleanDiff(
...
@@ -266,6 +266,21 @@ Cudd_bddBooleanDiff(
}
/* end of Cudd_bddBooleanDiff */
}
/* end of Cudd_bddBooleanDiff */
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
Cudd_bddVarIsDependent_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
var
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Checks whether a variable is dependent on others in a
Synopsis [Checks whether a variable is dependent on others in a
...
@@ -305,7 +320,11 @@ Cudd_bddVarIsDependent(
...
@@ -305,7 +320,11 @@ Cudd_bddVarIsDependent(
return
(
0
);
return
(
0
);
}
}
#ifdef USE_CASH_DUMMY
cacheOp
=
(
DD_CTFP
)
Cudd_bddVarIsDependent_dummy
;
#else
cacheOp
=
(
DD_CTFP
)
Cudd_bddVarIsDependent
;
cacheOp
=
(
DD_CTFP
)
Cudd_bddVarIsDependent
;
#endif
res
=
cuddCacheLookup2
(
dd
,
cacheOp
,
f
,
var
);
res
=
cuddCacheLookup2
(
dd
,
cacheOp
,
f
,
var
);
if
(
res
!=
NULL
)
{
if
(
res
!=
NULL
)
{
return
(
res
!=
zero
);
return
(
res
!=
zero
);
...
...
src/bdd/cudd/cuddBddIte.c
View file @
f26ea1ea
...
@@ -520,6 +520,22 @@ Cudd_bddXnor(
...
@@ -520,6 +520,22 @@ Cudd_bddXnor(
}
/* end of Cudd_bddXnor */
}
/* end of Cudd_bddXnor */
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
Cudd_bddLeq_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
g
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Determines whether f is less than or equal to g.]
Synopsis [Determines whether f is less than or equal to g.]
...
@@ -573,7 +589,11 @@ Cudd_bddLeq(
...
@@ -573,7 +589,11 @@ Cudd_bddLeq(
/* Here neither f nor g is constant. */
/* Here neither f nor g is constant. */
/* Check cache. */
/* Check cache. */
#ifdef USE_CASH_DUMMY
tmp
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_bddLeq_dummy
,
f
,
g
);
#else
tmp
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_bddLeq
,
f
,
g
);
tmp
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_bddLeq
,
f
,
g
);
#endif
if
(
tmp
!=
NULL
)
{
if
(
tmp
!=
NULL
)
{
return
(
tmp
==
one
);
return
(
tmp
==
one
);
}
}
...
@@ -605,7 +625,11 @@ Cudd_bddLeq(
...
@@ -605,7 +625,11 @@ Cudd_bddLeq(
res
=
Cudd_bddLeq
(
dd
,
fvn
,
gvn
)
&&
Cudd_bddLeq
(
dd
,
fv
,
gv
);
res
=
Cudd_bddLeq
(
dd
,
fvn
,
gvn
)
&&
Cudd_bddLeq
(
dd
,
fv
,
gv
);
/* Store result in cache and return. */
/* Store result in cache and return. */
#ifdef USE_CASH_DUMMY
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_bddLeq_dummy
,
f
,
g
,(
res
?
one
:
zero
));
#else
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_bddLeq
,
f
,
g
,(
res
?
one
:
zero
));
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_bddLeq
,
f
,
g
,(
res
?
one
:
zero
));
#endif
return
(
res
);
return
(
res
);
}
/* end of Cudd_bddLeq */
}
/* end of Cudd_bddLeq */
...
...
src/bdd/cudd/cuddClip.c
View file @
f26ea1ea
...
@@ -250,6 +250,34 @@ cuddBddClippingAndAbstract(
...
@@ -250,6 +250,34 @@ cuddBddClippingAndAbstract(
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
Cudd_bddClippingAnd_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
g
)
{
assert
(
0
);
return
0
;
}
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
cuddBddClippingAnd_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
g
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
...
@@ -309,8 +337,12 @@ cuddBddClippingAndRecur(
...
@@ -309,8 +337,12 @@ cuddBddClippingAndRecur(
}
}
F
=
Cudd_Regular
(
f
);
F
=
Cudd_Regular
(
f
);
G
=
Cudd_Regular
(
g
);
G
=
Cudd_Regular
(
g
);
#ifdef USE_CASH_DUMMY
cacheOp
=
(
DD_CTFP
)
(
direction
?
Cudd_bddClippingAnd_dummy
:
cuddBddClippingAnd_dummy
);
#else
cacheOp
=
(
DD_CTFP
)
cacheOp
=
(
DD_CTFP
)
(
direction
?
Cudd_bddClippingAnd
:
cuddBddClippingAnd
);
(
direction
?
Cudd_bddClippingAnd
:
cuddBddClippingAnd
);
#endif
if
(
F
->
ref
!=
1
||
G
->
ref
!=
1
)
{
if
(
F
->
ref
!=
1
||
G
->
ref
!=
1
)
{
r
=
cuddCacheLookup2
(
manager
,
cacheOp
,
f
,
g
);
r
=
cuddCacheLookup2
(
manager
,
cacheOp
,
f
,
g
);
if
(
r
!=
NULL
)
return
(
r
);
if
(
r
!=
NULL
)
return
(
r
);
...
...
src/bdd/cudd/cuddMatMult.c
View file @
f26ea1ea
...
@@ -319,6 +319,23 @@ Cudd_addOuterSum(
...
@@ -319,6 +319,23 @@ Cudd_addOuterSum(
/* Definition of static functions */
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
addMMRecur_dummy
(
DdManager
*
dd
,
DdNode
*
A
,
DdNode
*
B
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addMatrixMultiply.]
Synopsis [Performs the recursive step of Cudd_addMatrixMultiply.]
...
@@ -393,7 +410,11 @@ addMMRecur(
...
@@ -393,7 +410,11 @@ addMMRecur(
topA
=
cuddI
(
dd
,
A
->
index
);
topB
=
cuddI
(
dd
,
B
->
index
);
topA
=
cuddI
(
dd
,
A
->
index
);
topB
=
cuddI
(
dd
,
B
->
index
);
topV
=
ddMin
(
topA
,
topB
);
topV
=
ddMin
(
topA
,
topB
);
#ifdef USE_CASH_DUMMY
cacheOp
=
(
DD_CTFP
)
addMMRecur_dummy
;
#else
cacheOp
=
(
DD_CTFP
)
addMMRecur
;
cacheOp
=
(
DD_CTFP
)
addMMRecur
;
#endif
res
=
cuddCacheLookup2
(
dd
,
cacheOp
,
A
,
B
);
res
=
cuddCacheLookup2
(
dd
,
cacheOp
,
A
,
B
);
if
(
res
!=
NULL
)
{
if
(
res
!=
NULL
)
{
/* If the result is 0, there is no need to normalize.
/* If the result is 0, there is no need to normalize.
...
...
src/bdd/cudd/cuddPriority.c
View file @
f26ea1ea
...
@@ -1571,6 +1571,22 @@ cuddCProjectionRecur(
...
@@ -1571,6 +1571,22 @@ cuddCProjectionRecur(
}
/* end of cuddCProjectionRecur */
}
/* end of cuddCProjectionRecur */
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
DdNode
*
Cudd_bddClosestCube_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
g
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddClosestCube.]
Synopsis [Performs the recursive step of Cudd_bddClosestCube.]
...
@@ -1667,7 +1683,11 @@ cuddBddClosestCube(
...
@@ -1667,7 +1683,11 @@ cuddBddClosestCube(
F
=
Cudd_Regular
(
f
);
F
=
Cudd_Regular
(
f
);
G
=
Cudd_Regular
(
g
);
G
=
Cudd_Regular
(
g
);
if
(
F
->
ref
!=
1
||
G
->
ref
!=
1
)
{
if
(
F
->
ref
!=
1
||
G
->
ref
!=
1
)
{
#ifdef USE_CASH_DUMMY
res
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_bddClosestCube_dummy
,
f
,
g
);
#else
res
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_bddClosestCube
,
f
,
g
);
res
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_bddClosestCube
,
f
,
g
);
#endif
if
(
res
!=
NULL
)
return
(
res
);
if
(
res
!=
NULL
)
return
(
res
);
}
}
...
@@ -1817,7 +1837,11 @@ cuddBddClosestCube(
...
@@ -1817,7 +1837,11 @@ cuddBddClosestCube(
/* Only cache results that are different from azero to avoid
/* Only cache results that are different from azero to avoid
** storing results that depend on the value of the bound. */
** storing results that depend on the value of the bound. */
if
((
F
->
ref
!=
1
||
G
->
ref
!=
1
)
&&
res
!=
azero
)
if
((
F
->
ref
!=
1
||
G
->
ref
!=
1
)
&&
res
!=
azero
)
#ifdef USE_CASH_DUMMY
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_bddClosestCube_dummy
,
f
,
g
,
res
);
#else
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_bddClosestCube
,
f
,
g
,
res
);
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_bddClosestCube
,
f
,
g
,
res
);
#endif
cuddDeref
(
res
);
cuddDeref
(
res
);
return
(
res
);
return
(
res
);
...
...
src/bdd/cudd/cuddSat.c
View file @
f26ea1ea
...
@@ -390,6 +390,22 @@ Cudd_ShortestLength(
...
@@ -390,6 +390,22 @@ Cudd_ShortestLength(
}
/* end of Cudd_ShortestLength */
}
/* end of Cudd_ShortestLength */
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
Cudd_Decreasing_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
g
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Determines whether a BDD is negative unate in a
Synopsis [Determines whether a BDD is negative unate in a
...
@@ -434,7 +450,11 @@ Cudd_Decreasing(
...
@@ -434,7 +450,11 @@ Cudd_Decreasing(
/* From now on, f is not constant. */
/* From now on, f is not constant. */
/* Check cache. */
/* Check cache. */
#ifdef USE_CASH_DUMMY
cacheOp
=
(
DD_CTFP
)
Cudd_Decreasing_dummy
;
#else
cacheOp
=
(
DD_CTFP
)
Cudd_Decreasing
;
cacheOp
=
(
DD_CTFP
)
Cudd_Decreasing
;
#endif
res
=
cuddCacheLookup2
(
dd
,
cacheOp
,
f
,
dd
->
vars
[
i
]);
res
=
cuddCacheLookup2
(
dd
,
cacheOp
,
f
,
dd
->
vars
[
i
]);
if
(
res
!=
NULL
)
{
if
(
res
!=
NULL
)
{
return
(
res
);
return
(
res
);
...
@@ -768,6 +788,22 @@ Cudd_bddLeqUnless(
...
@@ -768,6 +788,22 @@ Cudd_bddLeqUnless(
}
/* end of Cudd_bddLeqUnless */
}
/* end of Cudd_bddLeqUnless */
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
Cudd_EqualSupNorm_dummy
(
DdManager
*
dd
,
DdNode
*
f
,
DdNode
*
g
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Compares two ADDs for equality within tolerance.]
Synopsis [Compares two ADDs for equality within tolerance.]
...
@@ -817,7 +853,11 @@ Cudd_EqualSupNorm(
...
@@ -817,7 +853,11 @@ Cudd_EqualSupNorm(
/* We only insert the result in the cache if the comparison is
/* We only insert the result in the cache if the comparison is
** successful. Therefore, if we hit we return 1. */
** successful. Therefore, if we hit we return 1. */
#ifdef USE_CASH_DUMMY
r
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_EqualSupNorm_dummy
,
f
,
g
);
#else
r
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_EqualSupNorm
,
f
,
g
);
r
=
cuddCacheLookup2
(
dd
,(
DD_CTFP
)
Cudd_EqualSupNorm
,
f
,
g
);
#endif
if
(
r
!=
NULL
)
{
if
(
r
!=
NULL
)
{
return
(
1
);
return
(
1
);
}
}
...
@@ -832,7 +872,11 @@ Cudd_EqualSupNorm(
...
@@ -832,7 +872,11 @@ Cudd_EqualSupNorm(
if
(
!
Cudd_EqualSupNorm
(
dd
,
fv
,
gv
,
tolerance
,
pr
))
return
(
0
);
if
(
!
Cudd_EqualSupNorm
(
dd
,
fv
,
gv
,
tolerance
,
pr
))
return
(
0
);
if
(
!
Cudd_EqualSupNorm
(
dd
,
fvn
,
gvn
,
tolerance
,
pr
))
return
(
0
);
if
(
!
Cudd_EqualSupNorm
(
dd
,
fvn
,
gvn
,
tolerance
,
pr
))
return
(
0
);
#ifdef USE_CASH_DUMMY
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_EqualSupNorm_dummy
,
f
,
g
,
DD_ONE
(
dd
));
#else
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_EqualSupNorm
,
f
,
g
,
DD_ONE
(
dd
));
cuddCacheInsert2
(
dd
,(
DD_CTFP
)
Cudd_EqualSupNorm
,
f
,
g
,
DD_ONE
(
dd
));
#endif
return
(
1
);
return
(
1
);
...
...
src/bdd/cudd/cuddZddIsop.c
View file @
f26ea1ea
...
@@ -219,6 +219,22 @@ Cudd_MakeBddFromZddCover(
...
@@ -219,6 +219,22 @@ Cudd_MakeBddFromZddCover(
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
#ifdef USE_CASH_DUMMY
/**Function********************************************************************
Synopsis We need to declare a function passed to cuddCacheLookup2 that can
be casted to DD_CTFP.
******************************************************************************/
static
DdNode
*
cuddZddIsop_dummy
(
DdManager
*
dd
,
DdNode
*
L
,
DdNode
*
U
)
{
assert
(
0
);
return
0
;
}
#endif
/**Function********************************************************************
/**Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIsop.]
Synopsis [Performs the recursive step of Cudd_zddIsop.]
...
@@ -273,7 +289,11 @@ cuddZddIsop(
...
@@ -273,7 +289,11 @@ cuddZddIsop(
** Hence we need a double hit in the cache to terminate the
** Hence we need a double hit in the cache to terminate the
** recursion. Clearly, collisions may evict only one of the two
** recursion. Clearly, collisions may evict only one of the two
** results. */
** results. */
#ifdef USE_CASH_DUMMY
cacheOp
=
(
DD_CTFP
)
cuddZddIsop_dummy
;
#else
cacheOp
=
(
DD_CTFP
)
cuddZddIsop
;
cacheOp
=
(
DD_CTFP
)
cuddZddIsop
;
#endif
r
=
cuddCacheLookup2
(
dd
,
cuddBddIsop
,
L
,
U
);
r
=
cuddCacheLookup2
(
dd
,
cuddBddIsop
,
L
,
U
);
if
(
r
)
{
if
(
r
)
{
*
zdd_I
=
cuddCacheLookup2Zdd
(
dd
,
cacheOp
,
L
,
U
);
*
zdd_I
=
cuddCacheLookup2Zdd
(
dd
,
cacheOp
,
L
,
U
);
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment