diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/misc/extra/extraZddTrunc.c | 338 | ||||
| -rw-r--r-- | src/sat/bmc/bmcMulti.c | 204 |
2 files changed, 542 insertions, 0 deletions
diff --git a/src/misc/extra/extraZddTrunc.c b/src/misc/extra/extraZddTrunc.c new file mode 100644 index 00000000..bfd75565 --- /dev/null +++ b/src/misc/extra/extraZddTrunc.c @@ -0,0 +1,338 @@ +/**CFile**************************************************************** + + FileName [extraZddTrunc.c] + + PackageName [extra] + + Synopsis [Procedure to truncate a ZDD using variable probabilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraZddTrunc.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> + +#include "misc/st/st.h" +#include "bdd/cudd/cuddInt.h" + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +ABC_NAMESPACE_IMPL_START + + +#define TEST_VAR_MAX 10 +#define TEST_SET_MAX 10 + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + + +// dynamic vector of intergers +typedef struct Vec_Int_t_ Vec_Int_t; +struct Vec_Int_t_ +{ + int nCap; + int nSize; + int * pArray; +}; +static inline Vec_Int_t * Vec_IntAlloc( int nCap ) +{ + Vec_Int_t * p; + p = ABC_ALLOC( Vec_Int_t, 1 ); + if ( nCap > 0 && nCap < 16 ) + nCap = 16; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; + return p; +} +static inline void Vec_IntFree( Vec_Int_t * p ) +{ + ABC_FREE( p->pArray ); + ABC_FREE( p ); +} +static inline int * Vec_IntReleaseArray( Vec_Int_t * p ) +{ + int * pArray = p->pArray; + p->nCap = 0; + p->nSize = 0; + p->pArray = NULL; + return pArray; +} +static inline int Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray[i] += Addition; +} +static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); + assert( p->pArray ); + p->nCap = nCapMin; +} +static inline int Vec_IntPop( Vec_Int_t * p ) +{ + assert( p->nSize > 0 ); + return p->pArray[--p->nSize]; +} +static inline void Vec_IntPush( Vec_Int_t * p, int Entry ) +{ + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Vec_IntGrow( p, 16 ); + else + Vec_IntGrow( p, 2 * p->nCap ); + } + p->pArray[p->nSize++] = Entry; +} +static inline void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) +{ + int i; + for ( i = 0; i < vVec2->nSize; i++ ) + Vec_IntPush( vVec1, vVec2->pArray[i] ); +} + + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Compute the set of subsets whose probability is more than ProbLimit.] + + Description [The resulting array has the following form: The first integer entry + is the number of resulting subsets. The following integer entries in the array + contain as many subsets. Each subset is an array of integers followed by -1. + See how subsets are printed in the included test procedure below.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_zddTruncate_rec( + DdManager * dd, + DdNode * zFunc, // zFunc is the ZDD to be truncated + double * pVarProbs, // pVarProbs is probabilities of each variable (should have at least dd->sizeZ entries) + double ProbLimit, // ProbLimit is the limit on the probabilities (only those more than this will be collected) + double ProbThis, // current path probability + Vec_Int_t * vSubset, // current subset under construction + Vec_Int_t * vResult ) // resulting subsets to be returned to the user +{ + // quit if probability of the path is less then the limit + if ( ProbThis < ProbLimit ) + return; + // quit if there is no subsets + if ( zFunc == Cudd_ReadZero(dd) ) + return; + // quit and save a new subset if there is one + if ( zFunc == Cudd_ReadOne(dd) ) + { + Vec_IntAddToEntry( vResult, 0, 1 ); + Vec_IntAppend( vResult, vSubset ); + Vec_IntPush( vResult, -1 ); + return; + } + // call recursively for the set without the given variable + Extra_zddTruncate_rec( dd, cuddE(zFunc), pVarProbs, ProbLimit, ProbThis, vSubset, vResult ); + // call recursively for the set with the given variable + Vec_IntPush( vSubset, Cudd_NodeReadIndex(zFunc) ); + Extra_zddTruncate_rec( dd, cuddT(zFunc), pVarProbs, ProbLimit, ProbThis * pVarProbs[Cudd_NodeReadIndex(zFunc)], vSubset, vResult ); + Vec_IntPop( vSubset ); +} +int * Extra_zddTruncate( + DdManager * dd, + DdNode * zFunc, // zFunc is the ZDD to be truncated + double * pVarProbs, // pVarProbs is probabilities of each variable (should have at least dd->sizeZ entries) + double ProbLimit ) // ProbLimit is the limit on the probabilities (only those more than this will be collected) +{ + Vec_Int_t * vSubset, * vResult; + int i, sizeZ = Cudd_ReadZddSize(dd); + int * pResult; + // check that probabilities are reasonable + assert( ProbLimit > 0 && ProbLimit <= 1 ); + for ( i = 0; i < sizeZ; i++ ) + assert( pVarProbs[i] > 0 && pVarProbs[i] <= 1 ); + // enumerate assignments satisfying the probability limit + vSubset = Vec_IntAlloc( sizeZ ); + vResult = Vec_IntAlloc( 10 * sizeZ ); + Vec_IntPush( vResult, 0 ); + Extra_zddTruncate_rec( dd, zFunc, pVarProbs, ProbLimit, 1, vSubset, vResult ); + Vec_IntFree( vSubset ); + pResult = Vec_IntReleaseArray( vResult ); + Vec_IntFree( vResult ); + return pResult; +} // end of Extra_zddTruncate + +/**Function************************************************************* + + Synopsis [Creates the combination composed of a single ZDD variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_zddVariable( DdManager * dd, int iVar ) +{ + DdNode * zRes; + do { + dd->reordered = 0; + zRes = cuddZddGetNode( dd, iVar, Cudd_ReadOne(dd), Cudd_ReadZero(dd) ); + } while (dd->reordered == 1); + return zRes; +} + +/**Function******************************************************************** + + Synopsis [Creates ZDD representing a given set of subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddCreateSubsets( + DdManager * dd, + int pSubsets[][TEST_VAR_MAX+1], + int nSubsets ) +{ + int i, k; + DdNode * zOne, * zVar, * zRes, * zTemp; + zRes = Cudd_ReadZero(dd); Cudd_Ref( zRes ); + for ( i = 0; i < nSubsets; i++ ) + { + zOne = Cudd_ReadOne(dd); Cudd_Ref( zOne ); + for ( k = 0; pSubsets[i][k] != -1; k++ ) + { + assert( pSubsets[i][k] < TEST_VAR_MAX ); + zVar = Extra_zddVariable( dd, pSubsets[i][k] ); + zOne = Cudd_zddUnateProduct( dd, zTemp = zOne, zVar ); Cudd_Ref( zOne ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + } + zRes = Cudd_zddUnion( dd, zRes, zOne ); Cudd_Ref( zRes ); + Cudd_RecursiveDerefZdd( dd, zOne ); + } + Cudd_Deref( zRes ); + return zRes; +} + +/**Function******************************************************************** + + Synopsis [Prints a set of subsets represented using as an array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_zddPrintSubsets( int * pSubsets ) +{ + int i, k, Counter = 0; + printf( "The set contains %d subsets:\n", pSubsets[0] ); + for ( i = k = 0; i < pSubsets[0]; i++ ) + { + printf( "Subset %3d : {", Counter ); + for ( k++; pSubsets[k] != -1; k++ ) + printf( " %d", pSubsets[k] ); + printf( " }\n" ); + Counter++; + } +} + +/**Function******************************************************************** + + Synopsis [Testbench for the above truncation procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_zddTruncateTest() +{ + // input data + int nSubsets = 5; + int pSubsets[TEST_SET_MAX][TEST_VAR_MAX+1] = { {0, 3, 5, -1}, {1, 2, 3, 6, 9, -1}, {1, 5, 7, 8, -1}, {2, 4, -1}, {0, 5, 6, 9, -1} }; + // varible probabilities + double pVarProbs[TEST_VAR_MAX] = { 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1 }; + double ProbLimit = 0.001; + // output data + int * pOutput; + // start the manager and create ZDD representing the input subsets + DdManager * dd = Cudd_Init( 0, TEST_VAR_MAX, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS , 0 ); + DdNode * zFunc = Extra_zddCreateSubsets( dd, pSubsets, nSubsets ); Cudd_Ref( zFunc ); + assert( nSubsets <= TEST_SET_MAX ); + // print the input ZDD + printf( "The initial ZDD representing %d subsets:\n", nSubsets ); + Cudd_zddPrintMinterm( dd, zFunc ); + // compute the result of truncation + pOutput = Extra_zddTruncate( dd, zFunc, pVarProbs, ProbLimit ); + // print the resulting ZDD + printf( "The resulting ZDD representing %d subsets:\n", pOutput[0] ); + // print the resulting subsets + Extra_zddPrintSubsets( pOutput ); + // cleanup + ABC_FREE( pOutput ); + Cudd_RecursiveDerefZdd( dd, zFunc ); + Cudd_Quit( dd ); +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c new file mode 100644 index 00000000..7a744228 --- /dev/null +++ b/src/sat/bmc/bmcMulti.c @@ -0,0 +1,204 @@ +/**CFile**************************************************************** + + FileName [bmcMulti.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Proving multi-output properties.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcMulti.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "proof/ssw/ssw.h" +#include "aig/gia/giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Divides outputs into solved and unsolved.] + + Description [Return array of unsolved outputs to extract into a new AIG. + Updates the resulting CEXes (vCexesOut) and current output map (vOutMap).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut, Vec_Int_t * vOutMap ) +{ + Abc_Cex_t * pCex; + Vec_Int_t * vLeftOver; + int i, iOut; + assert( Vec_PtrSize(vCexesIn) == Vec_IntSize(vOutMap) ); + vLeftOver = Vec_IntAlloc( Vec_PtrSize(vCexesIn) ); + Vec_IntForEachEntry( vOutMap, iOut, i ) + { + assert( Vec_PtrEntry(vCexesOut, iOut) == NULL ); + pCex = (Abc_Cex_t *)Vec_PtrEntry( vCexesIn, i ); + if ( pCex ) // found a CEX for output iOut + { + Vec_PtrWriteEntry( vCexesIn, i, NULL ); + Vec_PtrWriteEntry( vCexesOut, iOut, pCex ); + } + else // still unsolved + { + Vec_IntWriteEntry( vOutMap, Vec_IntSize(vLeftOver), iOut ); + Vec_IntPush( vLeftOver, i ); + } + } + Vec_IntShrink( vOutMap, Vec_IntSize(vLeftOver) ); + return vLeftOver; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManMultiReport( Aig_Man_t * p, char * pStr, int nTotalPo, int nTotalSize, abctime clkStart ) +{ + printf( "%3s : ", pStr ); + printf( "PI =%6d ", Saig_ManPiNum(p) ); + printf( "PO =%6d ", Saig_ManPoNum(p) ); + printf( "FF =%7d ", Saig_ManRegNum(p) ); + printf( "ND =%7d ", Aig_ManNodeNum(p) ); + printf( "Solved =%7d (%5.1f %%) ", nTotalPo-Saig_ManPoNum(p), 100.0*(nTotalPo-Saig_ManPoNum(p))/Abc_MaxInt(1, nTotalPo) ); + printf( "Size =%7d (%5.1f %%) ", Aig_ManObjNum(p), 100.0*Aig_ManObjNum(p)/Abc_MaxInt(1, nTotalSize) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fVerbose ) +{ + Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim; + Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc; + Vec_Int_t * vOutMap, * vLeftOver; + Vec_Ptr_t * vCexes; + Aig_Man_t * pTemp; + abctime clkStart = Abc_Clock(); + int nTimeToStop = TimeOutGlo ? TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0; + int nTotalPo = Saig_ManPoNum(p); + int nTotalSize = Aig_ManObjNum(p); + int i, RetValue = -1; + // create output map + vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs + vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers) + for ( i = 0; i < 1000; i++ ) + { + // synthesize +// p = Gia_ManMultiProveSyn( pTemp = p ); +// Aig_ManStop( pTemp ); +// if ( fVerbose ) +// Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart ); + + // perform SIM3 + Ssw_RarSetDefaultParams( pParsSim ); + pParsSim->fSolveAll = 1; + pParsSim->fNotVerbose = 1; + pParsSim->fSilent = 1; + pParsSim->TimeOut = TimeOutLoc; + pParsSim->nRandSeed = (i * 17) % 500; + RetValue *= Ssw_RarSimulate( p, pParsSim ); + // sort outputs + if ( p->vSeqModelVec ) + { + vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap ); + if ( Vec_IntSize(vLeftOver) == 0 ) + break; + // remove solved + p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) ); + Vec_IntFree( vLeftOver ); + Aig_ManStop( pTemp ); + } +// if ( fVerbose ) + Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart ); + + // perform BMC + Saig_ParBmcSetDefaultParams( pParsBmc ); + pParsBmc->fSolveAll = 1; + pParsBmc->fNotVerbose = 1; + pParsBmc->fSilent = 1; + pParsBmc->nTimeOut = TimeOutLoc; + RetValue *= Saig_ManBmcScalable( p, pParsBmc ); + // sort outputs + if ( p->vSeqModelVec ) + { + vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap ); + if ( Vec_IntSize(vLeftOver) == 0 ) + break; + // remove solved + p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) ); + Vec_IntFree( vLeftOver ); + Aig_ManStop( pTemp ); + } +// if ( fVerbose ) + Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart ); + + // increase timeout + TimeOutLoc *= TimeOutInc; + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + { + printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo ); + break; + } + } + Vec_IntFree( vOutMap ); + Aig_ManStop( p ); + return vCexes; +} +int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose ) +{ + Aig_Man_t * pAig; + if ( p->vSeqModelVec ) + Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL; + pAig = Gia_ManToAig( p, 0 ); + p->vSeqModelVec = Gia_ManMultiProveAig( pAig, 30, 2, 2, fVerbose ); + assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) ); +// Aig_ManStop( pAig ); + return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |