#include "aig/saig/saig.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "pdr.h"

Data Structures
struct	Pdr_Set_t_

struct	Pdr_Obl_t_

struct	Pdr_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Pdr_Set_t_	Pdr_Set_t
	INCLUDES ///. More...

typedef struct Pdr_Obl_t_	Pdr_Obl_t

typedef struct Pdr_Man_t_	Pdr_Man_t

Functions
static sat_solver *	Pdr_ManSolver (Pdr_Man_t *p, int k)
	MACRO DEFINITIONS ///. More...

static abctime	Pdr_ManTimeLimit (Pdr_Man_t *p)

Abc_Cex_t *	Pdr_ManDeriveCex (Pdr_Man_t *p)
	FUNCTION DECLARATIONS ///. More...

int	Pdr_ObjSatVar (Pdr_Man_t p, int k, int Pol, Aig_Obj_t pObj)

int	Pdr_ObjRegNum (Pdr_Man_t *p, int k, int iSatVar)

int	Pdr_ManFreeVar (Pdr_Man_t *p, int k)

sat_solver *	Pdr_ManNewSolver (sat_solver pSat, Pdr_Man_t p, int k, int fInit)

int	Pdr_ManCheckContainment (Pdr_Man_t p, int k, Pdr_Set_t pSet)

void	Pdr_ManPrintProgress (Pdr_Man_t *p, int fClose, abctime Time)
	DECLARATIONS ///. More...

void	Pdr_ManPrintClauses (Pdr_Man_t *p, int kStart)

void	Pdr_ManDumpClauses (Pdr_Man_t p, char pFileName, int fProved)

void	Pdr_ManReportInvariant (Pdr_Man_t *p)

void	Pdr_ManVerifyInvariant (Pdr_Man_t *p)

Pdr_Man_t *	Pdr_ManStart (Aig_Man_t pAig, Pdr_Par_t pPars, Vec_Int_t *vPrioInit)
	DECLARATIONS ///. More...

void	Pdr_ManStop (Pdr_Man_t *p)

sat_solver *	Pdr_ManCreateSolver (Pdr_Man_t *p, int k)
	DECLARATIONS ///. More...

sat_solver *	Pdr_ManFetchSolver (Pdr_Man_t *p, int k)

void	Pdr_ManSetPropertyOutput (Pdr_Man_t *p, int k)

Vec_Int_t *	Pdr_ManCubeToLits (Pdr_Man_t p, int k, Pdr_Set_t pCube, int fCompl, int fNext)

Vec_Int_t *	Pdr_ManLitsToCube (Pdr_Man_t p, int k, int pArray, int nArray)

void	Pdr_ManSolverAddClause (Pdr_Man_t p, int k, Pdr_Set_t pCube)

void	Pdr_ManCollectValues (Pdr_Man_t p, int k, Vec_Int_t vObjIds, Vec_Int_t *vValues)

int	Pdr_ManCheckCubeCs (Pdr_Man_t p, int k, Pdr_Set_t pCube)

int	Pdr_ManCheckCube (Pdr_Man_t p, int k, Pdr_Set_t pCube, Pdr_Set_t **ppPred, int nConfLimit)

Pdr_Set_t *	Pdr_ManTernarySim (Pdr_Man_t p, int k, Pdr_Set_t pCube)

Pdr_Set_t *	Pdr_SetAlloc (int nSize)
	DECLARATIONS ///. More...

Pdr_Set_t *	Pdr_SetCreate (Vec_Int_t vLits, Vec_Int_t vPiLits)

Pdr_Set_t *	Pdr_SetCreateFrom (Pdr_Set_t *pSet, int iRemove)

Pdr_Set_t *	Pdr_SetCreateSubset (Pdr_Set_t pSet, int pLits, int nLits)

Pdr_Set_t *	Pdr_SetDup (Pdr_Set_t *pSet)

Pdr_Set_t *	Pdr_SetRef (Pdr_Set_t *p)

void	Pdr_SetDeref (Pdr_Set_t *p)

int	Pdr_SetContains (Pdr_Set_t pOld, Pdr_Set_t pNew)

int	Pdr_SetContainsSimple (Pdr_Set_t pOld, Pdr_Set_t pNew)

int	Pdr_SetIsInit (Pdr_Set_t *p, int iRemove)

void	Pdr_SetPrint (FILE pFile, Pdr_Set_t p, int nRegs, Vec_Int_t *vFlopCounts)

int	Pdr_SetCompare (Pdr_Set_t pp1, Pdr_Set_t pp2)

Pdr_Obl_t *	Pdr_OblStart (int k, int prio, Pdr_Set_t pState, Pdr_Obl_t pNext)

Pdr_Obl_t *	Pdr_OblRef (Pdr_Obl_t *p)

void	Pdr_OblDeref (Pdr_Obl_t *p)

int	Pdr_QueueIsEmpty (Pdr_Man_t *p)

Pdr_Obl_t *	Pdr_QueueHead (Pdr_Man_t *p)

Pdr_Obl_t *	Pdr_QueuePop (Pdr_Man_t *p)

void	Pdr_QueueClean (Pdr_Man_t *p)

void	Pdr_QueuePush (Pdr_Man_t p, Pdr_Obl_t pObl)

void	Pdr_QueuePrint (Pdr_Man_t *p)

void	Pdr_QueueStop (Pdr_Man_t *p)

int	Pdr_ManCubeJust (Pdr_Man_t p, int k, Pdr_Set_t pCube)

Typedef Documentation

typedef struct Pdr_Man_t_ Pdr_Man_t

Definition at line 65 of file pdrInt.h.

typedef struct Pdr_Obl_t_ Pdr_Obl_t

Definition at line 54 of file pdrInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Pdr_Set_t_ Pdr_Set_t

INCLUDES ///.

CFile****************************************************************

FileName [pdrInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 44 of file pdrInt.h.

Function Documentation

int Pdr_ManCheckContainment	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pSet
	)

Function*************************************************************

Synopsis [Returns 1 if the clause is contained in higher clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file pdrCore.c.

 {
     Pdr_Set_t * pThis;
     Vec_Ptr_t * vArrayK;
     int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
     Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
             if ( Pdr_SetContains( pSet, pThis ) )
                 return 1;
     return 0;
 }

int Pdr_ManCheckCube	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube,
		Pdr_Set_t **	ppPred,
		int	nConfLimit
	)

Function*************************************************************

Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]

Description [Return 1/0 if cube or property are proved to hold/fail in k-th timeframe. Returns the predecessor bad state in ppPred.]

SideEffects []

SeeAlso []

Definition at line 286 of file pdrSat.c.

 { 
     int fUseLit = 1;
     int fLitUsed = 0;
     sat_solver * pSat;
     Vec_Int_t * vLits;
     int Lit, RetValue;
     abctime clk, Limit;
     p->nCalls++;
     pSat = Pdr_ManFetchSolver( p, k );
     if ( pCube == NULL ) // solve the property
     {
         clk = Abc_Clock();
         Lit = toLit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
         RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
         sat_solver_set_runtime_limit( pSat, Limit );
         if ( RetValue == l_Undef )
             return -1;
     }
     else // check relative containment in terms of next states
     {
         if ( fUseLit )
         {
             fLitUsed = 1;
             Vec_IntAddToEntry( p->vActVars, k, 1 );
             // add the cube in terms of current state variables
             vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
             // add activation literal
             Lit = toLit( Pdr_ManFreeVar(p, k) );
             // add activation literal
             Vec_IntPush( vLits, Lit );
             RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
             assert( RetValue == 1 );
             sat_solver_compress( pSat );
             // create assumptions
             vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
             // add activation literal
             Vec_IntPush( vLits, lit_neg(Lit) );
         }
         else
             vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
 
         // solve 
         clk = Abc_Clock();
         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
         RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
         sat_solver_set_runtime_limit( pSat, Limit );
         if ( RetValue == l_Undef )
             return -1;
 /*
         if ( RetValue == l_True )
         {
             int RetValue2 = Pdr_ManCubeJust( p, k, pCube );
             if ( RetValue2 )
                 p->nCasesSS++;
             else
                 p->nCasesSU++;
         }
         else
         {
             int RetValue2 = Pdr_ManCubeJust( p, k, pCube );
             if ( RetValue2 )
                 p->nCasesUS++;
             else
                 p->nCasesUU++;
         }
 */
     }
     clk = Abc_Clock() - clk;
     p->tSat += clk;
     assert( RetValue != l_Undef );
     if ( RetValue == l_False )
     {
         p->tSatUnsat += clk;
         p->nCallsU++;
         if ( ppPred )
             *ppPred = NULL;
         RetValue = 1;
     }
     else // if ( RetValue == l_True )
     {
         p->tSatSat += clk;
         p->nCallsS++;
         if ( ppPred )
             *ppPred = Pdr_ManTernarySim( p, k, pCube );
         RetValue = 0;
     }
 
 /* // for some reason, it does not work...
     if ( fLitUsed )
     {
         int RetValue;
         Lit = lit_neg(Lit);
         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
         assert( RetValue == 1 );
         sat_solver_compress( pSat );
     }
 */
     return RetValue;
 }

int Pdr_ManCheckCubeCs	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube
	)

Function*************************************************************

Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]

Description [Return 1/0 if cube or property are proved to hold/fail in k-th timeframe. Returns the predecessor bad state in ppPred.]

SideEffects []

SeeAlso []

Definition at line 258 of file pdrSat.c.

 { 
     sat_solver * pSat;
     Vec_Int_t * vLits;
     abctime Limit;
     int RetValue;
     pSat = Pdr_ManFetchSolver( p, k );
     vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
     Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
     RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
     sat_solver_set_runtime_limit( pSat, Limit );
     if ( RetValue == l_Undef )
         return -1;
     return (RetValue == l_False);
 }

void Pdr_ManCollectValues	(	Pdr_Man_t *	p,
		int	k,
		Vec_Int_t *	vObjIds,
		Vec_Int_t *	vValues
	)

Function*************************************************************

