src/sat/fraig/fraigApi.c File Reference

#include "fraigInt.h"
Include dependency graph for fraigApi.c:

Go to the source code of this file.

Functions

Fraig_NodeVec_t * Fraig_ManReadVecInputs (Fraig_Man_t *p)
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_ManSetTimeToGraph (Fraig_Man_t *p, int Time)
void Fraig_ManSetTimeToNet (Fraig_Man_t *p, int Time)
void Fraig_ManSetTimeTotal (Fraig_Man_t *p, int Time)
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 58 of file fraigApi.c.

00058 { return p->fChoicing;  }

int Fraig_ManReadConflicts ( Fraig_Man_t *  p  ) 

Definition at line 70 of file fraigApi.c.

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

Fraig_Node_t* Fraig_ManReadConst1 ( Fraig_Man_t *  p  ) 

Definition at line 49 of file fraigApi.c.

00049 { return p->pConst1;            }

int Fraig_ManReadDoSparse ( Fraig_Man_t *  p  ) 

Definition at line 57 of file fraigApi.c.

00057 { return p->fDoSparse;  }

int Fraig_ManReadFeedBack ( Fraig_Man_t *  p  ) 

Definition at line 56 of file fraigApi.c.

00056 { return p->fFeedBack;  }

int Fraig_ManReadFuncRed ( Fraig_Man_t *  p  ) 

Definition at line 55 of file fraigApi.c.

00055 { return p->fFuncRed;   }

char** Fraig_ManReadInputNames ( Fraig_Man_t *  p  ) 

Definition at line 51 of file fraigApi.c.

00051 { return p->ppInputNames;       }

int Fraig_ManReadInputNum ( Fraig_Man_t *  p  ) 

Definition at line 46 of file fraigApi.c.

00046 { return p->vInputs->nSize;     }

Fraig_Node_t** Fraig_ManReadInputs ( Fraig_Man_t *  p  ) 

Definition at line 43 of file fraigApi.c.

00043 { return p->vInputs->pArray;    }

int Fraig_ManReadInspects ( Fraig_Man_t *  p  ) 

Definition at line 72 of file fraigApi.c.

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

Fraig_Node_t* Fraig_ManReadIthNode ( Fraig_Man_t *  p,
int  i 
)

Definition at line 50 of file fraigApi.c.

