From 390a145f0a293ae37d969d2d8ce5086a31d78ab5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 13 Feb 2016 15:15:01 -0800 Subject: Adding support for a different bit-blasting of a multiplier and squarer. --- src/aig/gia/giaSatLut.c | 570 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 570 insertions(+) create mode 100644 src/aig/gia/giaSatLut.c (limited to 'src/aig/gia/giaSatLut.c') diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c new file mode 100644 index 00000000..7f18a485 --- /dev/null +++ b/src/aig/gia/giaSatLut.c @@ -0,0 +1,570 @@ +/**CFile**************************************************************** + + FileName [giaSatLut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSatLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "sat/bsat/satStore.h" +#include "misc/vec/vecWec.h" +#include "misc/util/utilNam.h" +#include "map/scl/sclCon.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Sbl_Man_t_ Sbl_Man_t; +struct Sbl_Man_t_ +{ + sat_solver * pSat; // SAT solver + Vec_Int_t * vCardVars; // candinality variables + int LogN; // max vars + int FirstVar; // first variable to be used + int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2) + int nInputs; // the number of inputs + // mapping + Vec_Wec_t * vMapping; // current mapping + // window + Gia_Man_t * pGia; + Vec_Int_t * vLeaves; // leaf nodes + Vec_Int_t * vNodes; // internal nodes + Vec_Int_t * vRoots; // driver nodes (a subset of vNodes) + Vec_Int_t * vRootVars; // driver nodes (as SAT variables) + // cuts + Vec_Wrd_t * vCutsI; // input bit patterns + Vec_Wrd_t * vCutsN; // node bit patterns + Vec_Int_t * vCutsNum; // cut counts for each obj + Vec_Int_t * vCutsStart; // starting cuts for each obj + Vec_Int_t * vCutsObj; // object to which this cut belongs + Vec_Wrd_t * vTempI; // temporary cuts + Vec_Wrd_t * vTempN; // temporary cuts + Vec_Int_t * vSolCuts; // cuts belonging to solution + Vec_Int_t * vSolCuts2; // cuts belonging to solution + // temporary + Vec_Int_t * vLits; // literals + Vec_Int_t * vAssump; // literals + Vec_Int_t * vPolar; // variables polarity +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Sbl_ManToMapping( Gia_Man_t * p ) +{ + Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) ); + int Obj, Fanin, k; + Gia_ManForEachLut( p, Obj ) + Gia_LutForEachFanin( p, Obj, Fanin, k ) + Vec_WecPush( vMapping, Obj, Fanin ); + return vMapping; +} +Vec_Int_t * Sbl_ManFromMapping( Gia_Man_t * p, Vec_Wec_t * vMap ) +{ + Vec_Int_t * vMapping, * vVec; int i, k, Obj; + vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) ); + Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 ); + Vec_WecForEachLevel( vMap, vVec, i ) + if ( Vec_IntSize(vVec) > 0 ) + { + Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) ); + Vec_IntPush( vMapping, Vec_IntSize(vVec) ); + Vec_IntForEachEntry( vVec, Obj, k ) + Vec_IntPush( vMapping, Obj ); + Vec_IntPush( vMapping, i ); + } + assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) ); + return vMapping; +} +void Sbl_ManUpdateMapping( Sbl_Man_t * p ) +{ + Vec_Int_t * vObj; + int i, c, b, iObj; + word CutI, CutN; + assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) ); + Vec_IntForEachEntry( p->vNodes, iObj, i ) + Vec_IntClear( Vec_WecEntry(p->vMapping, iObj) ); + Vec_IntForEachEntry( p->vSolCuts2, c, i ) + { + CutI = Vec_WrdEntry( p->vCutsI, c ); + CutN = Vec_WrdEntry( p->vCutsN, c ); + iObj = Vec_IntEntry( p->vCutsObj, c ); + iObj = Vec_IntEntry( p->vNodes, iObj ); + vObj = Vec_WecEntry( p->vMapping, iObj ); + assert( Vec_IntSize(vObj) == 0 ); + for ( b = 0; b < 64; b++ ) + if ( (CutI >> b) & 1 ) + Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) ); + for ( b = 0; b < 64; b++ ) + if ( (CutN >> b) & 1 ) + Vec_IntPush( vObj, Vec_IntEntry(p->vNodes, b) ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs ) +{ + int b, Count = 0; + printf( "{ " ); + for ( b = 0; b < 64; b++ ) + if ( (CutI >> b) & 1 ) + printf( "i%d ", b + 1 ), Count++; + printf( " " ); + for ( b = 0; b < 64; b++ ) + if ( (CutN >> b) & 1 ) + printf( "n%d ", nInputs + b + 1 ), Count++; + printf( "};\n" ); + return Count; +} +static int Sbl_ManFindAndPrintCut( Sbl_Man_t * p, int c ) +{ + return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c), Vec_IntSize(p->vLeaves) ); +} +static inline int Sbl_CutIsFeasible( word CutI, word CutN ) +{ + int Count = (CutI != 0) + (CutN != 0); + CutI = CutI & (CutI-1); CutN = CutN & (CutN-1); Count += (CutI != 0) + (CutN != 0); + CutI = CutI & (CutI-1); CutN = CutN & (CutN-1); Count += (CutI != 0) + (CutN != 0); + CutI = CutI & (CutI-1); CutN = CutN & (CutN-1); Count += (CutI != 0) + (CutN != 0); + CutI = CutI & (CutI-1); CutN = CutN & (CutN-1); Count += (CutI != 0) + (CutN != 0); + return Count <= 4; +} +static inline int Sbl_CutPushUncontained( Vec_Wrd_t * vCutsI, Vec_Wrd_t * vCutsN, word CutI, word CutN ) +{ + int i, k = 0; + assert( vCutsI->nSize == vCutsN->nSize ); + for ( i = 0; i < vCutsI->nSize; i++ ) + if ( (vCutsI->pArray[i] & CutI) == vCutsI->pArray[i] && (vCutsN->pArray[i] & CutN) == vCutsN->pArray[i] ) + return 1; + for ( i = 0; i < vCutsI->nSize; i++ ) + if ( (vCutsI->pArray[i] & CutI) != CutI || (vCutsN->pArray[i] & CutN) != CutN ) + { + Vec_WrdWriteEntry( vCutsI, k, vCutsI->pArray[i] ); + Vec_WrdWriteEntry( vCutsN, k, vCutsN->pArray[i] ); + k++; + } + Vec_WrdShrink( vCutsI, k ); + Vec_WrdShrink( vCutsN, k ); + Vec_WrdPush( vCutsI, CutI ); + Vec_WrdPush( vCutsN, CutN ); + return 0; +} +static inline void Sbl_ManComputeCutsOne( Sbl_Man_t * p, int Fan0, int Fan1, int Obj ) +{ + word * pCutsI = Vec_WrdArray(p->vCutsI); + word * pCutsN = Vec_WrdArray(p->vCutsN); + int Start0 = Vec_IntEntry( p->vCutsStart, Fan0 ); + int Start1 = Vec_IntEntry( p->vCutsStart, Fan1 ); + int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Fan0 ); + int Limit1 = Start1 + Vec_IntEntry( p->vCutsNum, Fan1 ); + int i, k; + Vec_WrdClear( p->vTempI ); + Vec_WrdClear( p->vTempN ); + for ( i = Start0; i < Limit0; i++ ) + for ( k = Start1; k < Limit1; k++ ) + if ( Sbl_CutIsFeasible(pCutsI[i] | pCutsI[k], pCutsN[i] | pCutsN[k]) ) + Sbl_CutPushUncontained( p->vTempI, p->vTempN, pCutsI[i] | pCutsI[k], pCutsN[i] | pCutsN[k] ); + Vec_IntPush( p->vCutsStart, Vec_WrdSize(p->vCutsI) ); + Vec_IntPush( p->vCutsNum, Vec_WrdSize(p->vTempI) + 1 ); + Vec_WrdAppend( p->vCutsI, p->vTempI ); + Vec_WrdAppend( p->vCutsN, p->vTempN ); + Vec_WrdPush( p->vCutsI, 0 ); + Vec_WrdPush( p->vCutsN, (((word)1) << Obj) ); + for ( i = 0; i <= Vec_WrdSize(p->vTempI); i++ ) + Vec_IntPush( p->vCutsObj, Obj ); +} +static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN ) +{ + word * pCutsI = Vec_WrdArray(p->vCutsI); + word * pCutsN = Vec_WrdArray(p->vCutsN); + int Start0 = Vec_IntEntry( p->vCutsStart, Obj ); + int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj ); + int i; +// printf( "Looking for:\n" ); +// Sbl_ManPrintCut( CutI, CutN, p->nInputs ); +// printf( "\n" ); + for ( i = Start0; i < Limit0; i++ ) + { +// Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs ); + if ( pCutsI[i] == CutI && pCutsN[i] == CutN ) + return i; + } + return -1; +} +int Sbl_ManComputeCuts( Sbl_Man_t * p ) +{ + Gia_Obj_t * pObj, * pFanin; + int i, k, Index, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes); + assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vNodes) <= 64 ); + // assign leaf cuts + Vec_IntClear( p->vCutsStart ); + Vec_IntClear( p->vCutsObj ); + Vec_IntClear( p->vCutsNum ); + Vec_WrdClear( p->vCutsI ); + Vec_WrdClear( p->vCutsN ); + Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i ) + { + Vec_IntPush( p->vCutsStart, Vec_WrdSize(p->vCutsI) ); + Vec_IntPush( p->vCutsObj, -1 ); + Vec_IntPush( p->vCutsNum, 1 ); + Vec_WrdPush( p->vCutsI, (((word)1) << i) ); + Vec_WrdPush( p->vCutsN, 0 ); + pObj->Value = i; + } + // assign internal cuts + Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) + { + assert( Gia_ObjIsAnd(pObj) ); + assert( ~Gia_ObjFanin0(pObj)->Value ); + assert( ~Gia_ObjFanin1(pObj)->Value ); + Sbl_ManComputeCutsOne( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value, i ); + pObj->Value = Vec_IntSize(p->vLeaves) + i; + } + assert( Vec_IntSize(p->vCutsStart) == nObjs ); + assert( Vec_IntSize(p->vCutsNum) == nObjs ); + assert( Vec_WrdSize(p->vCutsI) == Vec_WrdSize(p->vCutsN) ); + assert( Vec_WrdSize(p->vCutsI) == Vec_IntSize(p->vCutsObj) ); + // check that roots are mapped nodes + Vec_IntClear( p->vRootVars ); + Gia_ManForEachObjVec( p->vRoots, p->pGia, pObj, i ) + { + int Obj = Gia_ObjId(p->pGia, pObj); + if ( Gia_ObjIsCi(pObj) ) + continue; + assert( Gia_ObjIsLut(p->pGia, Obj) ); + assert( ~pObj->Value ); + Vec_IntPush( p->vRootVars, pObj->Value - Vec_IntSize(p->vLeaves) ); + } + // create current solution + Vec_IntClear( p->vPolar ); + Vec_IntClear( p->vSolCuts ); + Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) + { + word CutI = 0, CutN = 0; + int Obj = Gia_ObjId(p->pGia, pObj); + if ( !Gia_ObjIsLut(p->pGia, Obj) ) + continue; + assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i ); + // add node + Vec_IntPush( p->vPolar, i ); + Vec_IntPush( p->vSolCuts, i ); + // add its cut + Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k ) + { + assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut(p->pGia, Gia_ObjId(p->pGia, pFanin)) ); + assert( ~pFanin->Value ); + if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) ) + CutI |= ((word)1 << pFanin->Value); + else + CutN |= ((word)1 << (pFanin->Value - Vec_IntSize(p->vLeaves))); + } + // find the new cut + Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI, CutN ); + assert( Index >= 0 ); + Vec_IntPush( p->vPolar, p->FirstVar+Index ); + } + // clean value + Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i ) + pObj->Value = ~0; + Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) + pObj->Value = ~0; + return Vec_WrdSize(p->vCutsI); +} +int Sbl_ManCreateCnf( Sbl_Man_t * p ) +{ + int i, k, c, pLits[2], value; + word * pCutsN = Vec_WrdArray(p->vCutsN); + assert( p->FirstVar == sat_solver_nvars(p->pSat) ); + sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WrdSize(p->vCutsI) ); + //printf( "\n" ); + for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) + { + int Start0 = Vec_IntEntry( p->vCutsStart, Vec_IntSize(p->vLeaves) + i ); + int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Vec_IntSize(p->vLeaves) + i ) - 1; + // add main clause + Vec_IntClear( p->vLits ); + Vec_IntPush( p->vLits, Abc_Var2Lit(i, 1) ); + //printf( "Node %d implies cuts: ", i ); + for ( k = Start0; k < Limit0; k++ ) + { + Vec_IntPush( p->vLits, Abc_Var2Lit(p->FirstVar+k, 0) ); + //printf( "%d ", p->FirstVar+k ); + } + //printf( "\n" ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + // binary clauses + for ( k = Start0; k < Limit0; k++ ) + { + word Cut = pCutsN[k]; + //printf( "Cut %d implies root node %d.\n", p->FirstVar+k, i ); + // root clause + pLits[0] = Abc_Var2Lit( p->FirstVar+k, 1 ); + pLits[1] = Abc_Var2Lit( i, 0 ); + value = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( value ); + // fanin clauses + for ( c = 0; c < 64 && Cut; c++, Cut >>= 1 ) + { + if ( (Cut & 1) == 0 ) + continue; + //printf( "Cut %d implies fanin %d.\n", p->FirstVar+k, c ); + pLits[1] = Abc_Var2Lit( c, 0 ); + value = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( value ); + } + } + } + sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolar), Vec_IntSize(p->vPolar) ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN ) +{ + Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 ); + extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars ); + p->pSat = Sbm_AddCardinSolver( LogN, &p->vCardVars ); + p->LogN = LogN; + p->FirstVar = sat_solver_nvars( p->pSat ); + // window + p->pGia = pGia; + p->vLeaves = Vec_IntAlloc( 64 ); + p->vNodes = Vec_IntAlloc( 64 ); + p->vRoots = Vec_IntAlloc( 64 ); + p->vRootVars = Vec_IntAlloc( 64 ); + // cuts + p->vCutsI = Vec_WrdAlloc( 1000 ); // input bit patterns + p->vCutsN = Vec_WrdAlloc( 1000 ); // node bit patterns + p->vCutsNum = Vec_IntAlloc( 64 ); // cut counts for each obj + p->vCutsStart = Vec_IntAlloc( 64 ); // starting cuts for each obj + p->vCutsObj = Vec_IntAlloc( 1000 ); + p->vSolCuts = Vec_IntAlloc( 64 ); + p->vSolCuts2 = Vec_IntAlloc( 64 ); + p->vTempI = Vec_WrdAlloc( 32 ); + p->vTempN = Vec_WrdAlloc( 32 ); + // internal + p->vLits = Vec_IntAlloc( 64 ); + p->vAssump = Vec_IntAlloc( 64 ); + p->vPolar = Vec_IntAlloc( 1000 ); + // other + Gia_ManFillValue( pGia ); + p->vMapping = Sbl_ManToMapping( pGia ); + return p; +} + +void Sbl_ManStop( Sbl_Man_t * p ) +{ + sat_solver_delete( p->pSat ); + Vec_IntFree( p->vCardVars ); + Vec_WecFree( p->vMapping ); + // internal + Vec_IntFree( p->vLeaves ); + Vec_IntFree( p->vNodes ); + Vec_IntFree( p->vRoots ); + Vec_IntFree( p->vRootVars ); + // cuts + Vec_WrdFree( p->vCutsI ); + Vec_WrdFree( p->vCutsN ); + Vec_IntFree( p->vCutsNum ); + Vec_IntFree( p->vCutsStart ); + Vec_IntFree( p->vCutsObj ); + Vec_IntFree( p->vSolCuts ); + Vec_IntFree( p->vSolCuts2 ); + Vec_WrdFree( p->vTempI ); + Vec_WrdFree( p->vTempN ); + // temporary + Vec_IntFree( p->vLits ); + Vec_IntFree( p->vAssump ); + Vec_IntFree( p->vPolar ); + // other + ABC_FREE( p ); +} + +void Sbl_ManWindow( Sbl_Man_t * p ) +{ + int i, ObjId; + // collect leaves + Vec_IntClear( p->vLeaves ); + Gia_ManForEachCiId( p->pGia, ObjId, i ) + Vec_IntPush( p->vLeaves, ObjId ); + // collect internal + Vec_IntClear( p->vNodes ); + Gia_ManForEachAndId( p->pGia, ObjId ) + Vec_IntPush( p->vNodes, ObjId ); + // collect roots + Vec_IntClear( p->vRoots ); + Gia_ManForEachCoDriverId( p->pGia, ObjId, i ) + Vec_IntPush( p->vRoots, ObjId ); +} + +int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) +{ + abctime clk = Abc_Clock(), clk2; + int i, LogN = 6, nVars = 1 << LogN, status, Root; + Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN ); + int fKeepTrying = 1; + int StartSol; + + // derive window + Sbl_ManWindow( p ); + // derive cuts + Sbl_ManComputeCuts( p ); + // derive SAT instance + Sbl_ManCreateCnf( p ); + + if ( fVerbose ) + Vec_IntPrint( p->vSolCuts ); + + if ( fVerbose ) + printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n", + sat_solver_nclauses(p->pSat), Vec_IntSize(p->vNodes), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vNodes), + sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) ); + + // create assumptions + // cardinality + Vec_IntClear( p->vAssump ); + Vec_IntPush( p->vAssump, -1 ); + // unused variables + for ( i = Vec_IntSize(p->vNodes); i < nVars; i++ ) + Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) ); + // root variables + Vec_IntForEachEntry( p->vRootVars, Root, i ) + Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) ); +// Vec_IntPrint( p->vAssump ); + + StartSol = Vec_IntSize(p->vSolCuts) + 1; +// StartSol = 30; + while ( fKeepTrying && StartSol-fKeepTrying > 0 ) + { + if ( fVerbose ) + printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying ); + // for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ ) + // Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) ); + Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) ); + // solve the problem + clk2 = Abc_Clock(); + status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 ); + if ( status == l_True ) + { + int Count = 0, LitCount = 0; + if ( fVerbose ) + { + printf( "Inputs = %d. ANDs = %d. Total = %d. All vars = %d.\n", + Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), + Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vNodes), nVars ); + for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) + printf( "%d", sat_solver_var_value(p->pSat, i) ); + printf( "\n" ); + for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) + if ( sat_solver_var_value(p->pSat, i) ) + { + printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) ); + Count++; + } + printf( "Count = %d\n", Count ); + } +// for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) +// printf( "%d", sat_solver_var_value(p->pSat, i) ); +// printf( "\n" ); + Count = 1; + Vec_IntClear( p->vSolCuts2 ); + for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) + if ( sat_solver_var_value(p->pSat, i) ) + { + if ( fVerbose ) + printf( "Cut %3d : ", Count++ ); + if ( fVerbose ) + LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar ); + Vec_IntPush( p->vSolCuts2, i-p->FirstVar ); + } + if ( fVerbose ) + printf( "LitCount = %d.\n", LitCount ); + } + fKeepTrying = status == l_True ? fKeepTrying + 1 : 0; + if ( fVerbose ) + { + if ( status == l_False ) + printf( "UNSAT " ); + else if ( status == l_True ) + printf( "SAT " ); + else + printf( "UNDEC " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + printf( "\n" ); + } + } + + // update solution + Sbl_ManUpdateMapping( p ); + + Vec_IntFreeP( &pGia->vMapping ); + pGia->vMapping = Sbl_ManFromMapping( pGia, p->vMapping ); + + Sbl_ManStop( p ); + return 1; +} + +void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fVerbose ) +{ + Sbl_ManTestSat( p, fVerbose ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3