From: Fabio Somenzi (Fabio_at_colorado.edu)
Date: Sun Dec 10 2006 - 19:10:54 MST
Yes, you need to use Cudd_Regular as explained in the section of the
Programmer manual on complement pointers. (Of course, this returns the same
result for f and its negation.)
Complement pointers were fist described in:
@conference{Madre88,
author = "J. C. Madre and J. P. Billon ",
title = "Proving Circuit Correctness using Formal Comparison Between Expected and Extracted Behavior",
booktitle = dac88,
pages = "205-210",
year = 1988,
month = jun
}
Fabio
>>>>> "PM" == Pongstorn Maidee <maid0013_at_umn.edu> writes:
PM> Fabio Somenzi wrote:
>>>>>>> "PM" == Pongstorn Maidee <maid0013_at_umn.edu> writes:
>>>>>>>
>>>>>>>
>>
PM> Hi all,
PM> I tried a small example usign CUDD.
>>
PM> 1: f = Cudd_ReadOne(ddman);
PM> 2: var = Cudd_bddIthVar(ddman,3);
PM> 3: temp = Cudd_bddAnd(ddman,Cudd_not(var),f);
PM> 4: Cudd_Ref(temp);
>>
PM> I have 2 questions regarding this simple example.
PM> 1) Logically, "var AND one" is var. But, temp contains address which is
PM> not the same as var.
PM> Does this mean simple variables (projection
PM> functions) are handeled differently from internal nodes in CUDD?
>>
>> No, it means that if you dereference a complement pointer you read
>> bogus information. (Note that you are negating the variable.) Are
>> you familiar with the difference between a regular pointer and a
>> complement pointer?
>>
>>
>> Fabio
>>
>>
PM> I have no knowledge about CUDD data structure detail. I read through the
PM> document coming with CUDD. But, I cannot find those details. Could you
PM> please point me to where I can get the information. From what you
PM> mentioned, I think I have to get the regular pointer (using
PM> Cudd_Regular) to get the real node information from it.
PM> Thanks,
PM> Pongstorn
This archive was generated by hypermail 2.1.7 : Sun Dec 10 2006 - 19:17:21 MST