Skip to content

A
abc
Commit 94d35a25 by Alan Mishchenko
Options

Variable timeframe abstraction.

parent f8e933c7
Showing with 336 additions and 58 deletions
abcexe.dsp
......@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "C:/_projects/abc_niklas/" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "C:/_projects/abc" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "C:/_projects/abc_niklas/" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "C:/_projects/abc" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
BSC32=bscmake.exe
......
abclib.dsp
......@@ -41,7 +41,7 @@ RSC=rc.exe
# PROP Intermediate_Dir "ReleaseLib"
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "C:/_projects/abc_niklas/" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD CPP /nologo /MD /W3 /GX /O2 /I "C:/_projects/abc" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -64,7 +64,7 @@ LIB32=link.exe -lib
# PROP Intermediate_Dir "DebugLib"
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "C:/_projects/abc_niklas/" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "C:/_projects/abc" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
BSC32=bscmake.exe
......
src/aig/gia/giaAbsVta.c
......@@ -52,7 +52,7 @@ struct Vta_Man_t_
int nObjsAlloc; // the number of objects allocated
int nBins; // number of hash table entries
int * pBins; // hash table bins
Vta_Obj_t * pObjs; // hash table bins
Vta_Obj_t * pObjs; // storage for objects
Vec_Int_t * vOrder; // objects in DPS order
// abstraction
int nObjBits; // the number of bits to represent objects
......@@ -66,6 +66,7 @@ struct Vta_Man_t_
Vec_Int_t * vCla2Var; // map clauses into variables
Vec_Ptr_t * vCores; // unsat core for each frame
sat_solver2 * pSat; // incremental SAT solver
int iPivot;
};
......@@ -77,11 +78,19 @@ struct Vta_Man_t_
static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl )
{
return (pThis->Value == VTA_VAR0 && !fCompl) || (pThis->Value == VTA_VAR1 && fCompl);
if ( pThis->Value == VTA_VAR1 && fCompl )
return 1;
if ( pThis->Value == VTA_VAR0 && !fCompl )
return 1;
return 0;
}
static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl )
{
return (pThis->Value == VTA_VAR1 && !fCompl) || (pThis->Value == VTA_VAR0 && fCompl);
if ( pThis->Value == VTA_VAR0 && fCompl )
return 1;
if ( pThis->Value == VTA_VAR1 && !fCompl )
return 1;
return 0;
}
static inline Vta_Obj_t * Vta_ManObj( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
......@@ -89,20 +98,21 @@ static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert
#define Vta_ManForEachObj( p, pObj, i ) \
for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i ) \
for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define Vta_ManForEachObjVec( vVec, p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
#define Vta_ManForEachObjVecReverse( vVec, p, pObj, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
#define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )
#define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
#define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i ) \
for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
#define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
// abstraction is given as an array of integers:
// - the first entry is the number of timeframes (F)
......@@ -129,14 +139,15 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
***********************************************************************/
void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
int size = sizeof(Gia_ParVta_t);
memset( p, 0, sizeof(Gia_ParVta_t) );
p->nFramesStart = 10; // the number of starting frames
p->nFramesMax = 0; // the max number of frames
// p->nFramesOver = 4; // the number of overlapping frames
p->nConfLimit = 0; // conflict limit
p->nTimeOut = 60; // timeout in seconds
p->fVerbose = 1; // verbosity flag
p->nFramesStart = 5; // starting frame
p->nFramesMax = 10; // maximum frames
p->nFramesOver = 3; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nTimeOut = 60; // timeout in seconds
p->fUseTermVars = 0; // use terminal variables
p->fVerbose = 1; // verbose flag
p->iFrame = -1; // the number of frames covered
}
/**Function*************************************************************
......@@ -535,7 +546,7 @@ void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrd
{
Gia_Obj_t * pObj;
Vta_Obj_t * pThis0, * pThis1;
if ( !pThis->fVisit )
if ( pThis->fVisit )
return;
pThis->fVisit = 1;
pObj = Gia_ManObj( p->pGia, pThis->iObj );
......@@ -569,6 +580,54 @@ Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f )
SeeAlso []
***********************************************************************/
void Vta_ManSatVerify( Vta_Man_t * p )
{
Vta_Obj_t * pThis, * pThis0, * pThis1;
Gia_Obj_t * pObj;
int i;
Vta_ManForEachObj( p, pThis, i )
pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0);
Vta_ManForEachObjObj( p, pThis, pObj, i )
{
if ( !pThis->fAdded )
continue;
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
if ( Gia_ObjIsAnd(pObj) )
{
int iVar = Vta_ObjId(p, pThis);
int iVar0 = Vta_ObjId(p, pThis0);
int iVar1 = Vta_ObjId(p, pThis1);
if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
if ( pThis->iFrame == 0 )
assert( pThis->Value == VTA_VAR0 );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
else if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
else assert( 0 );
}
}
}
/**Function*************************************************************
Synopsis [Refines abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
{
Abc_Cex_t * pCex = NULL;
......@@ -578,17 +637,46 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
Gia_Obj_t * pObj;
int i, Counter;
Vta_ManSatVerify( p );
// collect nodes in a topological order
vOrder = Vta_ManCollectNodes( p, f );
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
pThis->Prio = VTA_LARGE;
pThis->Value = sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0;
pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
pThis->fVisit = 0;
}
// verify
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
if ( !pThis->fAdded )
continue;
Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
if ( Gia_ObjIsAnd(pObj) )
{
if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
else assert( 0 );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
pObj = Gia_ObjRoToRi( p->pGia, pObj );
if ( pThis->iFrame == 0 )
assert( pThis->Value == VTA_VAR0 );
else if ( pThis->Value == VTA_VAR0 )
assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
else if ( pThis->Value == VTA_VAR1 )
assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
else assert( 0 );
}
}
// compute distance in reverse order
pThis = Vta_ManObj( p, p->nObjs - 1 );
pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
pThis->Prio = 1;
// collect used and unused terms
vTermsUsed = Vec_PtrAlloc( 1015 );
......@@ -638,6 +726,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis->Prio = Counter++;
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
pThis->Prio = Counter++;
// printf( "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
Vec_PtrFree( vTermsUsed );
Vec_PtrFree( vTermsUnused );
......@@ -653,7 +743,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
// assumes that values are assigned!!!
assert( pThis->Value != 0 );
// propagate
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
......@@ -688,12 +777,17 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
else
pThis->Prio = 0;
}
else if ( Gia_ObjIsConst0(pObj) )
pThis->Prio = 0;
else
assert( 0 );
}
// select important values
pTop = Vta_ManObj( p, Vec_IntEntryLast(p->vOrder) );
pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
pTop->fVisit = 1;
vTermsToAdd = Vec_IntAlloc( 100 );
printf( "\n\n" );
Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
{
if ( !pThis->fVisit )
......@@ -703,13 +797,13 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
// skip terminal objects
if ( !pThis->fAdded )
{
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) );
Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
continue;
}
// assumes that values are assigned!!!
assert( pThis->Value != 0 );
// propagate
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
......@@ -722,31 +816,45 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
assert( pThis1->Prio <= pThis->Prio );
pThis0->fVisit = 1;
pThis1->fVisit = 1;
// printf( "And1 %d requires %d %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0), Vta_ObjId(p,pThis1) );
}
else if ( pThis->Value == VTA_VAR0 )
{
if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
{
if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
if ( pThis0->fVisit )
{
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
else if ( pThis1->fVisit )
{
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
}
else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
{
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
else
{
pThis1->fVisit = 1;
assert( pThis1->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
}
}
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
{
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
{
pThis1->fVisit = 1;
assert( pThis1->Prio == pThis->Prio );
// printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
}
else assert( 0 );
}
......@@ -761,15 +869,17 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
assert( pThis0 );
pThis0->fVisit = 1;
assert( pThis0->Prio == pThis->Prio );
// printf( "Reg %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
}
}
else assert( 0 );
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
}
//printf( "\n" );
// verify
Vta_ManForEachObjVec( p->vOrder, p, pThis, i )
if ( !pThis->fAdded )
pThis->Value = VTA_VARX;
Vta_ManForEachObjVec( vOrder, p, pThis, i )
pThis->Value = VTA_VARX;
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
{
assert( !pThis->fAdded );
......@@ -786,6 +896,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
assert( pThis0 && pThis1 );
// printf( "AND %d %d %d ", Vta_ObjId(p, pThis), Vta_ObjId(p,pThis0), Vta_ObjId(p,pThis1) );
if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
pThis->Value = VTA_VAR1;
else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
......@@ -806,17 +917,30 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
pThis->Value = VTA_VAR1;
else
pThis->Value = VTA_VARX;
// printf( "RO %d ", Vta_ObjId(p, pThis), Vta_ObjId(p,pThis0) );
}
else
{
// printf( "RO %d frame0 ", Vta_ObjId(p, pThis) );
pThis->Value = VTA_VAR0;
}
}
else if ( Gia_ObjIsConst0(pObj) )
{
// printf( "CONST0 %d ", Vta_ObjId(p, pThis) );
pThis->Value = VTA_VAR0;
}
else assert( 0 );
// printf( "val = %d. \n", (pThis->Value==VTA_VAR0) ? 0 : ((pThis->Value==VTA_VAR0) ? 1 : 2 ) );
// double check the solver
assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
}
// check the output
if ( pTop->Value != VTA_VAR1 )
if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
else
printf( "Verification OK.\n" );
// produce true counter-example
if ( pTop->Prio == 0 )
......@@ -840,8 +964,9 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
// perform refinement
else
{
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
}
Vec_IntFree( vTermsToAdd );
return pCex;
......@@ -901,6 +1026,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vCla2Var = Vec_IntAlloc( 1000 );
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
p->iPivot = Gia_ObjFaninId0p(p->pGia, Gia_ManPo(p->pGia, 0));
return p;
}
......@@ -952,10 +1078,10 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
int nConfPrev = pSat->stats.conflicts;
if ( piRetValue )
*piRetValue = 1;
if ( pnConfls )
*pnConfls = 0;
// solve the problem
RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( pnConfls )
*pnConfls = (int)pSat->stats.conflicts - nConfPrev;
if ( RetValue == l_Undef )
{
if ( piRetValue )
......@@ -968,8 +1094,6 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
*piRetValue = 0;
return NULL;
}
if ( pnConfls )
*pnConfls = (int)pSat->stats.conflicts - nConfPrev;
if ( fVerbose )
{
// printf( "%6d", (int)pSat->stats.conflicts - nConfPrev );
......@@ -1081,8 +1205,21 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
int iMainVar = Vta_ObjId(p, pThis);
assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
if ( iObj == 317 && iFrame == 0 )
{
int s = 0;
}
if ( pThis->fAdded )
{
// if ( p->iPivot == iObj )
// printf( "Pivot in frame %d is already added\n", iFrame );
return;
}
// if ( p->iPivot == iObj )
// printf( "Adding pivot in frame %d\n", iFrame );
// printf( "(%d,%d) ", iObj, iFrame );
pThis->fAdded = 1;
if ( Gia_ObjIsAnd(pObj) )
{
......@@ -1148,6 +1285,7 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
int i, Entry;
Vec_IntForEachEntry( vOne, Entry, i )
Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
printf( "\n\n" );
}
/**Function*************************************************************
......@@ -1169,6 +1307,49 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vga_ManPrintCore( Vta_Man_t * p, Vec_Int_t * vCore, int Lift )
{
int i, Entry, iObj, iFrame;
Vec_IntForEachEntry( vCore, Entry, i )
{
iObj = (Entry & p->nObjMask);
iFrame = (Entry >> p->nObjBits);
printf( "%d*%d ", iObj, iFrame+Lift );
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
{
Vta_Obj_t * pThis = p->pObjs + nObjOld;
Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
for ( ; pThis < pLimit; pThis++ )
Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
p->nObjs = nObjOld;
}
/**Function*************************************************************
......@@ -1208,34 +1389,54 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
if ( f < p->pPars->nFramesStart )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
else
// for ( f = 0; f < p->pPars->nFramesStart; f++ )
// Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
{
// create bookmark to be used for rollback
int nObjOld;
int nClaOld;
//start:
nObjOld = p->nObjs;
nClaOld = Vec_IntSize(p->vCla2Var);
sat_solver2_bookmark( p->pSat );
// load the time frame
for ( i = 1; i <= Abc_MinInt(4, p->pPars->nFramesStart); i++ )
for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesOver, p->pPars->nFramesStart); i++ )
{
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
//Vga_ManPrintCore( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
}
// iterate as long as there are counter-examples
while ( 1 )
for ( i = 1; ; i++ )
{
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, NULL );
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
goto finish;
if ( vCore != NULL )
break;
printf( "Frame %d iter %d...\n", f, i );
assert( Status == 0 );
pCex = Vta_ManRefineAbstraction( p, f );
goto finish;
if ( pCex != NULL )
goto finish;
}
assert( Status == 1 );
/*
// valid core is obtained
Vta_ManUnsatCoreRemap( p, vCore );
Vec_IntSort( vCore, 0 );
printf( "Double checked core...\n" );
Vga_ManPrintCore( p, vCore, 0 );
// Vec_IntSort( vCore, 0 );
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
Vga_ManRollBack( p, nObjOld );
Vec_IntShrink( p->vCla2Var, nClaOld );
// load this timeframe
Vga_ManLoadSlice( p, vCore, 0 );
*/
Vec_IntFree( vCore );
// goto start;
}
// run SAT solver
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
......@@ -1252,13 +1453,20 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
}
// add the core
Vta_ManUnsatCoreRemap( p, vCore );
if ( f >= p->pPars->nFramesStart )
{
// printf( "Core to record:\n" );
// Vga_ManPrintCore( p, vCore, 0 );
}
// add in direct topological order
Vec_IntSort( vCore, 0 );
// Vec_IntSort( vCore, 1 );
Vec_PtrPush( p->vCores, vCore );
// print the result
Vta_ManAbsPrintFrame( p, vCore, f+1, p->pPars->fVerbose );
if ( f == p->pPars->nFramesStart-1 )
break;
// if ( f == p->pPars->nFramesStart-1 )
// break;
}
finish:
// analize the results
......
src/base/abci/abc.c
......@@ -26404,7 +26404,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParVta_t Pars, Pars2, * pPars = &Pars;
Gia_ParVta_t Pars, * pPars = &Pars;
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
......@@ -26483,7 +26483,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
return 0;
}
if ( pPars->nFramesMax > 0 )
if ( pPars->nFramesMax < 0 )
{
Abc_Print( 1, "The number of starting frames should be a positive integer.\n" );
return 0;
......
src/sat/bsat/satSolver2.c
......@@ -141,7 +141,7 @@ static inline satset* clause_read (sat_solver2* s, cla h) { return (h & 1
static inline cla clause_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; }
static inline int clause_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); }
static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot; }
static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot); }
//static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; }
//static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
......@@ -150,8 +150,8 @@ static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1
static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; }
static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; }
static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause_read(s, s->units[v]); }
//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; }
static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; }
static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; }
//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; }
// these two only work after creating a clause before the solver is called
int clause_is_partA (sat_solver2* s, int h) { return clause_read(s, h)->partA; }
......@@ -501,8 +501,12 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
for (c = s->qtail-1; c >= bound; c--)
{
x = lit_var(trail[c]);
var_set_value(s, x, varX);
s->reasons[x] = 0;
// if ( s->units[x] == 0 || var_level(s, x) > 0 )
{
var_set_value(s, x, varX);
s->units[x] = 0; // temporary?
}
if ( c < lastLev )
var_set_polar(s, x, !lit_sign(trail[c]));
}
......@@ -1551,7 +1555,7 @@ void sat_solver2_rollback( sat_solver2* s )
{
int i, k, j;
assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->clauses) );
assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) );
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
veci_resize(&s->order, 0);
if ( s->hClausePivot > 1 || s->hLearntPivot > 1 )
......@@ -1581,18 +1585,24 @@ void sat_solver2_rollback( sat_solver2* s )
s->units[i] = 0;
}
// reset
if ( s->hClausePivot < veci_size(&s->clauses) )
{
satset* first = satset_read(&s->clauses, s->hClausePivot);
s->stats.clauses = first->Id;
veci_resize(&s->clauses, s->hClausePivot);
}
if ( s->hLearntPivot < veci_size(&s->learnts) )
{
satset* first = satset_read(&s->learnts, s->hLearntPivot);
veci_resize(&s->claActs, first->Id);
veci_resize(&s->claActs, first->Id+1);
if ( s->fProofLogging ) {
veci_resize(&s->claProofs, first->Id);
veci_resize(&s->claProofs, first->Id+1);
Sat_ProofReduce( s );
}
s->stats.learnts = first->Id;
veci_resize(&s->learnts, s->hLearntPivot);
}
veci_resize(&s->clauses, s->hClausePivot);
veci_resize(&s->learnts, s->hLearntPivot);
for ( i = s->iVarPivot; i < s->size*2; i++ )
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
s->size = s->iVarPivot;
// initialize other vars
......@@ -1628,9 +1638,67 @@ void sat_solver2_rollback( sat_solver2* s )
s->stats.learnts = 0;
s->stats.learnts_literals = 0;
s->stats.tot_literals = 0;
// initialize clause pointers
s->hClausePivot = 1;
s->hLearntPivot = 1;
s->hLearntLast = -1; // the last learnt clause
}
}
// find the clause in the watcher lists
int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose )
{
int i, k, Found = 0;
if ( Hand >= s->clauses.size )
return 1;
for ( i = 0; i < s->size*2; i++ )
{
cla* pArray = veci_begin(&s->wlists[i]);
for ( k = 0; k < veci_size(&s->wlists[i]); k++ )
if ( (pArray[k] >> 1) == Hand )
{
if ( fVerbose )
printf( "Clause found in list %d.\n", k );
Found = 1;
break;
}
}
if ( Found == 0 )
{
if ( fVerbose )
printf( "Clause with hand %d is not found.\n", Hand );
}
return Found;
}
// verify that all clauses are satisfied
void sat_solver2_verify( sat_solver2* s )
{
satset * c;
int i, k, v, Counter = 0;
satset_foreach_entry( &s->clauses, c, i, 1 )
{
for ( k = 0; k < (int)c->nEnts; k++ )
{
v = lit_var(c->pEnts[k]);
if ( sat_solver2_var_value(s, v) ^ lit_sign(c->pEnts[k]) )
break;
}
if ( k == (int)c->nEnts )
{
printf( "Clause %d is not satisfied. ", c->Id );
satset_print( c );
sat_solver2_find_clause( s, satset_handle(&s->clauses, c), 1 );
Counter++;
}
}
if ( Counter == 0 )
printf( "Verification passed.\n" );
else
printf( "Verification failed!\n" );
}
int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
{
int restart_iter = 0;
......@@ -1798,6 +1866,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
printf("==============================================================================\n");
solver2_canceluntil(s,0);
if ( status == l_True )
sat_solver2_verify( s );
return status;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment