/**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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Clu_Man_t_ Clu_Man_t;
struct Clu_Man_t_
{
// parameters
int nFrames; // the K of the K-step induction
int nPref; // the number of timeframes to skip
int nClausesMax; // the max number of 4-clauses to consider
int nLutSize; // the max cut size
int nLevels; // the number of levels for cut computation
int nCutsMax; // the maximum number of cuts to compute at a node
int nBatches; // the number of clause batches to use
int fStepUp; // increase cut size for each batch
int fTarget; // tries to prove the property
int fVerbose;
int fVeryVerbose;
// internal parameters
int nSimWords; // the number of simulation words
int nSimWordsPref; // the number of simulation words in the prefix
int nSimFrames; // the number of frames to simulate
int nBTLimit; // the largest number of backtracks (0 = infinite)
// the network
Aig_Man_t * pAig;
// SAT solvers
sat_solver * pSatMain;
sat_solver * pSatBmc;
// CNF for the test solver
Cnf_Dat_t * pCnf;
int fFail;
int fFiltering;
int fNothingNew;
// clauses
Vec_Int_t * vLits;
Vec_Int_t * vClauses;
Vec_Int_t * vCosts;
int nClauses;
int nCuts;
int nOneHots;
int nOneHotsProven;
// clauses proven
Vec_Int_t * vLitsProven;
Vec_Int_t * vClausesProven;
// 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 Lits[2], nLitsTot, RetValue, i;
// set the output literals
nLitsTot = 2 * p->pCnf->nVars;
pObj = Aig_ManPo(p->pAig, 0);
for ( i = 0; i < p->nPref + p->nFrames; i++ )
{
Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue != l_False )
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Runs the SAT solver on the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausRunSat( Clu_Man_t * p )
{
Aig_Obj_t * pObj;
int * pLits;
int i, RetValue;
pLits = ABC_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
RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
ABC_FREE( pLits );
if ( RetValue == l_False )
return 1;
// get the counter-example
assert( RetValue == l_True );
return 0;
}
/**Function*************************************************************
Synopsis [Runs the SAT solver on the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausRunSat0( Clu_Man_t * p )
{
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, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_False )
return 1;
return 0;
}
/**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[16], uWord;
int nSeries, i, k, j;
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
// compute parameters
assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
assert( nWordsForSim % 8 == 0 );
// get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ )
pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
// add combinational patterns
memset( pScores, 0, sizeof(int) * 16 );
nSeries = nWordsForSim / 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];
transpose32a( Matrix );
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[16], uWord;
int iMint, i, k, b;
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
// compute parameters
assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
assert( nWordsForSim % 8 == 0 );
// get parameters
for ( i = 0; i < (int)pCut->nLeaves; i++ )
pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
// add combinational patterns
memset( pScores, 0, sizeof(int) * 16 );
for ( i = 0; i < nWordsForSim; 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 [Return the number of combinations appearing in the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores )
{
unsigned Matrix[32];
unsigned * pSims[16], uWord;
int iMint, i, j, k, b, nMints, nSeries;
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
// compute parameters
assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
assert( nWordsForSim % 8 == 0 );
// get parameters
for ( i = 0; i < (int)pCut->nFanins; i++ )
pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref;
// add combinational patterns
nMints = (1 << pCut->nFanins);
memset( pScores, 0, sizeof(int) * nMints );
if ( pCut->nLeafMax == 4 )
{
// convert the simulation patterns
nSeries = nWordsForSim / 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->nFanins; j++ )
Matrix[31-(k*4+j)] = pSims[j][i*8+k];
transpose32a( Matrix );
for ( k = 0; k < 32; k++ )
for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
pScores[uWord & 0xF]++;
}
}
else
{
// go through the simulation patterns
for ( i = 0; i < nWordsForSim; i++ )
for ( k = 0; k < 32; k++ )
{
iMint = 0;
for ( b = 0; b < (int)pCut->nFanins; b++ )
if ( pSims[b][i] & (1 << k) )
iMint |= (1 << b);
pScores[iMint]++;
}
}
}
/**Function*************************************************************
Synopsis [Returns the cut-off cost.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSelectClauses( Clu_Man_t * p )
{
int * pCostCount, nClauCount, Cost, CostMax, i, c;
assert( Vec_IntSize(p->vClauses) > p->nClausesMax );
// count how many implications have each cost
CostMax = p->nSimWords * 32 + 1;
pCostCount = ABC_ALLOC( int, CostMax );
memset( pCostCount, 0, sizeof(int) * CostMax );
Vec_IntForEachEntry( p->vCosts, Cost, i )
{
if ( Cost == -1 )
continue;
assert( Cost < CostMax );
pCostCount[ Cost ]++;
}
assert( pCostCount[0] == 0 );
// select the bound on the cost (above this bound, implication will be included)
nClauCount = 0;
for ( c = CostMax - 1; c > 0; c-- )
{
assert( pCostCount[c] >= 0 );
nClauCount += pCostCount[c];
if ( nClauCount >= p->nClausesMax )
break;
}
// collect implications with the given costs
nClauCount = 0;
Vec_IntForEachEntry( p->vCosts, Cost, i )
{
if ( Cost >= c && nClauCount < p->nClausesMax )
{
nClauCount++;
continue;
}
Vec_IntWriteEntry( p->vCosts, i, -1 );
}
ABC_FREE( pCostCount );
p->nClauses = nClauCount;
if ( p->fVerbose )
printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
return c;
}
/**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 []
***********************************************************************/
void Fra_ClausRecordClause2( Clu_Man_t * p, Aig_Cut_t * pCut, int iMint, int Cost )
{
int i;
for ( i = 0; i < (int)pCut->nFanins; i++ )
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, Cost );
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSmlNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
pSims = Fra_ObjSim(pSeq, pObj->Id);
for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
if ( pSims[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if implications holds.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSmlNodesAreImp( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
unsigned * pSimL, * pSimR;
int k;
pSimL = Fra_ObjSim(pSeq, pObj1->Id);
pSimR = Fra_ObjSim(pSeq, pObj2->Id);
for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
if ( pSimL[k] & ~pSimR[k] ) // !(Obj1 -> Obj2)
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if implications holds.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSmlNodesAreImpC( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
unsigned * pSimL, * pSimR;
int k;
pSimL = Fra_ObjSim(pSeq, pObj1->Id);
pSimR = Fra_ObjSim(pSeq, pObj2->Id);
for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
if ( pSimL[k] & pSimR[k] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
{
Aig_Obj_t * pObj1, * pObj2;
unsigned * pSims1, * pSims2;
int CostMax, i, k, nCountConst, nCountImps;
nCountConst = nCountImps = 0;
CostMax = p->nSimWords * 32;
/*
// add the property
{
Aig_Obj_t * pObj;
int Lits[1];
pObj = Aig_ManPo( p->pAig, 0 );
Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
Vec_IntPush( p->vLits, Lits[0] );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountConst++;
// printf( "Added the target property to the set of clauses to be inductively checked.\n" );
}
*/
pSeq->nWordsPref = p->nSimWordsPref;
Aig_ManForEachLoSeq( p->pAig, pObj1, i )
{
pSims1 = Fra_ObjSim( pSeq, pObj1->Id );
if ( Fra_ClausSmlNodeIsConst( pSeq, pObj1 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountConst++;
continue;
}
Aig_ManForEachLoSeq( p->pAig, pObj2, k )
{
pSims2 = Fra_ObjSim( pSeq, pObj2->Id );
if ( Fra_ClausSmlNodesAreImp( pSeq, pObj1, pObj2 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 0 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountImps++;
continue;
}
if ( Fra_ClausSmlNodesAreImp( pSeq, pObj2, pObj1 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 0 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountImps++;
continue;
}
if ( Fra_ClausSmlNodesAreImpC( pSeq, pObj1, pObj2 ) )
{
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
Vec_IntPush( p->vCosts, CostMax );
nCountImps++;
continue;
}
}
if ( nCountConst + nCountImps > p->nClausesMax / 2 )
break;
}
pSeq->nWordsPref = 0;
if ( p->fVerbose )
printf( "Collected %d register constants and %d one-hotness implications.\n", nCountConst, nCountImps );
p->nOneHots = nCountConst + nCountImps;
p->nOneHotsProven = 0;
return 0;
}
/**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
{
Aig_MmFixed_t * pMemCuts;
// Aig_ManCut_t * pManCut;
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 );
Aig_ManRandom(1);
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
if ( p->fTarget && pSeq->fNonConstOut )
{
printf( "Property failed after sequential simulation!\n" );
Fra_SmlStop( pSeq );
return 0;
}
if ( p->fVerbose )
{
ABC_PRT( "Sim-seq", clock() - clk );
}
clk = clock();
if ( fRefs )
{
Fra_ClausCollectLatchClauses( p, pSeq );
if ( p->fVerbose )
{
ABC_PRT( "Lat-cla", clock() - clk );
}
}
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
// pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
if ( p->fVerbose )
{
ABC_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;
// }
}
if ( p->fVerbose )
{
ABC_PRT( "Infoseq", clock() - clk );
}
Fra_SmlStop( pSeq );
// perform combinational simulation
clk = clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
if ( p->fVerbose )
{
ABC_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 );
// Aig_ManCutStop( pManCut );
if ( p->fVerbose )
{
ABC_PRT( "Infocmb", clock() - clk );
}
if ( p->fVerbose )
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 );
if ( Vec_IntSize(p->vClauses) > p->nClausesMax )
Fra_ClausSelectClauses( p );
else
p->nClauses = Vec_IntSize( p->vClauses );
return 1;
}
/**Function*************************************************************
Synopsis [Processes the clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
{
// Aig_MmFixed_t * pMemCuts;
Aig_ManCut_t * pManCut;
Fra_Sml_t * pComb, * pSeq;
Aig_Obj_t * pObj;
Aig_Cut_t * pCut;
int i, k, j, clk, nCuts = 0;
int ScoresSeq[1<<12], ScoresComb[1<<12];
assert( p->nLutSize < 13 );
// simulate the AIG
clk = clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
if ( p->fTarget && pSeq->fNonConstOut )
{
printf( "Property failed after sequential simulation!\n" );
Fra_SmlStop( pSeq );
return 0;
}
if ( p->fVerbose )
{
//ABC_PRT( "Sim-seq", clock() - clk );
}
// perform combinational simulation
clk = clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
if ( p->fVerbose )
{
//ABC_PRT( "Sim-cmb", clock() - clk );
}
clk = clock();
if ( fRefs )
{
Fra_ClausCollectLatchClauses( p, pSeq );
if ( p->fVerbose )
{
//ABC_PRT( "Lat-cla", clock() - clk );
}
}
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
// pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
if ( p->fVerbose )
{
//ABC_PRT( "Cuts ", clock() - clk );
}
// collect combinational info for each cut
clk = clock();
Aig_ManForEachNode( p->pAig, pObj, i )
{
if ( pObj->Level > (unsigned)p->nLevels )
continue;
Aig_ObjForEachCut( pManCut, pObj, pCut, k )
if ( pCut->nFanins > 1 )
{
nCuts++;
Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq );
Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb );
// write the clauses
for ( j = 0; j < (1<<pCut->nFanins); j++ )
if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 )
Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] );
}
}
Fra_SmlStop( pSeq );
Fra_SmlStop( pComb );
p->nCuts = nCuts;
// Aig_MmFixedStop( pMemCuts, 0 );
Aig_ManCutStop( pManCut );
p->pAig->pManCuts = NULL;
if ( p->fVerbose )
{
printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n",
Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", clock() - clk );
}
// filter out clauses that are contained in the already proven clauses
assert( p->nClauses == 0 );
p->nClauses = Vec_IntSize( p->vClauses );
if ( Vec_IntSize( p->vClausesProven ) > 0 )
{
int RetValue, k, Beg;
int End = -1; // Suppress "might be used uninitialized"
int * pStart;
// reset the solver
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
if ( p->pSatMain == NULL )
{
printf( "Error: Main solver is unsat.\n" );
return -1;
}
// add the proven clauses
Beg = 0;
pStart = Vec_IntArray(p->vLitsProven);
Vec_IntForEachEntry( p->vClausesProven, End, i )
{
assert( End - Beg <= p->nLutSize );
// 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;
}
assert( End == Vec_IntSize(p->vLitsProven) );
// check the clauses
Beg = 0;
pStart = Vec_IntArray(p->vLits);
Vec_IntForEachEntry( p->vClauses, End, i )
{
assert( Vec_IntEntry( p->vCosts, i ) >= 0 );
assert( End - Beg <= p->nLutSize );
// check the clause
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
// the clause holds
if ( RetValue == l_False )
{
Vec_IntWriteEntry( p->vCosts, i, -1 );
p->nClauses--;
}
Beg = End;
}
assert( End == Vec_IntSize(p->vLits) );
if ( p->fVerbose )
printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n",
Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) );
}
p->fFiltering = 0;
if ( p->nClauses > p->nClausesMax )
{
Fra_ClausSelectClauses( p );
p->fFiltering = 1;
}
return 1;
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausBmcClauses( Clu_Man_t * p )
{
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;
// skip through the prefix variables
if ( p->nPref )
{
nLitsTot = p->nPref * 2 * p->pCnf->nVars;
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] += nLitsTot;
}
// go through the timeframes
nLitsTot = 2 * p->pCnf->nVars;
pStart = Vec_IntArray(p->vLits);
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 <= p->nLutSize );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)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->nPref + 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 [Cleans simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausSimInfoClean( Clu_Man_t * p )
{
assert( p->pCnf->nVars <= Vec_PtrSize(p->vCexes) );
Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
p->nCexes = 0;
}
/**Function*************************************************************
Synopsis [Reallocs simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausSimInfoRealloc( Clu_Man_t * p )
{
assert( p->nCexes == p->nCexesAlloc );
Vec_PtrReallocSimInfo( p->vCexes );
Vec_PtrCleanSimInfo( p->vCexes, p->nCexesAlloc/32, 2 * p->nCexesAlloc/32 );
p->nCexesAlloc *= 2;
}
/**Function*************************************************************
Synopsis [Records simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
{
int i;
if ( p->nCexes == p->nCexesAlloc )
Fra_ClausSimInfoRealloc( p );
assert( p->nCexes < p->nCexesAlloc );
for ( i = 0; i < p->pCnf->nVars; i++ )
{
if ( pModel[i] == l_True )
{
assert( Aig_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
Aig_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes );
}
}
p->nCexes++;
}
/**Function*************************************************************
Synopsis [Uses the simulation info.]
Description [Returns 1 if the simulation info disproved the clause.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
{
unsigned * pSims[16], uWord;
int nWords, iVar, i, w;
for ( i = 0; i < nLits; i++ )
{
iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars;
assert( iVar > 0 && iVar < p->pCnf->nVars );
pSims[i] = (unsigned *)Vec_PtrEntry( p->vCexes, iVar );
}
nWords = p->nCexes / 32;
for ( w = 0; w < nWords; w++ )
{
uWord = ~(unsigned)0;
for ( i = 0; i < nLits; i++ )
uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
if ( uWord )
return 1;
}
if ( p->nCexes % 32 )
{
uWord = ~(unsigned)0;
for ( i = 0; i < nLits; i++ )
uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
if ( uWord & Aig_InfoMask( p->nCexes % 32 ) )
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClausInductiveClauses( Clu_Man_t * p )
{
// Aig_Obj_t * pObjLi, * pObjLo;
int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2];
p->fFail = 0;
// reset the solver
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
if ( p->pSatMain == NULL )
{
printf( "Error: Main solver is unsat.\n" );
return -1;
}
Fra_ClausSimInfoClean( p );
/*
// 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 constant registers
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
if ( Aig_ObjFanin0(pObjLi) == Aig_ManConst1(p->pAig) )
{
for ( k = 0; k < p->nFrames; k++ )
{
Lits[0] = k * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObjLo->Id], Aig_ObjFaninC0(pObjLi) );
RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
if ( RetValue == 0 )
{
printf( "Error: Solver is UNSAT after adding constant-register clauses.\n" );
return -1;
}
}
}
*/
// add the proven clauses
nLitsTot = 2 * p->pCnf->nVars;
pStart = Vec_IntArray(p->vLitsProven);
for ( f = 0; f < p->nFrames; f++ )
{
Beg = 0;
Vec_IntForEachEntry( p->vClausesProven, End, i )
{
assert( End - Beg <= p->nLutSize );
// 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->vLitsProven); i++ )
p->vLitsProven->pArray[i] += nLitsTot;
}
// return clauses back to normal
nLitsTot = (p->nFrames) * nLitsTot;
for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
p->vLitsProven->pArray[i] -= nLitsTot;
/*
// add the proven clauses
nLitsTot = 2 * p->pCnf->nVars;
pStart = Vec_IntArray(p->vLitsProven);
Beg = 0;
Vec_IntForEachEntry( p->vClausesProven, End, i )
{
assert( End - Beg <= p->nLutSize );
// 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;
}
*/
// add the clauses
nLitsTot = 2 * p->pCnf->nVars;
pStart = Vec_IntArray(p->vLits);
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 <= p->nLutSize );
// 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 ( p->fTarget )
{
if ( Fra_ClausRunSat0( p ) )
{
if ( p->fVerbose )
printf( " Property holds. " );
}
else
{
if ( p->fVerbose )
printf( " Property fails. " );
// return -2;
p->fFail = 1;
}
}
/*
// 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 <= p->nLutSize );
if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
{
fFlag = 1;
// printf( "s-" );
Beg = End;
Vec_IntWriteEntry( p->vCosts, i, -1 );
Counter++;
continue;
}
else
{
fFlag = 0;
// printf( "s?" );
}
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
// the problem is not solved
if ( RetValue != l_False )
{
// printf( "S- " );
Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
// RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
// assert( RetValue );
Beg = End;
Vec_IntWriteEntry( p->vCosts, i, -1 );
Counter++;
continue;
}
// printf( "S+ " );
// assert( !fFlag );
/*
// 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 proved 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;
// if ( fFail )
// return -2;
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 nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose )
{
Clu_Man_t * p;
p = ABC_ALLOC( Clu_Man_t, 1 );
memset( p, 0, sizeof(Clu_Man_t) );
p->pAig = pAig;
p->nFrames = nFrames;
p->nPref = nPref;
p->nClausesMax = nClausesMax;
p->nLutSize = nLutSize;
p->nLevels = nLevels;
p->nCutsMax = nCutsMax;
p->nBatches = nBatches;
p->fStepUp = fStepUp;
p->fTarget = fTarget;
p->fVerbose = fVerbose;
p->fVeryVerbose = fVeryVerbose;
p->nSimWords = 512;//1024;//64;
p->nSimFrames = 32;//8;//32;
p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
p->vLits = Vec_IntAlloc( 1<<14 );
p->vClauses = Vec_IntAlloc( 1<<12 );
p->vCosts = Vec_IntAlloc( 1<<12 );
p->vLitsProven = Vec_IntAlloc( 1<<14 );
p->vClausesProven= Vec_IntAlloc( 1<<12 );
p->nCexesAlloc = 1024;
p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, 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->vLitsProven ) Vec_IntFree( p->vLitsProven );
if ( p->vClausesProven ) Vec_IntFree( p->vClausesProven );
if ( p->vCosts ) Vec_IntFree( p->vCosts );
if ( p->pCnf ) Cnf_DataFree( p->pCnf );
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausAddToStorage( Clu_Man_t * p )
{
int * pStart;
int Beg, End, Counter, i, k;
Beg = 0;
Counter = 0;
pStart = Vec_IntArray( p->vLits );
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 <= p->nLutSize );
for ( k = Beg; k < End; k++ )
Vec_IntPush( p->vLitsProven, pStart[k] );
Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
Beg = End;
Counter++;
if ( i < p->nOneHots )
p->nOneHotsProven++;
}
if ( p->fVerbose )
printf( "Added to storage %d proved clauses (including %d one-hot clauses)\n", Counter, p->nOneHotsProven );
Vec_IntClear( p->vClauses );
Vec_IntClear( p->vLits );
Vec_IntClear( p->vCosts );
p->nClauses = 0;
p->fNothingNew = (int)(Counter == 0);
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausPrintIndClauses( Clu_Man_t * p )
{
int Counters[9] = {0};
int * pStart;
int Beg, End, i;
Beg = 0;
pStart = Vec_IntArray( p->vLitsProven );
Vec_IntForEachEntry( p->vClausesProven, End, i )
{
if ( End - Beg >= 8 )
Counters[8]++;
else
Counters[End - Beg]++;
//printf( "%d ", End-Beg );
Beg = End;
}
printf( "SUMMARY: Total proved clauses = %d. ", Vec_IntSize(p->vClausesProven) );
printf( "Clause per lit: " );
for ( i = 0; i < 8; i++ )
if ( Counters[i] )
printf( "%d=%d ", i, Counters[i] );
if ( Counters[8] )
printf( ">7=%d ", Counters[8] );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Writes the clauses into an AIGER file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
{
Aig_Obj_t * pLiteral;
int NodeId = pVar2Id[ lit_var(Lit) ];
assert( NodeId >= 0 );
pLiteral = (Aig_Obj_t *)Aig_ManObj( p->pAig, NodeId )->pData;
return Aig_NotCond( pLiteral, lit_sign(Lit) );
}
/**Function*************************************************************
Synopsis [Writes the clauses into an AIGER file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausWriteIndClauses( Clu_Man_t * p )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
Aig_Man_t * pNew;
Aig_Obj_t * pClause, * pLiteral;
char * pName;
int * pStart, * pVar2Id;
int Beg, End, i, k;
// create mapping from SAT vars to node IDs
pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
if ( p->pCnf->pVarNums[i] >= 0 )
{
assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
pVar2Id[ p->pCnf->pVarNums[i] ] = i;
}
// start the manager
pNew = Aig_ManDupWithoutPos( p->pAig );
// add the clauses
Beg = 0;
pStart = Vec_IntArray( p->vLitsProven );
Vec_IntForEachEntry( p->vClausesProven, End, i )
{
pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] );
for ( k = Beg + 1; k < End; k++ )
{
pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
pClause = Aig_Or( pNew, pClause, pLiteral );
}
Aig_ObjCreatePo( pNew, pClause );
Beg = End;
}
ABC_FREE( pVar2Id );
Aig_ManCleanup( pNew );
pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
Ioa_WriteAiger( pNew, pName, 0, 1 );
Aig_ManStop( pNew );
}
/**Function*************************************************************
Synopsis [Checks if the clause holds using the given simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausEstimateCoverageOne( Fra_Sml_t * pSim, int * pLits, int nLits, int * pVar2Id, unsigned * pResult )
{
unsigned * pSims[16];
int iVar, i, w;
for ( i = 0; i < nLits; i++ )
{
iVar = lit_var(pLits[i]);
pSims[i] = Fra_ObjSim( pSim, pVar2Id[iVar] );
}
for ( w = 0; w < pSim->nWordsTotal; w++ )
{
pResult[w] = ~(unsigned)0;
for ( i = 0; i < nLits; i++ )
pResult[w] &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
}
}
/**Function*************************************************************
Synopsis [Estimates the coverage of state space by clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausEstimateCoverage( Clu_Man_t * p )
{
int nCombSimWords = (1<<11);
Fra_Sml_t * pComb;
unsigned * pResultTot, * pResultOne;
int nCovered, Beg, End, i, w;
int * pStart, * pVar2Id;
int clk = clock();
// simulate the circuit with nCombSimWords * 32 = 64K patterns
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
// create mapping from SAT vars to node IDs
pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
if ( p->pCnf->pVarNums[i] >= 0 )
{
assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
pVar2Id[ p->pCnf->pVarNums[i] ] = i;
}
// get storage for one assignment and all assignments
assert( Aig_ManPoNum(p->pAig) > 2 );
pResultOne = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 0)->Id );
pResultTot = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 1)->Id );
// start the OR of don't-cares
for ( w = 0; w < nCombSimWords; w++ )
pResultTot[w] = 0;
// check clauses
Beg = 0;
pStart = Vec_IntArray( p->vLitsProven );
Vec_IntForEachEntry( p->vClausesProven, End, i )
{
Fra_ClausEstimateCoverageOne( pComb, pStart + Beg, End-Beg, pVar2Id, pResultOne );
Beg = End;
for ( w = 0; w < nCombSimWords; w++ )
pResultTot[w] |= pResultOne[w];
}
// count the total number of patterns contained in the don't-care
nCovered = 0;
for ( w = 0; w < nCombSimWords; w++ )
nCovered += Aig_WordCountOnes( pResultTot[w] );
Fra_SmlStop( pComb );
ABC_FREE( pVar2Id );
// print the result
printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
ABC_PRT( "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
{
Clu_Man_t * p;
int clk, clkTotal = clock(), clkInd;
int b, Iter, Counter, nPrefOld;
int nClausesBeg = 0;
// create the manager
p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fTarget, fVerbose, fVeryVerbose );
if ( p->fVerbose )
{
printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
//ABC_PRT( "Sim-seq", clock() - clk );
}
assert( !p->fTarget || Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
clk = clock();
// derive CNF
// if ( p->fTarget )
// p->pAig->nRegs++;
p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
// if ( p->fTarget )
// p->pAig->nRegs--;
if ( fVerbose )
{
//ABC_PRT( "CNF ", clock() - clk );
}
// check BMC
clk = clock();
p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
if ( p->pSatBmc == NULL )
{
printf( "Error: BMC solver is unsat.\n" );
Fra_ClausFree( p );
return 1;
}
if ( p->fTarget && !Fra_ClausRunBmc( p ) )
{
printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames );
Fra_ClausFree( p );
return 1;
}
if ( fVerbose )
{
//ABC_PRT( "SAT-bmc", clock() - clk );
}
// start the SAT solver
clk = clock();
p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
if ( p->pSatMain == NULL )
{
printf( "Error: Main solver is unsat.\n" );
Fra_ClausFree( p );
return 1;
}
for ( b = 0; b < p->nBatches; b++ )
{
// if ( fVerbose )
printf( "*** BATCH %d: ", b+1 );
if ( b && p->nLutSize < 12 && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
p->nLutSize++;
printf( "Using %d-cuts.\n", p->nLutSize );
// try solving without additional clauses
if ( p->fTarget && Fra_ClausRunSat( p ) )
{
printf( "Problem is inductive without strengthening.\n" );
Fra_ClausFree( p );
return 1;
}
if ( fVerbose )
{
// ABC_PRT( "SAT-ind", clock() - clk );
}
// collect the candidate inductive clauses using 4-cuts
clk = clock();
nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
// Fra_ClausProcessClauses( p, fRefs );
Fra_ClausProcessClauses2( p, fRefs );
p->nPref = nPrefOld;
p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
nClausesBeg = p->nClauses;
//ABC_PRT( "Clauses", clock() - clk );
// check clauses using BMC
if ( fBmc )
{
clk = clock();
Counter = Fra_ClausBmcClauses( p );
p->nClauses -= Counter;
if ( fVerbose )
{
printf( "BMC disproved %d clauses. ", Counter );
ABC_PRT( "Time", clock() - clk );
}
}
// prove clauses inductively
clkInd = clk = clock();
Counter = 1;
for ( Iter = 0; Counter > 0; Iter++ )
{
if ( fVerbose )
printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
Counter = Fra_ClausInductiveClauses( p );
if ( Counter > 0 )
p->nClauses -= Counter;
if ( fVerbose )
{
printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
// printf( "\n" );
ABC_PRT( "Time", clock() - clk );
}
clk = clock();
}
// add proved clauses to storage
Fra_ClausAddToStorage( p );
// report the results
if ( p->fTarget )
{
if ( Counter == -1 )
printf( "Fra_Claus(): Internal error. " );
else if ( p->fFail )
printf( "Property FAILS during refinement. " );
else
printf( "Property HOLDS inductively after strengthening. " );
ABC_PRT( "Time ", clock() - clkTotal );
if ( !p->fFail )
break;
}
else
{
printf( "Finished proving inductive clauses. " );
ABC_PRT( "Time ", clock() - clkTotal );
}
}
// verify the computed interpolant
Fra_InvariantVerify( pAig, nFrames, p->vClausesProven, p->vLitsProven );
// printf( "THIS COMMAND IS KNOWN TO HAVE A BUG!\n" );
// if ( !p->fTarget && p->fVerbose )
if ( p->fVerbose )
{
Fra_ClausPrintIndClauses( p );
Fra_ClausEstimateCoverage( p );
}
if ( !p->fTarget )
{
Fra_ClausWriteIndClauses( p );
}
/*
// print the statistic into a file
{
FILE * pTable;
assert( p->nBatches == 1 );
pTable = fopen( "stats.txt", "a+" );
fprintf( pTable, "%s ", pAig->pName );
fprintf( pTable, "%d ", Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig) );
fprintf( pTable, "%d ", Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig) );
fprintf( pTable, "%d ", Aig_ManRegNum(pAig) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pAig) );
fprintf( pTable, "%d ", p->nCuts );
fprintf( pTable, "%d ", nClausesBeg );
fprintf( pTable, "%d ", p->nClauses );
fprintf( pTable, "%d ", Iter );
fprintf( pTable, "%.2f ", (float)(clkInd-clkTotal)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "%.2f ", (float)(clock()-clkInd)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "%.2f ", (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "\n" );
fclose( pTable );
}
*/
// clean the manager
Fra_ClausFree( p );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END