/**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 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; // clauses Vec_Int_t * vLits; Vec_Int_t * vClauses; Vec_Int_t * vCosts; int nClauses; // counter-examples Vec_Ptr_t * vCexes; int nCexes; int nCexesAlloc; }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Runs the SAT solver on the problem.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Fra_ClausRunBmc( Clu_Man_t * p ) { Aig_Obj_t * pObj; int 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[4], 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[4], 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 [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 ) { 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<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; 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 ); 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<nLeaves); j++ ) if ( uScores & (1 << j) ) Fra_ClausRecordClause( p, pCut, j, Scores[j] ); } Fra_SmlStop( pComb ); Aig_MmFixedStop( pMemCuts, 0 ); 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 [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 < 5 ); 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[4], 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, fFail = 0, fFlag;//, Lits[2]; // 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 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 < 5 ); // 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; 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 < 5 ); 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 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->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->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->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 [] ***********************************************************************/ int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fBmc, int fRefs, int fVerbose, int fVeryVerbose ) { Clu_Man_t * p; int clk, clkTotal = clock(); int Iter, Counter, nPrefOld; assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 ); // create the manager p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, 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; } // 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 ); 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 ( Counter == -2 ) printf( "Property FAILS during refinement. " ); else printf( "Property HOLDS inductively after strengthening. " ); PRT( "Time ", clock() - clkTotal ); // clean the manager Fra_ClausFree( p ); return 1; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////