diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-27 12:12:23 -0500 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-27 12:12:23 -0500 |
commit | a27a7bc827d29021cf1f418874731b8855a836fd (patch) | |
tree | 5edae1f6afb9e402899724d735299e865bee9976 /src | |
parent | 236be8414960ecb4a99488b3497de3e809facb7d (diff) | |
download | abc-a27a7bc827d29021cf1f418874731b8855a836fd.tar.gz abc-a27a7bc827d29021cf1f418874731b8855a836fd.tar.bz2 abc-a27a7bc827d29021cf1f418874731b8855a836fd.zip |
User-controlable SAT sweeper and other small changes.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/gia.h | 8 | ||||
-rw-r--r-- | src/aig/gia/giaSweeper.c | 202 | ||||
-rw-r--r-- | src/aig/gia/module.make | 3 | ||||
-rw-r--r-- | src/base/abci/abc.c | 74 | ||||
-rw-r--r-- | src/map/mapper/module.make | 1 | ||||
-rw-r--r-- | src/misc/mvc/module.make | 3 | ||||
-rw-r--r-- | src/misc/tim/module.make | 3 | ||||
-rw-r--r-- | src/opt/dar/module.make | 1 | ||||
-rw-r--r-- | src/opt/dau/module.make | 3 | ||||
-rw-r--r-- | src/opt/sim/module.make | 1 | ||||
-rw-r--r-- | src/proof/abs/module.make | 3 | ||||
-rw-r--r-- | src/proof/llb/module.make | 3 | ||||
-rw-r--r-- | src/sat/bmc/module.make | 3 |
13 files changed, 277 insertions, 31 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index cce8d6d9..5e1e4793 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -993,8 +993,9 @@ extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerb /*=== giaSweep.c ============================================================*/ extern Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars ); /*=== giaSweeper.c ============================================================*/ -extern Gia_Man_t * Gia_SweeperStart(); +extern Gia_Man_t * Gia_SweeperStart( Gia_Man_t * p ); extern void Gia_SweeperStop( Gia_Man_t * p ); +extern int Gia_SweeperIsRunning( Gia_Man_t * pGia ); extern void Gia_SweeperPrintStats( Gia_Man_t * p ); extern void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax ); extern void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds ); @@ -1005,11 +1006,12 @@ extern void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId ); extern int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId ); extern int Gia_SweeperCondPop( Gia_Man_t * p ); extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId ); +extern Vec_Int_t * Gia_SweeperCondVector( Gia_Man_t * p ); extern int Gia_SweeperCondCheckUnsat( Gia_Man_t * p ); extern int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int ProbeId1, int ProbeId2 ); -extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames ); +extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames ); extern Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc ); -extern Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeConds, Vec_Int_t * vProbeOuts ); +extern Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ); /*=== giaSwitch.c ============================================================*/ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 07435d81..ea4c2b0e 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -113,6 +113,7 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia ) { Swp_Man_t * p; int Lit; + assert( pGia->pHTable != NULL ); pGia->pData = p = ABC_CALLOC( Swp_Man_t, 1 ); p->pGia = pGia; p->nConfMax = 1000; @@ -150,11 +151,12 @@ static inline void Swp_ManStop( Gia_Man_t * pGia ) ABC_FREE( p ); pGia->pData = NULL; } -Gia_Man_t * Gia_SweeperStart() +Gia_Man_t * Gia_SweeperStart( Gia_Man_t * pGia ) { - Gia_Man_t * pGia; - pGia = Gia_ManStart( 10000 ); - Gia_ManHashStart( pGia ); + if ( pGia == NULL ) + pGia = Gia_ManStart( 10000 ); + if ( pGia->pHTable == NULL ) + Gia_ManHashStart( pGia ); Swp_ManStart( pGia ); pGia->fSweeper = 1; return pGia; @@ -164,7 +166,11 @@ void Gia_SweeperStop( Gia_Man_t * pGia ) pGia->fSweeper = 0; Swp_ManStop( pGia ); Gia_ManHashStop( pGia ); - Gia_ManStop( pGia ); +// Gia_ManStop( pGia ); +} +int Gia_SweeperIsRunning( Gia_Man_t * pGia ) +{ + return (pGia->pData != NULL); } double Gia_SweeperMemUsage( Gia_Man_t * pGia ) { @@ -311,6 +317,11 @@ int Gia_SweeperCondPop( Gia_Man_t * p ) Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; return Vec_IntPop( pSwp->vCondProbes ); } +Vec_Int_t * Gia_SweeperCondVector( Gia_Man_t * p ) +{ + Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; + return pSwp->vCondProbes; +} /**Function************************************************************* @@ -335,13 +346,14 @@ static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOb Gia_ManExtract_rec( p, Gia_ObjFanin1(pObj), vObjIds ); Vec_IntPush( vObjIds, Gia_ObjId(p, pObj) ); } -Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames ) +Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames ) { Vec_Int_t * vObjIds, * vValues; Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, ProbeId; - assert( Vec_IntSize(vProbeIds) == Vec_PtrSize(vOutNames) ); + assert( vInNames == NULL || Gia_ManPiNum(p) == Vec_PtrSize(vInNames) ); + assert( vOutNames == NULL || Vec_IntSize(vProbeIds) == Vec_PtrSize(vOutNames) ); // create new Gia_ManIncrementTravId( p ); vObjIds = Vec_IntAlloc( 1000 ); @@ -386,8 +398,8 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V Gia_ManStop( pTemp ); } // copy names if present - if ( p->vNamesIn ) - pNew->vNamesIn = Vec_PtrDupStr( p->vNamesIn ); + if ( vInNames ) + pNew->vNamesIn = Vec_PtrDupStr( vInNames ); if ( vOutNames ) pNew->vNamesOut = Vec_PtrDupStr( vOutNames ); return pNew; @@ -861,6 +873,62 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_SweeperGen64Patterns( Gia_Man_t * pGiaCond, Vec_Wrd_t * vSim ) +{ + Vec_Int_t * vCex; + int i, k; + for ( i = 0; i < 64; i++ ) + { + if ( Gia_SweeperCondCheckUnsat( pGiaCond ) != 0 ) + return 0; + vCex = Gia_SweeperGetCex( pGiaCond ); + for ( k = 0; k < Gia_ManPiNum(pGiaCond); k++ ) + { + if ( Vec_IntEntry(vCex, k) ) + Abc_InfoXorBit( (unsigned *)Vec_WrdEntryP(vSim, i), k ); + printf( "%d", Vec_IntEntry(vCex, k) ); + } + printf( "\n" ); + } + return 1; +} +int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim ) +{ + Gia_Obj_t * pObj; + word Sim, Sim0, Sim1; + int i, Count = 0; + assert( Vec_WrdEntry(vSim, 0) == 0 ); +// assert( Vec_WrdEntry(vSim, 1) != 0 ); // may not hold + Gia_ManForEachAnd( p, pObj, i ) + { + Sim0 = Vec_WrdEntry( vSim, Gia_ObjFaninId0p( p, pObj ) ); + Sim1 = Vec_WrdEntry( vSim, Gia_ObjFaninId1p( p, pObj ) ); + Sim = (Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0) & (Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1); + Vec_WrdWriteEntry( vSim, i, Sim ); + if ( pObj->fMark0 == 1 ) // considered + continue; + if ( pObj->fMark1 == 1 ) // non-constant + continue; + if ( (pObj->fPhase ? ~Sim : Sim) != 0 ) + { + pObj->fMark1 = 1; + Count++; + } + } + return Count; +} + +/**Function************************************************************* + Synopsis [Performs conditional sweeping of the cone.] Description [Returns the result as a new GIA manager with as many inputs @@ -871,9 +939,121 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeConds, Vec_Int_t * vProbeOuts ) +void Gia_SweeperSweepInt( Gia_Man_t * pGiaCond, Gia_Man_t * pGiaOuts, Vec_Wrd_t * vSim ) +{ +} +Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) +{ + Gia_Man_t * pGiaCond, * pGiaOuts; + Vec_Int_t * vProbeConds; + Vec_Wrd_t * vSim; + Gia_Obj_t * pObj; + int i, Count; + // sweeper is running + assert( Gia_SweeperIsRunning(p) ); + // extract conditions and logic cones + vProbeConds = Gia_SweeperCondVector( p ); + pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL ); + pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL ); + Gia_ManSetPhase( pGiaOuts ); + // start the sweeper for the conditions + Gia_SweeperStart( pGiaCond ); + Gia_ManForEachPo( pGiaCond, pObj, i ) + Gia_SweeperCondPush( pGiaCond, Gia_SweeperProbeCreate(pGiaCond, Gia_ObjFaninLit0p(pGiaCond, pObj)) ); + // generate 64 patterns that satisfy the conditions + vSim = Vec_WrdStart( Gia_ManObjNum(pGiaOuts) ); + Gia_SweeperGen64Patterns( pGiaCond, vSim ); + Count = Gia_SweeperSimulate( pGiaOuts, vSim ); + printf( "Disproved %d nodes.\n", Count ); + + // consider the remaining ones +// Gia_SweeperSweepInt( pGiaCond, pGiaOuts, vSim ); + Vec_WrdFree( vSim ); + Gia_ManStop( pGiaOuts ); + Gia_SweeperStop( pGiaCond ); + return pGiaCond; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits ) +{ + if ( Vec_IntSize(vLits) == 0 ) + return 0; + while ( Vec_IntSize(vLits) > 1 ) + { + int i, k = 0, Lit1, Lit2, LitRes; + Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i ) + { + LitRes = Gia_ManHashAnd( p, Lit1, Lit2 ); + Vec_IntWriteEntry( vLits, k++, LitRes ); + } + if ( Vec_IntSize(vLits) & 1 ) + Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) ); + Vec_IntShrink( vLits, k ); + } + assert( Vec_IntSize(vLits) == 1 ); + return Vec_IntEntry(vLits, 0); +} + +/**Function************************************************************* + + Synopsis [Sweeper sweeper test.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ) { - return NULL; + Gia_Man_t * pGia; + Gia_Obj_t * pObj; + Vec_Int_t * vLits, * vOuts; + int i, k, Lit; + + // create sweeper + Gia_SweeperStart( p ); + + // create 1-hot constraint + vLits = Vec_IntAlloc( 1000 ); + for ( i = 0; i < Gia_ManPiNum(p); i++ ) + for ( k = i+1; k < Gia_ManPiNum(p); k++ ) + { + int Lit0 = Gia_Obj2Lit(p, Gia_ManPi(p, i)); + int Lit1 = Gia_Obj2Lit(p, Gia_ManPi(p, k)); + Vec_IntPush( vLits, Abc_LitNot(Gia_ManHashAnd(p, Lit0, Lit1)) ); + } + Lit = 0; + for ( i = 0; i < Gia_ManPiNum(p); i++ ) + Lit = Gia_ManHashOr( p, Lit, Gia_Obj2Lit(p, Gia_ManPi(p, i)) ); + Vec_IntPush( vLits, Lit ); + Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ManCreateAndGate( p, vLits ) ) ); + Vec_IntFree( vLits ); +//Gia_ManPrint( p ); + + // create outputs + vOuts = Vec_IntAlloc( Gia_ManPoNum(p) ); + Gia_ManForEachPo( p, pObj, i ) + Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); + + // perform the sweeping + pGia = Gia_SweeperSweep( p, vOuts ); + Vec_IntFree( vOuts ); + + Gia_SweeperStop( p ); + return pGia; } diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index ea036907..17147f49 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -1,5 +1,4 @@ -SRC += src/aig/gia/gia.c \ - src/aig/gia/giaAig.c \ +SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ src/aig/gia/giaAigerExt.c \ src/aig/gia/giaBidec.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7a99f0f9..673ed6c0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -346,6 +346,7 @@ static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9CFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Srm2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Filter ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -811,6 +812,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&choice", Abc_CommandAbc9Choice, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fraig", Abc_CommandAbc9Fraig, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&cfraig", Abc_CommandAbc9CFraig, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&srm", Abc_CommandAbc9Srm, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&srm2", Abc_CommandAbc9Srm2, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&filter", Abc_CommandAbc9Filter, 0 ); @@ -26835,6 +26837,78 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); + Gia_Man_t * pTemp; + int c; + int nWords = 1; + int nConfs = 0; + int fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF ) + { + switch ( c ) + { + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + nWords = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nWords < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfs < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9CFraig(): There is no AIG.\n" ); + return 1; + } + pTemp = Gia_SweeperFraigTest( pAbc->pGia, nWords, nConfs, fVerbose ); + Abc_CommandUpdate9( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" ); + Abc_Print( -2, "\t performs conditional combinational SAT sweeping\n" ); + Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", nWords ); + Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfs ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) { char * pFileNameIn = NULL; diff --git a/src/map/mapper/module.make b/src/map/mapper/module.make index bd6447d8..aa6e6a41 100644 --- a/src/map/mapper/module.make +++ b/src/map/mapper/module.make @@ -4,7 +4,6 @@ SRC += src/map/mapper/mapper.c \ src/map/mapper/mapperCreate.c \ src/map/mapper/mapperCut.c \ src/map/mapper/mapperCutUtils.c \ - src/map/mapper/mapperFanout.c \ src/map/mapper/mapperLib.c \ src/map/mapper/mapperMatch.c \ src/map/mapper/mapperRefs.c \ diff --git a/src/misc/mvc/module.make b/src/misc/mvc/module.make index 23735ca2..6ffa17ff 100644 --- a/src/misc/mvc/module.make +++ b/src/misc/mvc/module.make @@ -1,5 +1,4 @@ -SRC += src/misc/mvc/mvc.c \ - src/misc/mvc/mvcApi.c \ +SRC += src/misc/mvc/mvcApi.c \ src/misc/mvc/mvcCompare.c \ src/misc/mvc/mvcContain.c \ src/misc/mvc/mvcCover.c \ diff --git a/src/misc/tim/module.make b/src/misc/tim/module.make index 00609901..3c27a908 100644 --- a/src/misc/tim/module.make +++ b/src/misc/tim/module.make @@ -1,5 +1,4 @@ -SRC += src/misc/tim/tim.c \ - src/misc/tim/timBox.c \ +SRC += src/misc/tim/timBox.c \ src/misc/tim/timDump.c \ src/misc/tim/timMan.c \ src/misc/tim/timTime.c \ diff --git a/src/opt/dar/module.make b/src/opt/dar/module.make index ef9ddbd5..60917bb3 100644 --- a/src/opt/dar/module.make +++ b/src/opt/dar/module.make @@ -6,5 +6,4 @@ SRC += src/opt/dar/darBalance.c \ src/opt/dar/darMan.c \ src/opt/dar/darPrec.c \ src/opt/dar/darRefact.c \ - src/opt/dar/darResub.c \ src/opt/dar/darScript.c diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make index d481c74a..5a3df1d5 100644 --- a/src/opt/dau/module.make +++ b/src/opt/dau/module.make @@ -1,5 +1,4 @@ -SRC += src/opt/dau/dau.c \ - src/opt/dau/dauCanon.c \ +SRC += src/opt/dau/dauCanon.c \ src/opt/dau/dauCore.c \ src/opt/dau/dauDivs.c \ src/opt/dau/dauDsd.c \ diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make index 54058402..77012361 100644 --- a/src/opt/sim/module.make +++ b/src/opt/sim/module.make @@ -1,5 +1,4 @@ SRC += src/opt/sim/simMan.c \ - src/opt/sim/simSat.c \ src/opt/sim/simSeq.c \ src/opt/sim/simSupp.c \ src/opt/sim/simSwitch.c \ diff --git a/src/proof/abs/module.make b/src/proof/abs/module.make index 7b8c8166..30ba6c22 100644 --- a/src/proof/abs/module.make +++ b/src/proof/abs/module.make @@ -1,5 +1,4 @@ -SRC += src/proof/abs/abs.c \ - src/proof/abs/absDup.c \ +SRC += src/proof/abs/absDup.c \ src/proof/abs/absGla.c \ src/proof/abs/absGlaOld.c \ src/proof/abs/absIter.c \ diff --git a/src/proof/llb/module.make b/src/proof/llb/module.make index 849a9e0e..b08c42af 100644 --- a/src/proof/llb/module.make +++ b/src/proof/llb/module.make @@ -1,5 +1,4 @@ -SRC += src/proof/llb/llb.c \ - src/proof/llb/llb1Cluster.c \ +SRC += src/proof/llb/llb1Cluster.c \ src/proof/llb/llb1Constr.c \ src/proof/llb/llb1Core.c \ src/proof/llb/llb1Group.c \ diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index b35577fb..fd50ec23 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -1,5 +1,4 @@ -SRC += src/sat/bmc/bmc.c \ - src/sat/bmc/bmcBmc.c \ +SRC += src/sat/bmc/bmcBmc.c \ src/sat/bmc/bmcBmc2.c \ src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcCexCut.c \ |