luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/proof/fra/fraClau.c

746 lines
24 KiB
C
Raw Blame History

/**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 "src/sat/cnf/cnf.h"
#include "src/sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
/*
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_ManForEachCo( 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_ManForEachCi( 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 = ABC_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 )
{
ABC_FREE( p->pMapCsMainToCsTest );
ABC_FREE( p->pMapCsTestToCsMain );
ABC_FREE( p->pMapCsTestToNsTest );
ABC_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 );
ABC_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 = ABC_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 = (sat_solver *)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 = (sat_solver *)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 = (sat_solver *)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 [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, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)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),
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)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;
// 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),
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)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 ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink