From 93010f37310ddb688e38dfbb7e736b86679daa36 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 22 Aug 2016 21:25:15 +0200 Subject: [PATCH] ported fix for CUDD existsAbstractRepresentative from Philip's branch to game-branch Former-commit-id: 5841f78c33cbdb3afcfc469423b6f64a46c90285 --- .../3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c | 23 +++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index 9643cbfaa..ef0c3f6f8 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -535,19 +535,34 @@ cuddBddExistAbstractRepresentativeRecur( /* Cube is guaranteed to be a cube at this point. */ if (F == one) { if (fIsNegated) { -// printf("return in preprocessing...\n"); + // printf("return in preprocessing...\n"); return f; } if (cube == one) { -// printf("return in preprocessing...\n"); + // printf("return in preprocessing...\n"); return one; + } else { + res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube)); + if (res == NULL) { + return(NULL); + } + cuddRef(res); + + res1 = cuddBddIteRecur(manager, manager->vars[cube->index], zero, res); + if (res1 == NULL) { + Cudd_IterDerefBdd(manager,res); + Cudd_IterDerefBdd(manager,zero); + return(NULL); + } + cuddDeref(res); + return(res1); } } else if (cube == one) { -// printf("return in preprocessing...\n"); + // printf("return in preprocessing...\n"); return f; } - /* From now on, cube is non-constant, but f might be constant. */ + /* From now on, cube and f are non-constant. */ // printf("F perm %i and cube perm %i\n", manager->perm[F->index], manager->perm[cube->index]);