summaryrefslogtreecommitdiffstats
path: root/src/opt/res
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/res')
-rw-r--r--src/opt/res/res.h4
-rw-r--r--src/opt/res/resCore.c53
-rw-r--r--src/opt/res/resFilter.c2
-rw-r--r--src/opt/res/resSat.c150
4 files changed, 193 insertions, 16 deletions
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 ///
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 07:21:05 +0000