diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2005-08-28 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2005-08-28 08:01:00 -0700 |
| commit | 3c25decf65704916943b0569e6d0608072550a89 (patch) | |
| tree | c4b532e8edd1e2226bc84268e4e2368db8ee295d /src/sat/fraig/fraigInt.h | |
| parent | 28db025b8393e307328d51ff6901c4ebab669e95 (diff) | |
| download | abc-3c25decf65704916943b0569e6d0608072550a89.tar.gz abc-3c25decf65704916943b0569e6d0608072550a89.tar.bz2 abc-3c25decf65704916943b0569e6d0608072550a89.zip | |
Version abc50828
Diffstat (limited to 'src/sat/fraig/fraigInt.h')
| -rw-r--r-- | src/sat/fraig/fraigInt.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 1139bdc0..5f8b3496 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -178,6 +178,7 @@ struct Fraig_ManStruct_t_ Msat_Solver_t * pSat; // the SAT solver Msat_IntVec_t * vProj; // the temporary array of projection vars int nSatNums; // the counter of SAT variables + int * pModel; // the assignment, which satisfies the miter // these arrays belong to the solver Msat_IntVec_t * vVarsInt; // the temporary array of variables Msat_ClauseVec_t * vAdjacents; // the temporary storage for connectivity @@ -378,6 +379,7 @@ extern void Fraig_FeedBackInit( Fraig_Man_t * p ); extern void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); extern void Fraig_FeedBackTest( Fraig_Man_t * p ); extern int Fraig_FeedBackCompress( Fraig_Man_t * p ); +extern int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode ); /*=== fraigMem.c =============================================================*/ extern Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize ); extern void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose ); @@ -404,6 +406,7 @@ extern Fraig_Node_t * Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_No extern void Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); extern int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand ); extern int Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ); +extern int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand ); extern void Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask ); extern void Fraig_TablePrintStatsS( Fraig_Man_t * pMan ); extern void Fraig_TablePrintStatsF( Fraig_Man_t * pMan ); |