diff options
Diffstat (limited to 'src/aig/fra/fraClaus.c')
| -rw-r--r-- | src/aig/fra/fraClaus.c | 1561 |
1 files changed, 0 insertions, 1561 deletions
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c deleted file mode 100644 index 7e8d7dd1..00000000 --- a/src/aig/fra/fraClaus.c +++ /dev/null @@ -1,1561 +0,0 @@ -/**CFile**************************************************************** - - FileName [fraClaus.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [New FRAIG package.] - - Synopsis [Induction with clause strengthening.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 30, 2007.] - - Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "fra.h" -#include "cnf.h" -#include "satSolver.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Clu_Man_t_ Clu_Man_t; -struct Clu_Man_t_ -{ - // parameters - int nFrames; // 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 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; - // clauses proven - Vec_Int_t * vLitsProven; - Vec_Int_t * vClausesProven; - int nClausesProven; - // 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, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)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 = 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, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); - 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, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)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 * pSims[16]; - int iMint, i, k, b, nMints; - 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 ); - // 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 = 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 ); - } - 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; - 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 constants and %d implications.\n", nCountConst, nCountImps ); - 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 ); - pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames ); - if ( pSeq->fNonConstOut ) - { - printf( "Property failed after sequential simulation!\n" ); - Fra_SmlStop( pSeq ); - return 0; - } -if ( p->fVerbose ) -{ -PRT( "Sim-seq", clock() - clk ); -} - - -clk = clock(); - if ( fRefs ) - { - Fra_ClausCollectLatchClauses( p, pSeq ); -if ( p->fVerbose ) -{ -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 ) -{ -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 ) -{ -PRT( "Infoseq", clock() - clk ); -} - Fra_SmlStop( pSeq ); - - // perform combinational simulation -clk = clock(); - srand( 0xAABBAABB ); - pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); -if ( p->fVerbose ) -{ -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 ) -{ -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 ); - pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames ); - if ( pSeq->fNonConstOut ) - { - printf( "Property failed after sequential simulation!\n" ); - Fra_SmlStop( pSeq ); - return 0; - } -if ( p->fVerbose ) -{ -PRT( "Sim-seq", clock() - clk ); -} - - // perform combinational simulation -clk = clock(); - srand( 0xAABBAABB ); - pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); -if ( p->fVerbose ) -{ -PRT( "Sim-cmb", clock() - clk ); -} - - -clk = clock(); - if ( fRefs ) - { - Fra_ClausCollectLatchClauses( p, pSeq ); -if ( p->fVerbose ) -{ -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 ) -{ -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 ); -// Aig_MmFixedStop( pMemCuts, 0 ); - Aig_ManCutStop( pManCut ); - p->pAig->pManCuts = NULL; -if ( p->fVerbose ) -{ -PRT( "Infosim", 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 ); - - // 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, End, * pStart; - // reset the solver - if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); - p->pSatMain = 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, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)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, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); - for ( k = Beg; k < End; k++ ) - pStart[k] = lit_neg( pStart[k] ); - - if ( RetValue != l_False ) - { - Beg = End; - Vec_IntWriteEntry( p->vCosts, i, -1 ); - Counter++; - continue; - } -/* - // add the clause - RetValue = sat_solver_addclause( p->pSatBmc, pStart + Beg, pStart + End ); - // assert( RetValue == 1 ); - if ( RetValue == 0 ) - { - printf( "Error: Solver is UNSAT after adding BMC clauses.\n" ); - return -1; - } -*/ - Beg = End; - - // simplify the solver - if ( p->pSatBmc->qtail != p->pSatBmc->qhead ) - { - RetValue = sat_solver_simplify(p->pSatBmc); - assert( RetValue != 0 ); - assert( p->pSatBmc->qtail == p->pSatBmc->qhead ); - } - } - // increment literals - for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) - p->vLits->pArray[i] += nLitsTot; - } - - // return clauses back to normal - nLitsTot = (p->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( Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 ); - Aig_InfoSetBit( 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] = 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 = 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 ( 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, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); - for ( k = Beg; k < End; k++ ) - pStart[k] = lit_neg( pStart[k] ); - - // the problem is not solved - if ( RetValue != l_False ) - { -// 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 fVerbose, int fVeryVerbose ) -{ - Clu_Man_t * p; - p = ALLOC( Clu_Man_t, 1 ); - memset( p, 0, sizeof(Clu_Man_t) ); - p->pAig = pAig; - p->nFrames = nFrames; - p->nPref = nPref; - p->nClausesMax = nClausesMax; - p->nLutSize = nLutSize; - p->nLevels = nLevels; - p->nCutsMax = nCutsMax; - p->nBatches = nBatches; - p->fStepUp = fStepUp; - 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 ); - 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 ( p->fVerbose ) - printf( "Added to storage %d proved clauses\n", Counter ); - - 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 [] - -***********************************************************************/ -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 fVerbose, int fVeryVerbose ) -{ - Clu_Man_t * p; - int clk, clkTotal = clock(); - int b, Iter, Counter, nPrefOld; - - assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 ); - - // create the manager - p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fVerbose, fVeryVerbose ); - -clk = clock(); - // derive CNF - p->pAig->nRegs++; - p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) ); - p->pAig->nRegs--; -if ( fVerbose ) -{ -PRT( "CNF ", clock() - clk ); -} - - // check BMC -clk = clock(); - p->pSatBmc = 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 ( !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 ) -{ -PRT( "SAT-bmc", clock() - clk ); -} - - // start the SAT solver -clk = clock(); - p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 ); - if ( p->pSatMain == NULL ) - { - printf( "Error: Main solver is unsat.\n" ); - Fra_ClausFree( p ); - return 1; - } - - - for ( b = 0; b < p->nBatches; b++ ) - { -// if ( fVerbose ) - printf( "*** BATCH %d: ", b+1 ); - if ( b && (!p->fFiltering || p->fNothingNew || p->fStepUp) ) - p->nLutSize++; - printf( "Using %d-cuts.\n", p->nLutSize ); - - // try solving without additional clauses - if ( Fra_ClausRunSat( p ) ) - { - printf( "Problem is inductive without strengthening.\n" ); - Fra_ClausFree( p ); - return 1; - } - if ( fVerbose ) - { - 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; - - //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.\n", Counter ); - PRT( "Cla-bmc", clock() - clk ); - } - } - - - // prove clauses inductively - 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" ); - PRT( "Time", clock() - clk ); - } - clk = clock(); - } - if ( Counter == -1 ) - printf( "Fra_Claus(): Internal error. " ); - else if ( p->fFail ) - printf( "Property FAILS during refinement. " ); - else - printf( "Property HOLDS inductively after strengthening. " ); - PRT( "Time ", clock() - clkTotal ); - - if ( !p->fFail ) - break; - - // add proved clauses to storage - Fra_ClausAddToStorage( p ); - } - - // clean the manager - Fra_ClausFree( p ); - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |