Version abc70123

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                                ///