Skip to content

A
abc
Commit 719b06f9 by Alan Mishchenko
Options

Variable timeframe abstraction.

parent b9163754
Showing with 266 additions and 208 deletions
src/aig/gia/giaAbsVta.c
...@@ -98,7 +98,7 @@ static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert ...@@ -98,7 +98,7 @@ static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert
// - the following entries give the object IDs // - the following entries give the object IDs
// invariant: assert( vec[vec[0]+2] == size(vec) ); // invariant: assert( vec[vec[0]+2] == size(vec) );
extern void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis ); extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -342,6 +342,7 @@ static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame ...@@ -342,6 +342,7 @@ static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame
{ {
Vta_Obj_t * pThis; Vta_Obj_t * pThis;
int * pPlace; int * pPlace;
assert( iObj >= 0 && iFrame >= -1 );
if ( p->nObjs == p->nObjsAlloc ) if ( p->nObjs == p->nObjsAlloc )
{ {
p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc ); p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
...@@ -370,78 +371,6 @@ static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame ) ...@@ -370,78 +371,6 @@ static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Finds the set of clauses involved in the UNSAT core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Vta_ManUnsatCore( Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue )
{
Vec_Int_t * vPres;
Vec_Int_t * vCore;
int k, i, Entry, RetValue, clk = clock();
if ( piRetValue )
*piRetValue = -1;
// solve the problem
RetValue = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_Undef )
{
// if ( fVerbose )
printf( "Conflict limit is reached.\n" );
return NULL;
}
if ( RetValue == l_True )
{
// if ( fVerbose )
printf( "The BMC problem is SAT.\n" );
if ( piRetValue )
*piRetValue = 0;
return NULL;
}
if ( fVerbose )
{
printf( "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
Abc_PrintTime( 1, "Time", clock() - clk );
}
assert( RetValue == l_False );
// derive the UNSAT core
clk = clock();
vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
if ( fVerbose )
{
printf( "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
// remap core into variables
clk = clock();
vPres = Vec_IntStart( sat_solver2_nvars(pSat) );
k = 0;
Vec_IntForEachEntry( vCore, Entry, i )
{
Entry = Vec_IntEntry(vCla2Var, Entry);
if ( Vec_IntEntry(vPres, Entry) )
continue;
Vec_IntWriteEntry( vPres, Entry, 1 );
Vec_IntWriteEntry( vCore, k++, Entry );
}
Vec_IntShrink( vCore, k );
Vec_IntFree( vPres );
if ( fVerbose )
{
printf( "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return vCore;
}
/**Function*************************************************************
Synopsis [Remaps core into frame/node pairs.] Synopsis [Remaps core into frame/node pairs.]
Description [] Description []
...@@ -460,7 +389,9 @@ void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore ) ...@@ -460,7 +389,9 @@ void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore )
pThis = Vta_ManObj( p, Entry ); pThis = Vta_ManObj( p, Entry );
Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj; Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj;
Vec_IntWriteEntry( vCore, i, Entry ); Vec_IntWriteEntry( vCore, i, Entry );
//printf( "%d^%d ", pThis->iObj, pThis->iFrame );
} }
//printf( "\n" );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -804,7 +735,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p ) ...@@ -804,7 +735,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
} }
// add clauses // add clauses
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i ) Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
Vga_ManAddClausesOne( p, pThis ); Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
} }
Vec_PtrFree( vTermsUsed ); Vec_PtrFree( vTermsUsed );
...@@ -827,38 +758,43 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) ...@@ -827,38 +758,43 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
{ {
Vta_Man_t * p; Vta_Man_t * p;
p = ABC_CALLOC( Vta_Man_t, 1 ); p = ABC_CALLOC( Vta_Man_t, 1 );
p->pGia = pGia; p->pGia = pGia;
p->pPars = pPars; p->pPars = pPars;
// internal data // internal data
p->nObjsAlloc = (1 << 20); p->nObjsAlloc = (1 << 20);
p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc ); p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
p->nObjs = 1; p->nObjs = 1;
p->nBins = Abc_PrimeCudd( p->nObjsAlloc/2 ); p->nBins = Abc_PrimeCudd( p->nObjsAlloc/2 );
p->pBins = ABC_CALLOC( int, p->nBins ); p->pBins = ABC_CALLOC( int, p->nBins );
p->vOrder = Vec_IntAlloc( 1013 ); p->vOrder = Vec_IntAlloc( 1013 );
// abstraction // abstraction
p->nObjBits = Gia_Base2Log( Gia_ManObjNum(pGia) ); p->nObjBits = Gia_Base2Log( Gia_ManObjNum(pGia) );
p->nObjMask = (1 << p->nObjBits) - 1; p->nObjMask = (1 << p->nObjBits) - 1;
assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask ); assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
p->nWords = 1; p->nWords = 1;
p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords ); p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
// start the abstraction // start the abstraction
if ( pGia->vObjClasses == NULL ) if ( pGia->vObjClasses == NULL )
p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart ); p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
else else
{ {
p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses ); p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
// update parameters // update parameters
if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) ) if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) )
printf( "Starting frame count is set in accordance with abstraction (%d).\n", Vec_PtrSize(p->vFrames) ); {
pPars->nFramesStart = Vec_PtrSize(p->vFrames); printf( "Starting frame count is changed to match the abstraction (from %d to %d).\n", pPars->nFramesStart, Vec_PtrSize(p->vFrames) );
if ( pPars->nFramesMax ) pPars->nFramesStart = Vec_PtrSize(p->vFrames);
}
if ( pPars->nFramesMax && pPars->nFramesMax < pPars->nFramesStart )
{
printf( "Maximum frame count is changed to match the starting frames (from %d to %d).\n", pPars->nFramesMax, pPars->nFramesStart );
pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart ); pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart );
}
} }
// other data // other data
p->vCla2Var = Vec_IntAlloc( 1000 ); p->vCla2Var = Vec_IntAlloc( 1000 );
p->vCores = Vec_PtrAlloc( 100 ); p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new(); p->pSat = sat_solver2_new();
return p; return p;
} }
...@@ -888,6 +824,82 @@ void Vga_ManStop( Vta_Man_t * p ) ...@@ -888,6 +824,82 @@ void Vga_ManStop( Vta_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Finds the set of clauses involved in the UNSAT core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue )
{
Vec_Int_t * vPres;
Vec_Int_t * vCore;
int k, i, Entry, RetValue, clk = clock();
int nConfPrev = pSat->stats.conflicts;
if ( piRetValue )
*piRetValue = 1;
// 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 ( RetValue == l_Undef )
{
// if ( fVerbose )
printf( "Conflict limit is reached.\n" );
if ( piRetValue )
*piRetValue = -1;
return NULL;
}
if ( RetValue == l_True )
{
// if ( fVerbose )
printf( "The BMC problem is SAT.\n" );
if ( piRetValue )
*piRetValue = 0;
return NULL;
}
if ( fVerbose )
{
printf( "%6d", (int)pSat->stats.conflicts - nConfPrev );
// printf( "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
assert( RetValue == l_False );
// derive the UNSAT core
clk = clock();
vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
if ( fVerbose )
{
// printf( "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
// remap core into variables
clk = clock();
vPres = Vec_IntStart( sat_solver2_nvars(pSat) );
k = 0;
Vec_IntForEachEntry( vCore, Entry, i )
{
Entry = Vec_IntEntry(vCla2Var, Entry);
if ( Vec_IntEntry(vPres, Entry) )
continue;
Vec_IntWriteEntry( vPres, Entry, 1 );
Vec_IntWriteEntry( vCore, k++, Entry );
}
Vec_IntShrink( vCore, k );
Vec_IntFree( vPres );
if ( fVerbose )
{
// printf( "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
return vCore;
}
/**Function*************************************************************
Synopsis [] Synopsis []
Description [] Description []
...@@ -918,12 +930,13 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames ) ...@@ -918,12 +930,13 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
} }
pCountAll[iFrame+1]++; pCountAll[iFrame+1]++;
pCountAll[0]++; pCountAll[0]++;
printf( "%5d%5d ", pCountAll[0], pCountUni[0] );
for ( k = 0; k < nFrames; k++ )
printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] );
printf( "\n" );
} }
// printf( "%5d%5d", pCountAll[0], pCountUni[0] );
printf( "%7d", pCountAll[0] );
for ( k = 0; k < nFrames; k++ )
// printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] );
printf( "%4d", pCountAll[k+1] );
printf( "\n" );
ABC_FREE( pCountAll ); ABC_FREE( pCountAll );
ABC_FREE( pCountUni ); ABC_FREE( pCountUni );
} }
...@@ -939,59 +952,56 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames ) ...@@ -939,59 +952,56 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis ) void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
{ {
Vta_Obj_t * pThis0, * pThis1; Vta_Obj_t * pThis0, * pThis1;
Gia_Obj_t * pObj; Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
int i = Vta_ObjId( p, pThis ); Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
assert( !pThis->fAdded && !pThis->fNew ); int iMainVar = Vta_ObjId(p, pThis);
pObj = Gia_ManObj( p->pGia, pThis->iObj ); assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
assert( pThis->fAdded == 0 );
pThis->fAdded = 1;
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
{ {
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame ); pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame ); pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
if ( pThis0 && pThis1 ) sat_solver2_add_and( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Vta_ObjId(p, pThis1),
{ Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
pThis->fAdded = 1; Vec_IntPush( p->vCla2Var, iMainVar );
sat_solver2_add_and( p->pSat, Vec_IntPush( p->vCla2Var, iMainVar );
Vta_ObjId(p, pThis), Vta_ObjId(p, pThis0), Vta_ObjId(p, pThis1), Vec_IntPush( p->vCla2Var, iMainVar );
Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); //printf( "Adding node %d (var %d)\n", iObj, iMainVar );
Vec_IntPush( p->vCla2Var, i );
Vec_IntPush( p->vCla2Var, i );
Vec_IntPush( p->vCla2Var, i );
}
} }
else if ( Gia_ObjIsRo(p->pGia, pObj) ) else if ( Gia_ObjIsRo(p->pGia, pObj) )
{ {
if ( pThis->iFrame == 0 ) //printf( "Adding flop %d (var %d)\n", iObj, iMainVar );
if ( iFrame == 0 )
{ {
pThis->fAdded = 1; /*
sat_solver2_add_constraint( p->pSat, pThis->iObj, 1, 0 ); pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
Vec_IntPush( p->vCla2Var, i ); sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0 );
Vec_IntPush( p->vCla2Var, i ); Vec_IntPush( p->vCla2Var, iMainVar );
Vec_IntPush( p->vCla2Var, iMainVar );
*/
sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
Vec_IntPush( p->vCla2Var, iMainVar );
} }
else else
{ {
pObj = Gia_ObjRoToRi( p->pGia, pObj ); pObj = Gia_ObjRoToRi( p->pGia, pObj );
pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 ); pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
if ( pThis0 ) sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0 );
{ Vec_IntPush( p->vCla2Var, iMainVar );
pThis->fAdded = 1; Vec_IntPush( p->vCla2Var, iMainVar );
sat_solver2_add_buffer( p->pSat,
Vta_ObjId(p, pThis), Vta_ObjId(p, pThis0),
Gia_ObjFaninC0(pObj), 0 );
Vec_IntPush( p->vCla2Var, i );
Vec_IntPush( p->vCla2Var, i );
}
} }
} }
else if ( Gia_ObjIsConst0(pObj) ) else if ( Gia_ObjIsConst0(pObj) )
{ {
pThis->fAdded = 1; //printf( "Adding const %d (var %d)\n", iObj, iMainVar );
sat_solver2_add_const( p->pSat, Vta_ObjId(p, pThis), 1, 0 ); sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
Vec_IntPush( p->vCla2Var, i ); Vec_IntPush( p->vCla2Var, iMainVar );
} }
else if ( !Gia_ObjIsPi(p->pGia, pObj) ) else //if ( !Gia_ObjIsPi(p->pGia, pObj) )
assert( 0 ); assert( 0 );
} }
...@@ -1008,25 +1018,28 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis ) ...@@ -1008,25 +1018,28 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, Vta_Obj_t * pThis )
***********************************************************************/ ***********************************************************************/
void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift ) void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
{ {
Gia_Obj_t * pObj; int i, Entry;
Vta_Obj_t * pThis;
int i, Entry, iObjPrev = p->nObjs;
Vec_IntForEachEntry( vOne, Entry, i ) Vec_IntForEachEntry( vOne, Entry, i )
{ Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
pObj = Gia_ManObj( p->pGia, Entry & p->nObjMask ); }
if ( Gia_ObjIsPi(p->pGia, pObj) )
continue; /**Function*************************************************************
pThis = Vga_ManFindOrAdd( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
pThis->fNew = 0; Synopsis [Returns the output literal.]
// add constraint variable
if ( Gia_ObjIsRo(p->pGia, pObj) && (Entry >> p->nObjBits) + Lift == 0 ) Description []
{
pThis = Vga_ManFindOrAdd( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift ); SideEffects []
pThis->fNew = 0;
} SeeAlso []
}
for ( i = iObjPrev; i < p->nObjs; i++ ) ***********************************************************************/
Vga_ManAddClausesOne( p, Vta_ManObj(p, i) ); static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
{
Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
assert( pThis != NULL && pThis->fAdded );
return Gia_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1043,19 +1056,24 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift ) ...@@ -1043,19 +1056,24 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{ {
Vta_Man_t * p; Vta_Man_t * p;
Vta_Obj_t * pThis;
Vec_Int_t * vCore; Vec_Int_t * vCore;
Abc_Cex_t * pCex = NULL; Abc_Cex_t * pCex = NULL;
int f, i, Limit, Status, RetValue = -1; Gia_Obj_t * pObj;
int i, f, Status, RetValue = -1;
// preconditions // preconditions
assert( Gia_ManPoNum(pAig) == 1 ); assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
// start the manager // start the manager
p = Vga_ManStart( pAig, pPars ); p = Vga_ManStart( pAig, pPars );
// perform initial abstraction // perform initial abstraction
if ( p->pPars->fVerbose )
printf( "Frame Confl All F0 F1 F2 F3 ...\n" );
for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{ {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
printf( "Frame %4d : ", f ); printf( "%3d :", f );
//printf( "\n" );
p->pPars->iFrame = f; p->pPars->iFrame = f;
// realloc storage for abstraction marks // realloc storage for abstraction marks
if ( f == p->nWords * 32 ) if ( f == p->nWords * 32 )
...@@ -1065,43 +1083,54 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1065,43 +1083,54 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{ {
// load this timeframe // load this timeframe
Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 ); Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 );
// Vga_ManAddClausesOne( p, 0, f );
// run SAT solver // run SAT solver
vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status ); vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status );
if ( vCore == NULL && Status == 0 ) assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 )
break;
if ( Status == 0 )
{ {
// make sure, there was no initial abstraction (otherwise, it was invalid) // make sure, there was no initial abstraction (otherwise, it was invalid)
assert( pAig->vObjClasses == NULL ); assert( pAig->vObjClasses == NULL );
// derive counter-example // derive counter-example
pCex = NULL; pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
pCex->iPo = 0;
pCex->iFrame = p->pPars->iFrame;
Vta_ManForEachObj( p, pThis, i )
{
pObj = Gia_ManObj( p->pGia, pThis->iObj );
if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
}
} }
} }
else else
{ {
break; /*
// load the time frame // load the time frame
Limit = Abc_MinInt(3, p->pPars->nFramesStart); int Limit = Abc_MinInt(3, p->pPars->nFramesStart);
for ( i = 1; i <= Limit; i++ ) for ( i = 1; i <= Limit; i++ )
Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i ); Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i );
// Vga_ManAddClausesOne( p, 0, f );
// iterate as long as there are counter-examples // iterate as long as there are counter-examples
while ( 1 ) do {
{ vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status );
vCore = Vta_ManUnsatCore( p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &RetValue ); assert( (vCore != NULL) == (Status == 1) );
if ( RetValue ) // resource limit is reached if ( Status == -1 ) // resource limit is reached
{
assert( vCore == NULL );
break; break;
}
if ( vCore != NULL ) if ( vCore != NULL )
{ {
// unroll the solver, add the core // rollback and add the core
// return and double check // return and double check
break; break;
} }
pCex = Vta_ManRefineAbstraction( p ); pCex = Vta_ManRefineAbstraction( p );
if ( pCex != NULL ) }
break; while ( pCex == NULL );
} if ( Status == -1 ) // resource limit is reached
break;
*/
} }
if ( pCex != NULL ) if ( pCex != NULL )
{ {
...@@ -1121,7 +1150,11 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1121,7 +1150,11 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// print the result // print the result
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Vta_ManAbsPrintFrame( p, vCore, f+1 ); Vta_ManAbsPrintFrame( p, vCore, f+1 );
if ( f == p->pPars->nFramesStart-1 )
break;
} }
// analize the results
if ( pCex == NULL ) if ( pCex == NULL )
{ {
assert( Vec_PtrSize(p->vCores) > 0 ); assert( Vec_PtrSize(p->vCores) > 0 );
...@@ -1129,6 +1162,17 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) ...@@ -1129,6 +1162,17 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
printf( "Replacing the old abstraction by a new one.\n" ); printf( "Replacing the old abstraction by a new one.\n" );
Vec_IntFreeP( &pAig->vObjClasses ); Vec_IntFreeP( &pAig->vObjClasses );
pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
if ( Status == -1 )
printf( "SAT solver ran out of resources at %d conflicts in frame %d.\n", pPars->nConfLimit, f );
else
printf( "SAT solver completed %d frames and produced an abstraction.\n", f+1 );
}
else
{
ABC_FREE( p->pGia->pCexSeq );
p->pGia->pCexSeq = pCex;
if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
printf( "Gia_VtaPerform(): CEX verification has failed!\n" );
} }
Vga_ManStop( p ); Vga_ManStop( p );
return RetValue; return RetValue;
......
src/aig/gia/giaFrames.c
...@@ -189,11 +189,12 @@ Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames ) ...@@ -189,11 +189,12 @@ Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames )
iStop = (f+1 < Vec_IntSize(vLimit)) ? Vec_IntEntry(vLimit, f+1) : 0; iStop = (f+1 < Vec_IntSize(vLimit)) ? Vec_IntEntry(vLimit, f+1) : 0;
for ( k = iStop - 1; k >= iStart; k-- ) for ( k = iStop - 1; k >= iStart; k-- )
{ {
pObj = Gia_ManObj(pNew, k); assert( Gia_ManObj(pNew, k)->Value > 0 );
if ( Gia_ObjIsCo(pObj) ) pObj = Gia_ManObj(p, Gia_ManObj(pNew, k)->Value);
if ( Gia_ObjIsCo(pObj) || Gia_ObjIsPi(p, pObj) )
continue; continue;
assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) );
Entry = ((fMax-f) << nObjBits) | pObj->Value; Entry = ((fMax-f) << nObjBits) | Gia_ObjId(p, pObj);
Vec_IntPush( vOne, Entry ); Vec_IntPush( vOne, Entry );
// printf( "%d ", Gia_ManObj(pNew, k)->Value ); // printf( "%d ", Gia_ManObj(pNew, k)->Value );
} }
......
src/aig/gia/giaMan.c
...@@ -277,6 +277,7 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) ...@@ -277,6 +277,7 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
nObjMask = (1 << nObjBits) - 1; nObjMask = (1 << nObjBits) - 1;
assert( Gia_ManObjNum(p) <= nObjMask ); assert( Gia_ManObjNum(p) <= nObjMask );
// print info about frames // print info about frames
printf( "Frame All F0 F1 F2 F3 ...\n" );
for ( i = 0; i < nFrames; i++ ) for ( i = 0; i < nFrames; i++ )
{ {
iStart = Vec_IntEntry( vAbs, i+1 ); iStart = Vec_IntEntry( vAbs, i+1 );
...@@ -298,10 +299,13 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) ...@@ -298,10 +299,13 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
pCountAll[0]++; pCountAll[0]++;
} }
assert( pCountAll[0] == (unsigned)(iStop - iStart) ); assert( pCountAll[0] == (unsigned)(iStop - iStart) );
printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); // printf( "%5d%5d ", pCountAll[0], pCountUni[0] );
printf( "%3d :", i );
printf( "%6d", pCountAll[0] );
for ( k = 0; k < nFrames; k++ ) for ( k = 0; k < nFrames; k++ )
if ( k <= i ) if ( k <= i )
printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); // printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] );
printf( "%4d", pCountAll[k+1] );
printf( "\n" ); printf( "\n" );
} }
assert( iStop == Vec_IntSize(vAbs) ); assert( iStop == Vec_IntSize(vAbs) );
......
src/sat/bsat/satProof.c
...@@ -443,12 +443,13 @@ void Sat_ProofCheck( sat_solver2 * s ) ...@@ -443,12 +443,13 @@ void Sat_ProofCheck( sat_solver2 * s )
{ {
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Vec_Rec_t * vResolves; Vec_Rec_t * vResolves;
Vec_Int_t * vUsed, * vTemp; Vec_Int_t * vUsed, * vTemp;
satset * pSet, * pSet0, * pSet1; satset * pSet, * pSet0, * pSet1;
int i, k, Handle, Counter = 0, clk = clock(); int i, k, hRoot, Handle, Counter = 0, clk = clock();
if ( s->hLearntLast < 0 )
return;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
// collect visited clauses // collect visited clauses
vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
Proof_CleanCollected( vProof, vUsed ); Proof_CleanCollected( vProof, vUsed );
...@@ -509,7 +510,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ ...@@ -509,7 +510,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
if ( pFanin && !pFanin->mark ) if ( pFanin && !pFanin->mark )
{ {
pFanin->mark = 1; pFanin->mark = 1;
Vec_IntPush( vCore, pNode->pEnts[i] >> 2 ); Vec_IntPush( vCore, pNode->pEnts[k] >> 2 );
} }
} }
// clean core clauses and reexpress core in terms of clause IDs // clean core clauses and reexpress core in terms of clause IDs
...@@ -586,13 +587,14 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) ...@@ -586,13 +587,14 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
satset * pNode, * pFanin; satset * pNode, * pFanin;
Aig_Man_t * pAig; Aig_Man_t * pAig;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i, k, iVar, Lit, Entry; int i, k, iVar, Lit, Entry, hRoot;
if ( s->hLearntLast < 0 )
return NULL;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Sat_ProofInterpolantCheckVars( s, vGlobVars ); Sat_ProofInterpolantCheckVars( s, vGlobVars );
...@@ -683,16 +685,17 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) ...@@ -683,16 +685,17 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
satset * pNode, * pFanin; satset * pNode, * pFanin;
Tru_Man_t * pTru; Tru_Man_t * pTru;
int nVars = Vec_IntSize(vGlobVars); int nVars = Vec_IntSize(vGlobVars);
int nWords = (nVars < 6) ? 1 : (1 << (nVars-6)); int nWords = (nVars < 6) ? 1 : (1 << (nVars-6));
word * pRes = ABC_ALLOC( word, nWords ); word * pRes = ABC_ALLOC( word, nWords );
int i, k, iVar, Lit, Entry; int i, k, iVar, Lit, Entry, hRoot;
assert( nVars > 0 && nVars <= 16 ); assert( nVars > 0 && nVars <= 16 );
if ( s->hLearntLast < 0 )
return NULL;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Sat_ProofInterpolantCheckVars( s, vGlobVars ); Sat_ProofInterpolantCheckVars( s, vGlobVars );
...@@ -789,9 +792,11 @@ void * Sat_ProofCore( sat_solver2 * s ) ...@@ -789,9 +792,11 @@ void * Sat_ProofCore( sat_solver2 * s )
{ {
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
Vec_Int_t * vCore, * vUsed; Vec_Int_t * vCore, * vUsed;
int hRoot;
if ( s->hLearntLast < 0 )
return NULL;
hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
// collect visited clauses // collect visited clauses
vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
// collect core clauses // collect core clauses
......
src/sat/bsat/satSolver.h
...@@ -292,19 +292,19 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i ...@@ -292,19 +292,19 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i
assert( Cid ); assert( Cid );
return 4; return 4;
} }
static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int fCompl ) static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int iVar2, int fCompl )
{ {
lit Lits[2]; lit Lits[2];
int Cid; int Cid;
assert( iVar >= 0 ); assert( iVar >= 0 );
Lits[0] = toLitCond( iVar, fCompl ); Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar+1, 0 ); Lits[1] = toLitCond( iVar2, 0 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 ); Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid ); assert( Cid );
Lits[0] = toLitCond( iVar, fCompl ); Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar+1, 1 ); Lits[1] = toLitCond( iVar2, 1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 ); Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid ); assert( Cid );
return 2; return 2;
......
src/sat/bsat/satSolver2.c
...@@ -150,7 +150,8 @@ static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1 ...@@ -150,7 +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 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 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 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]); 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 // 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; } int clause_is_partA (sat_solver2* s, int h) { return clause_read(s, h)->partA; }
...@@ -1102,7 +1103,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) ...@@ -1102,7 +1103,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
if (solver2_dlevel(s) <= s->root_level){ if (solver2_dlevel(s) <= s->root_level){
#ifdef SAT_USE_ANALYZE_FINAL #ifdef SAT_USE_ANALYZE_FINAL
proof_id = solver2_analyze_final(s, confl, 0); proof_id = solver2_analyze_final(s, confl, 0);
if ( proof_id > 0 ) assert( proof_id > 0 );
// if ( proof_id > 0 )
solver2_record(s,&s->conf_final, proof_id); solver2_record(s,&s->conf_final, proof_id);
#endif #endif
veci_delete(&learnt_clause); veci_delete(&learnt_clause);
...@@ -1307,11 +1309,11 @@ void sat_solver2_setnvars(sat_solver2* s,int n) ...@@ -1307,11 +1309,11 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
void sat_solver2_delete(sat_solver2* s) void sat_solver2_delete(sat_solver2* s)
{ {
veci * pCore; // veci * pCore;
// report statistics // report statistics
printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits ); printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits );
/*
pCore = Sat_ProofCore( s ); pCore = Sat_ProofCore( s );
printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
veci_delete( pCore ); veci_delete( pCore );
...@@ -1319,7 +1321,7 @@ void sat_solver2_delete(sat_solver2* s) ...@@ -1319,7 +1321,7 @@ void sat_solver2_delete(sat_solver2* s)
if ( s->fProofLogging ) if ( s->fProofLogging )
Sat_ProofCheck( s ); Sat_ProofCheck( s );
*/
// delete vectors // delete vectors
veci_delete(&s->order); veci_delete(&s->order);
veci_delete(&s->trail_lim); veci_delete(&s->trail_lim);
...@@ -1392,7 +1394,7 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) ...@@ -1392,7 +1394,7 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end)
// delete duplicates // delete duplicates
last = lit_Undef; last = lit_Undef;
for (i = j = begin; i < end; i++){ for (i = j = begin; i < end; i++){
//printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -var_value(s, lit_var(*i)) : var_value(s, lit_var(*i))));
if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i)) if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
return true; // tautology return true; // tautology
else if (*i != last && var_value(s, lit_var(*i)) == varX) else if (*i != last && var_value(s, lit_var(*i)) == varX)
...@@ -1634,9 +1636,9 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -1634,9 +1636,9 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
int restart_iter = 0; int restart_iter = 0;
ABC_INT64_T nof_conflicts; ABC_INT64_T nof_conflicts;
ABC_INT64_T nof_learnts = sat_solver2_nclauses(s) / 3; ABC_INT64_T nof_learnts = sat_solver2_nclauses(s) / 3;
lbool status = l_Undef; lbool status = l_Undef;
// lbool* values = s->assigns; int proof_id;
lit* i; lit * i;
s->hLearntLast = -1; s->hLearntLast = -1;
...@@ -1659,7 +1661,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -1659,7 +1661,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
//printf("solve: "); printlits(begin, end); printf("\n"); //printf("solve: "); printlits(begin, end); printf("\n");
for (i = begin; i < end; i++){ for (i = begin; i < end; i++){
// switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
switch (var_value(s, *i)) { switch (var_value(s, *i)) {
case var1: // l_True: case var1: // l_True:
break; break;
...@@ -1723,17 +1724,19 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -1723,17 +1724,19 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
if (r != NULL) if (r != NULL)
{ {
satset* confl = r; satset* confl = r;
solver2_analyze_final(s, confl, 1); proof_id = solver2_analyze_final(s, confl, 1);
veci_push(&s->conf_final, lit_neg(p)); veci_push(&s->conf_final, lit_neg(p));
} }
else else
{ {
proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
veci_resize(&s->conf_final,0); veci_resize(&s->conf_final,0);
veci_push(&s->conf_final, lit_neg(p)); veci_push(&s->conf_final, lit_neg(p));
// the two lines below are a bug fix by Siert Wieringa // the two lines below are a bug fix by Siert Wieringa
if (var_level(s, lit_var(p)) > 0) if (var_level(s, lit_var(p)) > 0)
veci_push(&s->conf_final, p); veci_push(&s->conf_final, p);
} }
solver2_record(s, &s->conf_final, proof_id);
solver2_canceluntil(s, 0); solver2_canceluntil(s, 0);
return l_False; return l_False;
} }
...@@ -1741,9 +1744,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -1741,9 +1744,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
{ {
satset* confl = solver2_propagate(s); satset* confl = solver2_propagate(s);
if (confl != NULL){ if (confl != NULL){
solver2_analyze_final(s, confl, 0); proof_id = solver2_analyze_final(s, confl, 0);
assert(s->conf_final.size > 0); assert(s->conf_final.size > 0);
solver2_canceluntil(s, 0); solver2_canceluntil(s, 0);
solver2_record(s,&s->conf_final, proof_id);
return l_False; return l_False;
} }
} }
......
src/sat/bsat/satSolver2.h
...@@ -355,20 +355,20 @@ static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, ...@@ -355,20 +355,20 @@ static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB,
clause_set_partA( pSat, Cid, 1 ); clause_set_partA( pSat, Cid, 1 );
return 4; return 4;
} }
static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark )
{ {
lit Lits[2]; lit Lits[2];
int Cid; int Cid;
assert( iVar >= 0 ); assert( iVar >= 0 );
Lits[0] = toLitCond( iVar, fCompl ); Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar+1, 0 ); Lits[1] = toLitCond( iVar2, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark ) if ( fMark )
clause_set_partA( pSat, Cid, 1 ); clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVar, fCompl ); Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar+1, 1 ); Lits[1] = toLitCond( iVar2, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark ) if ( fMark )
clause_set_partA( pSat, Cid, 1 ); clause_set_partA( pSat, Cid, 1 );
......
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