diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-08 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-08 08:01:00 -0800 |
| commit | f2d4f6c26eb610cf4843004fc6955a1548aa9f8f (patch) | |
| tree | 089ca0bde7ecc2bb0acec04aeb28c52ecc18139f /src/opt/mfs/mfsInter.c | |
| parent | 5a6924060bffb688101f54711f967305fc3fa480 (diff) | |
| download | abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.tar.gz abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.tar.bz2 abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.zip | |
Version abc80208
Diffstat (limited to 'src/opt/mfs/mfsInter.c')
| -rw-r--r-- | src/opt/mfs/mfsInter.c | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 16db5061..65acd4eb 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -220,6 +220,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) Kit_Graph_t * pGraph; Hop_Obj_t * pFunc; int nFanins, status; + int c, i, * pGloVars; // derive the SAT solver for interpolation pSat = Abc_MfsCreateSolverResub( p, pCands, nCands ); @@ -235,6 +236,16 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) pCnf = sat_solver_store_release( pSat ); sat_solver_delete( pSat ); + // set the global variables + pGloVars = Int_ManSetGlobalVars( p->pMan, nCands ); + for ( c = 0; c < nCands; c++ ) + { + // get the variable number of this divisor + i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; + // get the corresponding SAT variable + pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + } + // derive the interpolant nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth ); Sto_ManFree( pCnf ); |