Changes to LUT mappers.

1 files changed, 243 insertions, 18 deletions

diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index 1893814e..223882b8 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "if.h"
-#include "sat/bsat/satSolver.h"
+#include "aig/gia/giaAig.h"
+#include "sat/bsat/satStore.h"
+#include "sat/cnf/cnf.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -67,30 +70,53 @@ int If_ManStrCheck( char * pStr, int * pnVars, int * pnObjs )
         if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
         {
             if ( pStr[i+1] == '=' )
-                Marks[pStr[i] - 'a'] = 2, MaxDef = 1 + Abc_MaxInt(MaxDef, pStr[i] - 'a');
-            else
-                Marks[pStr[i] - 'a'] = 1, MaxVar = 1 + Abc_MaxInt(MaxVar, pStr[i] - 'a');
+                Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a');
             continue;
         }
         printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
         RetValue = 0;
     }
+    if ( !RetValue )
+        return 0;
+    for ( i = 0; pStr[i]; i++ )
+    {
+        if ( pStr[i] == '=' || pStr[i] == ';' || 
+             pStr[i] == '(' || pStr[i] == ')' || 
+             pStr[i] == '[' || pStr[i] == ']' || 
+             pStr[i] == '<' || pStr[i] == '>' || 
+             pStr[i] == '{' || pStr[i] == '}' )
+            continue;
+        if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
+        {
+            if ( pStr[i+1] != '=' && Marks[pStr[i] - 'a'] != 2 )
+                Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a');
+            continue;
+        }
+        printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
+        RetValue = 0;
+    }
+    if ( !RetValue )
+        return 0;
+    MaxVar++;
+    MaxDef++;
     for ( i = 0; i < MaxDef; i++ )
         if ( Marks[i] == 0 )
-            printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + Marks[i] ), RetValue = 0;
+            printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + i ), RetValue = 0;
     for ( i = 0; i < MaxVar; i++ )
         if ( Marks[i] == 2 )
-            printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + Marks[i] ), RetValue = 0;
+            printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
     for ( i = MaxVar; i < MaxDef; i++ )
         if ( Marks[i] == 1 )
-            printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + Marks[i] ), RetValue = 0;
-    *pnVars = RetValue ? MaxVar : 0;
-    *pnObjs = RetValue ? MaxDef : 0;
-    return RetValue;
+            printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
+    if ( !RetValue )
+        return 0;
+    *pnVars = MaxVar;
+    *pnObjs = MaxDef;
+    return 1;
 }
-int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFans, int ppFans[][6] )
+int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFans, int ppFans[][6], int * pFirsts, int * pnSatVars )
 {
-    int i, k, n, f;
+    int i, k, n, f, nPars = nVars;
     char Next = 0;
     assert( nVars < nObjs );
     for ( i = nVars; i < nObjs; i++ )
@@ -117,12 +143,104 @@ int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFan
         for ( f = 0; f < pnFans[i]; f++ )
         {
             ppFans[i][f] = pStr[k + 3 + f] - 'a';
+            assert( ppFans[i][k] < i );
             if ( ppFans[i][f] < 0 || ppFans[i][f] >= nObjs )
                 printf( "Error!\n" );
         }
+        if ( pTypes[i] != IF_DSD_PRIME )
+            continue;
+        pFirsts[i] = nPars;
+        nPars += (1 << pnFans[i]);
     }
+    *pnSatVars = nPars;
     return 1;
 }
