CUDD (C 인터페이스)의 BDD에서 작동하지 않아 컴퓨터 이미지를 만들 때 일부 변수를 제거 할 수 있는지 잘 모르겠습니다. 국가에서 BDD의 다른 상태로) 어떻게 모든 변수를 얻기 위해 결과 BDD (최종 BDD)를 여행하는지, 누구든지 우리가 CUDD로 그렇게 할 수 있는지 말해 줄 수 있습니까? 건배CUDD (C 인터페이스)로 계산 이미지를 수행 한 후 BDD의 모든 변수 가져 오기
나는 CUDD를 사용한 적이 없지만 BDD에서 사용되는 변수 목록은 보통 이라고합니다. BDD에서 변수를 제거하는 작업은 일반적으로 존재 정량화을 통해 수행됩니다.
소스 코드를 Grepping, 내가
/**Function********************************************************************
Synopsis [Finds the variables on which a DD depends.]
Description [Finds the variables on which a DD depends.
Returns a BDD consisting of the product of the variables if
successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_VectorSupport Cudd_ClassifySupport]
******************************************************************************/
DdNode *
Cudd_Support(
DdManager * dd /* manager */,
DdNode * f /* DD whose support is sought */)
및
/**Function********************************************************************
Synopsis [Existentially abstracts all the variables in cube from f.]
Description [Existentially abstracts all the variables in cube from f.
Returns the abstracted BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddUnivAbstract Cudd_addExistAbstract]
******************************************************************************/
DdNode *
Cudd_bddExistAbstract(
DdManager * manager,
DdNode * f,
DdNode * cube)
사랑스러운를 발견했습니다, 감사합니다, 나는 그것을 시도 할 것이다, 게다가, 당신은 정확히 단어 "추상적 인 말씀 해주십시오 수 "여기에 의미가 있니? 나는 정말로 그것을 얻지 않는다, 환호. –
'a & b'는'c '에 신경 쓰지 않는'a & b & c'의 _abstraction_입니다. 반대로 'a & b & c'는 'a & b'의 _refinement_입니다. – adl
BDD에서 변수를 집계하기 위해 존재하는 계량화를 사용할 수 없습니다. 예를 들어, 두 변수 사이에서 간단한 XOR을 취하십시오. 상위 변수를 사용하여 실존 적 수량화를하면 두 변수를 모두 잃게됩니다. 즉, 필요한 존재 수량의 수는 변수의 수와 같지 않습니다. 사실, CUDD는 정확한 결과를보고하지만 실존 적 수량화를 사용하지는 않습니다. – meolic