diff options
Diffstat (limited to 'src/proof/fra/fraClaus.c')
| -rw-r--r-- | src/proof/fra/fraClaus.c | 1875 |
1 files changed, 1875 insertions, 0 deletions
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c new file mode 100644 index 00000000..e71219b5 --- /dev/null +++ b/src/proof/fra/fraClaus.c @@ -0,0 +1,1875 @@ +/**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 "src/sat/cnf/cnf.h" +#include "src/sat/bsat/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( Abc_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 ); + Abc_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 & Abc_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 ); + Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + 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 + |