diff options
Diffstat (limited to 'src/abc8/fra/fraClau.c')
| -rw-r--r-- | src/abc8/fra/fraClau.c | 759 |
1 files changed, 0 insertions, 759 deletions
diff --git a/src/abc8/fra/fraClau.c b/src/abc8/fra/fraClau.c deleted file mode 100644 index fc239a40..00000000 --- a/src/abc8/fra/fraClau.c +++ /dev/null @@ -1,759 +0,0 @@ -/**CFile**************************************************************** - - FileName [fraClau.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" - -/* - This code is inspired by the paper: Aaron Bradley and Zohar Manna, - "Checking safety by inductive generalization of counterexamples to - induction", FMCAD '07. -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Cla_Man_t_ Cla_Man_t; -struct Cla_Man_t_ -{ - // SAT solvers - sat_solver * pSatMain; - sat_solver * pSatTest; - sat_solver * pSatBmc; - // CNF for the test solver -// Cnf_Dat_t * pCnfTest; - // SAT variables - Vec_Int_t * vSatVarsMainCs; - Vec_Int_t * vSatVarsTestCs; - Vec_Int_t * vSatVarsTestNs; - Vec_Int_t * vSatVarsBmcNs; - // helper variables - int nSatVarsTestBeg; - int nSatVarsTestCur; - // counter-examples - Vec_Int_t * vCexMain0; - Vec_Int_t * vCexMain; - Vec_Int_t * vCexTest; - Vec_Int_t * vCexBase; - Vec_Int_t * vCexAssm; - Vec_Int_t * vCexBmc; - // mapping of CS into NS var numbers - int * pMapCsMainToCsTest; - int * pMapCsTestToCsMain; - int * pMapCsTestToNsTest; - int * pMapCsTestToNsBmc; -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Saves variables corresponding to latch outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Fra_ClauSaveLatchVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int fCsVars ) -{ - Vec_Int_t * vVars; - Aig_Obj_t * pObjLo, * pObjLi; - int i; - vVars = Vec_IntAlloc( Aig_ManRegNum(pMan) ); - Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i ) - Vec_IntPush( vVars, pCnf->pVarNums[fCsVars? pObjLo->Id : pObjLi->Id] ); - return vVars; -} - -/**Function************************************************************* - - Synopsis [Saves variables corresponding to latch outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf ) -{ - Vec_Int_t * vVars; - Aig_Obj_t * pObj; - int i; - vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) ); - Aig_ManForEachPo( pMan, pObj, i ) - Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] ); - return vVars; -} - -/**Function************************************************************* - - Synopsis [Saves variables corresponding to latch outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStarting ) -{ - Vec_Int_t * vVars; - Aig_Obj_t * pObj; - int i; - vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting ); - Aig_ManForEachPi( pMan, pObj, i ) - { - if ( i < nStarting ) - continue; - Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] ); - } - return vVars; -} - -/**Function************************************************************* - - Synopsis [Saves variables corresponding to latch outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, int nVarsMax ) -{ - int * pMapping, Var, i; - assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) ); - pMapping = ALLOC( int, nVarsMax ); - for ( i = 0; i < nVarsMax; i++ ) - pMapping[i] = -1; - Vec_IntForEachEntry( vSatVarsFrom, Var, i ) - pMapping[Var] = Vec_IntEntry(vSatVarsTo,i); - return pMapping; -} - - -/**Function************************************************************* - - Synopsis [Deletes the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ClauStop( Cla_Man_t * p ) -{ - free( p->pMapCsMainToCsTest ); - free( p->pMapCsTestToCsMain ); - free( p->pMapCsTestToNsTest ); - free( p->pMapCsTestToNsBmc ); - Vec_IntFree( p->vSatVarsMainCs ); - Vec_IntFree( p->vSatVarsTestCs ); - Vec_IntFree( p->vSatVarsTestNs ); - Vec_IntFree( p->vSatVarsBmcNs ); - Vec_IntFree( p->vCexMain0 ); - Vec_IntFree( p->vCexMain ); - Vec_IntFree( p->vCexTest ); - Vec_IntFree( p->vCexBase ); - Vec_IntFree( p->vCexAssm ); - Vec_IntFree( p->vCexBmc ); - if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); - if ( p->pSatTest ) sat_solver_delete( p->pSatTest ); - if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Takes the AIG with the single output to be checked.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) -{ - Cla_Man_t * p; - Cnf_Dat_t * pCnfMain; - Cnf_Dat_t * pCnfTest; - Cnf_Dat_t * pCnfBmc; - Aig_Man_t * pFramesMain; - Aig_Man_t * pFramesTest; - Aig_Man_t * pFramesBmc; - assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); - - // start the manager - p = ALLOC( Cla_Man_t, 1 ); - memset( p, 0, sizeof(Cla_Man_t) ); - p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) ); - p->vCexMain = Vec_IntAlloc( Aig_ManRegNum(pMan) ); - p->vCexTest = Vec_IntAlloc( Aig_ManRegNum(pMan) ); - p->vCexBase = Vec_IntAlloc( Aig_ManRegNum(pMan) ); - p->vCexAssm = Vec_IntAlloc( Aig_ManRegNum(pMan) ); - p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) ); - - // derive two timeframes to be checked - pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs -//Aig_ManShow( pFramesMain, 0, NULL ); - assert( Aig_ManPoNum(pFramesMain) == 2 ); - Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output - pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 ); -//Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 ); - p->pSatMain = Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 ); -/* - { - int i; - Aig_Obj_t * pObj; - Aig_ManForEachObj( pFramesMain, pObj, i ) - printf( "%d -> %d \n", pObj->Id, pCnfMain->pVarNums[pObj->Id] ); - printf( "\n" ); - } -*/ - - // derive one timeframe to be checked - pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL ); - assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) ); - pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) ); - p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 ); - p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest ); - - // derive one timeframe to be checked for BMC - pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL ); -//Aig_ManShow( pFramesBmc, 0, NULL ); - assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) ); - pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) ); - p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 ); - - // create variable sets - p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) ); - p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 ); - p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 ); - p->vSatVarsBmcNs = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc ); - assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsMainCs) ); - assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsBmcNs) ); - - // create mapping of CS into NS vars - p->pMapCsMainToCsTest = Fra_ClauCreateMapping( p->vSatVarsMainCs, p->vSatVarsTestCs, Aig_ManObjNumMax(pFramesMain) ); - p->pMapCsTestToCsMain = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsMainCs, Aig_ManObjNumMax(pFramesTest) ); - p->pMapCsTestToNsTest = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsTestNs, Aig_ManObjNumMax(pFramesTest) ); - p->pMapCsTestToNsBmc = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsBmcNs, Aig_ManObjNumMax(pFramesTest) ); - - // cleanup - Cnf_DataFree( pCnfMain ); - Cnf_DataFree( pCnfTest ); - Cnf_DataFree( pCnfBmc ); - Aig_ManStop( pFramesMain ); - Aig_ManStop( pFramesTest ); - Aig_ManStop( pFramesBmc ); - if ( p->pSatMain == NULL || p->pSatTest == NULL || p->pSatBmc == NULL ) - { - Fra_ClauStop( p ); - return NULL; - } - return p; -} - -/**Function************************************************************* - - Synopsis [Splits off second half and returns it as a new vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec ) -{ - Vec_Int_t * vPart; - int Entry, i; - assert( Vec_IntSize(vVec) > 1 ); - vPart = Vec_IntAlloc( Vec_IntSize(vVec) / 2 + 1 ); - Vec_IntForEachEntryStart( vVec, Entry, i, Vec_IntSize(vVec) / 2 ) - Vec_IntPush( vPart, Entry ); - Vec_IntShrink( vVec, Vec_IntSize(vVec) / 2 ); - return vPart; -} - -/**Function************************************************************* - - Synopsis [Appends the contents of the second vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) -{ - int Entry, i; - Vec_IntForEachEntry( vVec2, Entry, i ) - Vec_IntPush( vVec1, Entry ); -} - -/**Function************************************************************* - - Synopsis [Complements all literals in the clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Vec_IntComplement( Vec_Int_t * vVec ) -{ - int i; - for ( i = 0; i < Vec_IntSize(vVec); i++ ) - vVec->pArray[i] = lit_neg( vVec->pArray[i] ); -} - -/**Function************************************************************* - - Synopsis [Checks if the property holds. Returns counter-example if not.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex ) -{ - int nBTLimit = 0; - int RetValue, iVar, i; - sat_solver_act_var_clear( p->pSatMain ); - RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); - Vec_IntClear( vCex ); - if ( RetValue == l_False ) - return 1; - assert( RetValue == l_True ); - Vec_IntForEachEntry( p->vSatVarsMainCs, iVar, i ) - Vec_IntPush( vCex, sat_solver_var_literal(p->pSatMain, iVar) ); -/* - { - int i; - for (i = 0; i < p->pSatMain->size; i++) - printf( "%d=%d ", i, p->pSatMain->model.ptr[i] == l_True ); - printf( "\n" ); - } -*/ - return 0; -} - -/**Function************************************************************* - - Synopsis [Checks if the clause holds using BMC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause ) -{ - int nBTLimit = 0; - int RetValue; - RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause), - (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); - if ( RetValue == l_False ) - return 1; - assert( RetValue == l_True ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Lifts the clause to depend on NS variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ClauRemapClause( int * pMap, Vec_Int_t * vClause, Vec_Int_t * vRemapped, int fInv ) -{ - int iLit, i; - Vec_IntClear( vRemapped ); - Vec_IntForEachEntry( vClause, iLit, i ) - { - assert( pMap[lit_var(iLit)] >= 0 ); - iLit = toLitCond( pMap[lit_var(iLit)], lit_sign(iLit) ^ fInv ); - Vec_IntPush( vRemapped, iLit ); - } -} - -/**Function************************************************************* - - Synopsis [Checks if the clause holds. Returns counter example if not.] - - Description [Uses test SAT solver.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex ) -{ - int nBTLimit = 0; - int RetValue, iVar, i; - int nClauseSize = Vec_IntSize( vClause ); - // complement literals - Vec_IntPush( vClause, toLit( p->nSatVarsTestCur++ ) ); // helper positive - Vec_IntComplement( vClause ); // helper negative (the clause is C v h') - // add the clause - RetValue = sat_solver_addclause( p->pSatTest, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); - assert( RetValue == 1 ); - // complement all literals - Vec_IntPop( vClause ); // helper removed - Vec_IntComplement( vClause ); - // create the assumption in terms of NS variables - Fra_ClauRemapClause( p->pMapCsTestToNsTest, vClause, p->vCexAssm, 0 ); - // add helper literals - for ( i = p->nSatVarsTestBeg; i < p->nSatVarsTestCur - 1; i++ ) - Vec_IntPush( p->vCexAssm, toLitCond(i,1) ); // other helpers negative - Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper - // try to solve - RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm), - (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); - if ( vCex ) - Vec_IntClear( vCex ); - if ( RetValue == l_False ) - return 1; - assert( RetValue == l_True ); - if ( vCex ) - { - Vec_IntForEachEntry( p->vSatVarsTestCs, iVar, i ) - Vec_IntPush( vCex, sat_solver_var_literal(p->pSatTest, iVar) ); - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Reduces the counter-example by removing complemented literals.] - - Description [Removes literals from vMain that differ from those in the - counter-example (vNew). Relies on the fact that the PI variables are - assigned in the increasing order.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew ) -{ - int LitM, LitN, VarM, VarN, i, j, k; - assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) ); - for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); ) - { - LitM = Vec_IntEntry( vMain, i ); - LitN = Vec_IntEntry( vNew, j ); - VarM = lit_var( LitM ); - VarN = lit_var( LitN ); - if ( VarM < VarN ) - { - assert( 0 ); - } - else if ( VarM > VarN ) - { - j++; - } - else // if ( VarM == VarN ) - { - i++; - j++; - if ( LitM == LitN ) - Vec_IntWriteEntry( vMain, k++, LitM ); - } - } - assert( i == Vec_IntSize(vMain) ); - Vec_IntShrink( vMain, k ); -} - -/**Function************************************************************* - - Synopsis [Computes the minimal invariant that holds.] - - Description [On entrace, vBasis does not hold, vBasis+vExtra holds but - is not minimal. On exit, vBasis is unchanged, vBasis+vExtra is minimal.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ClauMinimizeClause_rec( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra ) -{ - Vec_Int_t * vExtra2; - int nSizeOld; - if ( Vec_IntSize(vExtra) == 1 ) - return; - nSizeOld = Vec_IntSize( vBasis ); - vExtra2 = Vec_IntSplitHalf( vExtra ); - - // try the first half - Vec_IntAppend( vBasis, vExtra ); - if ( Fra_ClauCheckClause( p, vBasis, NULL ) ) - { - Vec_IntShrink( vBasis, nSizeOld ); - Fra_ClauMinimizeClause_rec( p, vBasis, vExtra ); - return; - } - Vec_IntShrink( vBasis, nSizeOld ); - - // try the second half - Vec_IntAppend( vBasis, vExtra2 ); - if ( Fra_ClauCheckClause( p, vBasis, NULL ) ) - { - Vec_IntShrink( vBasis, nSizeOld ); - Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 ); - return; - } -// Vec_IntShrink( vBasis, nSizeOld ); - - // find the smallest with the second half added - Fra_ClauMinimizeClause_rec( p, vBasis, vExtra ); - Vec_IntShrink( vBasis, nSizeOld ); - Vec_IntAppend( vBasis, vExtra ); - // find the smallest with the second half added - Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 ); - Vec_IntShrink( vBasis, nSizeOld ); - Vec_IntAppend( vExtra, vExtra2 ); - Vec_IntFree( vExtra2 ); -} - -/**Function************************************************************* - - Synopsis [Minimizes the clauses using a simple method.] - - Description [The input and output clause are in vExtra.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra ) -{ - int iLit, iLit2, i, k; - Vec_IntForEachEntryReverse( vExtra, iLit, i ) - { - // copy literals without the given one - Vec_IntClear( vBasis ); - Vec_IntForEachEntry( vExtra, iLit2, k ) - if ( k != i ) - Vec_IntPush( vBasis, iLit2 ); - // try whether it is inductive - if ( !Fra_ClauCheckClause( p, vBasis, NULL ) ) - continue; - // the clause is inductive - // remove the literal - for ( k = i; k < Vec_IntSize(vExtra)-1; k++ ) - Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) ); - Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 ); - } -} - -/**Function************************************************************* - - Synopsis [Prints the clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex ) -{ - int LitM, VarM, VarN, i, j, k; - assert( Vec_IntSize(vCex) <= Vec_IntSize(vSatCsVars) ); - for ( i = j = k = 0; i < Vec_IntSize(vCex) && j < Vec_IntSize(vSatCsVars); ) - { - LitM = Vec_IntEntry( vCex, i ); - VarM = lit_var( LitM ); - VarN = Vec_IntEntry( vSatCsVars, j ); - if ( VarM < VarN ) - { - assert( 0 ); - } - else if ( VarM > VarN ) - { - j++; - printf( "-" ); - } - else // if ( VarM == VarN ) - { - i++; - j++; - printf( "%d", !lit_sign(LitM) ); - } - } - assert( i == Vec_IntSize(vCex) ); -} - -/**Function************************************************************* - - Synopsis [Takes the AIG with the single output to be checked.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose ) -{ - Cla_Man_t * p; - int Iter, RetValue, fFailed, i; - assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); - // create the manager - p = Fra_ClauStart( pMan ); - if ( p == NULL ) - { - printf( "The property is trivially inductive.\n" ); - return 1; - } - // generate counter-examples and expand them - for ( Iter = 0; !Fra_ClauCheckProperty( p, p->vCexMain0 ) && Iter < nIters; Iter++ ) - { - if ( fVerbose ) - printf( "%4d : ", Iter ); - // remap clause into the test manager - Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 ); - if ( fVerbose && fVeryVerbose ) - Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain ); - // the main counter-example is in p->vCexMain - // intermediate counter-examples are in p->vCexTest - // generate the reduced counter-example to the inductive property - fFailed = 0; - for ( i = 0; !Fra_ClauCheckClause( p, p->vCexMain, p->vCexTest ); i++ ) - { - Fra_ClauReduceClause( p->vCexMain, p->vCexTest ); - Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 ); - -// if ( !Fra_ClauCheckBmc(p, p->vCexBmc) ) - if ( Vec_IntSize(p->vCexMain) < 1 ) - { - Vec_IntComplement( p->vCexMain0 ); - RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexMain0), Vec_IntArray(p->vCexMain0) + Vec_IntSize(p->vCexMain0) ); - if ( RetValue == 0 ) - { - printf( "\nProperty is proved after %d iterations.\n", Iter+1 ); - return 0; - } - fFailed = 1; - break; - } - } - if ( fFailed ) - { - if ( fVerbose ) - printf( " Reducing failed after %d iterations (BMC failed).\n", i ); - continue; - } - if ( Vec_IntSize(p->vCexMain) == 0 ) - { - if ( fVerbose ) - printf( " Reducing failed after %d iterations (nothing left).\n", i ); - continue; - } - if ( fVerbose ) - printf( " " ); - if ( fVerbose && fVeryVerbose ) - Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain ); - if ( fVerbose ) - printf( " LitsInd = %3d. ", Vec_IntSize(p->vCexMain) ); - // minimize the inductive property - Vec_IntClear( p->vCexBase ); - if ( Vec_IntSize(p->vCexMain) > 1 ) -// Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain ); - Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain ); - assert( Vec_IntSize(p->vCexMain) > 0 ); - if ( fVerbose && fVeryVerbose ) - Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain ); - if ( fVerbose ) - printf( " LitsRed = %3d. ", Vec_IntSize(p->vCexMain) ); - if ( fVerbose ) - printf( "\n" ); - // add the clause to the solver - Fra_ClauRemapClause( p->pMapCsTestToCsMain, p->vCexMain, p->vCexAssm, 1 ); - RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm) ); - if ( RetValue == 0 ) - { - Iter++; - break; - } - if ( p->pSatMain->qtail != p->pSatMain->qhead ) - { - RetValue = sat_solver_simplify(p->pSatMain); - assert( RetValue != 0 ); - assert( p->pSatMain->qtail == p->pSatMain->qhead ); - } - } - - // report the results - if ( Iter == nIters ) - { - printf( "Property is not proved after %d iterations.\n", nIters ); - return 0; - } - printf( "Property is proved after %d iterations.\n", Iter ); - Fra_ClauStop( p ); - return 1; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |