[Buddy-developers] [ buddy-Bugs-1040620 ] Bug in bdd_appuni and in bdd_unique

[SourceForge.net <no...@so...>]

Bugs item #1040620, was opened at 2004-10-05 14:52
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658

Category: None
Group: None
Status: Open
Resolution: None
Priority: 5
Submitted By: Christophe Mauras (mauras)
Assigned to: Nobody/Anonymous (nobody)
Summary: Bug in bdd_appuni and in bdd_unique

Initial Comment:
It seems to me there is a bug in bdd_appuni and same in
bdd_unique. These operations may not depend on variable
order :

   Exists unique x0 such that (x0 or x1)
= (x0 or x1)[x0\0] xor (x0 or x1)[x0\1]
= x1 xor true
= not x1

   Exists unique x1 such that x0 or x1
= (x0 or x1)[x1\0] xor (x0 or x1)[x1\1]
= x0 xor true
= not x0
Here is the bug : Buddy reply 1

More simply :
  Exists unique x0 such that true
= (true)[x0\0] xor (true)[x0\1]
= true xor true
= false
Buddy reply 1

Please look at following code :

----------------------------------
#include "bdd.h"
#include "stdio.h"

main(void)
{
  bdd x0,x1,y0,y1,z0,z1,t;
  bdd_init (100,10);
  bdd_setvarnum(5);
  x0 = bdd_ithvar(0);
  x1 = bdd_ithvar(1);

  y0 = bdd_appuni(x0,x1,bddop_or,x0);
  printf("Result should be  1: 1 0 \n");
  bdd_printtable(y0);
  printf("Good!\n\n");

  y1 = bdd_appuni(x0,x1,bddop_or,x1);
  printf("Result should be  0: 1 0 \n");
  bdd_printtable(y1);
  printf("Bad !\n");

  z0 = bdd_unique(bdd_or(x0,x1),x0);
  printf("Result should be  1: 1 0 \n");
  bdd_printtable(z0);
  printf("Good!\n\n");

  z1 = bdd_unique(bdd_or(x0,x1),x1);
  printf("Result should be  0: 1 0 \n");
  bdd_printtable(z1);
  printf("Bad !\n");

  t = bdd_unique(bdd_true(), x0);
  printf("Result should be  0 \n");
  bdd_printtable(z1);
  printf("Bad !\n");


  bdd_done();
}

   


----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658