/**CFile****************************************************************
FileName [satProof2.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver.]
Synopsis [Proof logging.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 1, 2004.]
Revision [$Id: satProof2.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__sat__bsat__satProof2_h
#define ABC__sat__bsat__satProof2_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "misc/vec/vec.h"
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Prf_Man_t_ Prf_Man_t;
struct Prf_Man_t_
{
int iFirst; // first learned clause with proof
int iFirst2; // first learned clause with proof
int nWords; // the number of proof words
word * pInfo; // pointer to the current proof
Vec_Wrd_t * vInfo; // proof information
Vec_Int_t * vSaved; // IDs of saved clauses
Vec_Int_t * vId2Pr; // mapping proof IDs of problem clauses into bitshifts (user's array)
};
////////////////////////////////////////////////////////////////////////
/// GLOBAL VARIABLES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Prf_BitWordNum( int nWidth ) { return (nWidth >> 6) + ((nWidth & 63) > 0); }
static inline int Prf_ManSize( Prf_Man_t * p ) { return Vec_WrdSize( p->vInfo ) / p->nWords; }
static inline void Prf_ManClearNewInfo( Prf_Man_t * p ) { int w; for ( w = 0; w < p->nWords; w++ ) Vec_WrdPush( p->vInfo, 0 ); }
static inline word * Prf_ManClauseInfo( Prf_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vInfo, Id * p->nWords ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Prf_Man_t * Prf_ManAlloc()
{
Prf_Man_t * p;
p = ABC_CALLOC( Prf_Man_t, 1 );
p->iFirst = -1;
p->iFirst2 = -1;
p->vInfo = Vec_WrdAlloc( 1000 );
p->vSaved = Vec_IntAlloc( 1000 );
return p;
}
static inline void Prf_ManStop( Prf_Man_t * p )
{
if ( p == NULL )
return;
Vec_IntFree( p->vSaved );
Vec_WrdFree( p->vInfo );
ABC_FREE( p );
}
static inline void Prf_ManStopP( Prf_Man_t ** p )
{
Prf_ManStop( *p );
*p = NULL;
}
static inline double Prf_ManMemory( Prf_Man_t * p )
{
return Vec_WrdMemory(p->vInfo) + Vec_IntMemory(p->vSaved) + sizeof(Prf_Man_t);
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Prf_ManRestart( Prf_Man_t * p, Vec_Int_t * vId2Pr, int iFirst, int nWidth )
{
assert( p->iFirst == -1 );
p->iFirst = iFirst;
p->nWords = Prf_BitWordNum( nWidth );
p->vId2Pr = vId2Pr;
p->pInfo = NULL;
Vec_WrdClear( p->vInfo );
}
static inline void Prf_ManGrow( Prf_Man_t * p, int nWidth )
{
Vec_Wrd_t * vInfoNew;
int i, w, nSize, nWordsNew;
assert( p->iFirst >= 0 );
assert( p->pInfo == NULL );
if ( nWidth < 64 * p->nWords )
return;
// get word count after resizing
nWordsNew = Abc_MaxInt( Prf_BitWordNum(nWidth), 2 * p->nWords );
// remap the entries
nSize = Prf_ManSize( p );
vInfoNew = Vec_WrdAlloc( (nSize + 1000) * nWordsNew );
for ( i = 0; i < nSize; i++ )
{
p->pInfo = Prf_ManClauseInfo( p, i );
for ( w = 0; w < p->nWords; w++ )
Vec_WrdPush( vInfoNew, p->pInfo[w] );
for ( ; w < nWordsNew; w++ )
Vec_WrdPush( vInfoNew, 0 );
}
Vec_WrdFree( p->vInfo );
p->vInfo = vInfoNew;
p->nWords = nWordsNew;
p->pInfo = NULL;
}
static inline void Prf_ManShrink( Prf_Man_t * p, int iClause )
{
assert( p->iFirst >= 0 );
assert( iClause - p->iFirst >= 0 );
assert( iClause - p->iFirst < Prf_ManSize(p) );
Vec_WrdShrink( p->vInfo, (iClause - p->iFirst) * p->nWords );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Prf_ManAddSaved( Prf_Man_t * p, int i, int iNew )
{
assert( p->iFirst >= 0 );
if ( i < p->iFirst )
return;
if ( Vec_IntSize(p->vSaved) == 0 )
{
assert( p->iFirst2 == -1 );
p->iFirst2 = iNew;
}
Vec_IntPush( p->vSaved, i );
}
static inline void Prf_ManCompact( Prf_Man_t * p, int iNew )
{
int i, w, k = 0, Entry, nSize;
assert( p->iFirst >= 0 );
assert( p->pInfo == NULL );
nSize = Prf_ManSize( p );
Vec_IntForEachEntry( p->vSaved, Entry, i )
{
assert( Entry - p->iFirst >= 0 && Entry - p->iFirst < nSize );
p->pInfo = Prf_ManClauseInfo( p, Entry - p->iFirst );
for ( w = 0; w < p->nWords; w++ )
Vec_WrdWriteEntry( p->vInfo, k++, p->pInfo[w] );
}
Vec_WrdShrink( p->vInfo, k );
Vec_IntClear( p->vSaved );
p->pInfo = NULL;
// update first
if ( p->iFirst2 == -1 )
p->iFirst = iNew;
else
p->iFirst = p->iFirst2;
p->iFirst2 = -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Prf_ManChainResolve( Prf_Man_t * p, clause * c )
{
assert( p->iFirst >= 0 );
assert( p->pInfo != NULL );
// add to proof info
if ( c->lrn ) // learned clause
{
if ( clause_id(c) >= p->iFirst )
{
word * pProofStart;
int w;
assert( clause_id(c) - p->iFirst >= 0 );
assert( clause_id(c) - p->iFirst < Prf_ManSize(p) );
pProofStart = Prf_ManClauseInfo( p, clause_id(c) - p->iFirst );
for ( w = 0; w < p->nWords; w++ )
p->pInfo[w] |= pProofStart[w];
}
}
else // problem clause
{
if ( clause_id(c) >= 0 ) // has proof ID
{
int Entry;
if ( p->vId2Pr == NULL )
Entry = clause_id(c);
else
Entry = Vec_IntEntry( p->vId2Pr, clause_id(c) );
if ( Entry >= 0 )
{
assert( Entry < 64 * p->nWords );
Abc_InfoSetBit( (unsigned *)p->pInfo, Entry );
}
}
}
}
static inline void Prf_ManChainStart( Prf_Man_t * p, clause * c )
{
assert( p->iFirst >= 0 );
// prepare info for new clause
Prf_ManClearNewInfo( p );
// get pointer to the proof
assert( p->pInfo == NULL );
p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
// add to proof info
Prf_ManChainResolve( p, c );
}
static inline int Prf_ManChainStop( Prf_Man_t * p )
{
assert( p->pInfo != NULL );
p->pInfo = NULL;
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
{
Vec_Int_t * vCore;
int i, Entry;
assert( p->iFirst >= 0 );
assert( p->pInfo == NULL );
assert( Prf_ManSize(p) > 0 );
vCore = Vec_IntAlloc( 64 * p->nWords );
p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
if ( p->vId2Pr == NULL )
{
for ( i = 0; i < 64 * p->nWords; i++ )
if ( Abc_InfoHasBit( (unsigned *)p->pInfo, i ) )
Vec_IntPush( vCore, i );
}
else
{
Vec_IntForEachEntry( p->vId2Pr, Entry, i )
{
if ( Entry < 0 )
continue;
assert( Entry < 64 * p->nWords );
if ( Abc_InfoHasBit( (unsigned *)p->pInfo, Entry ) )
Vec_IntPush( vCore, i );
}
}
p->pInfo = NULL;
Vec_IntSort( vCore, 1 );
return vCore;
}
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////