From b1a913fb5e85ba04646632f3d771ad79bfd8a720 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 23 Jan 2007 08:01:00 -0800 Subject: Version abc70123 --- src/opt/res/res.h | 4 +- src/opt/res/resCore.c | 53 ++++++++++++++--- src/opt/res/resFilter.c | 2 +- src/opt/res/resSat.c | 150 ++++++++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 193 insertions(+), 16 deletions(-) (limited to 'src/opt/res') diff --git a/src/opt/res/res.h b/src/opt/res/res.h index 91171d3b..4a887741 100644 --- a/src/opt/res/res.h +++ b/src/opt/res/res.h @@ -93,9 +93,9 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj ) extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ); extern int Res_WinVisitMffc( Res_Win_t * p ); /*=== resFilter.c ==========================================================*/ -extern Vec_Ptr_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ); +extern Vec_Vec_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ); /*=== resSat.c ==========================================================*/ -extern Hop_Obj_t * Res_SatFindFunction( Hop_Man_t * pMan, Res_Win_t * pWin, Vec_Ptr_t * vFanins, Abc_Ntk_t * pAig ); +extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ); /*=== resSim.c ==========================================================*/ extern Res_Sim_t * Res_SimAlloc( int nWords ); extern void Res_SimFree( Res_Sim_t * p ); diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index 0335712d..17d1c62e 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -20,6 +20,8 @@ #include "abc.h" #include "res.h" +#include "kit.h" +#include "satStore.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -42,15 +44,24 @@ ***********************************************************************/ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose ) { + Int_Man_t * pMan; + Sto_Man_t * pCnf; Res_Win_t * pWin; Res_Sim_t * pSim; Abc_Ntk_t * pAig; Abc_Obj_t * pObj; Hop_Obj_t * pFunc; + Kit_Graph_t * pGraph; + Vec_Vec_t * vResubs; Vec_Ptr_t * vFanins; - int i, nNodesOld; + Vec_Int_t * vMemory; + unsigned * puTruth; + int i, k, nNodesOld, nFanins; assert( Abc_NtkHasAig(pNtk) ); assert( nWindow > 0 && nWindow < 100 ); + vMemory = Vec_IntAlloc(0); + // start the interpolation manager + pMan = Int_ManAlloc( 512 ); // start the window pWin = Res_WinAlloc(); pSim = Res_SimAlloc( nSimWords ); @@ -72,20 +83,44 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerb // create the AIG for the window pAig = Res_WndStrash( pWin ); // prepare simulation info - if ( Res_SimPrepare( pSim, pAig ) ) + if ( !Res_SimPrepare( pSim, pAig ) ) { - // find resub candidates for the node - vFanins = Res_FilterCandidates( pWin, pSim ); - // check using SAT - pFunc = Res_SatFindFunction( pNtk->pManFunc, pWin, vFanins, pAig ); - // update the network - if ( pFunc == NULL ) - Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels ); + Abc_NtkDelete( pAig ); + continue; + } + // find resub candidates for the node + vResubs = Res_FilterCandidates( pWin, pSim ); + if ( vResubs ) + { + // iterate through the resubstitutions + Vec_VecForEachLevel( vResubs, vFanins, k ) + { + extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); + pCnf = Res_SatProveUnsat( pAig, vFanins ); + if ( pCnf == NULL ) + continue; + // interplate this proof + nFanins = Int_ManInterpolate( pMan, pCnf, fVerbose, &puTruth ); + assert( nFanins == Vec_PtrSize(vFanins) - 2 ); + Sto_ManFree( pCnf ); + // transform interpolant into the AIG + pGraph = Kit_TruthToGraph( puTruth, nFanins, vMemory ); + // derive the AIG for the decomposition tree + pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph ); + Kit_GraphFree( pGraph ); + // update the network + if ( pFunc == NULL ) + Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels ); + break; + } + Vec_VecFree( vResubs ); } Abc_NtkDelete( pAig ); } Res_WinFree( pWin ); Res_SimFree( pSim ); + Int_ManFree( pMan ); + Vec_IntFree( vMemory ); // check the resulting network if ( !Abc_NtkCheck( pNtk ) ) { diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c index e2e295a0..65e9953f 100644 --- a/src/opt/res/resFilter.c +++ b/src/opt/res/resFilter.c @@ -40,7 +40,7 @@ SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ) +Vec_Vec_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ) { unsigned * pInfo; Abc_Obj_t * pFanin; diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c index 39ca9ad6..770152cf 100644 --- a/src/opt/res/resSat.c +++ b/src/opt/res/resSat.c @@ -21,19 +21,116 @@ #include "abc.h" #include "res.h" #include "hop.h" -//#include "bf.h" +#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern int Res_SatAddConst1( sat_solver * pSat, int iVar ); +extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ); +extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Loads AIG into the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) +{ + void * pCnf; + sat_solver * pSat; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; + int i, nNodes, status; + + // make sure the constant node is not involved + assert( Abc_ObjFanoutNum(Abc_AigConst1(pAig)) == 0 ); + + // collect reachable nodes + vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); + // assign unique numbers to each node + nNodes = 0; + Abc_NtkForEachPi( pAig, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vFanins, pObj, i ) + pObj->pCopy = (void *)nNodes++; + + // start the solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + + // add clause for AND gates + Vec_PtrForEachEntry( vNodes, pObj, i ) + Res_SatAddAnd( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + // add clauses for the POs + Vec_PtrForEachEntry( vFanins, pObj, i ) + Res_SatAddEqual( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); + // add trivial clauses + pObj = Vec_PtrEntry(vFanins, 0); + Res_SatAddConst1( pSat, (int)pObj->pCopy ); + pObj = Vec_PtrEntry(vFanins, 1); + Res_SatAddConst1( pSat, (int)pObj->pCopy ); + // bookmark the clauses of A + sat_solver_store_mark_clauses_a( pSat ); + // duplicate the clauses + pObj = Vec_PtrEntry(vFanins, 1); + Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy ); + // add the equality clauses + Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 ) + Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 ); + // bookmark the roots + sat_solver_store_mark_roots( pSat ); + Vec_PtrFree( vNodes ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); + if ( status == l_False ) + pCnf = sat_solver_store_release( pSat ); + else if ( status == l_True ) + pCnf = NULL; + else + pCnf = NULL; + sat_solver_delete( pSat ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_SatAddConst1( sat_solver * pSat, int iVar ) +{ + lit Lit = lit_var(iVar); + if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] Description [] @@ -42,11 +139,56 @@ SeeAlso [] ***********************************************************************/ -Hop_Obj_t * Res_SatFindFunction( Hop_Man_t * pMan, Res_Win_t * pWin, Vec_Ptr_t * vFanins, Abc_Ntk_t * pAig ) +int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) { - return NULL; + lit Lits[2]; + + Lits[0] = toLitCond( iVar0, 0 ); + Lits[1] = toLitCond( iVar1, !fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar0, 1 ); + Lits[1] = toLitCond( iVar1, fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + return 1; } +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) +{ + lit Lits[3]; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar0, fCompl0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar1, fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 0 ); + Lits[1] = toLitCond( iVar0, !fCompl0 ); + Lits[2] = toLitCond( iVar1, !fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3