From aeb7f7ea11ac4ab5046754bbc1a2dacae49c18ca Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 2 Oct 2012 17:27:36 -0700 Subject: Combined old reparametrization command with the new one. --- src/aig/gia/gia.h | 2 - src/aig/gia/giaReparam.c | 203 ---------------------------------------------- src/aig/gia/module.make | 1 - src/base/abci/abc.c | 66 +++------------ src/proof/abs/abs.h | 4 + src/proof/abs/absRpmOld.c | 201 +++++++++++++++++++++++++++++++++++++++++++++ src/proof/abs/module.make | 1 + 7 files changed, 218 insertions(+), 260 deletions(-) delete mode 100644 src/aig/gia/giaReparam.c create mode 100644 src/proof/abs/absRpmOld.c (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 25187a33..fd47d2c7 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -857,8 +857,6 @@ extern void Gia_MmStepEntryRecycle( Gia_MmStep_t * p, char * pEnt extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p ); /*=== giaPat.c ===========================================================*/ extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit ); -/*=== giaReparam.c ===========================================================*/ -extern Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ); /*=== giaRetime.c ===========================================================*/ extern Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose ); /*=== giaSat.c ============================================================*/ diff --git a/src/aig/gia/giaReparam.c b/src/aig/gia/giaReparam.c deleted file mode 100644 index a63af649..00000000 --- a/src/aig/gia/giaReparam.c +++ /dev/null @@ -1,203 +0,0 @@ -/**CFile**************************************************************** - - FileName [gia.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: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" -#include "giaAig.h" -#include "aig/saig/saig.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Specialized duplication.] - - Description [Replaces registers by PIs/POs and PIs by registers.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupIn2Ff( Gia_Man_t * p ) -{ - Vec_Int_t * vPiOuts; - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int i; - vPiOuts = Vec_IntAlloc( Gia_ManPiNum(p) ); - pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * Gia_ManPiNum(p) ); - pNew->pName = Abc_UtilStrsav( p->pName ); - pNew->pSpec = Abc_UtilStrsav( p->pSpec ); - Gia_ManFillValue( p ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachPi( p, pObj, i ) - Vec_IntPush( vPiOuts, Gia_ManAppendCi(pNew) ); - Gia_ManForEachRo( p, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachPi( 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_ManForEachPo( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManForEachRi( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManForEachPi( p, pObj, i ) - Gia_ManAppendCo( pNew, Vec_IntEntry(vPiOuts, i) ); - Gia_ManSetRegNum( pNew, Gia_ManPiNum(p) ); - Vec_IntFree( vPiOuts ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Reverses the above step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManDupFf2In_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) -{ - if ( pObj->Value != ~0 ) - return pObj->Value; - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManDupFf2In_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManDupFf2In_rec( pNew, Gia_ObjFanin1(pObj) ); - return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Reverses the above step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupFf2In( Gia_Man_t * p, int nFlopsOld ) -{ - 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_ManFillValue( p ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachRo( p, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - for ( i = Gia_ManPiNum(p) - nFlopsOld; i < Gia_ManPiNum(p); i++ ) - Gia_ManPi(p, i)->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachPo( p, pObj, i ) - Gia_ManDupFf2In_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManForEachPo( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManSetRegNum( pNew, nFlopsOld ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Reparameterized to get rid of useless primary inputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) -{ -// extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); - Aig_Man_t * pMan, * pTemp; - Gia_Man_t * pNew, * pTmp; - int nFlopsOld = Gia_ManRegNum(p); - if ( fVerbose ) - { - printf( "Original AIG:\n" ); - Gia_ManPrintStats( p, 0, 0 ); - } - - // perform input trimming - pNew = Gia_ManDupTrimmed( p, 1, 0, 0 ); - if ( fVerbose ) - { - printf( "After PI trimming:\n" ); - Gia_ManPrintStats( pNew, 0, 0 ); - } - // transform GIA - pNew = Gia_ManDupIn2Ff( pTmp = pNew ); - Gia_ManStop( pTmp ); - if ( fVerbose ) - { - printf( "After PI-2-FF transformation:\n" ); - Gia_ManPrintStats( pNew, 0, 0 ); - } - - // derive AIG - pMan = Gia_ManToAigSimple( pNew ); - Gia_ManStop( pNew ); - // perform min-reg retiming - pMan = Saig_ManRetimeMinArea( pTemp = pMan, 10, 0, 0, 1, 0 ); - Aig_ManStop( pTemp ); - // derive GIA - pNew = Gia_ManFromAigSimple( pMan ); - Aig_ManStop( pMan ); - if ( fVerbose ) - { - printf( "After min-area retiming:\n" ); - Gia_ManPrintStats( pNew, 0, 0 ); - } - - // transform back - pNew = Gia_ManDupFf2In( pTmp = pNew, nFlopsOld ); - Gia_ManStop( pTmp ); - if ( fVerbose ) - { - printf( "After FF-2-PI tranformation:\n" ); - Gia_ManPrintStats( pNew, 0, 0 ); - } - return pNew; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 5bdd4ff1..fcff9a9f 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -28,7 +28,6 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaMan.c \ src/aig/gia/giaMem.c \ src/aig/gia/giaPat.c \ - src/aig/gia/giaReparam.c \ src/aig/gia/giaRetime.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaShrink.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9f3d9a9e..f5f1b39b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -342,7 +342,6 @@ static int Abc_CommandAbc9Trace ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Rpm ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BackReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -791,7 +790,6 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&speedup", Abc_CommandAbc9Speedup, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&era", Abc_CommandAbc9Era, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dch", Abc_CommandAbc9Dch, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&rpm", Abc_CommandAbc9Rpm, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&back_reach", Abc_CommandAbc9BackReach, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 ); @@ -26725,52 +26723,6 @@ usage: } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Gia_Man_t * pTemp = NULL; - int c, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) - { - switch ( c ) - { - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( pAbc->pGia == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9Reparam(): There is no AIG.\n" ); - return 0; - } - pTemp = Gia_ManReparam( pAbc->pGia, fVerbose ); - Abc_CommandUpdate9( pAbc, pTemp ); - return 0; - -usage: - Abc_Print( -2, "usage: &reparam [-vh]\n" ); - Abc_Print( -2, "\t performs input trimming and reparameterization\n" ); - 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 [] @@ -26784,13 +26736,13 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose ); Gia_Man_t * pTemp; int c, nCutMax = 6; + int fUseOldAlgo = 0; int fVerbose = 0; int fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Cavwh" ) ) != EOF ) { switch ( c ) { @@ -26805,6 +26757,9 @@ int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nCutMax < 0 ) goto usage; break; + case 'a': + fUseOldAlgo ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -26822,15 +26777,18 @@ int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Rpm(): There is no AIG.\n" ); return 0; } - pTemp = Abs_RpmPerform( pAbc->pGia, nCutMax, fVerbose, fVeryVerbose ); - if ( pTemp ) - Abc_CommandUpdate9( pAbc, pTemp ); + if ( fUseOldAlgo ) + pTemp = Abs_RpmPerformOld( pAbc->pGia, fVerbose ); + else + pTemp = Abs_RpmPerform( pAbc->pGia, nCutMax, fVerbose, fVeryVerbose ); + Abc_CommandUpdate9( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &rpm [-C num] [-vwh]\n" ); + Abc_Print( -2, "usage: &rpm [-C num] [-avwh]\n" ); Abc_Print( -2, "\t performs structural reparametrization\n" ); Abc_Print( -2, "\t-C num : max cut size for testing range equivalence [default = %d]\n", nCutMax ); + Abc_Print( -2, "\t-a : toggle using old algorithm [default = %s]\n", fUseOldAlgo? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h index 5b4f89be..537a8a36 100644 --- a/src/proof/abs/abs.h +++ b/src/proof/abs/abs.h @@ -123,6 +123,10 @@ extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ); extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ); extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ); +/*=== absRpm.c =========================================================*/ +extern Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose ); +/*=== absRpmOld.c =========================================================*/ +extern Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose ); /*=== absOldCex.c ==========================================================*/ extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect ); diff --git a/src/proof/abs/absRpmOld.c b/src/proof/abs/absRpmOld.c new file mode 100644 index 00000000..362df8de --- /dev/null +++ b/src/proof/abs/absRpmOld.c @@ -0,0 +1,201 @@ +/**CFile**************************************************************** + + FileName [absRpmOld.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Old min-cut-based reparametrization.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: absRpmOld.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abs.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Specialized duplication.] + + Description [Replaces registers by PIs/POs and PIs by registers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupIn2Ff( Gia_Man_t * p ) +{ + Vec_Int_t * vPiOuts; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + vPiOuts = Vec_IntAlloc( Gia_ManPiNum(p) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * Gia_ManPiNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + Vec_IntPush( vPiOuts, Gia_ManAppendCi(pNew) ); + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachPi( 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_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ManAppendCo( pNew, Vec_IntEntry(vPiOuts, i) ); + Gia_ManSetRegNum( pNew, Gia_ManPiNum(p) ); + Vec_IntFree( vPiOuts ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Reverses the above step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManDupFf2In_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) +{ + if ( pObj->Value != ~0 ) + return pObj->Value; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupFf2In_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupFf2In_rec( pNew, Gia_ObjFanin1(pObj) ); + return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Reverses the above step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupFf2In( Gia_Man_t * p, int nFlopsOld ) +{ + 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_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + for ( i = Gia_ManPiNum(p) - nFlopsOld; i < Gia_ManPiNum(p); i++ ) + Gia_ManPi(p, i)->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachPo( p, pObj, i ) + Gia_ManDupFf2In_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, nFlopsOld ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Reparameterized to get rid of useless primary inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose ) +{ +// extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); + Aig_Man_t * pMan, * pTemp; + Gia_Man_t * pNew, * pTmp; + int nFlopsOld = Gia_ManRegNum(p); + if ( fVerbose ) + { + printf( "Original AIG:\n" ); + Gia_ManPrintStats( p, 0, 0 ); + } + + // perform input trimming + pNew = Gia_ManDupTrimmed( p, 1, 0, 0 ); + if ( fVerbose ) + { + printf( "After PI trimming:\n" ); + Gia_ManPrintStats( pNew, 0, 0 ); + } + // transform GIA + pNew = Gia_ManDupIn2Ff( pTmp = pNew ); + Gia_ManStop( pTmp ); + if ( fVerbose ) + { + printf( "After PI-2-FF transformation:\n" ); + Gia_ManPrintStats( pNew, 0, 0 ); + } + + // derive AIG + pMan = Gia_ManToAigSimple( pNew ); + Gia_ManStop( pNew ); + // perform min-reg retiming + pMan = Saig_ManRetimeMinArea( pTemp = pMan, 10, 0, 0, 1, 0 ); + Aig_ManStop( pTemp ); + // derive GIA + pNew = Gia_ManFromAigSimple( pMan ); + Aig_ManStop( pMan ); + if ( fVerbose ) + { + printf( "After min-area retiming:\n" ); + Gia_ManPrintStats( pNew, 0, 0 ); + } + + // transform back + pNew = Gia_ManDupFf2In( pTmp = pNew, nFlopsOld ); + Gia_ManStop( pTmp ); + if ( fVerbose ) + { + printf( "After FF-2-PI tranformation:\n" ); + Gia_ManPrintStats( pNew, 0, 0 ); + } + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/abs/module.make b/src/proof/abs/module.make index 7c35381f..7b8c8166 100644 --- a/src/proof/abs/module.make +++ b/src/proof/abs/module.make @@ -12,5 +12,6 @@ SRC += src/proof/abs/abs.c \ src/proof/abs/absRef.c \ src/proof/abs/absRefSelect.c \ src/proof/abs/absRpm.c \ + src/proof/abs/absRpmOld.c \ src/proof/abs/absVta.c \ src/proof/abs/absUtil.c -- cgit v1.2.3