00050 { 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.

00169 {
00170     int k;
00171     if ( i < 0 )
00172     {
00173         printf( "Requesting a PI with a negative number\n" );
00174         return NULL;
00175     }
00176     // create the PIs to fill in the interval
00177     if ( i >= p->vInputs->nSize )
00178         for ( k = p->vInputs->nSize; k <= i; k++ )
00179             Fraig_NodeCreatePi( p ); 
00180     return p->vInputs->pArray[i];
00181 }

int* Fraig_ManReadModel ( Fraig_Man_t *  p  ) 

Definition at line 60 of file fraigApi.c.

00060 { return p->pModel;     }

int Fraig_ManReadNodeNum ( Fraig_Man_t *  p  ) 

Definition at line 48 of file fraigApi.c.

00048 { return p->vNodes->nSize;      }

Fraig_Node_t** Fraig_ManReadNodes ( Fraig_Man_t *  p  ) 

Definition at line 45 of file fraigApi.c.

00045 { return p->vNodes->pArray;     }

char** Fraig_ManReadOutputNames ( Fraig_Man_t *  p  ) 

Definition at line 52 of file fraigApi.c.

00052 { return p->ppOutputNames;      }

int Fraig_ManReadOutputNum ( Fraig_Man_t *  p  ) 

Definition at line 47 of file fraigApi.c.

00047 { return p->vOutputs->nSize;    }

Fraig_Node_t** Fraig_ManReadOutputs ( Fraig_Man_t *  p  ) 

Definition at line 44 of file fraigApi.c.

00044 { return p->vOutputs->pArray;   }

int Fraig_ManReadPatternNumDynamic ( Fraig_Man_t *  p  ) 

Definition at line 64 of file fraigApi.c.

00064 { return p->iWordStart * 32;  }

int Fraig_ManReadPatternNumDynamicFiltered ( Fraig_Man_t *  p  ) 

Definition at line 66 of file fraigApi.c.

00066 { return p->iPatsPerm;        }

int Fraig_ManReadPatternNumRandom ( Fraig_Man_t *  p  ) 

Definition at line 62 of file fraigApi.c.

00062 { return p->nWordsRand * 32;  }

char* Fraig_ManReadSat ( Fraig_Man_t *  p  ) 

Definition at line 54 of file fraigApi.c.

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

int Fraig_ManReadSatFails ( Fraig_Man_t *  p  ) 

Definition at line 68 of file fraigApi.c.

00068 { return p->nSatFailsReal;    }

char* Fraig_ManReadVarsInt ( Fraig_Man_t *  p  ) 

Definition at line 53 of file fraigApi.c.

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

Fraig_NodeVec_t* Fraig_ManReadVecInputs ( Fraig_Man_t *  p  ) 

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

FileName [fraigApi.c]

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

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

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 40 of file fraigApi.c.

00040 { return p->vInputs;            }

Fraig_NodeVec_t* Fraig_ManReadVecNodes ( Fraig_Man_t *  p  ) 

Definition at line 42 of file fraigApi.c.

00042 { return p->vNodes;             }

Fraig_NodeVec_t* Fraig_ManReadVecOutputs ( Fraig_Man_t *  p  ) 

Definition at line 41 of file fraigApi.c.

00041 { return p->vOutputs;           }

int Fraig_ManReadVerbose ( Fraig_Man_t *  p  ) 

Definition at line 59 of file fraigApi.c.

00059 { return p->fVerbose;   }

void Fraig_ManSetChoicing ( Fraig_Man_t *  p,
int  fChoicing 
)

Definition at line 88 of file fraigApi.c.

00088 { p->fChoicing = fChoicing; }

void Fraig_ManSetDoSparse ( Fraig_Man_t *  p,
int  fDoSparse 
)

Definition at line 87 of file fraigApi.c.

00087 { p->fDoSparse = fDoSparse; }

void Fraig_ManSetFeedBack ( Fraig_Man_t *  p,
int  fFeedBack 
)

Definition at line 86 of file fraigApi.c.

00086 { 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 85 of file fraigApi.c.

00085 { p->fFuncRed  = fFuncRed;  }

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

Definition at line 95 of file fraigApi.c.

00095 { p->ppInputNames  = ppNames; }

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

Definition at line 94 of file fraigApi.c.

00094 { 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.

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

void Fraig_ManSetTimeToGraph ( Fraig_Man_t *  p,
int  Time 
)

Definition at line 91 of file fraigApi.c.

00091 { p->timeToAig = Time;      }

void Fraig_ManSetTimeToNet ( Fraig_Man_t *  p,
int  Time 
)

Definition at line 92 of file fraigApi.c.

00092 { p->timeToNet = Time;      }

void Fraig_ManSetTimeTotal ( Fraig_Man_t *  p,
int  Time 
)

Definition at line 93 of file fraigApi.c.

00093 { p->timeTotal = Time;      }

void Fraig_ManSetTryProve ( Fraig_Man_t *  p,
int  fTryProve 
)

Definition at line 89 of file fraigApi.c.

00089 { p->fTryProve = fTryProve; }

void Fraig_ManSetVerbose ( Fraig_Man_t *  p,
int  fVerbose 
)

Definition at line 90 of file fraigApi.c.

00090 { 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.

00213 {
00214     return Fraig_NodeAndCanon( p, p1, p2 );
00215 }

int Fraig_NodeComparePhase ( Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

Definition at line 154 of file fraigApi.c.

00154 { 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.

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

int Fraig_NodeIsAnd ( Fraig_Node_t *  p  ) 

Definition at line 153 of file fraigApi.c.

00153 {  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.

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

int Fraig_NodeIsVar ( Fraig_Node_t *  p  ) 

Definition at line 152 of file fraigApi.c.

00152 {  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.

00261 {
00262     Fraig_Node_t * pAnd1, * pAnd2, * pRes;
00263     pAnd1 = Fraig_NodeAndCanon( p, pC,          pT );     Fraig_Ref( pAnd1 );
00264     pAnd2 = Fraig_NodeAndCanon( p, Fraig_Not(pC), pE );   Fraig_Ref( pAnd2 );
00265     pRes  = Fraig_NodeOr( p, pAnd1, pAnd2 ); 
00266     Fraig_RecursiveDeref( p, pAnd1 );
00267     Fraig_RecursiveDeref( p, pAnd2 );
00268     Fraig_Deref( pRes );
00269     return pRes;
00270 }

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.

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

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.

00108 { return p->pData0;    }

Fraig_Node_t* Fraig_NodeReadData1 ( Fraig_Node_t *  p  ) 

Definition at line 109 of file fraigApi.c.

00109 { return p->pData1;    }

Fraig_Node_t* Fraig_NodeReadNextE ( Fraig_Node_t *  p  ) 

Definition at line 113 of file fraigApi.c.

00113 { return p->pNextE;    }

int Fraig_NodeReadNum ( Fraig_Node_t *  p  ) 

Definition at line 110 of file fraigApi.c.

00110 { return p->Num;       }

int Fraig_NodeReadNumFanouts ( Fraig_Node_t *  p  ) 

Definition at line 116 of file fraigApi.c.

00116 { return p->nFanouts;  }

int Fraig_NodeReadNumOnes ( Fraig_Node_t *  p  ) 

Definition at line 118 of file fraigApi.c.

00118 { return p->nOnes;     }

int Fraig_NodeReadNumRefs ( Fraig_Node_t *  p  ) 

Definition at line 115 of file fraigApi.c.

00115 { return p->nRefs;     }

Fraig_Node_t* Fraig_NodeReadOne ( Fraig_Node_t *  p  ) 

Definition at line 111 of file fraigApi.c.

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

unsigned* Fraig_NodeReadPatternsDynamic ( Fraig_Node_t *  p  ) 

Definition at line 124 of file fraigApi.c.

00124 { return p->puSimD;    }

unsigned* Fraig_NodeReadPatternsRandom ( Fraig_Node_t *  p  ) 

Definition at line 121 of file fraigApi.c.

00121 { return p->puSimR;    }

Fraig_Node_t* Fraig_NodeReadRepr ( Fraig_Node_t *  p  ) 

Definition at line 114 of file fraigApi.c.

00114 { return p->pRepr;     }

int Fraig_NodeReadSimInv ( Fraig_Node_t *  p  ) 

Definition at line 117 of file fraigApi.c.

00117 { return p->fInv;      }

Fraig_Node_t* Fraig_NodeReadTwo ( Fraig_Node_t *  p  ) 

Definition at line 112 of file fraigApi.c.

00112 { 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.

00286 {
00287 //    assert( pMan->fChoicing );
00288     pNodeNew->pNextE = pNodeOld->pNextE;
00289     pNodeOld->pNextE = pNodeNew;
00290     pNodeNew->pRepr  = pNodeOld;
00291 }

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.

00137 { p->pData0  = pData;  }

void Fraig_NodeSetData1 ( Fraig_Node_t *  p,
Fraig_Node_t *  pData 
)

Definition at line 138 of file fraigApi.c.

00138 { p->pData1  = pData;  }

Generated on Tue Jan 5 12:19:38 2010 for abc70930 by  doxygen 1.6.1