Synopsis [Collects values of the RO/RI variables in k-th SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file pdrSat.c.

 {
     sat_solver * pSat;
     Aig_Obj_t * pObj;
     int iVar, i;
     Vec_IntClear( vValues );
     pSat = Pdr_ManSolver(p, k);
     Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
     {
         iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
         Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
     }
 }

sat_solver* Pdr_ManCreateSolver	(	Pdr_Man_t *	p,
		int	k
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [pdrSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [SAT solver procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Creates new SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file pdrSat.c.

 {
     sat_solver * pSat;
     Aig_Obj_t * pObj;
     int i;
     assert( Vec_PtrSize(p->vSolvers) == k );
     assert( Vec_VecSize(p->vClauses) == k );
     assert( Vec_IntSize(p->vActVars) == k );
     // create new solver
     pSat = sat_solver_new();
     pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
     Vec_PtrPush( p->vSolvers, pSat );
     Vec_VecExpand( p->vClauses, k );
     Vec_IntPush( p->vActVars, 0 );
     // add property cone
     Saig_ManForEachPo( p->pAig, pObj, i )
         Pdr_ObjSatVar( p, k, 1, pObj );
     return pSat;
 }

int Pdr_ManCubeJust	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube
	)

Function*************************************************************

Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 688 of file pdrUtil.c.

 {
     Aig_Obj_t * pNode;
     int i, v, fCompl;
 //    return 0;
     for ( i = 0; i < 4; i++ )
     {
         // derive new assignment
         p->pCubeJust->nLits = 0;
         p->pCubeJust->Sign  = 0;
         Aig_ManIncrementTravId( p->pAig );
         for ( v = 0; v < pCube->nLits; v++ )
         {
             if ( pCube->Lits[v] == -1 )
                 continue;
             pNode  = Saig_ManLi( p->pAig, lit_var(pCube->Lits[v]) );
             fCompl = lit_sign(pCube->Lits[v]) ^ Aig_ObjFaninC0(pNode);
             if ( !Pdr_NtkFindSatAssign_rec( p->pAig, Aig_ObjFanin0(pNode), !fCompl, p->pCubeJust, i ) )
                 break;
         }
         if ( v < pCube->nLits )
             continue;
         // figure this out!!!
         if ( p->pCubeJust->nLits == 0 )
             continue;
         // successfully derived new assignment
         Vec_IntSelectSort( p->pCubeJust->Lits, p->pCubeJust->nLits );
         // check assignment against this cube
         if ( Pdr_SetContainsSimple( p->pCubeJust, pCube ) )
             continue;
 //printf( "\n" );
 //Pdr_SetPrint( stdout, pCube,        Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
 //Pdr_SetPrint( stdout, p->pCubeJust, Saig_ManRegNum(p->pAig), NULL ); printf( "\n" );
         // check assignment against the clauses
         if ( Pdr_ManCheckContainment( p, k, p->pCubeJust ) )
             continue;
         // find good assignment
         return 1;
     }
     return 0;
 }

Vec_Int_t* Pdr_ManCubeToLits	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube,
		int	fCompl,
		int	fNext
	)

Function*************************************************************

Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file pdrSat.c.

 {
     Aig_Obj_t * pObj;
     int i, iVar, iVarMax = 0;
     abctime clk = Abc_Clock();
     Vec_IntClear( p->vLits );
     assert( !(fNext && fCompl) );
     for ( i = 0; i < pCube->nLits; i++ )
     {
         if ( pCube->Lits[i] == -1 )
             continue;
         if ( fNext )
             pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
         else
             pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
         iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
         iVarMax = Abc_MaxInt( iVarMax, iVar );
         Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
     }
 //    sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
     p->tCnf += Abc_Clock() - clk;
     return p->vLits;
 }

Abc_Cex_t * Pdr_ManDeriveCex ( Pdr_Man_t * p )

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Derives counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file pdrMan.c.

 {
     Abc_Cex_t * pCex;
     Pdr_Obl_t * pObl;
     int i, f, Lit, nFrames = 0;
     // count the number of frames
     for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
         nFrames++;
     // create the counter-example
     pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
 //    pCex->iPo    = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
     pCex->iPo    = p->iOutCur;
     pCex->iFrame = nFrames-1;
     for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
         for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
         {
             Lit = pObl->pState->Lits[i];
             if ( lit_sign(Lit) )
                 continue;
             assert( lit_var(Lit) < pCex->nPis );
             Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
         }
     assert( f == nFrames );
     if ( !Saig_ManVerifyCex(p->pAig, pCex) )
         printf( "CEX for output %d is not valid.\n", p->iOutCur );
     return pCex;
 }

void Pdr_ManDumpClauses	(	Pdr_Man_t *	p,
		char *	pFileName,
		int	fProved
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 313 of file pdrInv.c.

 {
     int fUseSupp = 1;
     FILE * pFile;
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
     Pdr_Set_t * pCube;
     char ** pNamesCi;
     int i, kStart;
     // create file
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
         Abc_Print( 1, "Cannot open file \"%s\" for writing invariant.\n", pFileName );
         return;
     } 
     // collect cubes
     kStart = Pdr_ManFindInvariantStart( p );
     vCubes = Pdr_ManCollectCubes( p, kStart );
     Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
 //    Pdr_ManDumpAig( p->pAig, vCubes );
     // collect variable appearances
     vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
     if ( fProved )
         fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
     else
         fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName );
     fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
     fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
     fprintf( pFile, ".o 1\n" );
     fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) );
     // output flop names
     pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 );
     if ( pNamesCi )
     {
         fprintf( pFile, ".ilb" );
         for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
             if ( !fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
                 fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] );
         fprintf( pFile, "\n" );
         ABC_FREE( pNamesCi );
         fprintf( pFile, ".ob inv\n" );
     }
     // output cubes
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {
         Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
         fprintf( pFile, " 1\n" ); 
     }
     fprintf( pFile, ".e\n\n" );
     fclose( pFile );
     Vec_IntFreeP( &vFlopCounts );
     Vec_PtrFree( vCubes );
     if ( fProved )
         Abc_Print( 1, "Inductive invariant was written into file \"%s\".\n", pFileName );
     else
         Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
 }

sat_solver* Pdr_ManFetchSolver	(	Pdr_Man_t *	p,
		int	k
	)

Function*************************************************************

Synopsis [Returns old or restarted solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file pdrSat.c.

 {
     sat_solver * pSat;
     Vec_Ptr_t * vArrayK;
     Pdr_Set_t * pCube;
     int i, j;
     pSat = Pdr_ManSolver(p, k);
     if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
         return pSat;
     assert( k < Vec_PtrSize(p->vSolvers) - 1 );
     p->nStarts++;
 //    sat_solver_delete( pSat );
 //    pSat = sat_solver_new();
     sat_solver_restart( pSat );
     // create new SAT solver
     pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
     // write new SAT solver
     Vec_PtrWriteEntry( p->vSolvers, k, pSat );
     Vec_IntWriteEntry( p->vActVars, k, 0 );
     // set the property output
     Pdr_ManSetPropertyOutput( p, k );
     // add the clauses
     Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
             Pdr_ManSolverAddClause( p, k, pCube );
     return pSat;
 }

int Pdr_ManFreeVar	(	Pdr_Man_t *	p,
		int	k
	)

Function*************************************************************

Synopsis [Returns the index of unused SAT variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 332 of file pdrCnf.c.

 {
     if ( p->pPars->fMonoCnf )
         return sat_solver_nvars( Pdr_ManSolver(p, k) );
     else
     {
         Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry( &p->vVar2Ids, k );
         Vec_IntPush( vVar2Ids, -1 );
         return Vec_IntSize( vVar2Ids ) - 1;
     }
 }

Vec_Int_t* Pdr_ManLitsToCube	(	Pdr_Man_t *	p,
		int	k,
		int *	pArray,
		int	nArray
	)

Function*************************************************************

Synopsis [Converts SAT variables into register IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file pdrSat.c.

 {
     int i, RegId;
     Vec_IntClear( p->vLits );
     for ( i = 0; i < nArray; i++ )
     {
         RegId = Pdr_ObjRegNum( p, k, lit_var(pArray[i]) );
         if ( RegId == -1 )
             continue;
         assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
         Vec_IntPush( p->vLits, toLitCond(RegId, !lit_sign(pArray[i])) );
     }
     assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
     return p->vLits;
 }

sat_solver* Pdr_ManNewSolver	(	sat_solver *	pSat,
		Pdr_Man_t *	p,
		int	k,
		int	fInit
	)

Function*************************************************************

Synopsis [Creates SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 435 of file pdrCnf.c.

 {
     assert( pSat != NULL );
     if ( p->pPars->fMonoCnf )
         return Pdr_ManNewSolver1( pSat, p, k, fInit );
     else
         return Pdr_ManNewSolver2( pSat, p, k, fInit );
 }

void Pdr_ManPrintClauses	(	Pdr_Man_t *	p,
		int	kStart
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file pdrInv.c.

 {
     Vec_Ptr_t * vArrayK;
     Pdr_Set_t * pCube;
     int i, k, Counter = 0;
     Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
     {
         Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
         {
             Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
             Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );  
             Abc_Print( 1, "\n" ); 
         }
     }
 }

void Pdr_ManPrintProgress	(	Pdr_Man_t *	p,
		int	fClose,
		abctime	Time
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [pdrInv.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Invariant computation, printing, verification.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file pdrInv.c.

 {
     Vec_Ptr_t * vVec;
     int i, ThisSize, Length, LengthStart;
     if ( Vec_PtrSize(p->vSolvers) < 2 )
         return;
     if ( Abc_FrameIsBatchMode() && !fClose )
         return;
     // count the total length of the printout
     Length = 0;
     Vec_VecForEachLevel( p->vClauses, vVec, i )
         Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
     // determine the starting point
     LengthStart = Abc_MaxInt( 0, Length - 60 );
     Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 );
     ThisSize = 5;
     if ( LengthStart > 0 )
     {
         Abc_Print( 1, " ..." );
         ThisSize += 4;
     }
     Length = 0;
     Vec_VecForEachLevel( p->vClauses, vVec, i )
     {
         if ( Length < LengthStart )
         {
             Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
             continue;
         }
         Abc_Print( 1, " %d", Vec_PtrSize(vVec) );
         Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
         ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
     }
     for ( i = ThisSize; i < 70; i++ )
         Abc_Print( 1, " " );
     Abc_Print( 1, "%6d", p->nQueMax );
     Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     if ( p->pPars->fSolveAll )
         Abc_Print( 1, "  CEX =%4d", p->pPars->nFailOuts );
     if ( p->pPars->nTimeOutOne )
         Abc_Print( 1, "  T/O =%3d", p->pPars->nDropOuts );
     Abc_Print( 1, "%s", fClose ? "\n":"\r" );
     if ( fClose )
         p->nQueMax = 0;
     fflush( stdout );
 }

void Pdr_ManReportInvariant ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 385 of file pdrInv.c.

 {
     Vec_Ptr_t * vCubes;
     int kStart = Pdr_ManFindInvariantStart( p );
     vCubes = Pdr_ManCollectCubes( p, kStart );
     Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", 
         kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
     Vec_PtrFree( vCubes );
 }

void Pdr_ManSetPropertyOutput	(	Pdr_Man_t *	p,
		int	k
	)

Function*************************************************************

Synopsis [Sets the property output to 0 (sat) forever.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file pdrSat.c.

 {
     sat_solver * pSat;
     Aig_Obj_t * pObj;
     int Lit, RetValue, i;
     pSat = Pdr_ManSolver(p, k);
     Saig_ManForEachPo( p->pAig, pObj, i )
     {
         // skip solved outputs
         if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
             continue;
         // skip timedout outputs
         if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
             continue;
         Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
         assert( RetValue == 1 );
     }
     sat_solver_compress( pSat );
 }

static sat_solver* Pdr_ManSolver	(	Pdr_Man_t *	p,
		int	k
	)

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 139 of file pdrInt.h.

139 { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }

Pdr_Man_t_::vSolvers

Vec_Ptr_t * vSolvers

Definition: pdrInt.h:83

Vec_PtrEntry

static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)

Definition: vecPtr.h:362

sat_solver_t

Definition: satSolver.h:91

void Pdr_ManSolverAddClause	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube
	)

Function*************************************************************

Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file pdrSat.c.

 {
     sat_solver * pSat;
     Vec_Int_t * vLits;
     int RetValue;
     pSat  = Pdr_ManSolver(p, k);
     vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
     RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
     assert( RetValue == 1 );
     sat_solver_compress( pSat );
 }

Pdr_Man_t* Pdr_ManStart	(	Aig_Man_t *	pAig,
		Pdr_Par_t *	pPars,
		Vec_Int_t *	vPrioInit
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [pdrMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Manager procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Creates manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file pdrMan.c.

 {
     Pdr_Man_t * p;
     p = ABC_CALLOC( Pdr_Man_t, 1 );
     p->pPars    = pPars;
     p->pAig     = pAig;
     p->vSolvers = Vec_PtrAlloc( 0 );
     p->vClauses = Vec_VecAlloc( 0 );
     p->pQueue   = NULL;
     p->pOrder   = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
     p->vActVars = Vec_IntAlloc( 256 );
     if ( !p->pPars->fMonoCnf )
         p->vVLits   = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
     // internal use
     p->vPrio    = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) );  // priority flops
     p->vLits    = Vec_IntAlloc( 100 );  // array of literals
     p->vCiObjs  = Vec_IntAlloc( 100 );  // cone leaves
     p->vCoObjs  = Vec_IntAlloc( 100 );  // cone roots
     p->vCiVals  = Vec_IntAlloc( 100 );  // cone leaf values
     p->vCoVals  = Vec_IntAlloc( 100 );  // cone root values
     p->vNodes   = Vec_IntAlloc( 100 );  // cone nodes
     p->vUndo    = Vec_IntAlloc( 100 );  // cone undos
     p->vVisits  = Vec_IntAlloc( 100 );  // intermediate
     p->vCi2Rem  = Vec_IntAlloc( 100 );  // CIs to be removed
     p->vRes     = Vec_IntAlloc( 100 );  // final result
     p->vSuppLits= Vec_IntAlloc( 100 );  // support literals
     p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) );
     p->pCnfMan  = Cnf_ManStart();
     // additional AIG data-members
     if ( pAig->pFanData == NULL )
         Aig_ManFanoutStart( pAig );
     if ( pAig->pTerSimData == NULL )
         pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
     // time spent on each outputs
     if ( pPars->nTimeOutOne )
     {
         int i;
         p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
         for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
             p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
     }
     if ( pPars->fSolveAll )
     {
         p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
         p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
         Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
     }
     return p;
 }

void Pdr_ManStop ( Pdr_Man_t * p )

Function*************************************************************

Synopsis [Frees manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file pdrMan.c.

 {
     Pdr_Set_t * pCla;
     sat_solver * pSat;
     int i, k;
     Aig_ManCleanMarkAB( p->pAig );
     if ( p->pPars->fVerbose ) 
     {
         Abc_Print( 1, "Block =%5d  Oblig =%6d  Clause =%6d  Call =%6d (sat=%.1f%%)  Start =%4d\n", 
             p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
         ABC_PRTP( "SAT solving", p->tSat,       p->tTotal );
         ABC_PRTP( "  unsat    ", p->tSatUnsat,  p->tTotal );
         ABC_PRTP( "  sat      ", p->tSatSat,    p->tTotal );
         ABC_PRTP( "Generalize ", p->tGeneral,   p->tTotal );
         ABC_PRTP( "Push clause", p->tPush,      p->tTotal );
         ABC_PRTP( "Ternary sim", p->tTsim,      p->tTotal );
         ABC_PRTP( "Containment", p->tContain,   p->tTotal );
         ABC_PRTP( "CNF compute", p->tCnf,       p->tTotal );
         ABC_PRTP( "TOTAL      ", p->tTotal,     p->tTotal );
         fflush( stdout );
     }
 //    Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
     Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
         sat_solver_delete( pSat );
     Vec_PtrFree( p->vSolvers );
     Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
         Pdr_SetDeref( pCla );
     Vec_VecFree( p->vClauses );
     Pdr_QueueStop( p );
     ABC_FREE( p->pOrder );
     Vec_IntFree( p->vActVars );
     // static CNF
     Cnf_DataFree( p->pCnf1 );
     Vec_IntFreeP( &p->vVar2Reg );
     // dynamic CNF
     Cnf_DataFree( p->pCnf2 );
     if ( p->pvId2Vars )
     for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
         ABC_FREE( p->pvId2Vars[i].pArray );
     ABC_FREE( p->pvId2Vars );
 //    Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
     for ( i = 0; i < Vec_PtrSize(&p->vVar2Ids); i++ )
         Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, i) );
     ABC_FREE( p->vVar2Ids.pArray );
     Vec_WecFreeP( &p->vVLits );
     // CNF manager
     Cnf_ManStop( p->pCnfMan );
     // internal use
     Vec_IntFreeP( &p->vPrio   );  // priority flops
     Vec_IntFree( p->vLits     );  // array of literals
     Vec_IntFree( p->vCiObjs   );  // cone leaves
     Vec_IntFree( p->vCoObjs   );  // cone roots
     Vec_IntFree( p->vCiVals   );  // cone leaf values
     Vec_IntFree( p->vCoVals   );  // cone root values
     Vec_IntFree( p->vNodes    );  // cone nodes
     Vec_IntFree( p->vUndo     );  // cone undos
     Vec_IntFree( p->vVisits   );  // intermediate
     Vec_IntFree( p->vCi2Rem   );  // CIs to be removed
     Vec_IntFree( p->vRes      );  // final result
     Vec_IntFree( p->vSuppLits );  // support literals
     ABC_FREE( p->pCubeJust );
     ABC_FREE( p->pTime4Outs );
     if ( p->vCexes )
         Vec_PtrFreeFree( p->vCexes );
     // additional AIG data-members
     if ( p->pAig->pFanData != NULL )
         Aig_ManFanoutStop( p->pAig );
     if ( p->pAig->pTerSimData != NULL )
         ABC_FREE( p->pAig->pTerSimData );
     ABC_FREE( p );
 }

Pdr_Set_t* Pdr_ManTernarySim	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube
	)

Function*************************************************************

Synopsis [Shrinks values using ternary simulation.]

Description [The cube contains the set of flop index literals which, when converted into a clause and applied to the combinational outputs, led to a satisfiable SAT run in frame k (values stored in the SAT solver). If the cube is NULL, it is assumed that the first property output was asserted and failed. The resulting array is a set of flop index literals that asserts the COs. Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]

SideEffects []

SeeAlso []

Definition at line 351 of file pdrTsim.c.

 {
     Pdr_Set_t * pRes;
     Vec_Int_t * vPrio   = p->vPrio;    // priority flops (flop indices)
     Vec_Int_t * vPiLits = p->vLits;    // array of literals (0/1 PI values)
     Vec_Int_t * vCiObjs = p->vCiObjs;  // cone leaves (CI obj IDs)
     Vec_Int_t * vCoObjs = p->vCoObjs;  // cone roots (CO obj IDs)
     Vec_Int_t * vCiVals = p->vCiVals;  // cone leaf values (0/1 CI values)
     Vec_Int_t * vCoVals = p->vCoVals;  // cone root values (0/1 CO values)
     Vec_Int_t * vNodes  = p->vNodes;   // cone nodes (node obj IDs)
     Vec_Int_t * vUndo   = p->vUndo;    // cone undos (node obj IDs)
     Vec_Int_t * vVisits = p->vVisits;  // intermediate (obj IDs)
     Vec_Int_t * vCi2Rem = p->vCi2Rem;  // CIs to be removed (CI obj IDs)
     Vec_Int_t * vRes    = p->vRes;     // final result (flop literals)
     Aig_Obj_t * pObj;
     int i, Entry, RetValue;
     abctime clk = Abc_Clock();
 
     // collect CO objects
     Vec_IntClear( vCoObjs );
     if ( pCube == NULL ) // the target is the property output
     {
 //        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
         Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, p->iOutCur)) );
     }
     else // the target is the cube
     {
         for ( i = 0; i < pCube->nLits; i++ )
         {
             if ( pCube->Lits[i] == -1 )
                 continue;
             pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
             Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
         }
     }
 if ( p->pPars->fVeryVerbose )
 {
 Abc_Print( 1, "Trying to justify cube " );
 if ( pCube )
     Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
 else
     Abc_Print( 1, "<prop=fail>" );
 Abc_Print( 1, " in frame %d.\n", k );
 }
 
     // collect CI objects
     Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
     // collect values
     Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
     Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
     // simulate for the first time
 if ( p->pPars->fVeryVerbose )
 Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
     RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
     assert( RetValue );
 
 #if 1
     // try removing high-priority flops
     Vec_IntClear( vCi2Rem );
     Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
     {
         if ( !Saig_ObjIsLo( p->pAig, pObj ) )
             continue;
         Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
         if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
             continue;
         Vec_IntClear( vUndo );
         if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
             Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
         else
             Pdr_ManExtendUndo( p->pAig, vUndo );
     }
     // try removing low-priority flops
     Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
     {
         if ( !Saig_ObjIsLo( p->pAig, pObj ) )
             continue;
         Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
         if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
             continue;
         Vec_IntClear( vUndo );
         if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
             Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
         else
             Pdr_ManExtendUndo( p->pAig, vUndo );
     }
 #else
     // try removing low-priority flops
     Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
     {
         if ( !Saig_ObjIsLo( p->pAig, pObj ) )
             continue;
         Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
         if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
             continue;
         Vec_IntClear( vUndo );
         if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
             Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
         else
             Pdr_ManExtendUndo( p->pAig, vUndo );
     }
     // try removing high-priority flops
     Vec_IntClear( vCi2Rem );
     Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
     {
         if ( !Saig_ObjIsLo( p->pAig, pObj ) )
             continue;
         Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
         if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
             continue;
         Vec_IntClear( vUndo );
         if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
             Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
         else
             Pdr_ManExtendUndo( p->pAig, vUndo );
     }
 #endif
 
 if ( p->pPars->fVeryVerbose )
 Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
     RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
     assert( RetValue );
 
     // derive the set of resulting registers
     Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
     assert( Vec_IntSize(vRes) > 0 );
     p->tTsim += Abc_Clock() - clk;
     pRes = Pdr_SetCreate( vRes, vPiLits );
     assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
     return pRes;
 }

