fraigApi.c File Reference

#include "fraigInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Fraig_NodeVec_t *	Fraig_ManReadVecInputs (Fraig_Man_t *p)
	DECLARATIONS ///. More...
Fraig_NodeVec_t *	Fraig_ManReadVecOutputs (Fraig_Man_t *p)
Fraig_NodeVec_t *	Fraig_ManReadVecNodes (Fraig_Man_t *p)
Fraig_Node_t **	Fraig_ManReadInputs (Fraig_Man_t *p)
Fraig_Node_t **	Fraig_ManReadOutputs (Fraig_Man_t *p)
Fraig_Node_t **	Fraig_ManReadNodes (Fraig_Man_t *p)
int	Fraig_ManReadInputNum (Fraig_Man_t *p)
int	Fraig_ManReadOutputNum (Fraig_Man_t *p)
int	Fraig_ManReadNodeNum (Fraig_Man_t *p)
Fraig_Node_t *	Fraig_ManReadConst1 (Fraig_Man_t *p)
Fraig_Node_t *	Fraig_ManReadIthNode (Fraig_Man_t *p, int i)
char **	Fraig_ManReadInputNames (Fraig_Man_t *p)
char **	Fraig_ManReadOutputNames (Fraig_Man_t *p)
char *	Fraig_ManReadVarsInt (Fraig_Man_t *p)
char *	Fraig_ManReadSat (Fraig_Man_t *p)
int	Fraig_ManReadFuncRed (Fraig_Man_t *p)
int	Fraig_ManReadFeedBack (Fraig_Man_t *p)
int	Fraig_ManReadDoSparse (Fraig_Man_t *p)
int	Fraig_ManReadChoicing (Fraig_Man_t *p)
int	Fraig_ManReadVerbose (Fraig_Man_t *p)
int *	Fraig_ManReadModel (Fraig_Man_t *p)
int	Fraig_ManReadPatternNumRandom (Fraig_Man_t *p)
int	Fraig_ManReadPatternNumDynamic (Fraig_Man_t *p)
int	Fraig_ManReadPatternNumDynamicFiltered (Fraig_Man_t *p)
int	Fraig_ManReadSatFails (Fraig_Man_t *p)
int	Fraig_ManReadConflicts (Fraig_Man_t *p)
int	Fraig_ManReadInspects (Fraig_Man_t *p)
void	Fraig_ManSetFuncRed (Fraig_Man_t *p, int fFuncRed)
void	Fraig_ManSetFeedBack (Fraig_Man_t *p, int fFeedBack)
void	Fraig_ManSetDoSparse (Fraig_Man_t *p, int fDoSparse)
void	Fraig_ManSetChoicing (Fraig_Man_t *p, int fChoicing)
void	Fraig_ManSetTryProve (Fraig_Man_t *p, int fTryProve)
void	Fraig_ManSetVerbose (Fraig_Man_t *p, int fVerbose)
void	Fraig_ManSetOutputNames (Fraig_Man_t *p, char **ppNames)
void	Fraig_ManSetInputNames (Fraig_Man_t *p, char **ppNames)
Fraig_Node_t *	Fraig_NodeReadData0 (Fraig_Node_t *p)
Fraig_Node_t *	Fraig_NodeReadData1 (Fraig_Node_t *p)
int	Fraig_NodeReadNum (Fraig_Node_t *p)
Fraig_Node_t *	Fraig_NodeReadOne (Fraig_Node_t *p)
Fraig_Node_t *	Fraig_NodeReadTwo (Fraig_Node_t *p)
Fraig_Node_t *	Fraig_NodeReadNextE (Fraig_Node_t *p)
Fraig_Node_t *	Fraig_NodeReadRepr (Fraig_Node_t *p)
int	Fraig_NodeReadNumRefs (Fraig_Node_t *p)
int	Fraig_NodeReadNumFanouts (Fraig_Node_t *p)
int	Fraig_NodeReadSimInv (Fraig_Node_t *p)
int	Fraig_NodeReadNumOnes (Fraig_Node_t *p)
unsigned *	Fraig_NodeReadPatternsRandom (Fraig_Node_t *p)
unsigned *	Fraig_NodeReadPatternsDynamic (Fraig_Node_t *p)
void	Fraig_NodeSetData0 (Fraig_Node_t *p, Fraig_Node_t *pData)
void	Fraig_NodeSetData1 (Fraig_Node_t *p, Fraig_Node_t *pData)
int	Fraig_NodeIsConst (Fraig_Node_t *p)
int	Fraig_NodeIsVar (Fraig_Node_t *p)
int	Fraig_NodeIsAnd (Fraig_Node_t *p)
int	Fraig_NodeComparePhase (Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t *	Fraig_ManReadIthVar (Fraig_Man_t *p, int i)
void	Fraig_ManSetPo (Fraig_Man_t *p, Fraig_Node_t *pNode)
Fraig_Node_t *	Fraig_NodeAnd (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t *	Fraig_NodeOr (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t *	Fraig_NodeExor (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t *	Fraig_NodeMux (Fraig_Man_t *p, Fraig_Node_t *pC, Fraig_Node_t *pT, Fraig_Node_t *pE)
void	Fraig_NodeSetChoice (Fraig_Man_t *pMan, Fraig_Node_t *pNodeOld, Fraig_Node_t *pNodeNew)

Function Documentation

int Fraig_ManReadChoicing

(

Fraig_Man_t *

p

)

Definition at line 61 of file fraigApi.c.

{ return p->fChoicing;  }

int Fraig_ManReadConflicts

(

Fraig_Man_t *

p

)

Definition at line 73 of file fraigApi.c.

{ return p->pSat? Msat_SolverReadBackTracks(p->pSat) : 0; }      

Fraig_Node_t* Fraig_ManReadConst1

(

Fraig_Man_t *

p

)

Definition at line 52 of file fraigApi.c.

{ return p->pConst1;            }

int Fraig_ManReadDoSparse

(

Fraig_Man_t *

p

)

Definition at line 60 of file fraigApi.c.

{ return p->fDoSparse;  }

int Fraig_ManReadFeedBack

(

Fraig_Man_t *

p

)

Definition at line 59 of file fraigApi.c.

{ return p->fFeedBack;  }

int Fraig_ManReadFuncRed

(

Fraig_Man_t *

p

)

Definition at line 58 of file fraigApi.c.

{ return p->fFuncRed;   }

char** Fraig_ManReadInputNames

(

Fraig_Man_t *

p

)

Definition at line 54 of file fraigApi.c.

{ return p->ppInputNames;       }

int Fraig_ManReadInputNum

(

Fraig_Man_t *

p

)

Definition at line 49 of file fraigApi.c.

{ return p->vInputs->nSize;     }

Fraig_Node_t** Fraig_ManReadInputs

(

Fraig_Man_t *

p

)

Definition at line 46 of file fraigApi.c.

{ return p->vInputs->pArray;    }

int Fraig_ManReadInspects

(

Fraig_Man_t *

p

)

Definition at line 75 of file fraigApi.c.

{ return p->pSat? Msat_SolverReadInspects(p->pSat) : 0;   }            

Fraig_Node_t* Fraig_ManReadIthNode	(	Fraig_Man_t *	p,
		int	i
	)

Definition at line 53 of file fraigApi.c.

{ assert ( i < p->vNodes->nSize  ); return p->vNodes->pArray[i];  }

Fraig_Node_t* Fraig_ManReadIthVar	(	Fraig_Man_t *	p,
		int	i
	)

Function*************************************************************

Synopsis [Returns a new primary input node.]

Description [If the node with this number does not exist, create a new PI node with this number.]

SideEffects []

SeeAlso []

Definition at line 168 of file fraigApi.c.

{
    int k;
    if ( i < 0 )
    {
        printf( "Requesting a PI with a negative number\n" );
        return NULL;
    }
    // create the PIs to fill in the interval
    if ( i >= p->vInputs->nSize )
        for ( k = p->vInputs->nSize; k <= i; k++ )
            Fraig_NodeCreatePi( p ); 
    return p->vInputs->pArray[i];
}

int* Fraig_ManReadModel

(

Fraig_Man_t *

p

)

Definition at line 63 of file fraigApi.c.

{ return p->pModel;     }

int Fraig_ManReadNodeNum

(

Fraig_Man_t *

p

)

Definition at line 51 of file fraigApi.c.

{ return p->vNodes->nSize;      }

Fraig_Node_t** Fraig_ManReadNodes

(

Fraig_Man_t *

p

)

Definition at line 48 of file fraigApi.c.

{ return p->vNodes->pArray;     }

char** Fraig_ManReadOutputNames

(

Fraig_Man_t *

p

)

Definition at line 55 of file fraigApi.c.

{ return p->ppOutputNames;      }

int Fraig_ManReadOutputNum

(

Fraig_Man_t *

p

)

Definition at line 50 of file fraigApi.c.

{ return p->vOutputs->nSize;    }

Fraig_Node_t** Fraig_ManReadOutputs

(

Fraig_Man_t *

p

)

Definition at line 47 of file fraigApi.c.

{ return p->vOutputs->pArray;   }

int Fraig_ManReadPatternNumDynamic

(

Fraig_Man_t *

p

)

Definition at line 67 of file fraigApi.c.

{ return p->iWordStart * 32;  }

int Fraig_ManReadPatternNumDynamicFiltered

(

Fraig_Man_t *

p

)

Definition at line 69 of file fraigApi.c.

{ return p->iPatsPerm;        }

int Fraig_ManReadPatternNumRandom

(

Fraig_Man_t *

p

)

Definition at line 65 of file fraigApi.c.

{ return p->nWordsRand * 32;  }

char* Fraig_ManReadSat

(

Fraig_Man_t *

p

)

Definition at line 57 of file fraigApi.c.

{ return (char *)p->pSat;       }

int Fraig_ManReadSatFails

(

Fraig_Man_t *

p

)

Definition at line 71 of file fraigApi.c.

{ return p->nSatFailsReal;    }      

char* Fraig_ManReadVarsInt

(

Fraig_Man_t *

p

)

Definition at line 56 of file fraigApi.c.

{ return (char *)p->vVarsInt;   }

ABC_NAMESPACE_IMPL_START Fraig_NodeVec_t* Fraig_ManReadVecInputs

(

Fraig_Man_t *

p

)

DECLARATIONS ///.

FUNCTION DEFINITIONS ///.

CFile****************************************************************

FileName [fraigApi.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Access APIs for the FRAIG manager and node.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id:

fraigApi.c,v 1.2 2005/07/08 01:01:30 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Access functions to read the data members of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fraigApi.c.

{ return p->vInputs;            }

Fraig_NodeVec_t* Fraig_ManReadVecNodes

(

Fraig_Man_t *

p

)

Definition at line 45 of file fraigApi.c.

{ return p->vNodes;             }

Fraig_NodeVec_t* Fraig_ManReadVecOutputs

(

Fraig_Man_t *

p

)

Definition at line 44 of file fraigApi.c.

{ return p->vOutputs;           }

int Fraig_ManReadVerbose

(

Fraig_Man_t *

p

)

Definition at line 62 of file fraigApi.c.

{ return p->fVerbose;   }

void Fraig_ManSetChoicing	(	Fraig_Man_t *	p,
		int	fChoicing
	)

Definition at line 91 of file fraigApi.c.

{ p->fChoicing = fChoicing; }

void Fraig_ManSetDoSparse	(	Fraig_Man_t *	p,
		int	fDoSparse
	)

Definition at line 90 of file fraigApi.c.

{ p->fDoSparse = fDoSparse; }

void Fraig_ManSetFeedBack	(	Fraig_Man_t *	p,
		int	fFeedBack
	)

Definition at line 89 of file fraigApi.c.

{ p->fFeedBack = fFeedBack; }

void Fraig_ManSetFuncRed	(	Fraig_Man_t *	p,
		int	fFuncRed
	)

Function*************************************************************

Synopsis [Access functions to set the data members of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file fraigApi.c.

{ p->fFuncRed  = fFuncRed;  }

void Fraig_ManSetInputNames	(	Fraig_Man_t *	p,
		char **	ppNames
	)

Definition at line 95 of file fraigApi.c.

{ p->ppInputNames  = ppNames; }

void Fraig_ManSetOutputNames	(	Fraig_Man_t *	p,
		char **	ppNames
	)

Definition at line 94 of file fraigApi.c.

{ p->ppOutputNames = ppNames; }

void Fraig_ManSetPo	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pNode
	)

Function*************************************************************

Synopsis [Creates a new PO node.]

Description [This procedure may take a complemented node.]

SideEffects []

SeeAlso []

Definition at line 194 of file fraigApi.c.

{
    // internal node may be a PO two times
    Fraig_Regular(pNode)->fNodePo = 1;
    Fraig_NodeVecPush( p->vOutputs, pNode );
}

void Fraig_ManSetTryProve	(	Fraig_Man_t *	p,
		int	fTryProve
	)

Definition at line 92 of file fraigApi.c.

{ p->fTryProve = fTryProve; }

void Fraig_ManSetVerbose	(	Fraig_Man_t *	p,
		int	fVerbose
	)

Definition at line 93 of file fraigApi.c.

{ p->fVerbose  = fVerbose;  }

Fraig_Node_t* Fraig_NodeAnd	(	Fraig_Man_t *	p,
		Fraig_Node_t *	p1,
		Fraig_Node_t *	p2
	)

Function*************************************************************

Synopsis [Perfoms the AND operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 212 of file fraigApi.c.

{
    return Fraig_NodeAndCanon( p, p1, p2 );
}

int Fraig_NodeComparePhase	(	Fraig_Node_t *	p1,
		Fraig_Node_t *	p2
	)

Definition at line 154 of file fraigApi.c.

{ assert( !Fraig_IsComplement(p1) ); assert( !Fraig_IsComplement(p2) ); return p1->fInv ^ p2->fInv; }

Fraig_Node_t* Fraig_NodeExor	(	Fraig_Man_t *	p,
		Fraig_Node_t *	p1,
		Fraig_Node_t *	p2
	)

Function*************************************************************

Synopsis [Perfoms the EXOR operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file fraigApi.c.

{
    return Fraig_NodeMux( p, p1, Fraig_Not(p2), p2 );
}

int Fraig_NodeIsAnd

(

Fraig_Node_t *

p

)

Definition at line 153 of file fraigApi.c.

{  return (Fraig_Regular(p))->NumPi <  0 && (Fraig_Regular(p))->Num > 0;  }

int Fraig_NodeIsConst

(

Fraig_Node_t *

p

)

Function*************************************************************

Synopsis [Checks the type of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file fraigApi.c.

{  return (Fraig_Regular(p))->Num   == 0;  }

int Fraig_NodeIsVar

(

Fraig_Node_t *

p

)

Definition at line 152 of file fraigApi.c.

{  return (Fraig_Regular(p))->NumPi >= 0;  }

Fraig_Node_t* Fraig_NodeMux	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pC,
		Fraig_Node_t *	pT,
		Fraig_Node_t *	pE
	)

Function*************************************************************

Synopsis [Perfoms the MUX operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 260 of file fraigApi.c.

{
    Fraig_Node_t * pAnd1, * pAnd2, * pRes;
    pAnd1 = Fraig_NodeAndCanon( p, pC,          pT );     Fraig_Ref( pAnd1 );
    pAnd2 = Fraig_NodeAndCanon( p, Fraig_Not(pC), pE );   Fraig_Ref( pAnd2 );
    pRes  = Fraig_NodeOr( p, pAnd1, pAnd2 ); 
    Fraig_RecursiveDeref( p, pAnd1 );
    Fraig_RecursiveDeref( p, pAnd2 );
    Fraig_Deref( pRes );
    return pRes;
}

Fraig_Node_t* Fraig_NodeOr	(	Fraig_Man_t *	p,
		Fraig_Node_t *	p1,
		Fraig_Node_t *	p2
	)

Function*************************************************************

Synopsis [Perfoms the OR operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 228 of file fraigApi.c.

{
    return Fraig_Not( Fraig_NodeAndCanon( p, Fraig_Not(p1), Fraig_Not(p2) ) );
}

Fraig_Node_t* Fraig_NodeReadData0

(

Fraig_Node_t *

p

)

Function*************************************************************

Synopsis [Access functions to read the data members of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file fraigApi.c.

{ return p->pData0;    }

Fraig_Node_t* Fraig_NodeReadData1

(

Fraig_Node_t *

p

)

Definition at line 109 of file fraigApi.c.

{ return p->pData1;    }

Fraig_Node_t* Fraig_NodeReadNextE

(

Fraig_Node_t *

p

)

Definition at line 113 of file fraigApi.c.

{ return p->pNextE;    }

int Fraig_NodeReadNum

(

Fraig_Node_t *

p

)

Definition at line 110 of file fraigApi.c.

{ return p->Num;       }

int Fraig_NodeReadNumFanouts

(

Fraig_Node_t *

p

)

Definition at line 116 of file fraigApi.c.

{ return p->nFanouts;  }

int Fraig_NodeReadNumOnes

(

Fraig_Node_t *

p

)

Definition at line 118 of file fraigApi.c.

{ return p->nOnes;     }

int Fraig_NodeReadNumRefs

(

Fraig_Node_t *

p

)

Definition at line 115 of file fraigApi.c.

{ return p->nRefs;     }

Fraig_Node_t* Fraig_NodeReadOne

(

Fraig_Node_t *

p

)

Definition at line 111 of file fraigApi.c.

{ assert (!Fraig_IsComplement(p)); return p->p1; }

unsigned* Fraig_NodeReadPatternsDynamic

(

Fraig_Node_t *

p

)

Definition at line 124 of file fraigApi.c.

{ return p->puSimD;    }

unsigned* Fraig_NodeReadPatternsRandom

(

Fraig_Node_t *

p

)

Definition at line 121 of file fraigApi.c.

{ return p->puSimR;    }

Fraig_Node_t* Fraig_NodeReadRepr

(

Fraig_Node_t *

p

)

Definition at line 114 of file fraigApi.c.

{ return p->pRepr;     }

int Fraig_NodeReadSimInv

(

Fraig_Node_t *

p

)

Definition at line 117 of file fraigApi.c.

{ return p->fInv;      }

Fraig_Node_t* Fraig_NodeReadTwo

(

Fraig_Node_t *

p

)

Definition at line 112 of file fraigApi.c.

{ assert (!Fraig_IsComplement(p)); return p->p2; }

void Fraig_NodeSetChoice	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNodeOld,
		Fraig_Node_t *	pNodeNew
	)

Function*************************************************************

Synopsis [Sets the node to be equivalent to the given one.]

Description [This procedure is a work-around for the equivalence check. Does not verify the equivalence. Use at the user's risk.]

SideEffects []

SeeAlso []

Definition at line 285 of file fraigApi.c.

{
//    assert( pMan->fChoicing );
    pNodeNew->pNextE = pNodeOld->pNextE;
    pNodeOld->pNextE = pNodeNew;
    pNodeNew->pRepr  = pNodeOld;
}

void Fraig_NodeSetData0	(	Fraig_Node_t *	p,
		Fraig_Node_t *	pData
	)

Function*************************************************************

Synopsis [Access functions to set the data members of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file fraigApi.c.

{ p->pData0  = pData;  }

void Fraig_NodeSetData1	(	Fraig_Node_t *	p,
		Fraig_Node_t *	pData
	)

Definition at line 138 of file fraigApi.c.

{ p->pData1  = pData;  }