mirror of https://github.com/YosysHQ/abc.git
590 lines
18 KiB
C
590 lines
18 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [saigGlaPba.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [Sequential AIG package.]
|
|
|
|
Synopsis [Gate level abstraction.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - June 20, 2005.]
|
|
|
|
Revision [$Id: saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "saig.h"
|
|
#include "sat/bsat/satSolver.h"
|
|
#include "sat/bsat/satStore.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
typedef struct Aig_Gla2Man_t_ Aig_Gla2Man_t;
|
|
struct Aig_Gla2Man_t_
|
|
{
|
|
// user data
|
|
Aig_Man_t * pAig;
|
|
int nStart;
|
|
int nFramesMax;
|
|
int fVerbose;
|
|
// unrolling
|
|
Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID
|
|
Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID)
|
|
Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID
|
|
// clause mapping
|
|
Vec_Int_t * vCla2Obj; // maps clause into its root object
|
|
Vec_Int_t * vCla2Fra; // maps clause into its frame
|
|
Vec_Int_t * vVec2Use; // maps vec ID into its used frames (nFrames per vec ID)
|
|
// SAT solver
|
|
sat_solver * pSat;
|
|
// statistics
|
|
clock_t timePre;
|
|
clock_t timeSat;
|
|
clock_t timeTotal;
|
|
};
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Adds constant to the solver.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static inline int Aig_Gla2AddConst( sat_solver * pSat, int iVar, int fCompl )
|
|
{
|
|
lit Lit = toLitCond( iVar, fCompl );
|
|
if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
|
|
return 0;
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Adds buffer to the solver.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static inline int Aig_Gla2AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
|
|
{
|
|
lit Lits[2];
|
|
|
|
Lits[0] = toLitCond( iVar0, 0 );
|
|
Lits[1] = toLitCond( iVar1, !fCompl );
|
|
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
|
|
return 0;
|
|
|
|
Lits[0] = toLitCond( iVar0, 1 );
|
|
Lits[1] = toLitCond( iVar1, fCompl );
|
|
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
|
|
return 0;
|
|
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Adds buffer to the solver.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static inline int Aig_Gla2AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
|
|
{
|
|
lit Lits[3];
|
|
|
|
Lits[0] = toLitCond( iVar, 1 );
|
|
Lits[1] = toLitCond( iVar0, fCompl0 );
|
|
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
|
|
return 0;
|
|
|
|
Lits[0] = toLitCond( iVar, 1 );
|
|
Lits[1] = toLitCond( iVar1, fCompl1 );
|
|
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
|
|
return 0;
|
|
|
|
Lits[0] = toLitCond( iVar, 0 );
|
|
Lits[1] = toLitCond( iVar0, !fCompl0 );
|
|
Lits[2] = toLitCond( iVar1, !fCompl1 );
|
|
if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
|
|
return 0;
|
|
|
|
return 1;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Finds existing SAT variable or creates a new one.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Aig_Gla2FetchVar( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int k )
|
|
{
|
|
int i, iVecId, iSatVar;
|
|
assert( k < p->nFramesMax );
|
|
iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
|
|
if ( iVecId == 0 )
|
|
{
|
|
iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax;
|
|
for ( i = 0; i < p->nFramesMax; i++ )
|
|
Vec_IntPush( p->vVec2Var, 0 );
|
|
Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
|
|
}
|
|
iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k );
|
|
if ( iSatVar == 0 )
|
|
{
|
|
iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
|
|
Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
|
|
Vec_IntPush( p->vVar2Inf, k );
|
|
Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar );
|
|
}
|
|
return iSatVar;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Assigns variables to the AIG nodes.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f )
|
|
{
|
|
int nVars = Vec_IntSize(p->vVar2Inf);
|
|
Aig_Gla2FetchVar( p, pObj, f );
|
|
if ( nVars == Vec_IntSize(p->vVar2Inf) )
|
|
return;
|
|
if ( Aig_ObjIsConst1(pObj) )
|
|
return;
|
|
if ( Saig_ObjIsPo( p->pAig, pObj ) )
|
|
{
|
|
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
|
|
return;
|
|
}
|
|
if ( Aig_ObjIsCi( pObj ) )
|
|
{
|
|
if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
|
|
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
|
|
return;
|
|
}
|
|
assert( Aig_ObjIsNode(pObj) );
|
|
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
|
|
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Creates SAT solver.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
|
|
{
|
|
Vec_Int_t * vPoLits;
|
|
Aig_Obj_t * pObj;
|
|
int i, f, ObjId, nVars, RetValue = 1;
|
|
|
|
// assign variables
|
|
for ( f = p->nFramesMax - 1; f >= 0; f-- )
|
|
// for ( f = 0; f < p->nFramesMax; f++ )
|
|
Aig_Gla2AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f );
|
|
|
|
// create SAT solver
|
|
p->pSat = sat_solver_new();
|
|
sat_solver_store_alloc( p->pSat );
|
|
sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 );
|
|
|
|
// add clauses
|
|
nVars = Vec_IntSize( p->vVar2Inf );
|
|
Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i )
|
|
{
|
|
if ( ObjId == -1 )
|
|
continue;
|
|
pObj = Aig_ManObj( p->pAig, ObjId );
|
|
if ( Aig_ObjIsNode(pObj) )
|
|
{
|
|
RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
|
|
Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f),
|
|
Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f),
|
|
Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
}
|
|
else if ( Saig_ObjIsLo(p->pAig, pObj) )
|
|
{
|
|
if ( f == 0 )
|
|
{
|
|
RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
}
|
|
else
|
|
{
|
|
Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
|
|
RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
|
|
Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1),
|
|
Aig_ObjFaninC0(pObjLi) );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
}
|
|
}
|
|
else if ( Saig_ObjIsPo(p->pAig, pObj) )
|
|
{
|
|
RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
|
|
Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f),
|
|
Aig_ObjFaninC0(pObj) );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
}
|
|
else if ( Aig_ObjIsConst1(pObj) )
|
|
{
|
|
RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 );
|
|
Vec_IntPush( p->vCla2Obj, ObjId );
|
|
|
|
Vec_IntPush( p->vCla2Fra, f );
|
|
}
|
|
else assert( Saig_ObjIsPi(p->pAig, pObj) );
|
|
}
|
|
|
|
// add output clause
|
|
vPoLits = Vec_IntAlloc( p->nFramesMax );
|
|
for ( f = p->nStart; f < p->nFramesMax; f++ )
|
|
Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManCo(p->pAig, 0), f) );
|
|
RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
|
|
Vec_IntFree( vPoLits );
|
|
Vec_IntPush( p->vCla2Obj, 0 );
|
|
Vec_IntPush( p->vCla2Fra, 0 );
|
|
assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
|
|
|
|
assert( nVars == Vec_IntSize(p->vVar2Inf) );
|
|
assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
|
|
// Sto_ManDumpClauses( ((Sto_Man_t *)p->pSat->pStore), "temp_sto.cnf" );
|
|
sat_solver_store_mark_roots( p->pSat );
|
|
|
|
if ( p->fVerbose )
|
|
printf( "The resulting SAT problem contains %d variables and %d clauses.\n",
|
|
p->pSat->size, p->pSat->stats.clauses );
|
|
return RetValue;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose )
|
|
{
|
|
Aig_Gla2Man_t * p;
|
|
int i;
|
|
|
|
p = ABC_CALLOC( Aig_Gla2Man_t, 1 );
|
|
p->pAig = pAig;
|
|
|
|
p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
|
|
p->vVec2Var = Vec_IntAlloc( 1 << 20 );
|
|
p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
|
|
p->vCla2Obj = Vec_IntAlloc( 1 << 20 );
|
|
p->vCla2Fra = Vec_IntAlloc( 1 << 20 );
|
|
|
|
// skip first vector ID
|
|
p->nStart = nStart;
|
|
p->nFramesMax = nFramesMax;
|
|
p->fVerbose = fVerbose;
|
|
for ( i = 0; i < p->nFramesMax; i++ )
|
|
Vec_IntPush( p->vVec2Var, -1 );
|
|
|
|
// skip first SAT variable
|
|
Vec_IntPush( p->vVar2Inf, -1 );
|
|
Vec_IntPush( p->vVar2Inf, -1 );
|
|
return p;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Aig_Gla2ManStop( Aig_Gla2Man_t * p )
|
|
{
|
|
Vec_IntFreeP( &p->vObj2Vec );
|
|
Vec_IntFreeP( &p->vVec2Var );
|
|
Vec_IntFreeP( &p->vVar2Inf );
|
|
Vec_IntFreeP( &p->vCla2Obj );
|
|
Vec_IntFreeP( &p->vCla2Fra );
|
|
Vec_IntFreeP( &p->vVec2Use );
|
|
|
|
if ( p->pSat )
|
|
sat_solver_delete( p->pSat );
|
|
ABC_FREE( p );
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Finds the set of clauses involved in the UNSAT core.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue )
|
|
{
|
|
Vec_Int_t * vCore;
|
|
void * pSatCnf;
|
|
Intp_Man_t * pManProof;
|
|
int RetValue;
|
|
clock_t clk = clock();
|
|
if ( piRetValue )
|
|
*piRetValue = -1;
|
|
// solve the problem
|
|
RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
|
|
if ( RetValue == l_Undef )
|
|
{
|
|
printf( "Conflict limit is reached.\n" );
|
|
return NULL;
|
|
}
|
|
if ( RetValue == l_True )
|
|
{
|
|
printf( "The BMC problem is SAT.\n" );
|
|
if ( piRetValue )
|
|
*piRetValue = 0;
|
|
return NULL;
|
|
}
|
|
if ( fVerbose )
|
|
{
|
|
printf( "SAT solver returned UNSAT after %7d conflicts. ", (int)pSat->stats.conflicts );
|
|
Abc_PrintTime( 1, "Time", clock() - clk );
|
|
}
|
|
assert( RetValue == l_False );
|
|
pSatCnf = sat_solver_store_release( pSat );
|
|
// derive the UNSAT core
|
|
clk = clock();
|
|
pManProof = Intp_ManAlloc();
|
|
vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, 0 );
|
|
Intp_ManFree( pManProof );
|
|
if ( fVerbose )
|
|
{
|
|
printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) );
|
|
Abc_PrintTime( 1, "Time", clock() - clk );
|
|
}
|
|
Sto_ManFree( (Sto_Man_t *)pSatCnf );
|
|
return vCore;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Collects abstracted objects.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
|
|
{
|
|
Vec_Int_t * vResult;
|
|
Aig_Obj_t * pObj;
|
|
int i, ClaId, iVecId;
|
|
// p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) );
|
|
|
|
vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
|
|
Vec_IntWriteEntry( vResult, 0, 1 ); // add const1
|
|
Vec_IntForEachEntry( vCore, ClaId, i )
|
|
{
|
|
pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) );
|
|
if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) || Aig_ObjIsConst1(pObj) )
|
|
continue;
|
|
assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
|
|
Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
|
|
/*
|
|
// add flop inputs with multiple fanouts
|
|
if ( Saig_ObjIsLo(p->pAig, pObj) )
|
|
{
|
|
Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
|
|
if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObjLi)) )
|
|
// if ( Aig_ObjRefs( Aig_ObjFanin0(pObjLi) ) > 1 )
|
|
Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObjLi), 1 );
|
|
}
|
|
else
|
|
{
|
|
if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) )
|
|
Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObj), 1 );
|
|
if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) )
|
|
Vec_IntWriteEntry( vResult, Aig_ObjFaninId1(pObj), 1 );
|
|
}
|
|
*/
|
|
if ( p->vVec2Use )
|
|
{
|
|
iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
|
|
Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
|
|
}
|
|
}
|
|
// printf( "Number of entries %d\n", Vec_IntCountPositive(vResult) );
|
|
|
|
// count the number of objects in each frame
|
|
if ( p->vVec2Use )
|
|
{
|
|
Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax );
|
|
int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax;
|
|
for ( f = 0; f < p->nFramesMax; f++ )
|
|
for ( v = 0; v < nVecIds; v++ )
|
|
if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) )
|
|
Vec_IntAddToEntry( vCounts, f, 1 );
|
|
Vec_IntForEachEntry( vCounts, Entry, f )
|
|
printf( "%d ", Entry );
|
|
printf( "\n" );
|
|
Vec_IntFree( vCounts );
|
|
}
|
|
return vResult;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Performs gate-level localization abstraction.]
|
|
|
|
Description [Returns array of objects included in the abstraction. This array
|
|
may contain only const1, flop outputs, and internal nodes, that is, objects
|
|
that should have clauses added to the SAT solver.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose )
|
|
{
|
|
Aig_Gla2Man_t * p;
|
|
Vec_Int_t * vCore, * vResult;
|
|
clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
|
|
clock_t clk, clk2 = clock();
|
|
assert( Saig_ManPoNum(pAig) == 1 );
|
|
|
|
if ( fVerbose )
|
|
{
|
|
if ( TimeLimit )
|
|
printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
|
|
else
|
|
printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
|
|
}
|
|
|
|
// start the solver
|
|
clk = clock();
|
|
p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
|
|
if ( !Aig_Gla2CreateSatSolver( p ) )
|
|
{
|
|
printf( "Error! SAT solver became UNSAT.\n" );
|
|
Aig_Gla2ManStop( p );
|
|
return NULL;
|
|
}
|
|
sat_solver_set_random( p->pSat, fSkipRand );
|
|
p->timePre += clock() - clk;
|
|
|
|
// set runtime limit
|
|
if ( TimeLimit )
|
|
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
|
|
|
|
// compute UNSAT core
|
|
clk = clock();
|
|
vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
|
|
if ( vCore == NULL )
|
|
{
|
|
Aig_Gla2ManStop( p );
|
|
return NULL;
|
|
}
|
|
p->timeSat += clock() - clk;
|
|
p->timeTotal += clock() - clk2;
|
|
|
|
// print stats
|
|
if ( fVerbose )
|
|
{
|
|
ABC_PRTP( "Pre ", p->timePre, p->timeTotal );
|
|
ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
|
|
ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
|
|
}
|
|
|
|
// prepare return value
|
|
vResult = Aig_Gla2ManCollect( p, vCore );
|
|
Vec_IntFree( vCore );
|
|
Aig_Gla2ManStop( p );
|
|
return vResult;
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|
|
|