/**CFile****************************************************************
FileName [giaCSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [A simple circuit-based solver.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Cbs3_Par_t_ Cbs3_Par_t;
struct Cbs3_Par_t_
{
// conflict limits
int nBTLimit; // limit on the number of conflicts
int nJustLimit; // limit on the size of justification queue
int nRestLimit; // limit on the number of restarts
// current parameters
int nBTThis; // number of conflicts
int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier
// other
int fVerbose;
};
typedef struct Cbs3_Que_t_ Cbs3_Que_t;
struct Cbs3_Que_t_
{
int iHead; // beginning of the queue
int iTail; // end of the queue
int nSize; // allocated size
int * pData; // nodes stored in the queue
};
typedef struct Cbs3_Man_t_ Cbs3_Man_t;
struct Cbs3_Man_t_
{
Cbs3_Par_t Pars; // parameters
Gia_Man_t * pAig; // AIG manager
Cbs3_Que_t pProp; // propagation queue
Cbs3_Que_t pJust; // justification queue
Cbs3_Que_t pClauses; // clause queue
Vec_Int_t * vModel; // satisfying assignment
Vec_Int_t * vTemp; // temporary storage
// circuit structure
int nVars;
int nVarsAlloc;
int var_inc;
Vec_Int_t vMap;
Vec_Int_t vRef;
Vec_Int_t vFans;
Vec_Wec_t vImps;
// internal data
Vec_Str_t vAssign;
Vec_Str_t vMark;
Vec_Int_t vLevReason;
Vec_Int_t vActs;
Vec_Int_t vWatches;
Vec_Int_t vWatchUpds;
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
int nSatUndec; // the number of timeouts
int nSatTotal; // the number of calls
// conflicts
int nConfUnsat; // conflicts in unsat problems
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
abctime timeJFront;
abctime timeSatLoad; // SAT solver loading time
abctime timeSatUnsat; // unsat
abctime timeSatSat; // sat
abctime timeSatUndec; // undecided
abctime timeTotal; // total runtime
// other statistics
int nPropCalls[3];
int nFails[2];
int nClauseConf;
int nDecs;
};
static inline int Cbs3_VarUnused( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry(&p->vLevReason, 3*iVar) == -1; }
static inline void Cbs3_VarSetUnused( Cbs3_Man_t * p, int iVar ) { Vec_IntWriteEntry(&p->vLevReason, 3*iVar, -1); }
static inline int Cbs3_VarMark0( Cbs3_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vMark, iVar); }
static inline void Cbs3_VarSetMark0( Cbs3_Man_t * p, int iVar, int Value ) { Vec_StrWriteEntry(&p->vMark, iVar, (char)Value); }
static inline int Cbs3_VarIsAssigned( Cbs3_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar) < 2; }
static inline void Cbs3_VarUnassign( Cbs3_Man_t * p, int iVar ) { assert( Cbs3_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)(2+Vec_StrEntry(&p->vAssign, iVar))); Cbs3_VarSetUnused(p, iVar); }
static inline int Cbs3_VarValue( Cbs3_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar); }
static inline void Cbs3_VarSetValue( Cbs3_Man_t * p, int iVar, int v ) { assert( !Cbs3_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)v); }
static inline int Cbs3_VarLit0( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 0) ); }
static inline int Cbs3_VarLit1( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 1) ); }
static inline int Cbs3_VarIsPi( Cbs3_Man_t * p, int iVar ) { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 0) ) == 0; }
static inline int Cbs3_VarIsJust( Cbs3_Man_t * p, int iVar ) { int * pLits = Vec_IntEntryP(&p->vFans, Abc_Var2Lit(iVar, 0)); return pLits[0] > 0 && Cbs3_VarValue(p, Abc_Lit2Var(pLits[0])) >= 2 && Cbs3_VarValue(p, Abc_Lit2Var(pLits[1])) >= 2; }
static inline int Cbs3_VarDecLevel( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar); }
static inline int Cbs3_VarReason0( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+1); }
static inline int Cbs3_VarReason1( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+2); }
static inline int * Cbs3_VarReasonP( Cbs3_Man_t * p, int iVar ) { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntryP(&p->vLevReason, 3*iVar+1); }
static inline int Cbs3_ClauseDecLevel( Cbs3_Man_t * p, int hClause ) { return Cbs3_VarDecLevel( p, p->pClauses.pData[hClause] ); }
static inline int Cbs3_ClauseSize( Cbs3_Man_t * p, int hClause ) { return p->pClauses.pData[hClause]; }
static inline int * Cbs3_ClauseLits( Cbs3_Man_t * p, int hClause ) { return p->pClauses.pData+hClause+1; }
static inline int Cbs3_ClauseLit( Cbs3_Man_t * p, int hClause, int i ) { return p->pClauses.pData[hClause+1+i]; }
static inline int * Cbs3_ClauseNext1p( Cbs3_Man_t * p, int hClause ) { return p->pClauses.pData+hClause+Cbs3_ClauseSize(p, hClause)+2; }
static inline void Cbs3_ClauseSetSize( Cbs3_Man_t * p, int hClause, int x ) { p->pClauses.pData[hClause] = x; }
static inline void Cbs3_ClauseSetLit( Cbs3_Man_t * p, int hClause, int i, int x ) { p->pClauses.pData[hClause+i+1] = x; }
static inline void Cbs3_ClauseSetNext( Cbs3_Man_t * p, int hClause, int n, int x ){ p->pClauses.pData[hClause+Cbs3_ClauseSize(p, hClause)+1+n] = x; }
#define Cbs3_QueForEachEntry( Que, iObj, i ) \
for ( i = (Que).iHead; (i < (Que).iTail) && ((iObj) = (Que).pData[i]); i++ )
#define Cbs3_ClauseForEachEntry( p, hClause, iObj, i ) \
for ( i = 1; i <= Cbs3_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )
#define Cbs3_ClauseForEachEntry1( p, hClause, iObj, i ) \
for ( i = 2; i <= Cbs3_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Sets default values of the parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs3_SetDefaultParams( Cbs3_Par_t * pPars )
{
memset( pPars, 0, sizeof(Cbs3_Par_t) );
pPars->nBTLimit = 1000; // limit on the number of conflicts
pPars->nJustLimit = 500; // limit on the size of justification queue
pPars->nRestLimit = 10; // limit on the number of restarts
pPars->fVerbose = 1; // print detailed statistics
}
void Cbs3_ManSetConflictNum( Cbs3_Man_t * p, int Num )
{
p->Pars.nBTLimit = Num;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cbs3_Man_t * Cbs3_ManAlloc( Gia_Man_t * pGia )
{
Cbs3_Man_t * p;
p = ABC_CALLOC( Cbs3_Man_t, 1 );
p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
p->pProp.pData = ABC_ALLOC( int, p->pProp.nSize );
p->pJust.pData = ABC_ALLOC( int, p->pJust.nSize );
p->pClauses.pData = ABC_ALLOC( int, p->pClauses.nSize );
p->pClauses.iHead = p->pClauses.iTail = 1;
p->vModel = Vec_IntAlloc( 1000 );
p->vTemp = Vec_IntAlloc( 1000 );
p->pAig = pGia;
Cbs3_SetDefaultParams( &p->Pars );
// circuit structure
Vec_IntPush( &p->vMap, -1 );
Vec_IntPush( &p->vRef, -1 );
Vec_IntPushTwo( &p->vFans, -1, -1 );
Vec_WecPushLevel( &p->vImps );
Vec_WecPushLevel( &p->vImps );
p->nVars = 1;
// internal data
p->nVarsAlloc = 1000;
Vec_StrFill( &p->vAssign, p->nVarsAlloc, 2 );
Vec_StrFill( &p->vMark, p->nVarsAlloc, 0 );
Vec_IntFill( &p->vLevReason, 3*p->nVarsAlloc, -1 );
Vec_IntFill( &p->vActs, p->nVarsAlloc, 0 );
Vec_IntFill( &p->vWatches, 2*p->nVarsAlloc, 0 );
Vec_IntGrow( &p->vWatchUpds, 1000 );
return p;
}
static inline void Cbs3_ManReset( Cbs3_Man_t * p )
{
assert( p->nVars == Vec_IntSize(&p->vMap) );
Vec_IntShrink( &p->vMap, 1 );
Vec_IntShrink( &p->vRef, 1 );
Vec_IntShrink( &p->vFans, 2 );
Vec_WecShrink( &p->vImps, 2 );
p->nVars = 1;
}
static inline void Cbs3_ManGrow( Cbs3_Man_t * p )
{
if ( p->nVarsAlloc < p->nVars )
{
p->nVarsAlloc = 2*p->nVars;
Vec_StrFill( &p->vAssign, p->nVarsAlloc, 2 );
Vec_StrFill( &p->vMark, p->nVarsAlloc, 0 );
Vec_IntFill( &p->vLevReason, 3*p->nVarsAlloc, -1 );
Vec_IntFill( &p->vActs, p->nVarsAlloc, 0 );
Vec_IntFill( &p->vWatches, 2*p->nVarsAlloc, 0 );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs3_ManStop( Cbs3_Man_t * p )
{
// circuit structure
Vec_IntErase( &p->vMap );
Vec_IntErase( &p->vRef );
Vec_IntErase( &p->vFans );
Vec_WecErase( &p->vImps );
// internal data
Vec_StrErase( &p->vAssign );
Vec_StrErase( &p->vMark );
Vec_IntErase( &p->vLevReason );
Vec_IntErase( &p->vActs );
Vec_IntErase( &p->vWatches );
Vec_IntErase( &p->vWatchUpds );
Vec_IntFree( p->vModel );
Vec_IntFree( p->vTemp );
ABC_FREE( p->pClauses.pData );
ABC_FREE( p->pProp.pData );
ABC_FREE( p->pJust.pData );
ABC_FREE( p );
}
int Cbs3_ManMemory( Cbs3_Man_t * p )
{
int nMem = sizeof(Cbs3_Man_t);
nMem += (int)Vec_IntMemory( &p->vMap );
nMem += (int)Vec_IntMemory( &p->vRef );
nMem += (int)Vec_IntMemory( &p->vFans );
nMem += (int)Vec_WecMemory( &p->vImps );
nMem += (int)Vec_StrMemory( &p->vAssign );
nMem += (int)Vec_StrMemory( &p->vMark );
nMem += (int)Vec_IntMemory( &p->vActs );
nMem += (int)Vec_IntMemory( &p->vWatches );
nMem += (int)Vec_IntMemory( &p->vWatchUpds );
nMem += (int)Vec_IntMemory( p->vModel );
nMem += (int)Vec_IntMemory( p->vTemp );
nMem += 4*p->pClauses.nSize;
nMem += 4*p->pProp.nSize;
nMem += 4*p->pJust.nSize;
return nMem;
}
/**Function*************************************************************
Synopsis [Returns satisfying assignment.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cbs3_ReadModel( Cbs3_Man_t * p )
{
return p->vModel;
}
/**Function*************************************************************
Synopsis [Activity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
//#define USE_ACTIVITY
#ifdef USE_ACTIVITY
static inline void Cbs3_ActReset( Cbs3_Man_t * p )
{
int i, * pAct = Vec_IntArray(&p->vActs);
for ( i = 0; i < p->nVars; i++ )
pAct[i] = (1 << 10);
p->var_inc = (1 << 5);
}
static inline void Cbs3_ActRescale( Cbs3_Man_t * p )
{
int i, * pAct = Vec_IntArray(&p->vActs);
for ( i = 0; i < p->nVars; i++ )
pAct[i] >>= 19;
p->var_inc >>= 19;
p->var_inc = Abc_MaxInt( (unsigned)p->var_inc, (1<<5) );
}
static inline void Cbs3_ActBumpVar( Cbs3_Man_t * p, int iVar )
{
int * pAct = Vec_IntArray(&p->vActs);
pAct[iVar] += p->var_inc;
if ((unsigned)pAct[iVar] & 0x80000000)
Cbs3_ActRescale(p);
}
static inline void Cbs3_ActDecay( Cbs3_Man_t * p )
{
p->var_inc += (p->var_inc >> 4);
}
#else
static inline void Cbs3_ActReset( Cbs3_Man_t * p ) {}
static inline void Cbs3_ActRescale( Cbs3_Man_t * p ) {}
static inline void Cbs3_ActBumpVar( Cbs3_Man_t * p, int iVar ) {}
static inline void Cbs3_ActDecay( Cbs3_Man_t * p ) {}
#endif
/**Function*************************************************************
Synopsis [Returns 1 if the solver is out of limits.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_ManCheckLimits( Cbs3_Man_t * p )
{
p->nFails[0] += p->Pars.nJustThis > p->Pars.nJustLimit;
p->nFails[1] += p->Pars.nBTThis > p->Pars.nBTLimit;
return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
}
/**Function*************************************************************
Synopsis [Saves the satisfying assignment as an array of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_ManSaveModel( Cbs3_Man_t * p, Vec_Int_t * vCex )
{
int i, iLit;
Vec_IntClear( vCex );
p->pProp.iHead = 0;
Cbs3_QueForEachEntry( p->pProp, iLit, i )
if ( Cbs3_VarIsPi(p, Abc_Lit2Var(iLit)) )
Vec_IntPush( vCex, Abc_Lit2LitV(Vec_IntArray(&p->vMap), iLit)-2 );
}
static inline void Cbs3_ManSaveModelAll( Cbs3_Man_t * p, Vec_Int_t * vCex )
{
int i, iLit;
Vec_IntClear( vCex );
p->pProp.iHead = 0;
Cbs3_QueForEachEntry( p->pProp, iLit, i )
{
int iVar = Abc_Lit2Var(iLit);
Vec_IntPush( vCex, Abc_Var2Lit(iVar, !Cbs3_VarValue(p, iVar)) );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_QueIsEmpty( Cbs3_Que_t * p )
{
return p->iHead == p->iTail;
}
static inline int Cbs3_QueSize( Cbs3_Que_t * p )
{
return p->iTail - p->iHead;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_QuePush( Cbs3_Que_t * p, int iObj )
{
if ( p->iTail == p->nSize )
{
p->nSize *= 2;
p->pData = ABC_REALLOC( int, p->pData, p->nSize );
}
p->pData[p->iTail++] = iObj;
}
static inline void Cbs3_QueGrow( Cbs3_Que_t * p, int Plus )
{
if ( p->iTail + Plus > p->nSize )
{
p->nSize *= 2;
p->pData = ABC_REALLOC( int, p->pData, p->nSize );
}
assert( p->iTail + Plus <= p->nSize );
}
/**Function*************************************************************
Synopsis [Returns 1 if the object in the queue.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_QueHasNode( Cbs3_Que_t * p, int iObj )
{
int i, iTemp;
Cbs3_QueForEachEntry( *p, iTemp, i )
if ( iTemp == iObj )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_QueStore( Cbs3_Que_t * p, int * piHeadOld, int * piTailOld )
{
int i;
*piHeadOld = p->iHead;
*piTailOld = p->iTail;
for ( i = *piHeadOld; i < *piTailOld; i++ )
Cbs3_QuePush( p, p->pData[i] );
p->iHead = *piTailOld;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_QueRestore( Cbs3_Que_t * p, int iHeadOld, int iTailOld )
{
p->iHead = iHeadOld;
p->iTail = iTailOld;
}
/**Function*************************************************************
Synopsis [Find variable with the highest ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_ManDecide( Cbs3_Man_t * p )
{
int i, iObj, iObjMax = 0;
#ifdef USE_ACTIVITY
Cbs3_QueForEachEntry( p->pJust, iObj, i )
if ( iObjMax == 0 ||
Vec_IntEntry(&p->vActs, iObjMax) < Vec_IntEntry(&p->vActs, iObj) ||
(Vec_IntEntry(&p->vActs, iObjMax) == Vec_IntEntry(&p->vActs, iObj) && Vec_IntEntry(&p->vMap, iObjMax) < Vec_IntEntry(&p->vMap, iObj)) )
iObjMax = iObj;
#else
Cbs3_QueForEachEntry( p->pJust, iObj, i )
// if ( iObjMax == 0 || iObjMax < iObj )
if ( iObjMax == 0 || Vec_IntEntry(&p->vMap, iObjMax) < Vec_IntEntry(&p->vMap, iObj) )
iObjMax = iObj;
#endif
return iObjMax;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_ManCancelUntil( Cbs3_Man_t * p, int iBound )
{
int i, iLit;
assert( iBound <= p->pProp.iTail );
p->pProp.iHead = iBound;
Cbs3_QueForEachEntry( p->pProp, iLit, i )
Cbs3_VarUnassign( p, Abc_Lit2Var(iLit) );
p->pProp.iTail = iBound;
}
/**Function*************************************************************
Synopsis [Assigns the variables a value.]
Description [Returns 1 if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_ManAssign( Cbs3_Man_t * p, int iLit, int Level, int iRes0, int iRes1 )
{
int iObj = Abc_Lit2Var(iLit);
assert( Cbs3_VarUnused(p, iObj) );
assert( !Cbs3_VarIsAssigned(p, iObj) );
Cbs3_VarSetValue( p, iObj, !Abc_LitIsCompl(iLit) );
Cbs3_QuePush( &p->pProp, iLit );
Vec_IntWriteEntry( &p->vLevReason, 3*iObj, Level );
Vec_IntWriteEntry( &p->vLevReason, 3*iObj+1, iRes0 );
Vec_IntWriteEntry( &p->vLevReason, 3*iObj+2, iRes1 );
}
/**Function*************************************************************
Synopsis [Prints conflict clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_ManPrintClause( Cbs3_Man_t * p, int Level, int hClause )
{
int i, iLit;
assert( Cbs3_QueIsEmpty( &p->pClauses ) );
printf( "Level %2d : ", Level );
Cbs3_ClauseForEachEntry( p, hClause, iLit, i )
printf( "%c%d ", Abc_LitIsCompl(iLit) ? '-':'+', Abc_Lit2Var(iLit) );
// printf( "%d=%d(%d) ", iObj, Cbs3_VarValue(p, Abc_Lit2Var(iLit)), Cbs3_VarDecLevel(p, Abc_Lit2Var(iLit)) );
printf( "\n" );
}
static inline void Cbs3_ManPrintCube( Cbs3_Man_t * p, int Level, int hClause )
{
int i, iObj;
assert( Cbs3_QueIsEmpty( &p->pClauses ) );
printf( "Level %2d : ", Level );
Cbs3_ClauseForEachEntry( p, hClause, iObj, i )
printf( "%c%d ", Cbs3_VarValue(p, iObj)? '+':'-', iObj );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Finalized the clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_ManCleanWatch( Cbs3_Man_t * p )
{
int i, iLit;
Vec_IntForEachEntry( &p->vWatchUpds, iLit, i )
Vec_IntWriteEntry( &p->vWatches, iLit, 0 );
Vec_IntClear( &p->vWatchUpds );
//Vec_IntForEachEntry( &p->vWatches, iLit, i )
// assert( iLit == 0 );
}
static inline void Cbs3_ManWatchClause( Cbs3_Man_t * p, int hClause, int Lit )
{
int * pLits = Cbs3_ClauseLits( p, hClause );
int * pPlace = Vec_IntEntryP( &p->vWatches, Abc_LitNot(Lit) );
if ( *pPlace == 0 )
Vec_IntPush( &p->vWatchUpds, Abc_LitNot(Lit) );
/*
if ( pClause->pLits[0] == Lit )
pClause->pNext0 = p->pWatches[lit_neg(Lit)];
else
{
assert( pClause->pLits[1] == Lit );
pClause->pNext1 = p->pWatches[lit_neg(Lit)];
}
p->pWatches[lit_neg(Lit)] = pClause;
*/
assert( Lit == pLits[0] || Lit == pLits[1] );
Cbs3_ClauseSetNext( p, hClause, Lit == pLits[1], *pPlace );
*pPlace = hClause;
}
static inline int Cbs3_QueFinish( Cbs3_Man_t * p, int Level )
{
Cbs3_Que_t * pQue = &(p->pClauses);
int i, iObj, hClauseC, hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1;
assert( pQue->iHead+1 < pQue->iTail );
Cbs3_ClauseSetSize( p, pQue->iHead, Size );
hClauseC = pQue->iHead = pQue->iTail;
//printf( "Adding cube: " ); Cbs3_ManPrintCube(p, Level, hClause);
if ( Size == 1 )
return hClause;
// create watched clause
pQue->iHead = hClause;
Cbs3_QueForEachEntry( p->pClauses, iObj, i )
{
if ( i == hClauseC )
break;
else if ( i == hClause ) // nlits
Cbs3_QuePush( pQue, iObj );
else // literals
Cbs3_QuePush( pQue, Abc_Var2Lit(iObj, Cbs3_VarValue(p, iObj)) ); // complement
}
Cbs3_QuePush( pQue, 0 ); // next0
Cbs3_QuePush( pQue, 0 ); // next1
pQue->iHead = pQue->iTail;
Cbs3_ManWatchClause( p, hClauseC, Cbs3_ClauseLit(p, hClauseC, 0) );
Cbs3_ManWatchClause( p, hClauseC, Cbs3_ClauseLit(p, hClauseC, 1) );
//printf( "Adding clause %d: ", hClauseC ); Cbs3_ManPrintClause(p, Level, hClauseC);
Cbs3_ActDecay( p );
return hClause;
}
/**Function*************************************************************
Synopsis [Returns conflict clause.]
Description [Performs conflict analysis.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_ManDeriveReason( Cbs3_Man_t * p, int Level )
{
Cbs3_Que_t * pQue = &(p->pClauses);
int i, k, iObj, iLitLevel, * pReason;
assert( pQue->pData[pQue->iHead] == 0 );
assert( pQue->pData[pQue->iHead+1] == 0 );
assert( pQue->iHead + 2 < pQue->iTail );
//for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
// assert( !Cbs3_VarMark0(p, pQue->pData[i]) );
// compact literals
Vec_IntClear( p->vTemp );
for ( i = k = pQue->iHead + 2; i < pQue->iTail; i++ )
{
iObj = pQue->pData[i];
if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
continue;
//if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
// Vec_IntPush( &p->vActStore, iObj );
//Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
// assigned - seen first time
Cbs3_VarSetMark0(p, iObj, 1);
Cbs3_ActBumpVar(p, iObj);
Vec_IntPush( p->vTemp, iObj );
// check decision level
iLitLevel = Cbs3_VarDecLevel( p, iObj );
if ( iLitLevel < Level )
{
pQue->pData[k++] = iObj;
continue;
}
assert( iLitLevel == Level );
pReason = Cbs3_VarReasonP( p, iObj );
if ( pReason[0] == 0 && pReason[1] == 0 ) // no reason
{
assert( pQue->pData[pQue->iHead+1] == 0 );
pQue->pData[pQue->iHead+1] = iObj;
}
else if ( pReason[0] != 0 ) // circuit reason
{
Cbs3_QuePush( pQue, pReason[0] );
if ( pReason[1] )
Cbs3_QuePush( pQue, pReason[1] );
}
else // clause reason
{
int i, * pLits, nLits = Cbs3_ClauseSize( p, pReason[1] );
assert( pReason[1] );
Cbs3_QueGrow( pQue, nLits );
pLits = Cbs3_ClauseLits( p, pReason[1] );
assert( iObj == Abc_Lit2Var(pLits[0]) );
for ( i = 1; i < nLits; i++ )
Cbs3_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
}
}
assert( pQue->pData[pQue->iHead] == 0 );
assert( pQue->pData[pQue->iHead+1] != 0 );
pQue->iTail = k;
// clear the marks
Vec_IntForEachEntry( p->vTemp, iObj, i )
Cbs3_VarSetMark0(p, iObj, 0);
return Cbs3_QueFinish( p, Level );
}
static inline int Cbs3_ManAnalyze( Cbs3_Man_t * p, int Level, int iVar, int iFan0, int iFan1 )
{
Cbs3_Que_t * pQue = &(p->pClauses);
assert( Cbs3_VarIsAssigned(p, iVar) );
assert( Cbs3_QueIsEmpty( pQue ) );
Cbs3_QuePush( pQue, 0 );
Cbs3_QuePush( pQue, 0 );
if ( iFan0 ) // circuit conflict
{
assert( Cbs3_VarIsAssigned(p, iFan0) );
assert( iFan1 == 0 || Cbs3_VarIsAssigned(p, iFan1) );
Cbs3_QuePush( pQue, iVar );
Cbs3_QuePush( pQue, iFan0 );
if ( iFan1 )
Cbs3_QuePush( pQue, iFan1 );
}
else // clause conflict
{
int i, * pLits, nLits = Cbs3_ClauseSize( p, iFan1 );
assert( iFan1 );
Cbs3_QueGrow( pQue, nLits );
pLits = Cbs3_ClauseLits( p, iFan1 );
assert( iVar == Abc_Lit2Var(pLits[0]) );
assert( Cbs3_VarValue(p, iVar) == Abc_LitIsCompl(pLits[0]) );
for ( i = 0; i < nLits; i++ )
Cbs3_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
}
return Cbs3_ManDeriveReason( p, Level );
}
/**Function*************************************************************
Synopsis [Propagate one assignment.]
Description [Returns handle of the conflict clause, if conflict occurs.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_ManPropagateClauses( Cbs3_Man_t * p, int Level, int Lit )
{
int i, Value, Cur, LitF = Abc_LitNot(Lit);
int * pPrev = Vec_IntEntryP( &p->vWatches, Lit );
//for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
for ( Cur = *pPrev; Cur; Cur = *pPrev )
{
int nLits = Cbs3_ClauseSize( p, Cur );
int * pLits = Cbs3_ClauseLits( p, Cur );
p->nPropCalls[1]++;
//printf( " Watching literal %c%d on level %d.\n", Abc_LitIsCompl(Lit) ? '-':'+', Abc_Lit2Var(Lit), Level );
// make sure the false literal is in the second literal of the clause
//if ( pCur->pLits[0] == LitF )
if ( pLits[0] == LitF )
{
//pCur->pLits[0] = pCur->pLits[1];
pLits[0] = pLits[1];
//pCur->pLits[1] = LitF;
pLits[1] = LitF;
//pTemp = pCur->pNext0;
//pCur->pNext0 = pCur->pNext1;
//pCur->pNext1 = pTemp;
ABC_SWAP( int, pLits[nLits], pLits[nLits+1] );
}
//assert( pCur->pLits[1] == LitF );
assert( pLits[1] == LitF );
// if the first literal is true, the clause is satisfied
//if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
if ( Cbs3_VarValue(p, Abc_Lit2Var(pLits[0])) == !Abc_LitIsCompl(pLits[0]) )
{
//ppPrev = &pCur->pNext1;
pPrev = Cbs3_ClauseNext1p(p, Cur);
continue;
}
// look for a new literal to watch
for ( i = 2; i < nLits; i++ )
{
// skip the case when the literal is false
//if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
if ( Cbs3_VarValue(p, Abc_Lit2Var(pLits[i])) == Abc_LitIsCompl(pLits[i]) )
continue;
// the literal is either true or unassigned - watch it
//pCur->pLits[1] = pCur->pLits[i];
//pCur->pLits[i] = LitF;
pLits[1] = pLits[i];
pLits[i] = LitF;
// remove this clause from the watch list of Lit
//*ppPrev = pCur->pNext1;
*pPrev = *Cbs3_ClauseNext1p(p, Cur);
// add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
//Intb_ManWatchClause( p, pCur, pCur->pLits[1] );
Cbs3_ManWatchClause( p, Cur, Cbs3_ClauseLit(p, Cur, 1) );
break;
}
if ( i < nLits ) // found new watch
continue;
// clause is unit - enqueue new implication
//if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) )
//{
// ppPrev = &pCur->pNext1;
// continue;
//}
// clause is unit - enqueue new implication
Value = Cbs3_VarValue(p, Abc_Lit2Var(pLits[0]));
if ( Value >= 2 ) // unassigned
{
Cbs3_ManAssign( p, pLits[0], Level, 0, Cur );
pPrev = Cbs3_ClauseNext1p(p, Cur);
continue;
}
// conflict detected - return the conflict clause
//return pCur;
if ( Value == Abc_LitIsCompl(pLits[0]) )
{
p->nClauseConf++;
return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(pLits[0]), 0, Cur );
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Performs resolution of two clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_ManResolve( Cbs3_Man_t * p, int Level, int hClause0, int hClause1 )
{
Cbs3_Que_t * pQue = &(p->pClauses);
int i, iObj, LevelMax = -1, LevelCur;
assert( pQue->pData[hClause0+1] != 0 );
assert( pQue->pData[hClause0+1] == pQue->pData[hClause1+1] );
//Cbs3_ClauseForEachEntry1( p, hClause0, iObj, i )
// assert( !Cbs3_VarMark0(p, iObj) );
//Cbs3_ClauseForEachEntry1( p, hClause1, iObj, i )
// assert( !Cbs3_VarMark0(p, iObj) );
assert( Cbs3_QueIsEmpty( pQue ) );
Cbs3_QuePush( pQue, 0 );
Cbs3_QuePush( pQue, 0 );
// for ( i = hClause0 + 1; (iObj = pQue->pData[i]); i++ )
Cbs3_ClauseForEachEntry1( p, hClause0, iObj, i )
{
if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
continue;
//if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
// Vec_IntPush( &p->vActStore, iObj );
//Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
// assigned - seen first time
Cbs3_VarSetMark0(p, iObj, 1);
Cbs3_ActBumpVar(p, iObj);
Cbs3_QuePush( pQue, iObj );
LevelCur = Cbs3_VarDecLevel( p, iObj );
if ( LevelMax < LevelCur )
LevelMax = LevelCur;
}
// for ( i = hClause1 + 1; (iObj = pQue->pData[i]); i++ )
Cbs3_ClauseForEachEntry1( p, hClause1, iObj, i )
{
if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
continue;
//if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
// Vec_IntPush( &p->vActStore, iObj );
//Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
// assigned - seen first time
Cbs3_VarSetMark0(p, iObj, 1);
Cbs3_ActBumpVar(p, iObj);
Cbs3_QuePush( pQue, iObj );
LevelCur = Cbs3_VarDecLevel( p, iObj );
if ( LevelMax < LevelCur )
LevelMax = LevelCur;
}
for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
Cbs3_VarSetMark0(p, pQue->pData[i], 0);
return Cbs3_ManDeriveReason( p, LevelMax );
}
/**Function*************************************************************
Synopsis [Propagates a variable.]
Description [Returns clause handle if conflict; 0 if no conflict.]
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs3_ManUpdateJFrontier( Cbs3_Man_t * p )
{
//abctime clk = Abc_Clock();
int iVar, iLit, i, k = p->pJust.iTail;
Cbs3_QueGrow( &p->pJust, Cbs3_QueSize(&p->pJust) + Cbs3_QueSize(&p->pProp) );
Cbs3_QueForEachEntry( p->pJust, iVar, i )
if ( Cbs3_VarIsJust(p, iVar) )
p->pJust.pData[k++] = iVar;
Cbs3_QueForEachEntry( p->pProp, iLit, i )
if ( Cbs3_VarIsJust(p, Abc_Lit2Var(iLit)) )
p->pJust.pData[k++] = Abc_Lit2Var(iLit);
p->pJust.iHead = p->pJust.iTail;
p->pJust.iTail = k;
//p->timeJFront += Abc_Clock() - clk;
}
int Cbs3_ManPropagateNew( Cbs3_Man_t * p, int Level )
{
int i, k, iLit, hClause, nLits, * pLits;
p->nPropCalls[0]++;
Cbs3_QueForEachEntry( p->pProp, iLit, i )
{
if ( (hClause = Cbs3_ManPropagateClauses(p, Level, iLit)) )
return hClause;
p->nPropCalls[2]++;
nLits = Vec_IntSize(Vec_WecEntry(&p->vImps, iLit));
pLits = Vec_IntArray(Vec_WecEntry(&p->vImps, iLit));
for ( k = 0; k < nLits; k += 2 )
{
int Value0 = Cbs3_VarValue(p, Abc_Lit2Var(pLits[k]));
int Value1 = pLits[k+1] ? Cbs3_VarValue(p, Abc_Lit2Var(pLits[k+1])) : -1;
if ( Value1 == -1 || Value1 == Abc_LitIsCompl(pLits[k+1]) ) // pLits[k+1] is false
{
if ( Value0 >= 2 ) // pLits[k] is unassigned
Cbs3_ManAssign( p, pLits[k], Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k+1]) );
else if ( Value0 == Abc_LitIsCompl(pLits[k]) ) // pLits[k] is false
return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]), Abc_Lit2Var(pLits[k+1]) );
}
if ( Value1 != -1 && Value0 == Abc_LitIsCompl(pLits[k]) ) // pLits[k] is false
{
if ( Value1 >= 2 ) // pLits[k+1] is unassigned
Cbs3_ManAssign( p, pLits[k+1], Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]) );
else if ( Value1 == Abc_LitIsCompl(pLits[k+1]) ) // pLits[k+1] is false
return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]), Abc_Lit2Var(pLits[k+1]) );
}
}
}
Cbs3_ManUpdateJFrontier( p );
// finalize propagation queue
p->pProp.iHead = p->pProp.iTail;
return 0;
}
/**Function*************************************************************
Synopsis [Solve the problem recursively.]
Description [Returns learnt clause if unsat, NULL if sat or undecided.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cbs3_ManSolve2_rec( Cbs3_Man_t * p, int Level )
{
Cbs3_Que_t * pQue = &(p->pClauses);
int iPropHead, iJustHead, iJustTail;
int hClause, hLearn0, hLearn1, iVar, iDecLit;
int nRef0, nRef1;
// propagate assignments
assert( !Cbs3_QueIsEmpty(&p->pProp) );
//if ( (hClause = Cbs3_ManPropagate( p, Level )) )
if ( (hClause = Cbs3_ManPropagateNew( p, Level )) )
return hClause;
// check for satisfying assignment
assert( Cbs3_QueIsEmpty(&p->pProp) );
if ( Cbs3_QueIsEmpty(&p->pJust) )
return 0;
// quit using resource limits
p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
if ( Cbs3_ManCheckLimits( p ) )
return 0;
// remember the state before branching
iPropHead = p->pProp.iHead;
iJustHead = p->pJust.iHead;
iJustTail = p->pJust.iTail;
// find the decision variable
p->nDecs++;
iVar = Cbs3_ManDecide( p );
assert( !Cbs3_VarIsPi(p, iVar) );
assert( Cbs3_VarIsJust(p, iVar) );
// chose decision variable using fanout count
nRef0 = Vec_IntEntry(&p->vRef, Abc_Lit2Var(Cbs3_VarLit0(p, iVar)));
nRef1 = Vec_IntEntry(&p->vRef, Abc_Lit2Var(Cbs3_VarLit1(p, iVar)));
// if ( nRef0 >= nRef1 || (nRef0 == nRef1) && (Abc_Random(0) & 1) )
if ( nRef0 >= nRef1 )
iDecLit = Abc_LitNot(Cbs3_VarLit0(p, iVar));
else
iDecLit = Abc_LitNot(Cbs3_VarLit1(p, iVar));
// decide on first fanin
Cbs3_ManAssign( p, iDecLit, Level+1, 0, 0 );
if ( !(hLearn0 = Cbs3_ManSolve2_rec( p, Level+1 )) )
return 0;
if ( pQue->pData[hLearn0+1] != Abc_Lit2Var(iDecLit) )
return hLearn0;
Cbs3_ManCancelUntil( p, iPropHead );
Cbs3_QueRestore( &p->pJust, iJustHead, iJustTail );
// decide on second fanin
Cbs3_ManAssign( p, Abc_LitNot(iDecLit), Level+1, 0, 0 );
if ( !(hLearn1 = Cbs3_ManSolve2_rec( p, Level+1 )) )
return 0;
if ( pQue->pData[hLearn1+1] != Abc_Lit2Var(iDecLit) )
return hLearn1;
hClause = Cbs3_ManResolve( p, Level, hLearn0, hLearn1 );
p->Pars.nBTThis++;
return hClause;
}
/**Function*************************************************************
Synopsis [Looking for a satisfying assignment of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_ManSolveInt( Cbs3_Man_t * p, int iLit )
{
int RetValue = 0;
assert( !p->pProp.iHead && !p->pProp.iTail );
assert( !p->pJust.iHead && !p->pJust.iTail );
p->Pars.nBTThis = p->Pars.nJustThis = 0;
Cbs3_ManAssign( p, iLit, 0, 0, 0 );
if ( !Cbs3_ManSolve2_rec(p, 0) && !Cbs3_ManCheckLimits(p) )
Cbs3_ManSaveModel( p, p->vModel );
else
RetValue = 1;
Cbs3_ManCancelUntil( p, 0 );
p->pJust.iHead = p->pJust.iTail = 0;
p->Pars.nBTTotal += p->Pars.nBTThis;
p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
if ( Cbs3_ManCheckLimits( p ) )
RetValue = -1;
return RetValue;
}
int Cbs3_ManSolve( Cbs3_Man_t * p, int iLit, int nRestarts )
{
int i, RetValue = -1;
assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
for ( i = 0; i < nRestarts; i++ )
if ( (RetValue = Cbs3_ManSolveInt(p, iLit)) != -1 )
break;
Cbs3_ManCleanWatch( p );
p->pClauses.iHead = p->pClauses.iTail = 1;
return RetValue;
}
/**Function*************************************************************
Synopsis [Prints statistics of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cbs3_ManSatPrintStats( Cbs3_Man_t * p )
{
printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
printf( "Conf = %6d ", p->Pars.nBTLimit );
printf( "Restart = %2d ", p->Pars.nRestLimit );
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
ABC_PRT( "Total time", p->timeTotal );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cbs3_ManAddVar( Cbs3_Man_t * p, int iGiaObj )
{
assert( Vec_IntSize(&p->vMap) == p->nVars );
Vec_IntPush( &p->vMap, iGiaObj );
Vec_IntPush( &p->vRef, Gia_ObjRefNumId(p->pAig, iGiaObj) );
Vec_IntPushTwo( &p->vFans, 0, 0 );
Vec_WecPushLevel(&p->vImps);
Vec_WecPushLevel(&p->vImps);
return Abc_Var2Lit( p->nVars++, 0 );
}
static inline void Cbs3_ManAddConstr( Cbs3_Man_t * p, int x, int x0, int x1 )
{
Vec_WecPushTwo( &p->vImps, x , x0, 0 ); // ~x + x0
Vec_WecPushTwo( &p->vImps, x , x1, 0 ); // ~x + x1
Vec_WecPushTwo( &p->vImps, 1^x0, 1^x , 0 ); // ~x + x0
Vec_WecPushTwo( &p->vImps, 1^x1, 1^x , 0 ); // ~x + x1
Vec_WecPushTwo( &p->vImps, 1^x , 1^x0, 1^x1 ); // x + ~x0 + ~x1
Vec_WecPushTwo( &p->vImps, x0, x , 1^x1 ); // x + ~x0 + ~x1
Vec_WecPushTwo( &p->vImps, x1, x , 1^x0 ); // x + ~x0 + ~x1
}
static inline void Cbs3_ManAddAnd( Cbs3_Man_t * p, int x, int x0, int x1 )
{
assert( x > 0 && x0 > 0 && x1 > 0 );
Vec_IntWriteEntry( &p->vFans, x, x0 );
Vec_IntWriteEntry( &p->vFans, x+1, x1 );
Cbs3_ManAddConstr( p, x, x0, x1 );
}
static inline int Cbs3_ManToSolver1_rec( Cbs3_Man_t * pSol, Gia_Man_t * p, int iObj, int Depth )
{
Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int Lit0, Lit1;
if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
return pObj->Value;
pObj->Value = Cbs3_ManAddVar( pSol, iObj );
if ( Gia_ObjIsCi(pObj) || Depth == 0 )
return pObj->Value;
assert( Gia_ObjIsAnd(pObj) );
Lit0 = Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId0(pObj, iObj), Depth - Gia_ObjFaninC0(pObj) );
Lit1 = Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId1(pObj, iObj), Depth - Gia_ObjFaninC1(pObj) );
Cbs3_ManAddAnd( pSol, pObj->Value, Lit0 ^ Gia_ObjFaninC0(pObj), Lit1 ^ Gia_ObjFaninC1(pObj) );
return pObj->Value;
}
static inline int Cbs3_ManToSolver1( Cbs3_Man_t * pSol, Gia_Man_t * p, Gia_Obj_t * pRoot, int nRestarts, int Depth )
{
//abctime clk = Abc_Clock();
assert( Gia_ObjIsCo(pRoot) );
Cbs3_ManReset( pSol );
Gia_ManIncrementTravId( p );
Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId0p(p, pRoot), Depth );
Cbs3_ManGrow( pSol );
Cbs3_ActReset( pSol );
//pSol->timeSatLoad += Abc_Clock() - clk;
return Cbs3_ManSolve( pSol, Gia_ObjFanin0Copy(pRoot), nRestarts );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cbs3_ManPrepare( Cbs3_Man_t * p )
{
int x, x0, x1;
Vec_WecInit( &p->vImps, Abc_Var2Lit(p->nVars, 0) );
Vec_IntForEachEntryDoubleStart( &p->vFans, x0, x1, x, 2 )
if ( x0 ) Cbs3_ManAddConstr( p, x, x0, x1 );
}
static inline int Cbs3_ManAddNode( Cbs3_Man_t * p, int iGiaObj, int iLit0, int iLit1 )
{
assert( Vec_IntSize(&p->vMap) == p->nVars );
Vec_IntPush( &p->vMap, iGiaObj );
Vec_IntPush( &p->vRef, Gia_ObjRefNumId(p->pAig, iGiaObj) );
Vec_IntPushTwo( &p->vFans, iLit0, iLit1 );
return Abc_Var2Lit( p->nVars++, 0 );
}
static inline int Cbs3_ManToSolver2_rec( Cbs3_Man_t * pSol, Gia_Man_t * p, int iObj, int Depth )
{
Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int Lit0, Lit1;
if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
return pObj->Value;
if ( Gia_ObjIsCi(pObj) || Depth == 0 )
return pObj->Value = Cbs3_ManAddNode(pSol, iObj, 0, 0);
assert( Gia_ObjIsAnd(pObj) );
Lit0 = Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId0(pObj, iObj), Depth - Gia_ObjFaninC0(pObj) );
Lit1 = Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId1(pObj, iObj), Depth - Gia_ObjFaninC1(pObj) );
return pObj->Value = Cbs3_ManAddNode(pSol, iObj, Lit0 ^ Gia_ObjFaninC0(pObj), Lit1 ^ Gia_ObjFaninC1(pObj));
}
static inline int Cbs3_ManToSolver2( Cbs3_Man_t * pSol, Gia_Man_t * p, Gia_Obj_t * pRoot, int nRestarts, int Depth )
{
//abctime clk = Abc_Clock();
assert( Gia_ObjIsCo(pRoot) );
Cbs3_ManReset( pSol );
Gia_ManIncrementTravId( p );
Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId0p(p, pRoot), Depth );
Cbs3_ManGrow( pSol );
Cbs3_ManPrepare( pSol );
Cbs3_ActReset( pSol );
//pSol->timeSatLoad += Abc_Clock() - clk;
return Cbs3_ManSolve( pSol, Gia_ObjFanin0Copy(pRoot), nRestarts );
}
/**Function*************************************************************
Synopsis [Procedure to test the new SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cbs3_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, int nRestarts, Vec_Str_t ** pvStatus, int fVerbose )
{
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs3_Man_t * p;
Vec_Int_t * vCex, * vVisit, * vCexStore;
Vec_Str_t * vStatus;
Gia_Obj_t * pRoot;
int i, status; // 1 = unsat, 0 = sat, -1 = undec
abctime clk, clkTotal = Abc_Clock();
//assert( Gia_ManRegNum(pAig) == 0 );
Gia_ManCreateRefs( pAig );
//Gia_ManLevelNum( pAig );
// create logic network
p = Cbs3_ManAlloc( pAig );
p->Pars.nBTLimit = nConfs;
p->Pars.nRestLimit = nRestarts;
// create resulting data-structures
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
vCexStore = Vec_IntAlloc( 10000 );
vVisit = Vec_IntAlloc( 100 );
vCex = Cbs3_ReadModel( p );
// solve for each output
Gia_ManForEachCo( pAig, pRoot, i )
{
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
{
Vec_IntClear( vCex );
Vec_StrPush( vStatus, (char)(!Gia_ObjFaninC0(pRoot)) );
if ( Gia_ObjFaninC0(pRoot) ) // const1
Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
continue;
}
clk = Abc_Clock();
status = Cbs3_ManToSolver2( p, pAig, pRoot, p->Pars.nRestLimit, 10000 );
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
p->nSatUndec++;
p->nConfUndec += p->Pars.nBTThis;
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
p->timeSatUndec += Abc_Clock() - clk;
continue;
}
if ( status == 1 )
{
p->nSatUnsat++;
p->nConfUnsat += p->Pars.nBTThis;
p->timeSatUnsat += Abc_Clock() - clk;
continue;
}
p->nSatSat++;
p->nConfSat += p->Pars.nBTThis;
//Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
Cec_ManSatAddToStore( vCexStore, vCex, i );
p->timeSatSat += Abc_Clock() - clk;
}
Vec_IntFree( vVisit );
p->nSatTotal = Gia_ManPoNum(pAig);
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Cbs3_ManSatPrintStats( p );
if ( fVerbose )
{
printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. ClaConf = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] );
printf( "Mem usage %.2f MB.\n", 1.0*Cbs3_ManMemory(p)/(1<<20) );
//Abc_PrintTime( 1, "JFront", p->timeJFront );
//Abc_PrintTime( 1, "Loading", p->timeSatLoad );
//printf( "Decisions = %d.\n", p->nDecs );
}
Cbs3_ManStop( p );
*pvStatus = vStatus;
return vCexStore;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END