Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit b0ce5e43 authored by Valentin Touzeau's avatar Valentin Touzeau Committed by EXT Valentin Touzeau
Browse files

Adds ZddMinDotProduct operator

parent 8aca80cb
......@@ -5,6 +5,9 @@
extern "C"
{
#include <extra.h>
DdNode *zddMinDotProduct(DdManager* dd, DdNode* S, DdNode* T);
DdNode* ZddMinDotProduct(DdManager* dd, DdNode* S, DdNode* T);
}
namespace exactlru
......@@ -127,10 +130,11 @@ ZDD ZDD::minDotProduct(const ZDD& other) const
// TODO: Reduce at each step (code Extra_zddMinDotProduct)
// TODO: Check failure
DdNode* u = Extra_zddDotProduct(_manager->getManager(), _zdd, other._zdd);
Cudd_Ref(u);
DdNode* res = Extra_zddMinimal(_manager->getManager(), u);
Cudd_Deref(u);
DdNode* res = zddMinDotProduct(_manager->getManager(), _zdd, other._zdd);
// DdNode* u = Extra_zddDotProduct(_manager->getManager(), _zdd, other._zdd);
// Cudd_Ref(u);
// DdNode* res = Extra_zddMinimal(_manager->getManager(), u);
// Cudd_Deref(u);
return ZDD(_manager, res);
}
......@@ -186,5 +190,151 @@ void ZDD::printDotToFile(char* filename, char* function) const
ASSERT((_zdd == nullptr) == (_manager == nullptr));
}
} // namespace exactlru
extern "C"
{
DdNode *zddMinDotProduct(
DdManager * dd,
DdNode * S,
DdNode * T)
{
DdNode *res;
do {
dd->reordered = 0;
res = ZddMinDotProduct(dd, S, T);
} while (dd->reordered == 1);
return(res);
} /* end of zddMinDotProduct */
DdNode *
ZddMinDotProduct(
DdManager * dd,
DdNode * S,
DdNode * T)
{
DdNode *zRes;
int TopS, TopT;
statLine(dd);
/* consider terminal cases */
if ( S == z0 || T == z0 )
return z0;
if ( S == z1 )
return T;
if ( T == z1 )
return S;
/* the operation is commutative - normalize the problem */
TopS = dd->permZ[S->index];
TopT = dd->permZ[T->index];
if ( TopS > TopT || (TopS == TopT && (unsigned long)S > (unsigned long)T) )
return ZddMinDotProduct(dd, T, S);
/* check cache */
zRes = cuddCacheLookup2Zdd(dd, ZddMinDotProduct, S, T);
if (zRes)
return zRes;
else
{
DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
if ( TopS == TopT )
{
/* compute the union of two cofactors of T (T0+T1) */
zTemp = extraZddMinUnion(dd, cuddE(T), cuddT(T) );
if ( zTemp == NULL )
return NULL;
cuddRef( zTemp );
/* compute MinDotProduct with the top element for subsets (S1, T0+T1) */
zSet0 = ZddMinDotProduct(dd, cuddT(S), zTemp );
if ( zSet0 == NULL )
{
Cudd_RecursiveDerefZdd(dd, zTemp);
return NULL;
}
cuddRef( zSet0 );
Cudd_RecursiveDerefZdd(dd, zTemp);
/* compute MinDotProduct with the top element for subsets (S0, T1) */
zSet1 = ZddMinDotProduct(dd, cuddE(S), cuddT(T) );
if ( zSet1 == NULL )
{
Cudd_RecursiveDerefZdd(dd, zSet0);
return NULL;
}
cuddRef( zSet1 );
/* compute the union of these two partial results (zSet0 + zSet1) */
zRes1 = extraZddMinUnion(dd, zSet0, zSet1 );
if ( zRes1 == NULL )
{
Cudd_RecursiveDerefZdd(dd, zSet0);
Cudd_RecursiveDerefZdd(dd, zSet1);
return NULL;
}
cuddRef( zRes1 );
Cudd_RecursiveDerefZdd(dd, zSet0);
Cudd_RecursiveDerefZdd(dd, zSet1);
/* compute MinDotProduct for subsets without the top-most element */
zRes0 = ZddMinDotProduct(dd, cuddE(S), cuddE(T) );
if ( zRes0 == NULL )
{
Cudd_RecursiveDerefZdd(dd, zRes1);
return NULL;
}
cuddRef( zRes0 );
}
else /* if ( TopS < TopT ) */
{
/* compute MinDotProduct with the top element for subsets (S1, T) */
zRes1 = ZddMinDotProduct(dd, cuddT(S), T );
if ( zRes1 == NULL )
return NULL;
cuddRef( zRes1 );
/* compute MinDotProduct for subsets without the top-most element */
zRes0 = ZddMinDotProduct(dd, cuddE(S), T );
if ( zRes0 == NULL )
{
Cudd_RecursiveDerefZdd(dd, zRes1);
return NULL;
}
cuddRef( zRes0 );
}
/* remove subsets with this element covering subsets without this element */
zRes1 = extraZddNotSubSet(dd, zTemp = zRes1, zRes0);
if ( zRes1 == NULL )
{
Cudd_RecursiveDerefZdd(dd, zTemp);
Cudd_RecursiveDerefZdd(dd, zRes0);
return NULL;
}
cuddRef( zRes1 );
Cudd_RecursiveDerefZdd(dd, zTemp);
/* create the new node */
zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
if ( zRes == NULL )
{
Cudd_RecursiveDerefZdd( dd, zRes0 );
Cudd_RecursiveDerefZdd( dd, zRes1 );
return NULL;
}
cuddDeref( zRes0 );
cuddDeref( zRes1 );
/* insert the result into cache */
cuddCacheInsert2(dd, ZddMinDotProduct, S, T, zRes);
return zRes;
}
} /* end of extraZddMinDotProduct */
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment