luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc71208

This commit is contained in:
Alan Mishchenko 2007-12-08 08:01:00 -08:00
parent 369f008e69
commit 65687f72ae
13 changed files with 1211 additions and 129 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abc.dsp
View File

@ -2626,6 +2626,10 @@ SOURCE=.\src\aig\fra\fraClau.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraClaus.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraCnf.c
# End Source File
# Begin Source File

2
src/aig/aig/aigHaig.c
View File

@ -192,7 +192,7 @@ clk = clock();
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
// create the SAT solver to be used for this problem
pSat = Cnf_DataWriteIntoSolver( pCnf );
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n",
Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) );

2
src/aig/cnf/cnf.h
View File

@ -134,7 +134,7 @@ extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
/*=== cnfMap.c ========================================================*/
extern void Cnf_DeriveMapping( Cnf_Man_t * p );
extern int Cnf_ManMapForCnf( Cnf_Man_t * p );

64
src/aig/cnf/cnfMan.c
View File

@ -172,12 +172,13 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
SeeAlso []
***********************************************************************/
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
{
sat_solver * pSat;
int i, status;
int i, f, status;
assert( nFrames > 0 );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, p->nVars );
sat_solver_setnvars( pSat, p->nVars * nFrames );
for ( i = 0; i < p->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
@ -186,6 +187,63 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
return NULL;
}
}
if ( nFrames > 1 )
{
Aig_Obj_t * pObjLo, * pObjLi;
int nLitsAll, * pLits, Lits[2];
nLitsAll = 2 * p->nVars;
pLits = p->pClauses[0];
for ( f = 1; f < nFrames; f++ )
{
// add equality of register inputs/outputs for different timeframes
Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
{
Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return NULL;
}
Lits[0]++;
Lits[1]--;
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return NULL;
}
}
// add clauses for the next timeframe
for ( i = 0; i < p->nLiterals; i++ )
pLits[i] += nLitsAll;
for ( i = 0; i < p->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
{
sat_solver_delete( pSat );
return NULL;
}
}
}
// return literals to their original state
nLitsAll = (f-1) * nLitsAll;
for ( i = 0; i < p->nLiterals; i++ )
pLits[i] -= nLitsAll;
}
if ( fInit )
{
Aig_Obj_t * pObjLo;
int Lits[1];
Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
{
Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) )
{
sat_solver_delete( pSat );
return NULL;
}
}
}
status = sat_solver_simplify(pSat);
if ( status == 0 )
{

2
src/aig/cnf/cnfWrite.c
View File

@ -207,6 +207,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// allocate CNF
pCnf = ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf->pMan = p->pManAig;
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ALLOC( int *, nClauses + 1 );
@ -346,6 +347,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
// allocate CNF
pCnf = ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf->pMan = p;
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ALLOC( int *, nClauses + 1 );

2
src/aig/fra/fraCec.c
View File

@ -54,7 +54,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
pCnf = Cnf_Derive( pMan, 0 );
// pCnf = Cnf_DeriveSimple( pMan, 0 );
// convert into the SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf );
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
Cnf_DataFree( pCnf );
// solve SAT

52
src/aig/fra/fraClau.c
View File

@ -233,7 +233,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
//Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain );
p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
/*
{
int i;
@ -248,7 +248,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL );
assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest );
p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
// derive one timeframe to be checked for BMC
@ -256,7 +256,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
//Aig_ManShow( pFramesBmc, 0, NULL );
assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc );
p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
// create variable sets
p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) );
@ -496,11 +496,11 @@ void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew )
LitN = Vec_IntEntry( vNew, j );
VarM = lit_var( LitM );
VarN = lit_var( LitN );
if ( VarM > VarN )
if ( VarM < VarN )
{
assert( 0 );
}
else if ( VarM < VarN )
else if ( VarM > VarN )
{
j++;
}
@ -587,14 +587,14 @@ void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExt
// copy literals without the given one
Vec_IntClear( vBasis );
Vec_IntForEachEntry( vExtra, iLit2, k )
if ( iLit2 != iLit )
if ( k != i )
Vec_IntPush( vBasis, iLit2 );
// try whether it is inductive
if ( !Fra_ClauCheckClause( p, vBasis, NULL ) )
continue;
// the clause is inductive
// remove the literal
for ( k = iLit; k < Vec_IntSize(vExtra)-1; k++ )
for ( k = i; k < Vec_IntSize(vExtra)-1; k++ )
Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) );
Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 );
}
@ -620,11 +620,11 @@ void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
LitM = Vec_IntEntry( vCex, i );
VarM = lit_var( LitM );
VarN = Vec_IntEntry( vSatCsVars, j );
if ( VarM > VarN )
if ( VarM < VarN )
{
assert( 0 );
}
else if ( VarM < VarN )
else if ( VarM > VarN )
{
j++;
printf( "-" );
@ -650,7 +650,7 @@ void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
SeeAlso []
***********************************************************************/
int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
{
Cla_Man_t * p;
int Iter, RetValue, fFailed, i;
@ -669,7 +669,7 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
printf( "%4d : ", Iter );
// remap clause into the test manager
Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 );
if ( fVerbose )
if ( fVerbose && fVeryVerbose )
Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
// the main counter-example is in p->vCexMain
// intermediate counter-examples are in p->vCexTest
@ -679,8 +679,17 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
{
Fra_ClauReduceClause( p->vCexMain, p->vCexTest );
Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 );
if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
// if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
if ( Vec_IntSize(p->vCexMain) < 1 )
{
Vec_IntComplement( p->vCexMain0 );
RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexMain0), Vec_IntArray(p->vCexMain0) + Vec_IntSize(p->vCexMain0) );
if ( RetValue == 0 )
{
printf( "\nProperty is proved after %d iterations.\n", Iter+1 );
return 0;
}
fFailed = 1;
break;
}
@ -698,14 +707,21 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
continue;
}
if ( fVerbose )
printf( " LitsAfterRed = %3d. ", Vec_IntSize(p->vCexMain) );
printf( " " );
if ( fVerbose && fVeryVerbose )
Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
if ( fVerbose )
printf( " LitsInd = %3d. ", Vec_IntSize(p->vCexMain) );
// minimize the inductive property
Vec_IntClear( p->vCexBase );
if ( Vec_IntSize(p->vCexMain) > 1 )
// Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain );
// Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
assert( Vec_IntSize(p->vCexMain) > 0 );
if ( fVerbose && fVeryVerbose )
Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
if ( fVerbose )
printf( " LitsAfterMin = %3d. ", Vec_IntSize(p->vCexMain) );
printf( " LitsRed = %3d. ", Vec_IntSize(p->vCexMain) );
if ( fVerbose )
printf( "\n" );
// add the clause to the solver
@ -716,6 +732,12 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose )
Iter++;
break;
}
if ( p->pSatMain->qtail != p->pSatMain->qhead )
{
RetValue = sat_solver_simplify(p->pSatMain);
assert( RetValue != 0 );
assert( p->pSatMain->qtail == p->pSatMain->qhead );
}
}
// report the results

912
src/aig/fra/fraClaus.c Normal file
View File

@ -0,0 +1,912 @@
/**CFile****************************************************************
FileName [fraClaus.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Induction with clause strengthening.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
#include "cnf.h"
#include "satSolver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Clu_Man_t_ Clu_Man_t;
struct Clu_Man_t_
{
// parameters
int nFrames;
int nClausesMax;
int fVerbose;
int fVeryVerbose;
int nSimWords;
int nSimFrames;
// the network
Aig_Man_t * pAig;
// SAT solvers
sat_solver * pSatMain;
sat_solver * pSatBmc;
// CNF for the test solver
Cnf_Dat_t * pCnf;
// the counter example
Vec_Int_t * vValues;
// clauses
Vec_Int_t * vLits;
Vec_Int_t * vClauses;
Vec_Int_t * vCosts;
int nClauses;
// counter-examples
Vec_Ptr_t * vCexes;
int nCexes;
int nCexesAlloc;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Runs the SAT solver on the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausRunBmc( Clu_Man_t * p )
{
Aig_Obj_t * pObj;
int * pLits;
int nBTLimit = 0;
int i, RetValue;
pLits = ALLOC( int, p->nFrames + 1 );
// set the output literals
pObj = Aig_ManPo(p->pAig, 0);
for ( i = 0; i < p->nFrames; i++ )
pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
// try to solve the problem
// sat_solver_act_var_clear( p->pSatBmc );
// RetValue = sat_solver_solve( p->pSatBmc, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
for ( i = 0; i < p->nFrames; i++ )
{
RetValue = sat_solver_solve( p->pSatBmc, pLits + i, pLits + i + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
{
free( pLits );
return 0;
}
}
free( pLits );
/*
// get the counter-example
assert( RetValue == l_True );
nVarsTot = p->nFrames * p->pCnf->nVars;
Aig_ManForEachObj( p->pAig, pObj, i )
Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatBmc, nVarsTot + p->pCnf->pVarNums[i]) );
*/
return 1;
}
/**Function*************************************************************
Synopsis [Runs the SAT solver on the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausRunSat( Clu_Man_t * p )
{
int nBTLimit = 0;
Aig_Obj_t * pObj;
int * pLits;
int i, nVarsTot, RetValue;
pLits = ALLOC( int, p->nFrames + 1 );
// set the output literals
pObj = Aig_ManPo(p->pAig, 0);
for ( i = 0; i <= p->nFrames; i++ )
pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames );
// try to solve the problem
// sat_solver_act_var_clear( p->pSatMain );
// RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
free( pLits );
if ( RetValue == l_False )
return 1;
// get the counter-example
assert( RetValue == l_True );
nVarsTot = p->nFrames * p->pCnf->nVars;
Aig_ManForEachObj( p->pAig, pObj, i )
Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatMain, nVarsTot + p->pCnf->pVarNums[i]) );
return 0;
}
/**Function*************************************************************
Synopsis [Runs the SAT solver on the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausRunSat0( Clu_Man_t * p )
{
int nBTLimit = 0;
Aig_Obj_t * pObj;
int Lits[2], RetValue;
pObj = Aig_ManPo(p->pAig, 0);
Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue == l_False )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
/*
int Fra_ClausProcessClausesCut( Clu_Man_t * p, Dar_Cut_t * pCut )
{
unsigned * pSimsC[4], * pSimsS[4];
int pLits[4];
int i, b, k, iMint, uMask, RetValue, nLeaves, nWordsTotal, nCounter;
// compute parameters
nLeaves = pCut->nLeaves;
nWordsTotal = p->pComb->nWordsTotal;
assert( nLeaves > 1 && nLeaves < 5 );
assert( nWordsTotal == p->pSeq->nWordsTotal );
// get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ )
{
pSimsC[i] = Fra_ObjSim( p->pComb, pCut->pLeaves[i] );
pSimsS[i] = Fra_ObjSim( p->pSeq, pCut->pLeaves[i] );
}
// add combinational patterns
uMask = 0;
for ( i = 0; i < nWordsTotal; i++ )
for ( k = 0; k < 32; k++ )
{
iMint = 0;
for ( b = 0; b < nLeaves; b++ )
if ( pSimsC[b][i] & (1 << k) )
iMint |= (1 << b);
uMask |= (1 << iMint);
}
// remove sequential patterns
for ( i = 0; i < nWordsTotal; i++ )
for ( k = 0; k < 32; k++ )
{
iMint = 0;
for ( b = 0; b < nLeaves; b++ )
if ( pSimsS[b][i] & (1 << k) )
iMint |= (1 << b);
uMask &= ~(1 << iMint);
}
if ( uMask == 0 )
return 0;
// add clauses for the remaining patterns
nCounter = 0;
for ( i = 0; i < (1<<nLeaves); i++ )
{
if ( (uMask & (1 << i)) == 0 )
continue;
nCounter++;
// continue;
// add every third clause
// if ( (nCounter % 2) == 0 )
// continue;
for ( b = 0; b < nLeaves; b++ )
pLits[b] = toLitCond( p->pCnf->pVarNums[pCut->pLeaves[b]], (i&(1<<b)) );
// add the clause
RetValue = sat_solver_addclause( p->pSatMain, pLits, pLits + nLeaves );
// assert( RetValue == 1 );
if ( RetValue == 0 )
{
printf( "Already UNSAT after %d clauses.\n", nCounter );
return -1;
}
}
return nCounter;
}
*/
/**Function*************************************************************
Synopsis [Return combinations appearing in the cut.]
Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.]
SideEffects []
SeeAlso []
***********************************************************************/
void transpose32a( unsigned a[32] )
{
int j, k;
unsigned long m, t;
for ( j = 16, m = 0x0000FFFF; j; j >>= 1, m ^= m << j )
{
for ( k = 0; k < 32; k = ((k | j) + 1) & ~j )
{
t = (a[k] ^ (a[k|j] >> j)) & m;
a[k] ^= t;
a[k|j] ^= (t << j);
}
}
}
/**Function*************************************************************
Synopsis [Return combinations appearing in the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
{
unsigned Matrix[32];
unsigned * pSims[4], uWord;
int nSeries, i, k, j;
// compute parameters
assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
assert( pSimMan->nWordsTotal % 8 == 0 );
// get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ )
pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] );
// add combinational patterns
memset( pScores, 0, sizeof(int) * 16 );
nSeries = pSimMan->nWordsTotal / 8;
for ( i = 0; i < nSeries; i++ )
{
memset( Matrix, 0, sizeof(unsigned) * 32 );
for ( k = 0; k < 8; k++ )
for ( j = 0; j < (int)pCut->nLeaves; j++ )
Matrix[31-(k*4+j)] = pSims[j][i*8+k];
/*
for ( k = 0; k < 32; k++ )
{
Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
}
printf( "\n" );
*/
transpose32a( Matrix );
/*
for ( k = 0; k < 32; k++ )
{
Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
}
printf( "\n" );
*/
for ( k = 0; k < 32; k++ )
for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
pScores[uWord & 0xF]++;
}
// collect patterns
uWord = 0;
for ( i = 0; i < 16; i++ )
if ( pScores[i] )
uWord |= (1 << i);
// Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
return (int)uWord;
}
/**Function*************************************************************
Synopsis [Return combinations appearing in the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
{
unsigned * pSims[4], uWord;
int iMint, i, k, b;
// compute parameters
assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
assert( pSimMan->nWordsTotal % 8 == 0 );
// get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ )
pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] );
// add combinational patterns
memset( pScores, 0, sizeof(int) * 16 );
for ( i = 0; i < pSimMan->nWordsTotal; i++ )
for ( k = 0; k < 32; k++ )
{
iMint = 0;
for ( b = 0; b < (int)pCut->nLeaves; b++ )
if ( pSims[b][i] & (1 << k) )
iMint |= (1 << b);
pScores[iMint]++;
}
// collect patterns
uWord = 0;
for ( i = 0; i < 16; i++ )
if ( pScores[i] )
uWord |= (1 << i);
// Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
return (int)uWord;
}
/**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost )
{
int i;
for ( i = 0; i < (int)pCut->nLeaves; i++ )
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pLeaves[i]], (iMint&(1<<i)) ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, Cost );
}
/**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausProcessClauses( Clu_Man_t * p )
{
Aig_MmFixed_t * pMemCuts;
Fra_Sml_t * pComb, * pSeq;
Aig_Obj_t * pObj;
Dar_Cut_t * pCut;
int Scores[16], uScores, i, k, j, clk, nCuts = 0;
// simulate the AIG
clk = clock();
srand( 0xAABBAABB );
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nSimFrames, p->nSimWords/p->nSimFrames );
if ( pSeq->fNonConstOut )
{
printf( "Property failed after sequential simulation!\n" );
Fra_SmlStop( pSeq );
return 0;
}
PRT( "Sim-seq", clock() - clk );
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
pMemCuts = Dar_ManComputeCuts( p->pAig, 10 );
PRT( "Cuts ", clock() - clk );
// collect sequential info for each cut
clk = clock();
Aig_ManForEachNode( p->pAig, pObj, i )
Dar_ObjForEachCut( pObj, pCut, k )
if ( pCut->nLeaves > 1 )
{
pCut->uTruth = Fra_ClausProcessClausesCut( p, pSeq, pCut, Scores );
// uScores = Fra_ClausProcessClausesCut2( p, pSeq, pCut, Scores );
// if ( uScores != pCut->uTruth )
// {
// int x = 0;
// }
}
PRT( "Infoseq", clock() - clk );
Fra_SmlStop( pSeq );
// perform combinational simulation
clk = clock();
srand( 0xAABBAABB );
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords );
PRT( "Sim-cmb", clock() - clk );
// collect combinational info for each cut
clk = clock();
Aig_ManForEachNode( p->pAig, pObj, i )
Dar_ObjForEachCut( pObj, pCut, k )
if ( pCut->nLeaves > 1 )
{
nCuts++;
uScores = Fra_ClausProcessClausesCut( p, pComb, pCut, Scores );
uScores &= ~pCut->uTruth; pCut->uTruth = 0;
if ( uScores == 0 )
continue;
// write the clauses
for ( j = 0; j < (1<<pCut->nLeaves); j++ )
if ( uScores & (1 << j) )
Fra_ClausRecordClause( p, pCut, j, Scores[j] );
}
Fra_SmlStop( pComb );
Aig_MmFixedStop( pMemCuts, 0 );
PRT( "Infocmb", clock() - clk );
printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n",
Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
return 1;
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausBmcClauses( Clu_Man_t * p )
{
int nBTLimit = 0;
int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
/*
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
printf( "%d ", p->vLits->pArray[i] );
printf( "\n" );
*/
// add the clauses
Counter = 0;
nLitsTot = 2 * p->pCnf->nVars;
for ( f = 0; f < p->nFrames; f++ )
{
Beg = 0;
Vec_IntForEachEntry( p->vClauses, End, i )
{
if ( Vec_IntEntry( p->vCosts, i ) == -1 )
{
Beg = End;
continue;
}
assert( Vec_IntEntry( p->vCosts, i ) > 0 );
assert( End - Beg < 5 );
pStart = Vec_IntArray(p->vLits);
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
if ( RetValue != l_False )
{
Beg = End;
Vec_IntWriteEntry( p->vCosts, i, -1 );
Counter++;
continue;
}
/*
// add the clause
RetValue = sat_solver_addclause( p->pSatBmc, pStart + Beg, pStart + End );
// assert( RetValue == 1 );
if ( RetValue == 0 )
{
printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
return -1;
}
*/
Beg = End;
// simplify the solver
if ( p->pSatBmc->qtail != p->pSatBmc->qhead )
{
RetValue = sat_solver_simplify(p->pSatBmc);
assert( RetValue != 0 );
assert( p->pSatBmc->qtail == p->pSatBmc->qhead );
}
}
// increment literals
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] += nLitsTot;
}
// return clauses back to normal
nLitsTot = p->nFrames * nLitsTot;
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] -= nLitsTot;
/*
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
printf( "%d ", p->vLits->pArray[i] );
printf( "\n" );
*/
return Counter;
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausInductiveClauses( Clu_Man_t * p )
{
int nBTLimit = 0;
int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
// reset the solver
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
if ( p->pSatMain == NULL )
{
printf( "Error: Main solver is unsat.\n" );
return -1;
}
/*
// check if the property holds
if ( Fra_ClausRunSat0( p ) )
printf( "Property holds without strengthening.\n" );
else
printf( "Property does not hold without strengthening.\n" );
*/
// add the clauses
nLitsTot = 2 * p->pCnf->nVars;
for ( f = 0; f < p->nFrames; f++ )
{
Beg = 0;
Vec_IntForEachEntry( p->vClauses, End, i )
{
if ( Vec_IntEntry( p->vCosts, i ) == -1 )
{
Beg = End;
continue;
}
assert( Vec_IntEntry( p->vCosts, i ) > 0 );
assert( End - Beg < 5 );
pStart = Vec_IntArray(p->vLits);
// add the clause to all timeframes
RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
if ( RetValue == 0 )
{
printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
return -1;
}
Beg = End;
}
// increment literals
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] += nLitsTot;
}
// simplify the solver
if ( p->pSatMain->qtail != p->pSatMain->qhead )
{
RetValue = sat_solver_simplify(p->pSatMain);
assert( RetValue != 0 );
assert( p->pSatMain->qtail == p->pSatMain->qhead );
}
// check if the property holds
if ( Fra_ClausRunSat0( p ) )
{
// printf( "Property holds with strengthening.\n" );
printf( " Property holds. " );
}
else
{
printf( " Property fails. " );
return -2;
}
/*
// add the property for the first K frames
for ( i = 0; i < p->nFrames; i++ )
{
Aig_Obj_t * pObj;
int Lits[2];
// set the output literals
pObj = Aig_ManPo(p->pAig, 0);
Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
// add the clause
RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
// assert( RetValue == 1 );
if ( RetValue == 0 )
{
printf( "Error: Solver is UNSAT after adding property for the first K frames.\n" );
return -1;
}
}
*/
// simplify the solver
if ( p->pSatMain->qtail != p->pSatMain->qhead )
{
RetValue = sat_solver_simplify(p->pSatMain);
assert( RetValue != 0 );
assert( p->pSatMain->qtail == p->pSatMain->qhead );
}
// check the clause in the last timeframe
Beg = 0;
Counter = 0;
Vec_IntForEachEntry( p->vClauses, End, i )
{
if ( Vec_IntEntry( p->vCosts, i ) == -1 )
{
Beg = End;
continue;
}
assert( Vec_IntEntry( p->vCosts, i ) > 0 );
assert( End - Beg < 5 );
pStart = Vec_IntArray(p->vLits);
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
// the problem is not solved
if ( RetValue != l_False )
{
Beg = End;
Vec_IntWriteEntry( p->vCosts, i, -1 );
Counter++;
continue;
}
// add the clause
RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
// assert( RetValue == 1 );
if ( RetValue == 0 )
{
printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
return -1;
}
Beg = End;
// simplify the solver
if ( p->pSatMain->qtail != p->pSatMain->qhead )
{
RetValue = sat_solver_simplify(p->pSatMain);
assert( RetValue != 0 );
assert( p->pSatMain->qtail == p->pSatMain->qhead );
}
}
// return clauses back to normal
nLitsTot = p->nFrames * nLitsTot;
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] -= nLitsTot;
return Counter;
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fVerbose, int fVeryVerbose )
{
Clu_Man_t * p;
p = ALLOC( Clu_Man_t, 1 );
memset( p, 0, sizeof(Clu_Man_t) );
p->pAig = pAig;
p->nFrames = nFrames;
p->nClausesMax = nClausesMax;
p->fVerbose = fVerbose;
p->fVeryVerbose = fVeryVerbose;
p->nSimWords = 256;//1024;//64;
p->nSimFrames = 16;//8;//32;
p->vValues = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
p->vLits = Vec_IntAlloc( 1<<14 );
p->vClauses = Vec_IntAlloc( 1<<12 );
p->vCosts = Vec_IntAlloc( 1<<12 );
p->nCexesAlloc = 1024;
p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig), p->nCexesAlloc/32 );
Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
return p;
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausFree( Clu_Man_t * p )
{
if ( p->vCexes ) Vec_PtrFree( p->vCexes );
if ( p->vLits ) Vec_IntFree( p->vLits );
if ( p->vClauses ) Vec_IntFree( p->vClauses );
if ( p->vCosts ) Vec_IntFree( p->vCosts );
if ( p->vValues ) Vec_IntFree( p->vValues );
if ( p->pCnf ) Cnf_DataFree( p->pCnf );
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
free( p );
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fBmc, int fVerbose, int fVeryVerbose )
{
Clu_Man_t * p;
int clk, clkTotal = clock();
int Iter, Counter;
assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
// create the manager
p = Fra_ClausAlloc( pAig, nFrames, nClausesMax, fVerbose, fVeryVerbose );
clk = clock();
// derive CNF
p->pAig->nRegs++;
p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
p->pAig->nRegs--;
PRT( "CNF ", clock() - clk );
// check BMC
clk = clock();
p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames, 1 );
if ( p->pSatBmc == NULL )
{
printf( "Error: BMC solver is unsat.\n" );
Fra_ClausFree( p );
return 1;
}
if ( !Fra_ClausRunBmc( p ) )
{
printf( "Problem trivially fails the base case.\n" );
Fra_ClausFree( p );
return 1;
}
PRT( "SAT try", clock() - clk );
// start the SAT solver
clk = clock();
p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
if ( p->pSatMain == NULL )
{
printf( "Error: Main solver is unsat.\n" );
Fra_ClausFree( p );
return 1;
}
// try solving without additional clauses
if ( Fra_ClausRunSat( p ) )
{
printf( "Problem is inductive without strengthening.\n" );
Fra_ClausFree( p );
return 1;
}
PRT( "SAT try", clock() - clk );
// collect the candidate inductive clauses using 4-cuts
clk = clock();
Fra_ClausProcessClauses( p );
p->nClauses = Vec_IntSize( p->vClauses );
PRT( "Clauses", clock() - clk );
// check clauses using BMC
if ( fBmc )
{
clk = clock();
Counter = Fra_ClausBmcClauses( p );
p->nClauses -= Counter;
printf( "BMC disproved %d clauses.\n", Counter );
PRT( "Cla-bmc", clock() - clk );
}
// prove clauses inductively
clk = clock();
Counter = 1;
for ( Iter = 0; Counter > 0; Iter++ )
{
printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
Counter = Fra_ClausInductiveClauses( p );
if ( Counter > 0 )
p->nClauses -= Counter;
printf( "End = %5d. ", p->nClauses );
// printf( "\n" );
PRT( "Time", clock() - clk );
clk = clock();
}
if ( Counter == -1 )
printf( "Fra_Claus(): Internal error.\n" );
else if ( Counter == -2 )
printf( "Property FAILS after %d iterations of refinement.\n", Iter );
else
printf( "Property HOLDS inductively after strengthening.\n" );
/*
clk = clock();
if ( Fra_ClausRunSat( p ) )
printf( "Problem is solved.\n" );
else
printf( "Problem is unsolved.\n" );
PRT( "SAT try", clock() - clk );
*/
PRT( "TOTAL ", clock() - clkTotal );
printf( "\n" );
// clean the manager
Fra_ClausFree( p );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/fra/fraInd.c
View File

@ -339,7 +339,7 @@ PRT( "Time", clock() - clk );
// Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
// Fra_ManPartitionTest2( pManAigNew );
// Aig_ManStop( pManAigNew );
// iterate the inductive case
p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@ -365,7 +365,7 @@ p->timeTrav += clock() - clk2;
pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
p->pSat = Cnf_DataWriteIntoSolver( pCnf );
p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
p->nSatVars = pCnf->nVars;
assert( p->pSat != NULL );
if ( p->pSat == NULL )

34
src/base/abci/abc.c
View File

@ -6193,8 +6193,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;//, * pNtkRes;
int c;
int fBmc;
int nFrames;
int nLevels;
int fVerbose;
int fVeryVerbose;
// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
// extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
@ -6207,20 +6210,34 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVeryVerbose = 0;
fVerbose = 1;
nLevels = 1000;
fBmc = 1;
nFrames = 1;
nLevels = 200;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FNbvwh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
@ -6232,9 +6249,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nLevels < 0 )
goto usage;
break;
case 'b':
fBmc ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -6355,12 +6378,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
// Abc_NtkDarHaigRecord( pNtk );
Abc_NtkDarClau( pNtk, 1000, fVerbose );
Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
return 0;
usage:
fprintf( pErr, "usage: test [-h]\n" );
fprintf( pErr, "usage: test [-vwh]\n" );
fprintf( pErr, "\t testbench for new procedures\n" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}

16
src/base/abci/abcDar.c
View File

@ -56,12 +56,20 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
if ( i < Abc_NtkPiNum(pNtk) )
{
assert( Abc_ObjIsPi(pObj) );
if ( !Abc_ObjIsPi(pObj) )
printf( "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
}
else
assert( Abc_ObjIsBo(pObj) );
Abc_NtkForEachCo( pNtk, pObj, i )
if ( i < Abc_NtkPoNum(pNtk) )
{
assert( Abc_ObjIsPo(pObj) );
if ( !Abc_ObjIsPo(pObj) )
printf( "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
}
else
assert( Abc_ObjIsBi(pObj) );
// print warning about initial values
@ -1401,9 +1409,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
SeeAlso []
***********************************************************************/
int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose )
{
extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose );
extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClauses, int fBmc, int fVerbose, int fVeryVerbose );
Aig_Man_t * pMan;
if ( Abc_NtkPoNum(pNtk) != 1 )
{
@ -1418,7 +1427,8 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
Fra_Clau( pMan, nStepsMax, fVerbose );
// Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
Fra_Claus( pMan, nFrames, nStepsMax, fBmc, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
return 1;
}

4
src/base/io/ioReadAiger.c
View File

@ -237,8 +237,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Counter++;
}
if ( Counter )
printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
// if ( Counter )
// printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
}
else
{

242
src/misc/vec/vecPtr.h
View File

@ -149,71 +149,6 @@ static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
return p;
}
/**Function*************************************************************
Synopsis [Allocates the array of simulation info.]
Description [Allocates the array containing given number of entries,
each of which contains given number of unsigned words of simulation data.
The resulting array can be freed using regular procedure Vec_PtrFree().
It is the responsibility of the user to ensure this array is never grown.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
{
void ** pMemory;
unsigned * pInfo;
int i;
pMemory = (void **)ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
pInfo = (unsigned *)(pMemory + nEntries);
for ( i = 0; i < nEntries; i++ )
pMemory[i] = pInfo + i * nWords;
return Vec_PtrAllocArray( pMemory, nEntries );
}
/**Function*************************************************************
Synopsis [Allocates the array of truth tables for the given number of vars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocTruthTables( int nVars )
{
Vec_Ptr_t * p;
unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
unsigned * pTruth;
int i, k, nWords;
nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
p = Vec_PtrAllocSimInfo( nVars, nWords );
for ( i = 0; i < nVars; i++ )
{
pTruth = (unsigned *)p->pArray[i];
if ( i < 5 )
{
for ( k = 0; k < nWords; k++ )
pTruth[k] = Masks[i];
}
else
{
for ( k = 0; k < nWords; k++ )
if ( k & (1 << (i-5)) )
pTruth[k] = ~(unsigned)0;
else
pTruth[k] = 0;
}
}
return p;
}
/**Function*************************************************************
Synopsis [Duplicates the integer array.]
@ -346,37 +281,6 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
return p->pArray[i];
}
/**Function*************************************************************
Synopsis [Resizes the array of simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
{
Vec_Ptr_t * vInfoNew;
int nWords;
assert( Vec_PtrSize(vInfo) > 2 );
// get the new array
nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
vInfoNew = Vec_PtrAllocSimInfo( 2*Vec_PtrSize(vInfo), nWords );
// copy the simulation info
memcpy( Vec_PtrEntry(vInfoNew,0), Vec_PtrEntry(vInfo,0), Vec_PtrSize(vInfo) * nWords * 4 );
// replace the array
free( vInfo->pArray );
vInfo->pArray = vInfoNew->pArray;
vInfo->nSize *= 2;
vInfo->nCap *= 2;
// free the old array
vInfoNew->pArray = NULL;
free( vInfoNew );
}
/**Function*************************************************************
Synopsis []
@ -753,6 +657,152 @@ static inline void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
p->nSize = k;
}
/**Function*************************************************************
Synopsis [Allocates the array of simulation info.]
Description [Allocates the array containing given number of entries,
each of which contains given number of unsigned words of simulation data.
The resulting array can be freed using regular procedure Vec_PtrFree().
It is the responsibility of the user to ensure this array is never grown.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
{
void ** pMemory;
unsigned * pInfo;
int i;
pMemory = (void **)ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
pInfo = (unsigned *)(pMemory + nEntries);
for ( i = 0; i < nEntries; i++ )
pMemory[i] = pInfo + i * nWords;
return Vec_PtrAllocArray( pMemory, nEntries );
}
/**Function*************************************************************
Synopsis [Cleans simulation info of each entry beginning with iWord.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrCleanSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords )
{
int i;
for ( i = 0; i < vInfo->nSize; i++ )
memset( (char*)Vec_PtrEntry(vInfo,i) + 4*iWord, 0, 4*(nWords-iWord) );
}
/**Function*************************************************************
Synopsis [Resizes the array of simulation info.]
Description [Doubles the number of objects for which siminfo is allocated.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
{
Vec_Ptr_t * vInfoNew;
int nWords;
assert( Vec_PtrSize(vInfo) > 1 );
// get the new array
nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
vInfoNew = Vec_PtrAllocSimInfo( 2*Vec_PtrSize(vInfo), nWords );
// copy the simulation info
memcpy( Vec_PtrEntry(vInfoNew,0), Vec_PtrEntry(vInfo,0), Vec_PtrSize(vInfo) * nWords * 4 );
// replace the array
free( vInfo->pArray );
vInfo->pArray = vInfoNew->pArray;
vInfo->nSize *= 2;
vInfo->nCap *= 2;
// free the old array
vInfoNew->pArray = NULL;
free( vInfoNew );
}
/**Function*************************************************************
Synopsis [Resizes the array of simulation info.]
Description [Doubles the number of simulation patterns stored for each object.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrReallocSimInfo( Vec_Ptr_t * vInfo )
{
Vec_Ptr_t * vInfoNew;
int nWords, i;
assert( Vec_PtrSize(vInfo) > 1 );
// get the new array
nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
vInfoNew = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), 2*nWords );
// copy the simulation info
for ( i = 0; i < vInfo->nSize; i++ )
memcpy( Vec_PtrEntry(vInfoNew,i), Vec_PtrEntry(vInfo,i), nWords * 4 );
// replace the array
free( vInfo->pArray );
vInfo->pArray = vInfoNew->pArray;
// free the old array
vInfoNew->pArray = NULL;
free( vInfoNew );
}
/**Function*************************************************************
Synopsis [Allocates the array of truth tables for the given number of vars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocTruthTables( int nVars )
{
Vec_Ptr_t * p;
unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
unsigned * pTruth;
int i, k, nWords;
nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
p = Vec_PtrAllocSimInfo( nVars, nWords );
for ( i = 0; i < nVars; i++ )
{
pTruth = (unsigned *)p->pArray[i];
if ( i < 5 )
{
for ( k = 0; k < nWords; k++ )
pTruth[k] = Masks[i];
}
else
{
for ( k = 0; k < nWords; k++ )
if ( k & (1 << (i-5)) )
pTruth[k] = ~(unsigned)0;
else
pTruth[k] = 0;
}
}
return p;
}
#endif