static abctime Pdr_ManTimeLimit ( Pdr_Man_t * p )

inlinestatic

Definition at line 141 of file pdrInt.h.

 {
     if ( p->timeToStop == 0 )
         return p->timeToStopOne;
     if ( p->timeToStopOne == 0 )
         return p->timeToStop;
     if ( p->timeToStop < p->timeToStopOne )
         return p->timeToStop;
     return p->timeToStopOne;
 }

void Pdr_ManVerifyInvariant ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 406 of file pdrInv.c.

 {
     sat_solver * pSat;
     Vec_Int_t * vLits;
     Vec_Ptr_t * vCubes;
     Pdr_Set_t * pCube;
     int i, kStart, kThis, RetValue, Counter = 0;
     abctime clk = Abc_Clock();
     // collect cubes used in the inductive invariant
     kStart = Pdr_ManFindInvariantStart( p );
     vCubes = Pdr_ManCollectCubes( p, kStart );
     // create solver with the cubes
     kThis = Vec_PtrSize(p->vSolvers);
     pSat  = Pdr_ManCreateSolver( p, kThis );
     // add the property output
 //    Pdr_ManSetPropertyOutput( p, kThis );
     // add the clauses
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {
         vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
         RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
         assert( RetValue );
         sat_solver_compress( pSat );
     }
     // check each clause
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {
         vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
         RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
         if ( RetValue != l_False )
         {
             Abc_Print( 1, "Verification of clause %d failed.\n", i );
             Counter++;
         }
     }
     if ( Counter )
         Abc_Print( 1, "Verification of %d clauses has failed.\n", Counter );
     else
     {
         Abc_Print( 1, "Verification of invariant with %d clauses was successful.  ", Vec_PtrSize(vCubes) );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
 //    sat_solver_delete( pSat );
     Vec_PtrFree( vCubes );
 }

int Pdr_ObjRegNum	(	Pdr_Man_t *	p,
		int	k,
		int	iSatVar
	)

Function*************************************************************

Synopsis [Returns register number for the given SAT variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 312 of file pdrCnf.c.

 {
     if ( p->pPars->fMonoCnf )
         return Pdr_ObjRegNum1( p, k, iSatVar );
     else
         return Pdr_ObjRegNum2( p, k, iSatVar );
 }

int Pdr_ObjSatVar	(	Pdr_Man_t *	p,
		int	k,
		int	Pol,
		Aig_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Returns SAT variable of the given object.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file pdrCnf.c.

 {
     if ( p->pPars->fMonoCnf )
         return Pdr_ObjSatVar1( p, k, pObj );
     else
         return Pdr_ObjSatVar2( p, k, pObj, 0, Pol );
 }

void Pdr_OblDeref ( Pdr_Obl_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 437 of file pdrUtil.c.

 {
     if ( --p->nRefs == 0 )
     {
         if ( p->pNext )
             Pdr_OblDeref( p->pNext );
         Pdr_SetDeref( p->pState );
         ABC_FREE( p );
     }
 }

Pdr_Obl_t* Pdr_OblRef ( Pdr_Obl_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 420 of file pdrUtil.c.

 {
     p->nRefs++;
     return p;
 }

Pdr_Obl_t* Pdr_OblStart	(	int	k,
		int	prio,
		Pdr_Set_t *	pState,
		Pdr_Obl_t *	pNext
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 396 of file pdrUtil.c.

 {
     Pdr_Obl_t * p;
     p = ABC_ALLOC( Pdr_Obl_t, 1 );
     p->iFrame = k;
     p->prio   = prio;
     p->nRefs  = 1;
     p->pState = pState;
     p->pNext  = pNext;
     p->pLink  = NULL;
     return p;    
 }

void Pdr_QueueClean ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file pdrUtil.c.

 {
     Pdr_Obl_t * pThis;
     while ( (pThis = Pdr_QueuePop(p)) )
         Pdr_OblDeref( pThis );
     pThis = NULL;
 }

Pdr_Obl_t* Pdr_QueueHead ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 475 of file pdrUtil.c.

 {
     return p->pQueue;
 }

int Pdr_QueueIsEmpty ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 459 of file pdrUtil.c.

 {
     return p->pQueue == NULL;
 }

Pdr_Obl_t* Pdr_QueuePop ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file pdrUtil.c.

 {
     Pdr_Obl_t * pRes = p->pQueue;
     if ( p->pQueue == NULL )
         return NULL;
     p->pQueue = p->pQueue->pLink;
     Pdr_OblDeref( pRes );
     p->nQueCur--;
     return pRes;
 }

void Pdr_QueuePrint ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 562 of file pdrUtil.c.

 {
     Pdr_Obl_t * pObl;
     for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
         Abc_Print( 1, "Frame = %2d.  Prio = %8d.\n", pObl->iFrame, pObl->prio );
 }

void Pdr_QueuePush	(	Pdr_Man_t *	p,
		Pdr_Obl_t *	pObl
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 532 of file pdrUtil.c.

 {
     Pdr_Obl_t * pTemp, ** ppPrev;
     p->nObligs++;
     p->nQueCur++;
     p->nQueMax = Abc_MaxInt( p->nQueMax, p->nQueCur );
     Pdr_OblRef( pObl );
     if ( p->pQueue == NULL )
     {
         p->pQueue = pObl;
         return;
     }
     for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink )
         if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) )
             break;
     *ppPrev = pObl;
     pObl->pLink = pTemp;
 }

void Pdr_QueueStop ( Pdr_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 580 of file pdrUtil.c.

 {
     Pdr_Obl_t * pObl;
     while ( !Pdr_QueueIsEmpty(p) )
     {
         pObl = Pdr_QueuePop(p);
         Pdr_OblDeref( pObl );
     }
     p->pQueue = NULL;
     p->nQueCur = 0;
 }

Pdr_Set_t* Pdr_SetAlloc ( int nSize )

DECLARATIONS ///.

CFile****************************************************************

FileName [pdrUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Various utilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:: pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file pdrUtil.c.

 {
     Pdr_Set_t * p;
     assert( nSize >= 0 && nSize < (1<<30) );
     p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) );
     return p;
 }

int Pdr_SetCompare	(	Pdr_Set_t **	pp1,
		Pdr_Set_t **	pp2
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 366 of file pdrUtil.c.

 {
     Pdr_Set_t * p1 = *pp1;
     Pdr_Set_t * p2 = *pp2;
     int i;
     for ( i = 0; i < p1->nLits && i < p2->nLits; i++ )
     {
         if ( p1->Lits[i] > p2->Lits[i] )
             return -1;
         if ( p1->Lits[i] < p2->Lits[i] )
             return 1;
     }
     if ( i == p1->nLits && i < p2->nLits )
         return -1;
     if ( i < p1->nLits && i == p2->nLits )
         return 1;
     return 0;
 }

int Pdr_SetContains	(	Pdr_Set_t *	pOld,
		Pdr_Set_t *	pNew
	)

Function*************************************************************

Synopsis [Return 1 if pOld set-theoretically contains pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file pdrUtil.c.

 {
     int * pOldInt, * pNewInt;
     assert( pOld->nLits > 0 );
     assert( pNew->nLits > 0 );
     if ( pOld->nLits < pNew->nLits )
         return 0;
     if ( (pOld->Sign & pNew->Sign) != pNew->Sign )
         return 0;
     pOldInt = pOld->Lits + pOld->nLits - 1;
     pNewInt = pNew->Lits + pNew->nLits - 1;
     while ( pNew->Lits <= pNewInt )
     {
         if ( pOld->Lits > pOldInt )
             return 0;
         assert( *pNewInt != -1 );
         assert( *pOldInt != -1 );
         if ( *pNewInt == *pOldInt )
             pNewInt--, pOldInt--;
         else if ( *pNewInt < *pOldInt )
             pOldInt--;
         else
             return 0;
     }
     return 1;
 }

int Pdr_SetContainsSimple	(	Pdr_Set_t *	pOld,
		Pdr_Set_t *	pNew
	)

Function*************************************************************

Synopsis [Return 1 if pOld set-theoretically contains pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file pdrUtil.c.

 {
     int * pOldInt, * pNewInt;
     assert( pOld->nLits > 0 );
     assert( pNew->nLits > 0 );
     pOldInt = pOld->Lits + pOld->nLits - 1;
     pNewInt = pNew->Lits + pNew->nLits - 1;
     while ( pNew->Lits <= pNewInt )
     {
         assert( *pOldInt != -1 );
         if ( *pNewInt == -1 )
         {
             pNewInt--;
             continue;
         }
         if ( pOld->Lits > pOldInt )
             return 0;
         assert( *pNewInt != -1 );
         assert( *pOldInt != -1 );
         if ( *pNewInt == *pOldInt )
             pNewInt--, pOldInt--;
         else if ( *pNewInt < *pOldInt )
             pOldInt--;
         else
             return 0;
     }
     return 1;
 }

Pdr_Set_t* Pdr_SetCreate	(	Vec_Int_t *	vLits,
		Vec_Int_t *	vPiLits
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file pdrUtil.c.

 {
     Pdr_Set_t * p;
     int i;
     assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<30) );
     p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) );
     p->nLits  = Vec_IntSize(vLits);
     p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
     p->nRefs  = 1;
     p->Sign   = 0;
     for ( i = 0; i < p->nLits; i++ )
     {
         p->Lits[i] = Vec_IntEntry(vLits, i);
         p->Sign   |= ((word)1 << (p->Lits[i] % 63));
     }
     Vec_IntSelectSort( p->Lits, p->nLits );
     // remember PI literals 
     for ( i = p->nLits; i < p->nTotal; i++ )
         p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
     return p;
 }

Pdr_Set_t* Pdr_SetCreateFrom	(	Pdr_Set_t *	pSet,
		int	iRemove
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file pdrUtil.c.

 {
     Pdr_Set_t * p;
     int i, k = 0;
     assert( iRemove >= 0 && iRemove < pSet->nLits );
     p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) );
     p->nLits  = pSet->nLits - 1;
     p->nTotal = pSet->nTotal - 1;
     p->nRefs  = 1;
     p->Sign   = 0;
     for ( i = 0; i < pSet->nTotal; i++ )
     {
         if ( i == iRemove )
             continue;
         p->Lits[k++] = pSet->Lits[i];
         if ( i >= pSet->nLits )
             continue;
         p->Sign   |= ((word)1 << (pSet->Lits[i] % 63));
     }
     assert( k == p->nTotal );
     return p;
 }

Pdr_Set_t* Pdr_SetCreateSubset	(	Pdr_Set_t *	pSet,
		int *	pLits,
		int	nLits
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file pdrUtil.c.

 {
     Pdr_Set_t * p;
     int i, k = 0;
     assert( nLits >= 0 && nLits <= pSet->nLits );
     p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) );
     p->nLits  = nLits;
     p->nTotal = nLits + pSet->nTotal - pSet->nLits;
     p->nRefs  = 1;
     p->Sign   = 0;
     for ( i = 0; i < nLits; i++ )
     {
         assert( pLits[i] >= 0 );
         p->Lits[k++] = pLits[i];
         p->Sign   |= ((word)1 << (pLits[i] % 63));
     }
     Vec_IntSelectSort( p->Lits, p->nLits );
     for ( i = pSet->nLits; i < pSet->nTotal; i++ )
         p->Lits[k++] = pSet->Lits[i];
     assert( k == p->nTotal );
     return p;
 }

void Pdr_SetDeref ( Pdr_Set_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file pdrUtil.c.

 {
     if ( --p->nRefs == 0 )
         ABC_FREE( p );
 }

Pdr_Set_t* Pdr_SetDup ( Pdr_Set_t * pSet )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file pdrUtil.c.

 {
     Pdr_Set_t * p;
     int i;
     p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) );
     p->nLits  = pSet->nLits;
     p->nTotal = pSet->nTotal;
     p->nRefs  = 1;
     p->Sign   = pSet->Sign;
     for ( i = 0; i < pSet->nTotal; i++ )
         p->Lits[i] = pSet->Lits[i];
     return p;
 }

int Pdr_SetIsInit	(	Pdr_Set_t *	pCube,
		int	iRemove
	)

Function*************************************************************

Synopsis [Return 1 if the state cube contains init state (000...0).]

Description []

SideEffects []

SeeAlso []

Definition at line 341 of file pdrUtil.c.

 {
     int i;
     for ( i = 0; i < pCube->nLits; i++ )
     {
         assert( pCube->Lits[i] != -1 );
         if ( i == iRemove )
             continue;
         if ( lit_sign( pCube->Lits[i] ) == 0 )
             return 0;
     }
     return 1;
 }

void Pdr_SetPrint	(	FILE *	pFile,
		Pdr_Set_t *	p,
		int	nRegs,
		Vec_Int_t *	vFlopCounts
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file pdrUtil.c.

 {
     char * pBuff;
     int i, k, Entry;
     pBuff = ABC_ALLOC( char, nRegs + 1 );
     for ( i = 0; i < nRegs; i++ )
         pBuff[i] = '-';
     pBuff[i] = 0;
     for ( i = 0; i < p->nLits; i++ )
     {
         if ( p->Lits[i] == -1 )
             continue;
         pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
     }
     if ( vFlopCounts )
     {
         // skip some literals
         k = 0;
         Vec_IntForEachEntry( vFlopCounts, Entry, i )
             if ( Entry ) 
                 pBuff[k++] = pBuff[i];
         pBuff[k] = 0;
     }
     fprintf( pFile, "%s", pBuff );
     ABC_FREE( pBuff );
 }

Pdr_Set_t* Pdr_SetRef ( Pdr_Set_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file pdrUtil.c.

 {
     p->nRefs++;
     return p;
 }

Data Structures

Typedefs

Functions

Typedef Documentation

Function Documentation