From 6da21b8b884632c901ae10955e23c0c8206e7e58 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 5 Mar 2015 23:00:30 -0800 Subject: Experiments with SAT-based cube enumeration. --- abclib.dsp | 4 + src/aig/gia/giaDup.c | 33 +++ src/aig/gia/giaMf.c | 4 +- src/aig/gia/giaQbf.c | 6 +- src/base/abci/abc.c | 68 +++++ src/map/if/ifSat.c | 7 +- src/sat/bmc/bmcEco.c | 6 - src/sat/bmc/bmcFx.c | 683 +++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bsat/satSolver.h | 38 +-- 9 files changed, 816 insertions(+), 33 deletions(-) create mode 100644 src/sat/bmc/bmcFx.c diff --git a/abclib.dsp b/abclib.dsp index c7bda043..1a04ffce 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -1583,6 +1583,10 @@ SOURCE=.\src\sat\bmc\bmcFault.c # End Source File # Begin Source File +SOURCE=.\src\sat\bmc\bmcFx.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\bmc\bmcICheck.c # End Source File # Begin Source File diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 029d1599..81362276 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -415,6 +415,39 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + { + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNot(Gia_ObjFanin0Copy(pObj)) ); + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.] diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index 03848f1e..b90e7bc9 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -346,9 +346,9 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) Gia_ManForEachAndReverseId( p->pGia, Id ) if ( Mf_ObjMapRefNum(p, Id) ) Vec_IntWriteEntry( vCnfIds, Id, Id ), iVar++; + Vec_IntWriteEntry( vCnfIds, 0, 0 ); Gia_ManForEachCiId( p->pGia, Id, i ) Vec_IntWriteEntry( vCnfIds, Id, Id ); - Vec_IntWriteEntry( vCnfIds, 0, 0 ); assert( iVar == nVars ); } else @@ -358,9 +358,9 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) Gia_ManForEachAndReverseId( p->pGia, Id ) if ( Mf_ObjMapRefNum(p, Id) ) Vec_IntWriteEntry( vCnfIds, Id, iVar++ ); + Vec_IntWriteEntry( vCnfIds, 0, iVar++ ); Gia_ManForEachCiId( p->pGia, Id, i ) Vec_IntWriteEntry( vCnfIds, Id, iVar++ ); - Vec_IntWriteEntry( vCnfIds, 0, iVar++ ); assert( iVar == nVars ); } // generate CNF diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index a14ec443..b7d678b3 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -75,7 +75,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose abctime clkStart = Abc_Clock(); pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1; + iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; Cnf_DataFree( pCnf ); // iterate through the SAT assignment vLits = Vec_IntAlloc( Gia_ManPiNum(pGia) ); @@ -180,7 +180,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) p->nPars = nPars; p->nVars = Gia_ManPiNum(pGia) - nPars; p->fVerbose = fVerbose; - p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1; + p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); p->pSatSyn = sat_solver_new(); p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) ); @@ -280,7 +280,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) { Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); - int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1; + int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof);// - 1; pCnf->pMan = NULL; Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) ); for ( i = 0; i < pCnf->nClauses; i++ ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 14d6ddbe..f1c19bd8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -437,6 +437,7 @@ static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Qbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9SatFx ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Maxi ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1043,6 +1044,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fftest", Abc_CommandAbc9FFTest, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&qbf", Abc_CommandAbc9Qbf, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 ); @@ -36534,6 +36536,72 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9SatFx( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Bmc_FxCompute( Gia_Man_t * p ); + extern int Bmc_FxComputeOne( Gia_Man_t * p ); + int c, nFrames = 1000, fDec = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fdvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'd': + fDec ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SatFx(): There is no AIG.\n" ); + return 0; + } + if ( fDec ) + Bmc_FxComputeOne( pAbc->pGia ); + else + Bmc_FxCompute( pAbc->pGia ); + return 0; + +usage: + Abc_Print( -2, "usage: &satfx [-F num] [-dvh]\n" ); + Abc_Print( -2, "\t performs SAT based shared logic extraction\n" ); + Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-d : toggles decomposing the first output [default = %s]\n", fDec? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + /**Function************************************************************* Synopsis [] diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 4af55203..4709d88c 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -54,10 +54,11 @@ void * If_ManSatBuildXY( int nLutSize ) sat_solver_setnvars( p, nVars ); for ( m = 0; m < nMintsF; m++ ) sat_solver_add_mux( p, + iVarM + m, iVarP0 + m % nMintsL, iVarP1 + 2 * (m / nMintsL) + 1, iVarP1 + 2 * (m / nMintsL), - iVarM + m ); + 0, 0, 0, 0 ); return p; } void * If_ManSatBuildXYZ( int nLutSize ) @@ -73,13 +74,13 @@ void * If_ManSatBuildXYZ( int nLutSize ) sat_solver_setnvars( p, nVars ); for ( m = 0; m < nMintsF; m++ ) sat_solver_add_mux41( p, + iVarM + m, iVarP0 + m % nMintsL, iVarP1 + (m >> nLutSize) % nMintsL, iVarP2 + 4 * (m >> (2 * nLutSize)) + 0, iVarP2 + 4 * (m >> (2 * nLutSize)) + 1, iVarP2 + 4 * (m >> (2 * nLutSize)) + 2, - iVarP2 + 4 * (m >> (2 * nLutSize)) + 3, - iVarM + m ); + iVarP2 + 4 * (m >> (2 * nLutSize)) + 3 ); return p; } void If_ManSatUnbuild( void * p ) diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c index c4fc3ba8..07fdd704 100644 --- a/src/sat/bmc/bmcEco.c +++ b/src/sat/bmc/bmcEco.c @@ -138,7 +138,6 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars ) { int nBTLimit = 1000000; - Vec_Int_t * vValues = Vec_IntAlloc( Vec_IntSize(vVars) ); Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vVars) ); int status, i, Div, iVar, nFinal, * pFinal, nIter = 0, RetValue = 0; int pLits[2], nVars = sat_solver_nvars( pSat ); @@ -154,10 +153,6 @@ int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars ) if ( status == l_False ) { RetValue = 1; break; } assert( status == l_True ); - // remember variable values - Vec_IntClear( vValues ); - Vec_IntForEachEntry( vVars, iVar, i ) - Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); // collect divisor literals Vec_IntClear( vLits ); Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0 @@ -189,7 +184,6 @@ int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars ) nIter++; } // assert( status == l_True ); - Vec_IntFree( vValues ); Vec_IntFree( vLits ); return RetValue; } diff --git a/src/sat/bmc/bmcFx.c b/src/sat/bmc/bmcFx.c new file mode 100644 index 00000000..4bf20bc9 --- /dev/null +++ b/src/sat/bmc/bmcFx.c @@ -0,0 +1,683 @@ +/**CFile**************************************************************** + + FileName [bmcFx.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [INT-FX: Interpolation-based logic sharing extraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcFx.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "misc/vec/vecWec.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create hash table to hash divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#define TAB_UNUSED 0x7FFF +typedef struct Tab_Obj_t_ Tab_Obj_t; // 16 bytes +struct Tab_Obj_t_ +{ + int Table; + int Next; + unsigned Cost : 17; + unsigned LitA : 15; + unsigned LitB : 15; + unsigned LitC : 15; + unsigned Func : 2; +}; +typedef struct Tab_Tab_t_ Tab_Tab_t; // 16 bytes +struct Tab_Tab_t_ +{ + int SizeMask; + int nBins; + Tab_Obj_t * pBins; +}; +static inline Tab_Tab_t * Tab_TabAlloc( int LogSize ) +{ + Tab_Tab_t * p = ABC_CALLOC( Tab_Tab_t, 1 ); + assert( LogSize >= 4 && LogSize <= 31 ); + p->SizeMask = (1 << LogSize) - 1; + p->pBins = ABC_CALLOC( Tab_Obj_t, p->SizeMask + 1 ); + p->nBins = 1; + return p; +} +static inline void Tab_TabFree( Tab_Tab_t * p ) +{ + ABC_FREE( p->pBins ); + ABC_FREE( p ); +} +static inline Vec_Int_t * Tab_TabFindBest( Tab_Tab_t * p, int nDivs ) +{ + char * pNames[5] = {"const1", "and", "xor", "mux", "none"}; + int * pOrder, i; + Vec_Int_t * vDivs = Vec_IntAlloc( 100 ); + Vec_Int_t * vCosts = Vec_IntAlloc( p->nBins ); + Tab_Obj_t * pEnt, * pLimit = p->pBins + p->nBins; + for ( pEnt = p->pBins; pEnt < pLimit; pEnt++ ) + Vec_IntPush( vCosts, -(int)pEnt->Cost ); + pOrder = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) ); + for ( i = 0; i < Vec_IntSize(vCosts); i++ ) + { + pEnt = p->pBins + pOrder[i]; + if ( i == nDivs || pEnt->Cost == 1 ) + break; + printf( "Lit0 = %5d. Lit1 = %5d. Lit2 = %5d. Func = %s. Cost = %3d.\n", + pEnt->LitA, pEnt->LitB, pEnt->LitC, pNames[pEnt->Func], pEnt->Cost ); + Vec_IntPushTwo( vDivs, pEnt->Func, pEnt->LitA ); + Vec_IntPushTwo( vDivs, pEnt->LitB, pEnt->LitC ); + } + Vec_IntFree( vCosts ); + ABC_FREE( pOrder ); + return vDivs; +} +static inline int Tab_Hash( int LitA, int LitB, int LitC, int Func, int Mask ) +{ + return (LitA * 50331653 + LitB * 100663319 + LitC + 201326611 + Func * 402653189) & Mask; +} +static inline void Tab_TabRehash( Tab_Tab_t * p ) +{ + Tab_Obj_t * pEnt, * pLimit, * pBin; + assert( p->nBins == p->SizeMask + 1 ); + // realloc memory + p->pBins = ABC_REALLOC( Tab_Obj_t, p->pBins, 2 * (p->SizeMask + 1) ); + memset( p->pBins + p->SizeMask + 1, 0, sizeof(Tab_Obj_t) * (p->SizeMask + 1) ); + // clean entries + pLimit = p->pBins + p->SizeMask + 1; + for ( pEnt = p->pBins; pEnt < pLimit; pEnt++ ) + pEnt->Table = pEnt->Next = 0; + // rehash entries + p->SizeMask = 2 * p->SizeMask + 1; + for ( pEnt = p->pBins + 1; pEnt < pLimit; pEnt++ ) + { + pBin = p->pBins + Tab_Hash( pEnt->LitA, pEnt->LitB, pEnt->LitC, pEnt->Func, p->SizeMask ); + pEnt->Next = pBin->Table; + pBin->Table = pEnt - p->pBins; + assert( !pEnt->Next || pEnt->Next != pBin->Table ); + } +} +static inline Tab_Obj_t * Tab_TabEntry( Tab_Tab_t * p, int i ) { return i ? p->pBins + i : NULL; } +static inline int Tab_TabHashAdd( Tab_Tab_t * p, int * pLits, int Func, int Cost ) +{ + if ( p->nBins == p->SizeMask + 1 ) + Tab_TabRehash( p ); + assert( p->nBins < p->SizeMask + 1 ); + { + Tab_Obj_t * pEnt, * pBin = p->pBins + Tab_Hash(pLits[0], pLits[1], pLits[2], Func, p->SizeMask); + for ( pEnt = Tab_TabEntry(p, pBin->Table); pEnt; pEnt = Tab_TabEntry(p, pEnt->Next) ) + if ( (int)pEnt->LitA == pLits[0] && (int)pEnt->LitB == pLits[1] && (int)pEnt->LitC == pLits[2] && (int)pEnt->Func == Func ) + { pEnt->Cost += Cost; return 1; } + pEnt = p->pBins + p->nBins; + pEnt->LitA = pLits[0]; + pEnt->LitB = pLits[1]; + pEnt->LitC = pLits[2]; + pEnt->Func = Func; + pEnt->Cost = Cost; + pEnt->Next = pBin->Table; + pBin->Table = p->nBins++; + assert( !pEnt->Next || pEnt->Next != pBin->Table ); + return 0; + } +} + + +/**Function************************************************************* + + Synopsis [Input is four literals. Output is type, polarity and fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +// name types +typedef enum { + DIV_CST = 0, // 0: constant 1 + DIV_AND, // 1: and (ordered fanins) + DIV_XOR, // 2: xor (ordered fanins) + DIV_MUX, // 3: mux (c, d1, d0) + DIV_NONE // 4: not used +} Div_Type_t; + +static inline Div_Type_t Bmc_FxDivOr( int LitA, int LitB, int * pLits, int * pPhase ) +{ + assert( LitA != LitB ); + if ( Abc_Lit2Var(LitA) == Abc_Lit2Var(LitB) ) + return DIV_CST; + if ( LitA > LitB ) + ABC_SWAP( int, LitA, LitB ); + pLits[0] = Abc_LitNot(LitA); + pLits[1] = Abc_LitNot(LitB); + *pPhase = 1; + return DIV_AND; +} +static inline Div_Type_t Bmc_FxDivXor( int LitA, int LitB, int * pLits, int * pPhase ) +{ + assert( LitA != LitB ); + *pPhase ^= Abc_LitIsCompl(LitA); + *pPhase ^= Abc_LitIsCompl(LitB); + pLits[0] = Abc_LitRegular(LitA); + pLits[1] = Abc_LitRegular(LitB); + return DIV_XOR; +} +static inline Div_Type_t Bmc_FxDivMux( int LitC, int LitCn, int LitT, int LitE, int * pLits, int * pPhase ) +{ + assert( LitC != LitCn ); + assert( Abc_Lit2Var(LitC) == Abc_Lit2Var(LitCn) ); + assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitT) ); + assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitE) ); + assert( Abc_Lit2Var(LitC) != Abc_Lit2Var(LitE) ); + if ( Abc_LitIsCompl(LitC) ) + { + LitC = Abc_LitRegular(LitC); + ABC_SWAP( int, LitT, LitE ); + } + if ( Abc_LitIsCompl(LitT) ) + { + *pPhase ^= 1; + LitT = Abc_LitNot(LitT); + LitE = Abc_LitNot(LitE); + } + pLits[0] = LitC; + pLits[1] = LitT; + pLits[2] = LitE; + return DIV_MUX; +} +static inline Div_Type_t Div_FindType( int LitA[2], int LitB[2], int * pLits, int * pPhase ) +{ + *pPhase = 0; + pLits[0] = pLits[1] = pLits[2] = TAB_UNUSED; + if ( LitA[0] == -1 && LitA[1] == -1 ) return DIV_CST; + if ( LitB[0] == -1 && LitB[1] == -1 ) return DIV_CST; + assert( LitA[0] >= 0 && LitB[0] >= 0 ); + assert( LitA[0] != LitB[0] ); + if ( LitA[1] == -1 && LitB[1] == -1 ) + return Bmc_FxDivOr( LitA[0], LitB[0], pLits, pPhase ); + assert( LitA[1] != LitB[1] ); + if ( LitA[1] == -1 || LitB[1] == -1 ) + { + if ( LitA[1] == -1 ) + { + ABC_SWAP( int, LitA[0], LitB[0] ); + ABC_SWAP( int, LitA[1], LitB[1] ); + } + assert( LitA[0] >= 0 && LitA[1] >= 0 ); + assert( LitB[0] >= 0 && LitB[1] == -1 ); + if ( Abc_Lit2Var(LitB[0]) == Abc_Lit2Var(LitA[0]) ) + return Bmc_FxDivOr( LitB[0], LitA[1], pLits, pPhase ); + if ( Abc_Lit2Var(LitB[0]) == Abc_Lit2Var(LitA[1]) ) + return Bmc_FxDivOr( LitB[0], LitA[0], pLits, pPhase ); + return DIV_NONE; + } + if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[0]) && Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[1]) ) + return Bmc_FxDivXor( LitA[0], LitB[1], pLits, pPhase ); + if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[0]) ) + return Bmc_FxDivMux( LitA[0], LitB[0], LitA[1], LitB[1], pLits, pPhase ); + if ( Abc_Lit2Var(LitA[0]) == Abc_Lit2Var(LitB[1]) ) + return Bmc_FxDivMux( LitA[0], LitB[1], LitA[1], LitB[0], pLits, pPhase ); + if ( Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[0]) ) + return Bmc_FxDivMux( LitA[1], LitB[0], LitA[0], LitB[1], pLits, pPhase ); + if ( Abc_Lit2Var(LitA[1]) == Abc_Lit2Var(LitB[1]) ) + return Bmc_FxDivMux( LitA[1], LitB[1], LitA[0], LitB[0], pLits, pPhase ); + return DIV_NONE; +} + +/**Function************************************************************* + + Synopsis [Returns the number of shared variables, or -1 if failed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Div_AddLit( int Lit, int pLits[2] ) +{ + if ( pLits[0] == -1 ) + pLits[0] = Lit; + else if ( pLits[1] == -1 ) + pLits[1] = Lit; + else return 1; + return 0; +} +int Div_FindDiv( Vec_Int_t * vA, Vec_Int_t * vB, int pLitsA[2], int pLitsB[2] ) +{ + int Counter = 0; + int * pBegA = vA->pArray, * pEndA = vA->pArray + vA->nSize; + int * pBegB = vB->pArray, * pEndB = vB->pArray + vB->nSize; + pLitsA[0] = pLitsA[1] = pLitsB[0] = pLitsB[1] = -1; + while ( pBegA < pEndA && pBegB < pEndB ) + { + if ( *pBegA == *pBegB ) + pBegA++, pBegB++, Counter++; + else if ( *pBegA < *pBegB ) + { + if ( Div_AddLit( *pBegA++, pLitsA ) ) + return -1; + } + else + { + if ( Div_AddLit( *pBegB++, pLitsB ) ) + return -1; + } + } + while ( pBegA < pEndA ) + if ( Div_AddLit( *pBegA++, pLitsA ) ) + return -1; + while ( pBegB < pEndB ) + if ( Div_AddLit( *pBegB++, pLitsB ) ) + return -1; + return Counter; +} + +void Div_CubePrintOne( Vec_Int_t * vCube, Vec_Str_t * vStr, int nVars ) +{ + int i, Lit; + Vec_StrFill( vStr, nVars, '-' ); + Vec_IntForEachEntry( vCube, Lit, i ) + Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') ); + printf( "%s\n", Vec_StrArray(vStr) ); +} +void Div_CubePrint( Vec_Wec_t * p, int nVars ) +{ + Vec_Int_t * vCube; int i; + Vec_Str_t * vStr = Vec_StrStart( nVars + 1 ); + Vec_WecForEachLevel( p, vCube, i ) + Div_CubePrintOne( vCube, vStr, nVars ); + Vec_StrFree( vStr ); +} + +Vec_Int_t * Div_CubePairs( Vec_Wec_t * p, int nVars, int nDivs ) +{ + int fVerbose = 0; + char * pNames[5] = {"const1", "and", "xor", "mux", "none"}; + Vec_Int_t * vCube1, * vCube2, * vDivs; + int i1, i2, i, k, pLitsA[2], pLitsB[2], pLits[4], Type, Phase, nBase, Count = 0; + Vec_Str_t * vStr = Vec_StrStart( nVars + 1 ); + Tab_Tab_t * pTab = Tab_TabAlloc( 5 ); + Vec_WecForEachLevel( p, vCube1, i ) + { + // add lit pairs + pLits[2] = TAB_UNUSED; + Vec_IntForEachEntry( vCube1, pLits[0], i1 ) + Vec_IntForEachEntryStart( vCube1, pLits[1], i2, i1+1 ) + { + Tab_TabHashAdd( pTab, pLits, DIV_AND, 1 ); + } + + Vec_WecForEachLevelStart( p, vCube2, k, i+1 ) + { + nBase = Div_FindDiv( vCube1, vCube2, pLitsA, pLitsB ); + if ( nBase == -1 ) + continue; + Type = Div_FindType(pLitsA, pLitsB, pLits, &Phase); + if ( Type >= DIV_AND && Type <= DIV_MUX ) + Tab_TabHashAdd( pTab, pLits, Type, nBase ); + + if ( fVerbose ) + { + printf( "Pair %d:\n", Count++ ); + Div_CubePrintOne( vCube1, vStr, nVars ); + Div_CubePrintOne( vCube2, vStr, nVars ); + printf( "Result = %d ", nBase ); + assert( nBase > 0 ); + + printf( "Type = %s ", pNames[Type] ); + printf( "LitA = %d ", pLits[0] ); + printf( "LitB = %d ", pLits[1] ); + printf( "LitC = %d ", pLits[2] ); + printf( "Phase = %d ", Phase ); + printf( "\n" ); + } + } + } + // print the table + printf( "Divisors = %d.\n", pTab->nBins ); + vDivs = Tab_TabFindBest( pTab, nDivs ); + // cleanup + Vec_StrFree( vStr ); + Tab_TabFree( pTab ); + return vDivs; +} + +/**Function************************************************************* + + Synopsis [Solve the enumeration problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_FxSolve( sat_solver * pSat, int iOut, int iAuxVar, Vec_Int_t * vVars, int fDumpPla, int fVerbose, int * pCounter, Vec_Wec_t * vCubes ) +{ + int nBTLimit = 1000000; + Vec_Int_t * vLevel = NULL; + Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vVars) ); + Vec_Int_t * vLits2 = Vec_IntAlloc( Vec_IntSize(vVars) ); + Vec_Str_t * vCube = Vec_StrStart( Vec_IntSize(vVars)+1 ); + int status, i, k, n, Lit, Lit2, iVar, nFinal, * pFinal, pLits[2], nIter = 0, RetValue = 0; + int Before, After, Total = 0, nLits = 0; + pLits[0] = Abc_Var2Lit( iOut + 1, 0 ); // F = 1 + pLits[1] = Abc_Var2Lit( iAuxVar, 0 ); // iNewLit + if ( vCubes ) + Vec_WecClear( vCubes ); + if ( fDumpPla ) + printf( ".i %d\n", Vec_IntSize(vVars) ); + if ( fDumpPla ) + printf( ".o %d\n", 1 ); + while ( 1 ) + { + // find onset minterm + status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + { RetValue = -1; break; } + if ( status == l_False ) + { RetValue = 1; break; } + assert( status == l_True ); + // collect divisor literals + Vec_IntClear( vLits ); + Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0 + Vec_IntForEachEntryReverse( vVars, iVar, i ) +// Vec_IntForEachEntry( vVars, iVar, i ) + Vec_IntPush( vLits, sat_solver_var_literal(pSat, iVar) ); + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + { RetValue = -1; break; } + if ( status == l_True ) + break; + assert( status == l_False ); + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + Before = nFinal; + //printf( "Before %d. ", nFinal ); + +/* + // save these literals + Vec_IntClear( vLits ); + for ( i = 0; i < nFinal; i++ ) + Vec_IntPush( vLits, Abc_LitNot(pFinal[i]) ); + Vec_IntReverseOrder( vLits ); + + // make one final run + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + assert( status == l_False ); + nFinal = sat_solver_final( pSat, &pFinal ); +*/ + + // save these literals + Vec_IntClear( vLits2 ); + for ( i = 0; i < nFinal; i++ ) + Vec_IntPush( vLits2, Abc_LitNot(pFinal[i]) ); + Vec_IntSort( vLits2, 1 ); + + // try removing literals from the cube + Vec_IntForEachEntry( vLits2, Lit2, k ) + { + if ( Lit2 == Abc_LitNot(pLits[0]) ) + continue; + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vLits2, Lit, n ) + if ( Lit != -1 && Lit != Lit2 ) + Vec_IntPush( vLits, Lit ); + // call sat + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + assert( 0 ); + if ( status == l_True ) // SAT + continue; + // Lit2 can be removed + Vec_IntWriteEntry( vLits2, k, -1 ); + } + + // make one final run + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vLits2, Lit2, k ) + if ( Lit2 != -1 ) + Vec_IntPush( vLits, Lit2 ); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + assert( status == l_False ); + + // put them back + nFinal = 0; + Vec_IntForEachEntry( vLits2, Lit2, k ) + if ( Lit2 != -1 ) + pFinal[nFinal++] = Abc_LitNot(Lit2); + + + //printf( "After %d. \n", nFinal ); + After = nFinal; + Total += Before - After; + + // get subset of literals + //nFinal = sat_solver_final( pSat, &pFinal ); + // compute cube and add clause + Vec_IntClear( vLits ); + Vec_IntPush( vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit) + if ( fDumpPla ) + Vec_StrFill( vCube, Vec_IntSize(vVars), '-' ); + if ( vCubes ) + vLevel = Vec_WecPushLevel( vCubes ); + for ( i = 0; i < nFinal; i++ ) + { + if ( pFinal[i] == pLits[0] ) + continue; + Vec_IntPush( vLits, pFinal[i] ); + iVar = Vec_IntFind( vVars, Abc_Lit2Var(pFinal[i]) ); + assert( iVar >= 0 && iVar < Vec_IntSize(vVars) ); + //printf( "%s%d ", Abc_LitIsCompl(pFinal[i]) ? "+":"-", iVar ); + if ( fDumpPla ) + Vec_StrWriteEntry( vCube, iVar, (char)(Abc_LitIsCompl(pFinal[i]) ? '0' : '1') ); + if ( vLevel ) + Vec_IntPush( vLevel, Abc_Var2Lit(iVar, Abc_LitIsCompl(pFinal[i])) ); + } + if ( vCubes ) + Vec_IntSort( vLevel, 0 ); + if ( fDumpPla ) + printf( "%s 1\n", Vec_StrArray(vCube) ); + status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + assert( status ); + nLits += Vec_IntSize(vLevel); + nIter++; + } + if ( fDumpPla ) + printf( ".e\n" ); + if ( fDumpPla ) + printf( ".p %d\n\n", nIter ); + if ( fVerbose ) + printf( "Cubes = %d. Reduced = %d. Lits = %d\n", nIter, Total, nLits ); + if ( pCounter ) + *pCounter = nIter; +// assert( status == l_True ); + Vec_IntFree( vLits ); + Vec_IntFree( vLits2 ); + Vec_StrFree( vCube ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_FxCompute( Gia_Man_t * p ) +{ + // create dual-output circuit with on-set/off-set + extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p ); + Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p ); + // create SAT solver + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p2, 8, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + // compute parameters + int nOuts = Gia_ManCoNum(p); + int nCiVars = Gia_ManCiNum(p), iCiVarBeg = pCnf->nVars - nCiVars;// - 1; + int o, i, n, RetValue, nCounter, iAuxVarStart = sat_solver_nvars( pSat ); + int nCubes[2][2] = {0}; + // create variables + Vec_Int_t * vVars = Vec_IntAlloc( nCiVars ); + for ( n = 0; n < nCiVars; n++ ) + Vec_IntPush( vVars, iCiVarBeg + n ); + sat_solver_setnvars( pSat, iAuxVarStart + 4*nOuts ); + // iterate through outputs + for ( o = 0; o < nOuts; o++ ) + for ( i = 0; i < 2; i++ ) + for ( n = 0; n < 2; n++ ) // 0=onset, 1=offset +// for ( n = 1; n >= 0; n-- ) // 0=onset, 1=offset + { + printf( "Out %3d %sset ", o, n ? "off" : " on" ); + RetValue = Bmc_FxSolve( pSat, Abc_Var2Lit(o, n), iAuxVarStart + 2*i*nOuts + Abc_Var2Lit(o, n), vVars, 0, 0, &nCounter, NULL ); + if ( RetValue == 0 ) + printf( "Mismatch\n" ); + if ( RetValue == -1 ) + printf( "Timeout\n" ); + nCubes[i][n] += nCounter; + } + // cleanup + Vec_IntFree( vVars ); + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Gia_ManStop( p2 ); + printf( "Onset = %5d. Offset = %5d. Onset = %5d. Offset = %5d.\n", nCubes[0][0], nCubes[0][1], nCubes[1][0], nCubes[1][1] ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_FxAddClauses( sat_solver * pSat, Vec_Int_t * vDivs, int iCiVarBeg, int iVarStart ) +{ + int i, Func, pLits[3], nDivs = Vec_IntSize(vDivs)/4; + assert( Vec_IntSize(vDivs) % 4 == 0 ); + // create new var for each divisor + for ( i = 0; i < nDivs; i++ ) + { + Func = Vec_IntEntry(vDivs, 4*i+0); + pLits[0] = Vec_IntEntry(vDivs, 4*i+1); + pLits[1] = Vec_IntEntry(vDivs, 4*i+2); + pLits[2] = Vec_IntEntry(vDivs, 4*i+3); + //printf( "Adding clause with vars %d %d -> %d\n", iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iVarStart + nDivs - 1 - i ); + if ( Func == DIV_AND ) + sat_solver_add_and( pSat, + iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), + Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), 0 ); + else if ( Func == DIV_XOR ) + sat_solver_add_xor( pSat, + iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), 0 ); + else if ( Func == DIV_MUX ) + sat_solver_add_mux( pSat, + iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iCiVarBeg + Abc_Lit2Var(pLits[2]), + Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), Abc_LitIsCompl(pLits[2]), 0 ); + else assert( 0 ); + } +} +int Bmc_FxComputeOne( Gia_Man_t * p ) +{ + int Extra = 1000; + int nIterMax = 5; + int nDiv2Add = 16; + // create SAT solver + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + // compute parameters + int nCiVars = Gia_ManCiNum(p); // PI count + int iCiVarBeg = pCnf->nVars - nCiVars;//- 1; // first PI var + int iCiVarCur = iCiVarBeg + nCiVars; // current unused PI var + int n, Iter, RetValue; + // create variables + int iAuxVarStart = sat_solver_nvars(pSat) + Extra; // the aux var + sat_solver_setnvars( pSat, iAuxVarStart + 1 + nIterMax ); + for ( Iter = 0; Iter < nIterMax; Iter++ ) + { + Vec_Wec_t * vCubes = Vec_WecAlloc( 1000 ); + // collect variables + Vec_Int_t * vVar2Sat = Vec_IntAlloc( iCiVarCur-iCiVarBeg ), * vDivs; +// for ( n = iCiVarCur - 1; n >= iCiVarBeg; n-- ) + for ( n = iCiVarBeg; n < iCiVarCur; n++ ) + Vec_IntPush( vVar2Sat, n ); + // iterate through outputs + printf( "\nIteration %d (Aux = %d)\n", Iter, iAuxVarStart + Iter ); + RetValue = Bmc_FxSolve( pSat, 0, iAuxVarStart + Iter, vVar2Sat, 1, 1, NULL, vCubes ); + if ( RetValue == 0 ) + printf( "Mismatch\n" ); + if ( RetValue == -1 ) + printf( "Timeout\n" ); + // print cubes + //Div_CubePrint( vCubes, nCiVars ); + vDivs = Div_CubePairs( vCubes, nCiVars, nDiv2Add ); + Vec_WecFree( vCubes ); + // add clauses and update variables + Bmc_FxAddClauses( pSat, vDivs, iCiVarBeg, iCiVarCur ); + iCiVarCur += Vec_IntSize(vDivs)/4; + Vec_IntFree( vDivs ); + // cleanup + assert( Vec_IntSize(vVar2Sat) <= nCiVars + Extra ); + Vec_IntFree( vVar2Sat ); + } + // cleanup + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index c82879de..ebc555d9 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -374,53 +374,53 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i assert( Cid ); return 4; } -static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, int iVarE, int iVarZ ) +static inline int sat_solver_add_mux( sat_solver * pSat, int iVarZ, int iVarC, int iVarT, int iVarE, int iComplC, int iComplT, int iComplE, int iComplZ ) { lit Lits[3]; int Cid; assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 ); - Lits[0] = toLitCond( iVarC, 1 ); - Lits[1] = toLitCond( iVarT, 1 ); + Lits[0] = toLitCond( iVarC, 1 ^ iComplC ); + Lits[1] = toLitCond( iVarT, 1 ^ iComplT ); Lits[2] = toLitCond( iVarZ, 0 ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarC, 1 ); - Lits[1] = toLitCond( iVarT, 0 ); - Lits[2] = toLitCond( iVarZ, 1 ); + Lits[0] = toLitCond( iVarC, 1 ^ iComplC ); + Lits[1] = toLitCond( iVarT, 0 ^ iComplT ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarC, 0 ); - Lits[1] = toLitCond( iVarE, 1 ); - Lits[2] = toLitCond( iVarZ, 0 ); + Lits[0] = toLitCond( iVarC, 0 ^ iComplC ); + Lits[1] = toLitCond( iVarE, 1 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarC, 0 ); - Lits[1] = toLitCond( iVarE, 0 ); - Lits[2] = toLitCond( iVarZ, 1 ); + Lits[0] = toLitCond( iVarC, 0 ^ iComplC ); + Lits[1] = toLitCond( iVarE, 0 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); if ( iVarT == iVarE ) return 4; - Lits[0] = toLitCond( iVarT, 0 ); - Lits[1] = toLitCond( iVarE, 0 ); - Lits[2] = toLitCond( iVarZ, 1 ); + Lits[0] = toLitCond( iVarT, 0 ^ iComplT ); + Lits[1] = toLitCond( iVarE, 0 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); - Lits[0] = toLitCond( iVarT, 1 ); - Lits[1] = toLitCond( iVarE, 1 ); - Lits[2] = toLitCond( iVarZ, 0 ); + Lits[0] = toLitCond( iVarT, 1 ^ iComplT ); + Lits[1] = toLitCond( iVarE, 1 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ ); Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); assert( Cid ); return 6; } -static inline int sat_solver_add_mux41( sat_solver * pSat, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3, int iVarZ ) +static inline int sat_solver_add_mux41( sat_solver * pSat, int iVarZ, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3 ) { lit Lits[4]; int Cid; -- cgit v1.2.3