From 716969190a4d6d944cfa24a085c9e7069d868dab Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 6 Nov 2017 16:43:32 -0800 Subject: Profiling quantification and other changes. --- abclib.dsp | 4 + src/aig/gia/gia.h | 11 +++ src/aig/gia/giaDup.c | 2 +- src/aig/gia/giaSim.c | 148 ++++++++++++++++++++++++++++++++++ src/aig/gia/giaUtil.c | 52 ++++++++++++ src/base/acb/acbSets.h | 61 ++++++++++++++ src/sat/glucose/AbcGlucose.cpp | 178 +++++++++++++++++++++++++++++++++++------ src/sat/glucose/AbcGlucose.h | 3 +- 8 files changed, 432 insertions(+), 27 deletions(-) create mode 100644 src/base/acb/acbSets.h diff --git a/abclib.dsp b/abclib.dsp index e9a9ea46..f93aff82 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -1091,6 +1091,10 @@ SOURCE=.\src\base\acb\acbSets.c # End Source File # Begin Source File +SOURCE=.\src\base\acb\acbSets.h +# End Source File +# Begin Source File + SOURCE=.\src\base\acb\acbUtil.c # End Source File # End Group diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 9acbbe48..920ebb06 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -198,6 +198,7 @@ struct Gia_Man_t_ int MappedArea; // area after mapping int MappedDelay; // delay after mapping // bit-parallel simulation + int fBuiltInSim; int iPatsPi; int nSimWords; Vec_Wrd_t * vSims; @@ -673,6 +674,11 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) if ( pFan1->fMark0 ) pFan1->fMark1 = 1; else pFan1->fMark0 = 1; pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj)); } + if ( p->fBuiltInSim ) + { + extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj ); + Gia_ManBuiltInSimPerform( p, Gia_ObjId( p, pObj ) ); + } return Gia_ObjId( p, pObj ) << 1; } static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 ) @@ -1469,6 +1475,10 @@ extern unsigned * Gia_SimDataCoExt( Gia_ManSim_t * p, int i ); extern void Gia_ManSimInfoInit( Gia_ManSim_t * p ); extern void Gia_ManSimInfoTransfer( Gia_ManSim_t * p ); extern void Gia_ManSimulateRound( Gia_ManSim_t * p ); +extern void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs ); +extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj ); +extern int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 ); +extern int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs ); /*=== giaSpeedup.c ============================================================*/ extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); @@ -1612,6 +1622,7 @@ extern void Gia_ManSwapPos( Gia_Man_t * p, int i ); extern Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p ); extern void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues ); extern Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p ); +extern int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 1d4f7a22..977ef42c 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1909,7 +1909,7 @@ Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds ) Gia_Man_t * pNew; int i, iLit0; Gia_Obj_t * pObj, * pRoot = Gia_ManObj( p, Abc_Lit2Var(iLit) ); Vec_Int_t * vObjs = Vec_IntAlloc( 1000 ); - assert( Gia_ObjIsAnd(pRoot) ); + //assert( Gia_ObjIsAnd(pRoot) ); if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) ) Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 90224062..aba7f712 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -748,6 +748,154 @@ void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut ) Vec_IntFree( vPatOut ); } + +/**Function************************************************************* + + Synopsis [Bit-parallel simulation during AIG construction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline word * Gia_ManBuiltInData( Gia_Man_t * p, int iObj ) +{ + return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj ); +} +void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs ) +{ + int i, k; + assert( !p->fBuiltInSim ); + assert( Gia_ManAndNum(p) == 0 ); + p->fBuiltInSim = 1; + p->nSimWords = nWords; + p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs ); + Vec_WrdFill( p->vSims, p->nSimWords, 0 ); + Gia_ManRandomW( 1 ); + for ( i = 0; i < Gia_ManCiNum(p); i++ ) + for ( k = 0; k < p->nSimWords; k++ ) + Vec_WrdPush( p->vSims, Gia_ManRandomW(0) ); +} +void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) ); + word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); int w; + assert( p->fBuiltInSim ); + if ( Gia_ObjFaninC0(pObj) ) + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, ~(pInfo0[w] | pInfo1[w]) ); + else + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, ~pInfo0[w] & pInfo1[w] ); + } + else + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, pInfo0[w] & ~pInfo1[w] ); + else + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, pInfo0[w] & pInfo1[w] ); + } + assert( Vec_WrdSize(p->vSims) == Gia_ManObjNum(p) * p->nSimWords ); +} +int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) ); + word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w; + assert( p->fBuiltInSim ); + +// printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) ); +// Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" ); +// Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" ); +// printf( "\n" ); + + if ( Abc_LitIsCompl(iLit0) ) + { + if ( Abc_LitIsCompl(iLit1) ) + for ( w = 0; w < p->nSimWords; w++ ) + if ( ~pInfo0[w] & ~pInfo1[w] ) + return 1; + else + for ( w = 0; w < p->nSimWords; w++ ) + if ( ~pInfo0[w] & pInfo1[w] ) + return 1; + } + else + { + if ( Abc_LitIsCompl(iLit1) ) + for ( w = 0; w < p->nSimWords; w++ ) + if ( pInfo0[w] & ~pInfo1[w] ) + return 1; + else + for ( w = 0; w < p->nSimWords; w++ ) + if ( pInfo0[w] & pInfo1[w] ) + return 1; + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Finds a satisfying assignment.] + + Description [Returns 1 if a sat assignment is found; 0 otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManObjCheckSat_rec( Gia_Man_t * p, int iLit, Vec_Int_t * vObjs ) +{ + int iObj = Abc_Lit2Var(iLit); + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + if ( pObj->fMark0 ) + return pObj->fMark1 == (unsigned)Abc_LitIsCompl(iLit); + pObj->fMark0 = 1; + pObj->fMark1 = Abc_LitIsCompl(iLit); + Vec_IntPush( vObjs, iObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( pObj->fMark1 == 0 ) // node value is 1 + { + if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit0(pObj, iObj), vObjs ) ) return 0; + if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit1(pObj, iObj), vObjs ) ) return 0; + } + else + { + if ( !Gia_ManObjCheckSat_rec( p, Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj)), vObjs ) ) return 0; + } + } + return 1; +} +int Gia_ManObjCheckOverlap1( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs ) +{ + Gia_Obj_t * pObj; + int i, Res0, Res1 = 0; +// Gia_ManForEachObj( p, pObj, i ) +// assert( pObj->fMark0 == 0 && pObj->fMark1 == 0 ); + Vec_IntClear( vObjs ); + Res0 = Gia_ManObjCheckSat_rec( p, iLit0, vObjs ); + if ( Res0 ) + Res1 = Gia_ManObjCheckSat_rec( p, iLit1, vObjs ); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fMark0 = pObj->fMark1 = 0; + return Res0 && Res1; +} +int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs ) +{ + if ( Gia_ManObjCheckOverlap1( p, iLit0, iLit1, vObjs ) ) + return 1; + return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 1c1edda7..204d3033 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -2075,6 +2075,58 @@ void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName ) fclose( pTable ); } +/**Function************************************************************* + + Synopsis [Check if two logic cones have overlap.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCheckSuppMark_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( pObj->fMark0 ) + return; + pObj->fMark0 = 1; + if ( Gia_ObjIsCi(pObj) ) + return; + Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin1(pObj) ); +} +void Gia_ManCheckSuppUnmark_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( !pObj->fMark0 ) + return; + pObj->fMark0 = 0; + if ( Gia_ObjIsCi(pObj) ) + return; + Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin1(pObj) ); +} +int Gia_ManCheckSupp_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( pObj->fMark0 ) + return 1; + if ( Gia_ObjIsCi(pObj) ) + return 0; + if ( Gia_ManCheckSupp_rec( p, Gia_ObjFanin0(pObj) ) ) + return 1; + return Gia_ManCheckSupp_rec( p, Gia_ObjFanin1(pObj) ); +} +int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 ) +{ + int Result; + if ( iNode1 == 0 || iNode2 == 0 ) + return 0; + Gia_ManCheckSuppMark_rec( p, Gia_ManObj(p, iNode1) ); + Result = Gia_ManCheckSupp_rec( p, Gia_ManObj(p, iNode2) ); + Gia_ManCheckSuppUnmark_rec( p, Gia_ManObj(p, iNode1) ); + return Result; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/acb/acbSets.h b/src/base/acb/acbSets.h new file mode 100644 index 00000000..e457b7a5 --- /dev/null +++ b/src/base/acb/acbSets.h @@ -0,0 +1,61 @@ +/**CFile**************************************************************** + + FileName [acbSets.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Hierarchical word-level netlist.] + + Synopsis [Reading data from file.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 21, 2015.] + + Revision [$Id: acbSets.h,v 1.00 2017/04/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__base__acb__acbSets_h +#define ABC__base__acb__acbSets_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_HEADER_END + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 2ff0dbd1..eea56d25 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -745,16 +745,16 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) SeeAlso [] ***********************************************************************/ -Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vCiSatVars, Vec_Int_t * vVar2Index ) +Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vCiSatVars, Vec_Int_t * vVar2Index, int CubeLimit ) { int fCreatePrime = 1; - int nSupp = Vec_IntSize(vCiSatVars); + int nCubes, nSupp = Vec_IntSize(vCiSatVars); Vec_Str_t * vSop = Vec_StrAlloc( 1000 ); Vec_Int_t * vLits = Vec_IntAlloc( nSupp ); Vec_Str_t * vCube = Vec_StrAlloc( nSupp + 4 ); Vec_StrFill( vCube, nSupp, '-' ); Vec_StrPrintF( vCube, " 1\n\0" ); - while ( 1 ) + for ( nCubes = 0; !CubeLimit || nCubes < CubeLimit; nCubes++ ) { int * pFinal, nFinal, iVar, i, k = 0; // generate onset minterm @@ -803,7 +803,7 @@ Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vCiSat Vec_StrPush( vSop, '\0' ); return vSop; } -Vec_Str_t * Glucose_GenerateSop( Gia_Man_t * p ) +Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit ) { bmcg_sat_solver * pSat[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() }; @@ -838,7 +838,7 @@ Vec_Str_t * Glucose_GenerateSop( Gia_Man_t * p ) Vec_IntWriteEntry( vVarMap, iFirstVar+i, i ); } - Vec_Str_t * vSop = Glucose_GenerateCubes( pSat, vVars, vVarMap ); + Vec_Str_t * vSop = Glucose_GenerateCubes( pSat, vVars, vVarMap, CubeLimit ); Vec_IntFree( vVarMap ); Vec_IntFree( vVars ); @@ -846,13 +846,53 @@ Vec_Str_t * Glucose_GenerateSop( Gia_Man_t * p ) bmcg_sat_solver_stop( pSat[1] ); return vSop; } -void Glucose_GenerateSopTest( Gia_Man_t * p ) +void bmcg_sat_solver_sopTest( Gia_Man_t * p ) { - Vec_Str_t * vSop = Glucose_GenerateSop( p ); + Vec_Str_t * vSop = bmcg_sat_solver_sop( p, 0 ); printf( "%s", Vec_StrArray(vSop) ); Vec_StrFree( vSop ); } +/**Function************************************************************* + + Synopsis [Computing d-literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#define Gia_CubeForEachVar( pCube, Value, i ) \ + for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ ) +#define Gia_SopForEachCube( pSop, nFanins, pCube ) \ + for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 ) + +void bmcg_sat_generate_dvars( Vec_Int_t * vCiVars, Vec_Str_t * vSop, Vec_Int_t * vDLits ) +{ + int i, Lit, Counter, nCubes = 0; + char Value, * pCube, * pSop = Vec_StrArray( vSop ); + Vec_Int_t * vCounts = Vec_IntStart( 2*Vec_IntSize(vCiVars) ); + Vec_IntClear( vDLits ); + Gia_SopForEachCube( pSop, Vec_IntSize(vCiVars), pCube ) + { + nCubes++; + Gia_CubeForEachVar( pCube, Value, i ) + { + if ( Value == '1' ) + Vec_IntAddToEntry( vCounts, 2*i, 1 ); + else if ( Value == '0' ) + Vec_IntAddToEntry( vCounts, 2*i+1, 1 ); + } + } + Vec_IntForEachEntry( vCounts, Counter, Lit ) + if ( Counter == nCubes ) + Vec_IntPush( vDLits, Abc_Var2Lit(Vec_IntEntry(vCiVars, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit)) ); + Vec_IntSort( vDLits, 0 ); + Vec_IntFree( vCounts ); +} + /**Function************************************************************* Synopsis [Performs SAT-based quantification.] @@ -864,20 +904,29 @@ void Glucose_GenerateSopTest( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData ) + +abctime clkQuaSetup = 0; +abctime clkQuaSolve = 0; +abctime clkQuaSynth = 0; + +int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ) { + abctime clk = Abc_Clock(), clkAll = Abc_Clock(); extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp ); Gia_Man_t * pMan, * pNew, * pTemp; Vec_Str_t * vSop; - int i, CiId, ObjId, Res, Count = 0, iNode = Abc_Lit2Var(iLit); + int i, CiId, ObjId, Res, nCubes, nNodes, Count = 0, iNode = Abc_Lit2Var(iLit); Vec_Int_t * vCisUsed = Vec_IntAlloc( 100 ); Gia_ManCollectCis( p, &iNode, 1, vCisUsed ); + Vec_IntSort( vCisUsed, 0 ); + if ( vDLits ) Vec_IntClear( vDLits ); + if ( iLit < 2 ) + return iLit; // remap into CI Ids Vec_IntForEachEntry( vCisUsed, ObjId, i ) Vec_IntWriteEntry( vCisUsed, i, Gia_ManIdToCioId(p, ObjId) ); // duplicate cone pNew = Gia_ManDupConeSupp( p, iLit, vCisUsed ); assert( Gia_ManCiNum(pNew) == Vec_IntSize(vCisUsed) ); -//Gia_AigerWrite( pNew, "test1.aig", 0, 0 ); // perform quantification one CI at a time assert( pFuncCiToKeep ); @@ -889,7 +938,7 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT Gia_ManStop( pTemp ); Count++; } -//Gia_AigerWrite( pNew, "test2.aig", 0, 0 ); + clkQuaSetup += Abc_Clock() - clk; if ( Gia_ManPoIsConst(pNew, 0) ) { int RetValue = Gia_ManPoIsConst1(pNew, 0); @@ -898,13 +947,25 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT return RetValue; } - vSop = Glucose_GenerateSop( pNew ); + clk = Abc_Clock(); + vSop = bmcg_sat_solver_sop( pNew, 0 ); + nNodes = Gia_ManAndNum(pNew); Gia_ManStop( pNew ); + clkQuaSolve += Abc_Clock() - clk; - printf( "Computed # with %d keep-vars and %d quant-vars with %d cubes.\n", - Vec_IntSize(vCisUsed) - Count, Count, Vec_StrCountEntry(vSop, '\n') ); - - pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 0 ); + clk = Abc_Clock(); + pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 ); + clkQuaSynth += Abc_Clock() - clk; + nCubes = Vec_StrCountEntry(vSop, '\n'); + if ( vDLits ) + { + // convert into object IDs + Vec_Int_t * vCisObjs = Vec_IntAlloc( Vec_IntSize(vCisUsed) ); + Vec_IntForEachEntry( vCisUsed, CiId, i ) + Vec_IntPush( vCisObjs, CiId + 1 ); + bmcg_sat_generate_dvars( vCisObjs, vSop, vDLits ); + Vec_IntFree( vCisObjs ); + } Vec_StrFree( vSop ); if ( Gia_ManPoIsConst(pMan, 0) ) { @@ -915,13 +976,18 @@ int bmcg_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiT } Res = Gia_ManDupConeBack( p, pMan, vCisUsed ); + + // report the result + printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", + nNodes, Vec_IntSize(vCisUsed) - Count, Count, nCubes, Gia_ManAndNum(pMan) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll ); + Vec_IntFree( vCisUsed ); Gia_ManStop( pMan ); return Res; } - /**Function************************************************************* Synopsis [Performs SAT-based quantification.] @@ -1001,16 +1067,20 @@ int Gia_ManFactorSop( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, in Gia_ManStop( pMan ); return Result; } -int bmcg_sat_solver_quantify3( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData ) +int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ) { - return bmcg_sat_solver_quantify2( p, iLit, fHash, pFuncCiToKeep, pData ); + return bmcg_sat_solver_quantify2( p, iLit, fHash, pFuncCiToKeep, pData, vDLits ); } -int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData ) +int bmcg_sat_solver_quantify3( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ) { + abctime clk, clkAll = Abc_Clock(); Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); // GIA objs Vec_Int_t * vCiVars = Vec_IntAlloc( 100 ); // CI SAT vars Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL; int i, iVar, iVarLast, Lit, RetValue, Count = 0, Result = -1; + if ( vDLits ) Vec_IntClear( vDLits ); + if ( iLit < 2 ) + return iLit; if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) ) Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 ); // assign variable number 0 to const0 node @@ -1018,10 +1088,15 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit Vec_IntPush( vObjsUsed, 0 ); Gia_ObjSetCopyArray( p, 0, iVar ); assert( iVar == 0 ); + // collect other variables + clk = Abc_Clock(); iVarLast = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit), vObjsUsed, vCiVars ); Gia_ManQuantLoadCnf( p, vObjsUsed, pSats ); + clkQuaSetup += Abc_Clock() - clk; + // check constants + clk = Abc_Clock(); Lit = Abc_Var2Lit( iVarLast, !Abc_LitIsCompl(iLit) ); RetValue = bmcg_sat_solver_addclause( pSats[0], &Lit, 1 ); // offset if ( !RetValue || bmcg_sat_solver_solve(pSats[0], NULL, 0) == GLUCOSE_UNSAT ) @@ -1036,6 +1111,26 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit Result = 0; goto cleanup; } +/* + // reorder CI SAT variables to have keep-vars first + Vec_Int_t * vCiVars2 = Vec_IntAlloc( 100 ); // CI SAT vars + Vec_IntForEachEntry( vCiVars, iVar, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) ); + assert( Gia_ObjIsCi(pObj) ); + if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) ) + Vec_IntPush( vCiVars2, iVar ); + } + Vec_IntForEachEntry( vCiVars, iVar, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) ); + assert( Gia_ObjIsCi(pObj) ); + if ( !pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) ) + Vec_IntPush( vCiVars2, iVar ); + } + ABC_SWAP( Vec_Int_t *, vCiVars2, vCiVars ); + Vec_IntFree( vCiVars2 ); +*/ // map CI SAT variables into their indexes used in the cubes vVarMap = Vec_IntStartFull( Vec_IntSize(vObjsUsed) ); Vec_IntForEachEntry( vCiVars, iVar, i ) @@ -1045,16 +1140,32 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) ) Vec_IntWriteEntry( vVarMap, iVar, i ), Count++; } + if ( Count == 0 || Count == Vec_IntSize(vCiVars) ) + { + Result = Count == 0 ? 1 : iLit; + goto cleanup; + } // generate cubes - vSop = Glucose_GenerateCubes( pSats, vCiVars, vVarMap ); + vSop = Glucose_GenerateCubes( pSats, vCiVars, vVarMap, 0 ); + clkQuaSolve += Abc_Clock() - clk; //printf( "%s", Vec_StrArray(vSop) ); - printf( "Computed # with %d keep-vars and %d quant-vars with %d cubes.\n", - Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n') ); // convert into object IDs Vec_IntForEachEntry( vCiVars, iVar, i ) Vec_IntWriteEntry( vCiVars, i, Vec_IntEntry(vObjsUsed, iVar) ); + // generate unate variables + if ( vDLits ) + bmcg_sat_generate_dvars( vCiVars, vSop, vDLits ); // convert into an AIG + clk = Abc_Clock(); + RetValue = Gia_ManAndNum(p); Result = Gia_ManFactorSop( p, vCiVars, vSop, fHash ); + clkQuaSynth += Abc_Clock() - clk; + + // report the result + printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ", + Vec_IntSize(vObjsUsed), Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n'), Gia_ManAndNum(p)-RetValue ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll ); + cleanup: Vec_IntForEachEntry( vObjsUsed, iVar, i ) Gia_ObjSetCopyArray( p, iVar, -1 ); @@ -1074,11 +1185,11 @@ void Glucose_QuantifyAigTest( Gia_Man_t * p ) bmcg_sat_solver * pSats[3] = { bmcg_sat_solver_start(), bmcg_sat_solver_start(), bmcg_sat_solver_start() }; abctime clk1 = Abc_Clock(); - int iRes1 = bmcg_sat_solver_quantify( pSats, p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL ); + int iRes1 = bmcg_sat_solver_quantify( pSats, p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL, NULL ); abctime clk1d = Abc_Clock()-clk1; abctime clk2 = Abc_Clock(); - int iRes2 = bmcg_sat_solver_quantify2( p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL ); + int iRes2 = bmcg_sat_solver_quantify2( p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL, NULL ); abctime clk2d = Abc_Clock()-clk2; Abc_PrintTime( 1, "Time1", clk1d ); @@ -1108,8 +1219,12 @@ void Glucose_QuantifyAigTest( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +abctime clkTrav = 0; +abctime clkSatRun = 0; + int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ) { + abctime clk; bmcg_sat_solver * pSats[2] = { pSat, NULL }; Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); int i, iVar, iSatVar[2], iSatLit[2], Lits[2], status; @@ -1122,14 +1237,25 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p, Gia_ObjSetCopyArray( p, 0, iVar ); assert( iVar == 0 ); +//printf( "%d ", iLit0 ); +//printf( "%d ", iLit1 ); +//printf( " -> " ); + clk = Abc_Clock(); iSatVar[0] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit0), vObjsUsed, NULL ); +//printf( "%d ", Vec_IntSize(vObjsUsed) ); iSatVar[1] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit1), vObjsUsed, NULL ); + clkTrav += Abc_Clock() - clk; +//printf( "%d ", Vec_IntSize(vObjsUsed) ); +//printf( "\n" ); + iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) ); iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) ); Gia_ManQuantLoadCnf( p, vObjsUsed, pSats ); Vec_IntForEachEntry( vObjsUsed, iVar, i ) Gia_ObjSetCopyArray( p, iVar, -1 ); Vec_IntFree( vObjsUsed ); + + clk = Abc_Clock(); if ( fEquiv ) { Lits[0] = iSatLit[0]; @@ -1141,6 +1267,7 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p, Lits[1] = iSatLit[1]; status = bmcg_sat_solver_solve( pSats[0], Lits, 2 ); } + clkSatRun += Abc_Clock() - clk; return status == GLUCOSE_UNSAT; } else @@ -1148,6 +1275,7 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p, Lits[0] = iSatLit[0]; Lits[1] = iSatLit[1]; status = bmcg_sat_solver_solve( pSats[0], Lits, 2 ); + clkSatRun += Abc_Clock() - clk; return status == GLUCOSE_SAT; } } diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index e2c05e1b..1bf29aed 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -93,8 +93,9 @@ extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ); extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); -extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData ); +extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); +extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars ); -- cgit v1.2.3