+Gia_Man_t * If_ManStrFindModel( int nVars, int nObjs, int nSatVars, int * pTypes, int * pnFans, int ppFans[][6], int * pFirsts )
+{
+    Gia_Man_t * pNew, * pTemp;
+    int * pVarsPar, * pVarsObj;
+    int i, k, n, Step, iLit, nMints, nPars = 0;
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( "model" );
+    Gia_ManHashStart( pNew );
+    pVarsPar = ABC_ALLOC( int, nSatVars );
+    pVarsObj = ABC_ALLOC( int, nObjs );
+    for ( i = 0; i < nSatVars; i++ )
+        pVarsPar[i] = Gia_ManAppendCi(pNew);
+    for ( i = 0; i < nVars; i++ )
+        pVarsObj[i] = pVarsPar[nSatVars - nVars + i];
+    for ( i = nVars; i < nObjs; i++ )
+    {
+        if ( pTypes[i] == IF_DSD_AND )
+        {
+            iLit = 1;
+            for ( k = 0; k < pnFans[i]; k++ )
+                iLit = Gia_ManHashAnd( pNew, iLit, pVarsObj[ppFans[i][k]] );
+            pVarsObj[i] = iLit;
+        }
+        else if ( pTypes[i] == IF_DSD_XOR )
+        {
+            iLit = 0;
+            for ( k = 0; k < pnFans[i]; k++ )
+                iLit = Gia_ManHashXor( pNew, iLit, pVarsObj[ppFans[i][k]] );
+            pVarsObj[i] = iLit;
+        }
+        else if ( pTypes[i] == IF_DSD_MUX )
+        {
+            assert( pnFans[i] == 3 );
+            pVarsObj[i] = Gia_ManHashMux( pNew, pVarsObj[ppFans[i][0]], pVarsObj[ppFans[i][1]], pVarsObj[ppFans[i][2]] );
+        }
+        else if ( pTypes[i] == IF_DSD_PRIME )
+        {
+            int pVarsData[64];
+            assert( pnFans[i] >= 1 && pnFans[i] <= 6 );
+            nMints = (1 << pnFans[i]);
+            for ( k = 0; k < nMints; k++ )
+                pVarsData[k] = pVarsPar[nPars++];
+            for ( Step = 1, k = 0; k < pnFans[i]; k++, Step <<= 1 )
+                for ( n = 0; n < nMints; n += Step << 1 )
+                    pVarsData[n] = Gia_ManHashMux( pNew, pVarsObj[ppFans[i][k]], pVarsData[n+Step], pVarsData[n] );
+            assert( Step == nMints );
+            pVarsObj[i] = pVarsData[0];
+        }
+        else assert( 0 );
+    }
+    assert( nPars + nVars == nSatVars );
+    Gia_ManAppendCo( pNew, pVarsObj[nObjs-1] );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    ABC_FREE( pVarsPar );
+    ABC_FREE( pVarsObj );
+    assert( Gia_ManPiNum(pNew) == nSatVars );
+    assert( Gia_ManPoNum(pNew) == 1 );
+    return pNew;
+}
+Gia_Man_t * If_ManStrFindCofactors( int nPars, Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp; 
+    Gia_Obj_t * pObj;
+    int i, m, nMints = 1 << (Gia_ManCiNum(p) - nPars);
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        if ( i < nPars )
+            pObj->Value = Gia_ManAppendCi( pNew );
+    for ( m = 0; m < nMints; m++ )
+    {
+        Gia_ManForEachCi( p, pObj, i )
+            if ( i >= nPars )
+                pObj->Value = ((m >> (i - nPars)) & 1);
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ManForEachPo( p, pObj, i )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
 
 /**Function*************************************************************
 
@@ -135,23 +253,70 @@ int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFan
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * If_ManSatBuild( char * pStr )
+static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
+{
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+    pAig->nRegs = 0;
+    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
+    Aig_ManStop( pAig );
+    return pCnf;
+}
+sat_solver * If_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
 {
-    int nVars, nObjs;
+    sat_solver * pSat;
+    Gia_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    int i;    
+    pCnf = Cnf_DeriveGiaRemapped( p );
+    // start the SAT solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    // add timeframe clauses
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            assert( 0 );
+    // inputs/outputs
+    *pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) );
+    Gia_ManForEachCi( p, pObj, i )
+        Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
+    *pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) );
+    Gia_ManForEachCo( p, pObj, i )
+        Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
+    Cnf_DataFree( pCnf );
+    return pSat;
+}
+
+sat_solver * If_ManSatBuild( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
+{
+    int nVars, nObjs, nSatVars;
     int pTypes[32] = {0};
     int pnFans[32] = {0};
     int ppFans[32][6] = {{0}};
+    int pFirsts[32] = {0};
+    Gia_Man_t * p1, * p2;
     sat_solver * pSat = NULL;
+    *pvPiVars = *pvPoVars = NULL;
     if ( !If_ManStrCheck(pStr, &nVars, &nObjs) )
         return NULL;
-    if ( !If_ManStrParse(pStr, nVars, nObjs, pTypes, pnFans, ppFans) )
+    if ( !If_ManStrParse(pStr, nVars, nObjs, pTypes, pnFans, ppFans, pFirsts, &nSatVars) )
+        return NULL;
+    p1 = If_ManStrFindModel(nVars, nObjs, nSatVars, pTypes, pnFans, ppFans, pFirsts);
+    if ( p1 == NULL )
         return NULL;
+//    Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
+    p2 = If_ManStrFindCofactors( nSatVars - nVars, p1 );
+    Gia_ManStop( p1 );
+    if ( p2 == NULL )
+        return NULL;
+//    Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
+    pSat = If_ManStrFindSolver( p2, pvPiVars, pvPoVars );
+    Gia_ManStop( p2 );
     return pSat;
 }
-
 /**Function*************************************************************
 
-  Synopsis    [Test procedure.]
+  Synopsis    []
 
   Description []
                
@@ -160,8 +325,68 @@ sat_solver * If_ManSatBuild( char * pStr )
   SeeAlso     []
 
 ***********************************************************************/
-void If_ManSatTest()
+void If_ManSatPrintPerm( char * pPerms, int nVars )
 {
+    int i;
+    for ( i = 0; i < nVars; i++ )
+        printf( "%c", 'a' + pPerms[i] );
+    printf( "\n" );
+}
+int If_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nVarsAll, Vec_Int_t * vLits )
+{
+    int v, Value, m, mNew, nMints = (1 << nVars);
+    assert( (1 << nVarsAll) == Vec_IntSize(vPoVars) );
+    assert( nMints <= Vec_IntSize(vPoVars) );
+    // remap minterms
+    Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
+    for ( m = 0; m < nMints; m++ )
+    {
+        mNew = 0;
+        for ( v = 0; v < nVarsAll; v++ )
+        {
+            assert( pPerm[v] < nVars );
+            if ( ((m >> pPerm[v]) & 1) )
+                mNew |= (1 << v);
+        }
+        assert( Vec_IntEntry(vLits, mNew) == -1 );
+        Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
+    }
+    // find assumptions
+    v = 0;
+    Vec_IntForEachEntry( vLits, Value, m )
+        if ( Value >= 0 )
+            Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) );
+    Vec_IntShrink( vLits, v );
+    // run SAT solver
+    Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+    return (int)(Value == l_True);
+}
+void If_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues )
+{
+    int i, iVar;
+    Vec_IntClear( vValues );
+    Vec_IntForEachEntry( vPiVars, iVar, i )
+        Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
+}
+int If_ManSatCheckAll_int( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, Vec_Int_t * vLits, char ** pPerms, int nPerms )
+{
+    int pPerm[IF_MAX_FUNC_LUTSIZE];
+    int p, i;
+    for ( p = 0; p < nPerms; p++ )
+    {
+        for ( i = 0; i < nVars; i++ )
+            pPerm[i] = (int)pPerms[p][i];
+        if ( If_ManSatCheckOne(pSat, vPoVars, pTruth, nVars, pPerm, nVars, vLits) )
+            return p;
+    }
+    return -1;
+}
+int If_ManSatCheckAll( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, Vec_Int_t * vLits, char ** pPerms, int nPerms )
+{
+    abctime clk = Abc_Clock();
+    int RetValue = If_ManSatCheckAll_int( pSat, vPoVars, pTruth, nVars, vLits, pPerms, nPerms );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////