summaryrefslogtreecommitdiffstats
path: root/src/sat/pdr
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/pdr')
-rw-r--r--src/sat/pdr/module.make8
-rw-r--r--src/sat/pdr/pdr.c53
-rw-r--r--src/sat/pdr/pdr.h79
-rw-r--r--src/sat/pdr/pdrClass.c223
-rw-r--r--src/sat/pdr/pdrCnf.c357
-rw-r--r--src/sat/pdr/pdrCore.c722
-rw-r--r--src/sat/pdr/pdrInt.h198
-rw-r--r--src/sat/pdr/pdrInv.c376
-rw-r--r--src/sat/pdr/pdrMan.c194
-rw-r--r--src/sat/pdr/pdrSat.c373
-rw-r--r--src/sat/pdr/pdrTsim.c450
-rw-r--r--src/sat/pdr/pdrUtil.c719
12 files changed, 0 insertions, 3752 deletions
diff --git a/src/sat/pdr/module.make b/src/sat/pdr/module.make
deleted file mode 100644
index 5cf4491c..00000000
--- a/src/sat/pdr/module.make
+++ /dev/null
@@ -1,8 +0,0 @@
-SRC += src/sat/pdr/pdr.c \
- src/sat/pdr/pdrCnf.c \
- src/sat/pdr/pdrCore.c \
- src/sat/pdr/pdrInv.c \
- src/sat/pdr/pdrMan.c \
- src/sat/pdr/pdrSat.c \
- src/sat/pdr/pdrTsim.c \
- src/sat/pdr/pdrUtil.c
diff --git a/src/sat/pdr/pdr.c b/src/sat/pdr/pdr.c
deleted file mode 100644
index 6bdf75b5..00000000
--- a/src/sat/pdr/pdr.c
+++ /dev/null
@@ -1,53 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pdr.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Netlist representation.]
-
- Synopsis []
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - November 20, 2010.]
-
- Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h
deleted file mode 100644
index 03854509..00000000
--- a/src/sat/pdr/pdr.h
+++ /dev/null
@@ -1,79 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pdr.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Property driven reachability.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - November 20, 2010.]
-
- Revision [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __PDR_H__
-#define __PDR_H__
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Pdr_Par_t_ Pdr_Par_t;
-struct Pdr_Par_t_
-{
- int iOutput; // zero-based number of primary output to solve
- int nRecycle; // limit on vars for recycling
- int nFrameMax; // limit on frame count
- int nConfLimit; // limit on SAT solver conflicts
- int nTimeOut; // timeout in seconds
- int fTwoRounds; // use two rounds for generalization
- int fMonoCnf; // monolythic CNF
- int fDumpInv; // dump inductive invariant
- int fShortest; // forces bug traces to be shortest
- int fSkipGeneral; // skips expensive generalization step
- int fVerbose; // verbose output
- int fVeryVerbose; // very verbose output
- int iFrame; // explored up to this frame
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== pdrCore.c ==========================================================*/
-extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c
deleted file mode 100644
index 3e990958..00000000
--- a/src/sat/pdr/pdrClass.c
+++ /dev/null
@@ -1,223 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pdrClass.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Property driven reachability.]
-
- Synopsis [Equivalence classes of register outputs.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - November 20, 2010.]
-
- Revision [$Id: pdrClass.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Performs duplication with the variable map.]
-
- Description [Var map contains -1 if const0 and <reg_num> otherwise.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap )
-{
- Aig_Man_t * pFrames;
- Aig_Obj_t * pObj;
- int i, iReg;
- assert( Vec_IntSize(vMap) == Aig_ManRegNum(pAig) );
- // start the fraig package
- pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) );
- pFrames->pName = Aig_UtilStrsav( pAig->pName );
- pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
- // create CI mapping
- Aig_ManCleanData( pAig );
- Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
- Aig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi(pFrames);
- Saig_ManForEachLo( pAig, pObj, i )
- {
- iReg = Vec_IntEntry(vMap, i);
- if ( iReg == -1 )
- pObj->pData = Aig_ManConst0(pFrames);
- else
- pObj->pData = Saig_ManLo(pAig, iReg)->pData;
- }
- // add internal nodes of this frame
- Aig_ManForEachNode( pAig, pObj, i )
- pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- // add output nodes
- Aig_ManForEachPo( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
- // finish off
- Aig_ManCleanup( pFrames );
- Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) );
- return pFrames;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates mapping of registers.]
-
- Description [Var map contains -1 if const0 and <reg_num> otherwise.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManCreateMap( Aig_Man_t * p )
-{
- Aig_Obj_t * pObj;
- Vec_Int_t * vMap;
- int * pLit2Id, Lit, i;
- pLit2Id = ABC_ALLOC( int, Aig_ManObjNumMax(p) * 2 );
- for ( i = 0; i < Aig_ManObjNumMax(p) * 2; i++ )
- pLit2Id[i] = -1;
- vMap = Vec_IntAlloc( Aig_ManRegNum(p) );
- Saig_ManForEachLi( p, pObj, i )
- {
- if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p) )
- {
- Vec_IntPush( vMap, -1 );
- continue;
- }
- Lit = 2 * Aig_ObjFaninId0(pObj) + Aig_ObjFaninC0(pObj);
- if ( pLit2Id[Lit] < 0 ) // the first time
- pLit2Id[Lit] = i;
- Vec_IntPush( vMap, pLit2Id[Lit] );
- }
- ABC_FREE( pLit2Id );
- return vMap;
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts reduced registers.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManCountMap( Vec_Int_t * vMap )
-{
- int i, Entry, Counter = 0;
- Vec_IntForEachEntry( vMap, Entry, i )
- if ( Entry != i )
- Counter++;
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts reduced registers.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManPrintMap( Vec_Int_t * vMap )
-{
- Vec_Int_t * vMarks;
- int f, i, iClass, Entry, Counter = 0;
- printf( " Consts: " );
- Vec_IntForEachEntry( vMap, Entry, i )
- if ( Entry == -1 )
- printf( "%d ", i );
- printf( "\n" );
- vMarks = Vec_IntAlloc( 100 );
- Vec_IntForEachEntry( vMap, iClass, f )
- {
- if ( iClass == -1 )
- continue;
- if ( iClass == f )
- continue;
- // check previous classes
- if ( Vec_IntFind( vMarks, iClass ) >= 0 )
- continue;
- Vec_IntPush( vMarks, iClass );
- // print class
- printf( " Class %d : ", iClass );
- Vec_IntForEachEntry( vMap, Entry, i )
- if ( Entry == iClass )
- printf( "%d ", i );
- printf( "\n" );
- }
- Vec_IntFree( vMarks );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManEquivClasses( Aig_Man_t * pAig )
-{
- Vec_Int_t * vMap;
- Aig_Man_t * pTemp;
- int f, nFrames = 100;
- assert( Saig_ManRegNum(pAig) > 0 );
- // start the map
- vMap = Vec_IntAlloc( 0 );
- Vec_IntFill( vMap, Aig_ManRegNum(pAig), -1 );
- // iterate and print changes
- for ( f = 0; f < nFrames; f++ )
- {
- // implement variable map
- pTemp = Pdr_ManRehashWithMap( pAig, vMap );
- // report the result
- printf( "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n",
- f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap),
- Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
- // recreate the map
- Pdr_ManPrintMap( vMap );
- Vec_IntFree( vMap );
- vMap = Pdr_ManCreateMap( pTemp );
- Aig_ManStop( pTemp );
- if ( Pdr_ManCountMap(vMap) == 0 )
- break;
- }
- Vec_IntFree( vMap );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrCnf.c b/src/sat/pdr/pdrCnf.c
deleted file mode 100644
index fddd292b..00000000
--- a/src/sat/pdr/pdrCnf.c
+++ /dev/null
@@ -1,357 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pdrCnf.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Property driven reachability.]
-
- Synopsis [CNF computation on demand.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - November 20, 2010.]
-
- Revision [$Id: pdrCnf.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*
- The CNF (p->pCnf2) is expressed in terms of object IDs.
- Each node in the CNF is marked if it has clauses (p->pCnf2->pObj2Count[Id] > 0).
- Each node in the CNF has the first clause (p->pCnf2->pObj2Clause)
- and the number of clauses (p->pCnf2->pObj2Count).
- Each node used in a CNF of any timeframe has its SAT var recorded.
- Each frame has a reserve mapping of SAT variables into ObjIds.
-*/
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Returns SAT variable of the given object.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{
- return p->pCnf1->pVarNums[ Aig_ObjId(pObj) ];
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns SAT variable of the given object.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{
- assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 );
- if ( p->pvId2Vars[Aig_ObjId(pObj)] == NULL )
- p->pvId2Vars[Aig_ObjId(pObj)] = Vec_IntStart( 16 );
- if ( Vec_IntGetEntry( p->pvId2Vars[Aig_ObjId(pObj)], k ) == 0 )
- {
- sat_solver * pSat = Pdr_ManSolver(p, k);
- Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
- int iVarNew = Vec_IntSize( vVar2Ids );
- assert( iVarNew > 0 );
- Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
- Vec_IntWriteEntry( p->pvId2Vars[Aig_ObjId(pObj)], k, iVarNew );
- sat_solver_setnvars( pSat, iVarNew + 1 );
- if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
- {
- int Lit = toLitCond( iVarNew, 1 );
- int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
- assert( RetValue == 1 );
- sat_solver_compress( pSat );
- }
- }
- return Vec_IntEntry( p->pvId2Vars[Aig_ObjId(pObj)], k );
-}
-
-/**Function*************************************************************
-
- Synopsis [Recursively adds CNF for the given object.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{
- sat_solver * pSat;
- Vec_Int_t * vLits;
- Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
- int nVarCount = Vec_IntSize(vVar2Ids);
- int iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj );
- int * pLit, i, iVar, nClauses, iFirstClause, RetValue;
- if ( nVarCount == Vec_IntSize(vVar2Ids) )
- return iVarThis;
- assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
- if ( Aig_ObjIsPi(pObj) )
- return iVarThis;
- nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
- iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
- assert( nClauses > 0 );
- pSat = Pdr_ManSolver(p, k);
- vLits = Vec_IntAlloc( 16 );
- for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
- {
- Vec_IntClear( vLits );
- for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
- {
- iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)) );
- Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
- }
- RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
- assert( RetValue );
- }
- Vec_IntFree( vLits );
- return iVarThis;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns SAT variable of the given object.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
-{
- if ( p->pPars->fMonoCnf )
- return Pdr_ObjSatVar1( p, k, pObj );
- else
- return Pdr_ObjSatVar2( p, k, pObj );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Returns register number for the given SAT variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Pdr_ObjRegNum1( Pdr_Man_t * p, int k, int iSatVar )
-{
- int RegId;
- assert( iSatVar >= 0 );
- // consider the case of auxiliary variable
- if ( iSatVar >= p->pCnf1->nVars )
- return -1;
- // consider the case of register output
- RegId = Vec_IntEntry( p->vVar2Reg, iSatVar );
- assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
- return RegId;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns register number for the given SAT variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar )
-{
- Aig_Obj_t * pObj;
- int ObjId;
- Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
- assert( iSatVar > 0 && iSatVar < Vec_IntSize(vVar2Ids) );
- ObjId = Vec_IntEntry( vVar2Ids, iSatVar );
- if ( ObjId == -1 ) // activation variable
- return -1;
- pObj = Aig_ManObj( p->pAig, ObjId );
- if ( Saig_ObjIsLi( p->pAig, pObj ) )
- return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig);
- assert( 0 ); // should be called for register inputs only
- return -1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns register number for the given SAT variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar )
-{
- if ( p->pPars->fMonoCnf )
- return Pdr_ObjRegNum1( p, k, iSatVar );
- else
- return Pdr_ObjRegNum2( p, k, iSatVar );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Returns the index of unused SAT variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManFreeVar( Pdr_Man_t * p, int k )
-{
- 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;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
-{
- Aig_Obj_t * pObj;
- int i;
- assert( pSat );
- if ( p->pCnf1 == NULL )
- {
- int nRegs = p->pAig->nRegs;
- p->pAig->nRegs = Aig_ManPoNum(p->pAig);
- p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) );
- p->pAig->nRegs = nRegs;
- assert( p->vVar2Reg == NULL );
- p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
- Saig_ManForEachLi( p->pAig, pObj, i )
- Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
- }
- pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
- sat_solver_set_runtime_limit( pSat, p->timeToStop );
- return pSat;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
-{
- Vec_Int_t * vVar2Ids;
- int i, Entry;
- assert( pSat );
- if ( p->pCnf2 == NULL )
- {
- p->pCnf2 = Cnf_DeriveOther( p->pAig );
- p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) );
- p->vVar2Ids = Vec_PtrAlloc( 256 );
- }
- // update the variable mapping
- vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( p->vVar2Ids, k );
- if ( vVar2Ids == NULL )
- {
- vVar2Ids = Vec_IntAlloc( 500 );
- Vec_PtrWriteEntry( p->vVar2Ids, k, vVar2Ids );
- }
- Vec_IntForEachEntry( vVar2Ids, Entry, i )
- {
- if ( Entry == -1 )
- continue;
- assert( Vec_IntEntry( p->pvId2Vars[Entry], k ) > 0 );
- Vec_IntWriteEntry( p->pvId2Vars[Entry], k, 0 );
- }
- Vec_IntClear( vVar2Ids );
- Vec_IntPush( vVar2Ids, -1 );
- // start the SAT solver
-// pSat = sat_solver_new();
- sat_solver_setnvars( pSat, 500 );
- sat_solver_set_runtime_limit( pSat, p->timeToStop );
- return pSat;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )
-{
- assert( pSat != NULL );
- if ( p->pPars->fMonoCnf )
- return Pdr_ManNewSolver1( pSat, p, k, fInit );
- else
- return Pdr_ManNewSolver2( pSat, p, k, fInit );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
deleted file mode 100644
index 025ada06..00000000
--- a/src/sat/pdr/pdrCore.c
+++ /dev/null
@@ -1,722 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pdrCore.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Property driven reachability.]
-
- Synopsis [Core procedures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - November 20, 2010.]
-
- Revision [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the state could be blocked.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
-{
- memset( pPars, 0, sizeof(Pdr_Par_t) );
- pPars->iOutput = -1; // zero-based output number
- pPars->nRecycle = 300; // limit on vars for recycling
- pPars->nFrameMax = 5000; // limit on number of timeframes
- pPars->nTimeOut = 0; // timeout in seconds
- pPars->nConfLimit = 100000; // limit on SAT solver conflicts
- pPars->fTwoRounds = 0; // use two rounds for generalization
- pPars->fMonoCnf = 0; // monolythic CNF
- pPars->fDumpInv = 0; // dump inductive invariant
- pPars->fShortest = 0; // forces bug traces to be shortest
- pPars->fVerbose = 0; // verbose output
- pPars->fVeryVerbose = 0; // very verbose output
- pPars->iFrame = -1; // explored up to this frame
-}
-
-/**Function*************************************************************
-
- Synopsis [Reduces clause using analyzeFinal.]
-
- Description [Assumes that the SAT solver just terminated an UNSAT call.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
- Pdr_Set_t * pCubeMin;
- Vec_Int_t * vLits;
- int i, Entry, nCoreLits, * pCoreLits;
- // get relevant SAT literals
- nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
- // translate them into register literals and remove auxiliary
- vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
- // skip if there is no improvement
- if ( Vec_IntSize(vLits) == pCube->nLits )
- return NULL;
- assert( Vec_IntSize(vLits) < pCube->nLits );
- // if the cube overlaps with init, add any literal
- Vec_IntForEachEntry( vLits, Entry, i )
- if ( lit_sign(Entry) == 0 ) // positive literal
- break;
- if ( i == Vec_IntSize(vLits) ) // only negative literals
- {
- // add the first positive literal
- for ( i = 0; i < pCube->nLits; i++ )
- if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
- {
- Vec_IntPush( vLits, pCube->Lits[i] );
- break;
- }
- assert( i < pCube->nLits );
- }
- // generate a starting cube
- pCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
- assert( !Pdr_SetIsInit(pCubeMin, -1) );
-/*
- // make sure the cube works
- {
- int RetValue;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
- assert( RetValue );
- }
-*/
- return pCubeMin;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the state could be blocked.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManPushClauses( Pdr_Man_t * p )
-{
- Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
- Vec_Ptr_t * vArrayK, * vArrayK1;
- int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
- int Counter = 0;
- int clk = clock();
- Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
- {
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
- vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
- Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
- {
- Counter++;
-
- // remove cubes in the same frame that are contained by pCubeK
- Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
- {
- if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
- continue;
- Pdr_SetDeref( pTemp );
- Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
- Vec_PtrPop(vArrayK);
- m--;
- }
-
- // check if the clause can be moved to the next frame
- RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 );
- if ( RetValue2 == -1 )
- return -1;
- if ( !RetValue2 )
- continue;
-
- {
- Pdr_Set_t * pCubeMin;
- pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
- if ( pCubeMin != NULL )
- {
-// printf( "%d ", pCubeK->nLits - pCubeMin->nLits );
- Pdr_SetDeref( pCubeK );
- pCubeK = pCubeMin;
- }
- }
-
- // if it can be moved, add it to the next frame
- Pdr_ManSolverAddClause( p, k+1, pCubeK );
- // check if the clause subsumes others
- Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
- {
- if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
- continue;
- Pdr_SetDeref( pCubeK1 );
- Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
- Vec_PtrPop(vArrayK1);
- i--;
- }
- // add the last clause
- Vec_PtrPush( vArrayK1, pCubeK );
- Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
- Vec_PtrPop(vArrayK);
- j--;
- }
- if ( Vec_PtrSize(vArrayK) == 0 )
- RetValue = 1;
- }
-
- // clean up the last one
- vArrayK = Vec_VecEntry( p->vClauses, kMax );
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
- Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
- {
- // remove cubes in the same frame that are contained by pCubeK
- Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
- {
- if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
- continue;
-/*
- printf( "===\n" );
- Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
- printf( "\n" );
- Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
- printf( "\n" );
-*/
- Pdr_SetDeref( pTemp );
- Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
- Vec_PtrPop(vArrayK);
- m--;
- }
- }
- p->tPush += clock() - clk;
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the clause is contained in higher clauses.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
-{
- 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;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Sorts literals by priority.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
-{
- int * pPrios = Vec_IntArray(p->vPrio);
- int * pArray = p->pOrder;
- int temp, i, j, best_i, nSize = pCube->nLits;
- // initialize variable order
- for ( i = 0; i < nSize; i++ )
- pArray[i] = i;
- for ( i = 0; i < nSize-1; i++ )
- {
- best_i = i;
- for ( j = i+1; j < nSize; j++ )
-// if ( pArray[j] < pArray[best_i] )
- if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
- best_i = j;
- temp = pArray[i];
- pArray[i] = pArray[best_i];
- pArray[best_i] = temp;
- }
-/*
- for ( i = 0; i < pCube->nLits; i++ )
- printf( "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
- printf( "\n" );
-*/
- return pArray;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the state could be blocked.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
-{
- Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
- int i, j, n, Lit, RetValue, clk = clock();
- int * pOrder;
- // if there is no induction, return
- *ppCubeMin = NULL;
- RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
- if ( RetValue == -1 )
- return -1;
- if ( RetValue == 0 )
- {
- p->tGeneral += clock() - clk;
- return 0;
- }
-
- // reduce clause using assumptions
-// pCubeMin = Pdr_SetDup( pCube );
- pCubeMin = Pdr_ManReduceClause( p, k, pCube );
- if ( pCubeMin == NULL )
- pCubeMin = Pdr_SetDup( pCube );
-
- // perform generalization
- if ( !p->pPars->fSkipGeneral )
- {
- // sort literals by their occurences
- pOrder = Pdr_ManSortByPriority( p, pCubeMin );
- // try removing literals
- for ( j = 0; j < pCubeMin->nLits; j++ )
- {
- // use ordering
- // i = j;
- i = pOrder[j];
-
- // check init state
- assert( pCubeMin->Lits[i] != -1 );
- if ( Pdr_SetIsInit(pCubeMin, i) )
- continue;
- // try removing this literal
- Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
- if ( RetValue == -1 )
- {
- Pdr_SetDeref( pCubeMin );
- return -1;
- }
- pCubeMin->Lits[i] = Lit;
- if ( RetValue == 0 )
- continue;
-
- // remove j-th entry
- for ( n = j; n < pCubeMin->nLits-1; n++ )
- pOrder[n] = pOrder[n+1];
- j--;
-
- // success - update the cube
- pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
- Pdr_SetDeref( pCubeTmp );
- assert( pCubeMin->nLits > 0 );
- i--;
-
- // get the ordering by decreasing priorit
- pOrder = Pdr_ManSortByPriority( p, pCubeMin );
- }
-
- if ( p->pPars->fTwoRounds )
- for ( j = 0; j < pCubeMin->nLits; j++ )
- {
- // use ordering
- // i = j;
- i = pOrder[j];
-
- // check init state
- assert( pCubeMin->Lits[i] != -1 );
- if ( Pdr_SetIsInit(pCubeMin, i) )
- continue;
- // try removing this literal
- Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
- if ( RetValue == -1 )
- {
- Pdr_SetDeref( pCubeMin );
- return -1;
- }
- pCubeMin->Lits[i] = Lit;
- if ( RetValue == 0 )
- continue;
-
- // remove j-th entry
- for ( n = j; n < pCubeMin->nLits-1; n++ )
- pOrder[n] = pOrder[n+1];
- j--;
-
- // success - update the cube
- pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
- Pdr_SetDeref( pCubeTmp );
- assert( pCubeMin->nLits > 0 );
- i--;
-
- // get the ordering by decreasing priorit
- pOrder = Pdr_ManSortByPriority( p, pCubeMin );
- }
- }
-
- assert( ppCubeMin != NULL );
- *ppCubeMin = pCubeMin;
- p->tGeneral += clock() - clk;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the state could be blocked.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
-{
- Pdr_Obl_t * pThis;
- Pdr_Set_t * pPred, * pCubeMin;
- int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
- int kMax = Vec_PtrSize(p->vSolvers)-1, clk;
- p->nBlocks++;
- // create first proof obligation
- assert( p->pQueue == NULL );
- pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
- Pdr_QueuePush( p, pThis );
- // try to solve it recursively
- while ( !Pdr_QueueIsEmpty(p) )
- {
- Counter++;
- pThis = Pdr_QueueHead( p );
- if ( pThis->iFrame == 0 )
- return 0; // SAT
- pThis = Pdr_QueuePop( p );
- assert( pThis->iFrame > 0 );
- assert( !Pdr_SetIsInit(pThis->pState, -1) );
-
- clk = clock();
- if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
- {
- p->tContain += clock() - clk;
- Pdr_OblDeref( pThis );
- continue;
- }
- p->tContain += clock() - clk;
-
- // check if the cube is already contained
- RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
- if ( RetValue == -1 ) // cube is blocked by clauses in this frame
- {
- Pdr_OblDeref( pThis );
- return -1;
- }
- if ( RetValue ) // cube is blocked by clauses in this frame
- {
- Pdr_OblDeref( pThis );
- continue;
- }
-
- // check if the cube holds with relative induction
- pCubeMin = NULL;
- RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
- if ( RetValue == -1 )
- {
- Pdr_OblDeref( pThis );
- return -1;
- }
- if ( RetValue ) // cube is blocked inductively in this frame
- {
- assert( pCubeMin != NULL );
-
- // k is the last frame where pCubeMin holds
- k = pThis->iFrame;
-
- // check other frames
- assert( pPred == NULL );
- for ( k = pThis->iFrame; k < kMax; k++ )
- if ( !Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ) )
- break;
-
- // add new clause
- if ( p->pPars->fVeryVerbose )
- {
- printf( "Adding cube " );
- Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
- printf( " to frame %d.\n", k );
- }
- // set priority flops
- for ( i = 0; i < pCubeMin->nLits; i++ )
- {
- assert( pCubeMin->Lits[i] >= 0 );
- assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
- Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
- }
-
- Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
- p->nCubes++;
- // add clause
- for ( i = 1; i <= k; i++ )
- Pdr_ManSolverAddClause( p, i, pCubeMin );
- // schedule proof obligation
- if ( k < kMax && !p->pPars->fShortest )
- {
- pThis->iFrame = k+1;
- pThis->prio = Prio--;
- Pdr_QueuePush( p, pThis );
- }
- else
- {
- Pdr_OblDeref( pThis );
- }
- }
- else
- {
- assert( pCubeMin == NULL );
- assert( pPred != NULL );
- pThis->prio = Prio--;
- Pdr_QueuePush( p, pThis );
-
- pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
- Pdr_QueuePush( p, pThis );
- }
-
- // check the timeout
- if ( p->timeToStop && time(NULL) > p->timeToStop )
- return -1;
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManSolveInt( Pdr_Man_t * p )
-{
- int fPrintClauses = 0;
- Pdr_Set_t * pCube;
- int k, RetValue = -1;
- int clkTotal = clock();
- int clkStart = clock();
- p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
- assert( Vec_PtrSize(p->vSolvers) == 0 );
- // create the first timeframe
- Pdr_ManCreateSolver( p, (k = 0) );
- while ( 1 )
- {
- p->nFrames = k;
- assert( k == Vec_PtrSize(p->vSolvers)-1 );
- RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
- if ( RetValue == -1 )
- {
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
- p->pPars->iFrame = k;
- return -1;
- }
- if ( RetValue == 0 )
- {
- RetValue = Pdr_ManBlockCube( p, pCube );
- if ( RetValue == -1 )
- {
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
- p->pPars->iFrame = k;
- return -1;
- }
- if ( RetValue == 0 )
- {
- if ( fPrintClauses )
- {
- printf( "*** Clauses after frame %d:\n", k );
- Pdr_ManPrintClauses( p, 0 );
- }
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- p->pPars->iFrame = k;
- return 0; // SAT
- }
- }
- else
- {
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- // open a new timeframe
- assert( pCube == NULL );
- Pdr_ManSetPropertyOutput( p, k );
- Pdr_ManCreateSolver( p, ++k );
- if ( fPrintClauses )
- {
- printf( "*** Clauses after frame %d:\n", k );
- Pdr_ManPrintClauses( p, 0 );
- }
- // push clauses into this timeframe
- RetValue = Pdr_ManPushClauses( p );
- if ( RetValue == -1 )
- {
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
- p->pPars->iFrame = k;
- return -1;
- }
- if ( RetValue )
- {
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- Pdr_ManReportInvariant( p );
- Pdr_ManVerifyInvariant( p );
- p->pPars->iFrame = k;
- return 1; // UNSAT
- }
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 0, clock() - clkStart );
- clkStart = clock();
- }
-
- // check the timeout
- if ( p->timeToStop && time(NULL) > p->timeToStop )
- {
- if ( fPrintClauses )
- {
- printf( "*** Clauses after frame %d:\n", k );
- Pdr_ManPrintClauses( p, 0 );
- }
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- printf( "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
- p->pPars->iFrame = k;
- return -1;
- }
- if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
- {
- if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
- p->pPars->iFrame = k;
- return -1;
- }
- }
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, Abc_Cex_t ** ppCex )
-{
- Pdr_Man_t * p;
- int RetValue;
- int clk = clock();
- p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
- RetValue = Pdr_ManSolveInt( p );
- *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
- if ( p->pPars->fDumpInv )
- Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
-
-// if ( *ppCex && pPars->fVerbose )
-// printf( "Found counter-example in frame %d after exploring %d frames.\n",
-// (*ppCex)->iFrame, p->nFrames );
- p->tTotal += clock() - clk;
- if ( pvPrioInit )
- {
- *pvPrioInit = p->vPrio;
- p->vPrio = NULL;
- }
- Pdr_ManStop( p );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
-{
-/*
- Vec_Int_t * vPrioInit = NULL;
- int RetValue, nTimeOut;
- if ( pPars->nTimeOut > 0 )
- return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
- nTimeOut = pPars->nTimeOut;
- pPars->nTimeOut = 10;
- RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
- pPars->nTimeOut = nTimeOut;
- if ( RetValue == -1 )
- RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
- Vec_IntFree( vPrioInit );
- return RetValue;
-*/
- return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h
deleted file mode 100644
index f49ee7d0..00000000
--- a/src/sat/pdr/pdrInt.h
+++ /dev/null
@@ -1,198 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#ifndef __PDR_INT_H__
-#define __PDR_INT_H__
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include "saig.h"
-#include "cnf.h"
-#include "satSolver.h"
-#include "pdr.h"
-
-ABC_NAMESPACE_HEADER_START
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Pdr_Set_t_ Pdr_Set_t;
-struct Pdr_Set_t_
-{
- word Sign; // signature
- int nRefs; // ref counter
- int nTotal; // total literals
- int nLits; // num flop literals
- int Lits[0];
-};
-
-typedef struct Pdr_Obl_t_ Pdr_Obl_t;
-struct Pdr_Obl_t_
-{
- int iFrame; // time frame
- int prio; // priority
- int nRefs; // reference counter
- Pdr_Set_t * pState; // state cube
- Pdr_Obl_t * pNext; // next one
- Pdr_Obl_t * pLink; // queue link
-};
-
-typedef struct Pdr_Man_t_ Pdr_Man_t;
-struct Pdr_Man_t_
-{
- // input problem
- Pdr_Par_t * pPars; // parameters
- Aig_Man_t * pAig; // user's AIG
- // static CNF representation
- Cnf_Dat_t * pCnf1; // CNF for this AIG
- Vec_Int_t * vVar2Reg; // mapping of SAT var into registers
- // dynamic CNF representation
- Cnf_Dat_t * pCnf2; // CNF for this AIG
- Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var
- Vec_Ptr_t * vVar2Ids; // for each used frame, maps SAT var into ObjId
- // data representation
- Vec_Ptr_t * vSolvers; // SAT solvers
- Vec_Vec_t * vClauses; // clauses by timeframe
- Pdr_Obl_t * pQueue; // proof obligations
- int * pOrder; // ordering of the lits
- Vec_Int_t * vActVars; // the counter of activation variables
- // internal use
- Vec_Int_t * vPrio; // priority flops
- Vec_Int_t * vLits; // array of literals
- Vec_Int_t * vCiObjs; // cone leaves
- Vec_Int_t * vCoObjs; // cone roots
- Vec_Int_t * vCiVals; // cone leaf values
- Vec_Int_t * vCoVals; // cone root values
- Vec_Int_t * vNodes; // cone nodes
- Vec_Int_t * vUndo; // cone undos
- Vec_Int_t * vVisits; // intermediate
- Vec_Int_t * vCi2Rem; // CIs to be removed
- Vec_Int_t * vRes; // final result
- Vec_Int_t * vSuppLits; // support literals
- Pdr_Set_t * pCubeJust; // justification
- // statistics
- int nBlocks; // the number of times blockState was called
- int nObligs; // the number of proof obligations derived
- int nCubes; // the number of cubes derived
- int nCalls; // the number of SAT calls
- int nCallsS; // the number of SAT calls (sat)
- int nCallsU; // the number of SAT calls (unsat)
- int nStarts; // the number of SAT solver restarts
- int nFrames; // frames explored
- int nCasesSS;
- int nCasesSU;
- int nCasesUS;
- int nCasesUU;
- // runtime
- int timeStart;
- int timeToStop;
- // time stats
- int tSat;
- int tSatSat;
- int tSatUnsat;
- int tGeneral;
- int tPush;
- int tTsim;
- int tContain;
- int tCnf;
- int tTotal;
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== pdrCex.c ==========================================================*/
-extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
-/*=== pdrCnf.c ==========================================================*/
-extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj );
-extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
-extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k );
-extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
-/*=== pdrCore.c ==========================================================*/
-extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
-/*=== pdrInv.c ==========================================================*/
-extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time );
-extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
-extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
-extern void Pdr_ManReportInvariant( Pdr_Man_t * p );
-extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p );
-/*=== pdrMan.c ==========================================================*/
-extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
-extern void Pdr_ManStop( Pdr_Man_t * p );
-extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
-/*=== pdrSat.c ==========================================================*/
-extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
-extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
-extern void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k );
-extern Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext );
-extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray );
-extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
-extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit );
-/*=== pdrTsim.c ==========================================================*/
-extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-/*=== pdrUtil.c ==========================================================*/
-extern Pdr_Set_t * Pdr_SetAlloc( int nSize );
-extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
-extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove );
-extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits );
-extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet );
-extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p );
-extern void Pdr_SetDeref( Pdr_Set_t * p );
-extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
-extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
-extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
-extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
-extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
-extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
-extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p );
-extern void Pdr_OblDeref( Pdr_Obl_t * p );
-extern int Pdr_QueueIsEmpty( Pdr_Man_t * p );
-extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p );
-extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p );
-extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
-extern void Pdr_QueuePrint( Pdr_Man_t * p );
-extern void Pdr_QueueStop( Pdr_Man_t * p );
-extern int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-
-ABC_NAMESPACE_HEADER_END
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c
deleted file mode 100644
index 2f630e28..00000000
--- a/src/sat/pdr/pdrInv.c
+++ /dev/null
@@ -1,376 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "abc.h" // for Abc_NtkCollectCioNames()
-#include "main.h" // for Abc_FrameReadGlobalFrame()
-
-#include "pdrInt.h"
-#include "extra.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
-{
- static int PastSize;
- Vec_Ptr_t * vVec;
- int i, ThisSize, Length, LengthStart;
- if ( Vec_PtrSize(p->vSolvers) < 2 )
- return;
- // count the total length of the printout
- Length = 0;
- Vec_VecForEachLevel( p->vClauses, vVec, i )
- Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
- // determine the starting point
- LengthStart = ABC_MAX( 0, Length - 70 );
- printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
- ThisSize = 6;
- if ( LengthStart > 0 )
- {
- printf( " ..." );
- ThisSize += 4;
- }
- Length = 0;
- Vec_VecForEachLevel( p->vClauses, vVec, i )
- {
- if ( Length < LengthStart )
- {
- Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
- continue;
- }
- printf( " %d", Vec_PtrSize(vVec) );
- Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
- ThisSize += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
- }
- if ( fClose )
- {
- for ( i = 0; i < PastSize - ThisSize; i++ )
- printf( " " );
- printf( "\n" );
- }
- else
- {
- printf( "\r" );
- PastSize = ThisSize;
- }
-// printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts how many times each flop appears in the set of cubes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
-{
- Vec_Int_t * vFlopCount;
- Pdr_Set_t * pCube;
- int i, n;
- vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
- Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
- for ( n = 0; n < pCube->nLits; n++ )
- {
- assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
- Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
- }
- return vFlopCount;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
-{
- Vec_Ptr_t * vArrayK;
- int k, kMax = Vec_PtrSize(p->vSolvers)-1;
- Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 )
- if ( Vec_PtrSize(vArrayK) == 0 )
- return k;
-// return -1;
- // if there is no starting point (as in case of SAT or undecided), return the last frame
-// printf( "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
- return kMax;
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of variables used in the clauses.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart )
-{
- Vec_Ptr_t * vResult;
- Vec_Ptr_t * vArrayK;
- Pdr_Set_t * pSet;
- int i, j;
- vResult = Vec_PtrAlloc( 100 );
- Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart )
- Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j )
- Vec_PtrPush( vResult, pSet );
- return vResult;
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of variables used in the clauses.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
-{
- Vec_Int_t * vFlopCounts;
- Vec_Ptr_t * vCubes;
- int i, Entry, Counter = 0;
- vCubes = Pdr_ManCollectCubes( p, kStart );
- vFlopCounts = Pdr_ManCountFlops( p, vCubes );
- Vec_IntForEachEntry( vFlopCounts, Entry, i )
- Counter += (Entry > 0);
- Vec_IntFreeP( &vFlopCounts );
- Vec_PtrFree( vCubes );
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
-{
- 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 )
- {
- printf( "C=%4d. F=%4d ", Counter++, k );
- Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
- printf( "\n" );
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
-{
- 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 )
- {
- printf( "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 );
- // 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 )
- printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
- else
- printf( "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManReportInvariant( Pdr_Man_t * p )
-{
- Vec_Ptr_t * vCubes;
- int kStart = Pdr_ManFindInvariantStart( p );
- vCubes = Pdr_ManCollectCubes( p, kStart );
- printf( "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 );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
-{
- sat_solver * pSat;
- Vec_Int_t * vLits;
- Vec_Ptr_t * vCubes;
- Pdr_Set_t * pCube;
- int i, kStart, kThis, RetValue, Counter = 0, clk = 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 )
- {
- printf( "Verification of clause %d failed.\n", i );
- Counter++;
- }
- }
- if ( Counter )
- printf( "Verification of %d clauses has failed.\n", Counter );
- else
- {
- printf( "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) );
- Abc_PrintTime( 1, "Time", clock() - clk );
- }
-// sat_solver_delete( pSat );
- Vec_PtrFree( vCubes );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c
deleted file mode 100644
index 95a38efb..00000000
--- a/src/sat/pdr/pdrMan.c
+++ /dev/null
@@ -1,194 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
-{
- 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 );
- // 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) );
- // 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) );
- p->timeStart = clock();
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Frees manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManStop( Pdr_Man_t * p )
-{
- Pdr_Set_t * pCla;
- sat_solver * pSat;
- int i, k;
- Aig_ManCleanMarkAB( p->pAig );
- if ( p->pPars->fVerbose )
- {
- printf( "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 );
- }
-// printf( "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++ )
- Vec_IntFreeP( &p->pvId2Vars[i] );
- ABC_FREE( p->pvId2Vars );
- Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
- // 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 );
- // 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 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
-{
- 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->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 );
- Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
- }
- assert( f == nFrames );
- return pCex;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c
deleted file mode 100644
index cc4c2b1b..00000000
--- a/src/sat/pdr/pdrSat.c
+++ /dev/null
@@ -1,373 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates new SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
-{
- sat_solver * pSat;
- 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
- Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
- return pSat;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns old or restarted solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
-{
- 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_rollback( 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;
-}
-
-/**Function*************************************************************
-
- Synopsis [Converts SAT variables into register IDs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )
-{
- Aig_Obj_t * pObj;
- int i, iVar, iVarMax = 0;
- int clk = clock();
- Vec_IntClear( p->vLits );
- 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, pObj ); assert( iVar >= 0 );
- iVarMax = ABC_MAX( 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 += clock() - clk;
- return p->vLits;
-}
-
-/**Function*************************************************************
-
- Synopsis [Sets the property output to 0 (sat) forever.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
-{
- sat_solver * pSat;
- int Lit, RetValue;
- pSat = Pdr_ManSolver(p, k);
- Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
- RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
- assert( RetValue == 1 );
- sat_solver_compress( pSat );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
- 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 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects values of the RO/RI variables in k-th SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )
-{
- 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, pObj ); assert( iVar >= 0 );
- Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
- }
-}
-
-/**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 []
-
-***********************************************************************/
-int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
- sat_solver * pSat;
- Vec_Int_t * vLits;
- int RetValue;
- pSat = Pdr_ManFetchSolver( p, k );
- vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
- RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
- if ( RetValue == l_Undef )
- return -1;
- return (RetValue == l_False);
-}
-
-/**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 []
-
-***********************************************************************/
-int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit )
-{
- int fUseLit = 1;
- int fLitUsed = 0;
- sat_solver * pSat;
- Vec_Int_t * vLits;
- int Lit, RetValue, clk;
- p->nCalls++;
- pSat = Pdr_ManFetchSolver( p, k );
- if ( pCube == NULL ) // solve the property
- {
- clk = clock();
- Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
- RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
- 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 = clock();
- RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
- 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 = 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;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c
deleted file mode 100644
index 6fec1605..00000000
--- a/src/sat/pdr/pdrTsim.c
+++ /dev/null
@@ -1,450 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pdrTsim.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Property driven reachability.]
-
- Synopsis [Ternary simulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - November 20, 2010.]
-
- Revision [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-#define PDR_ZER 1
-#define PDR_ONE 2
-#define PDR_UND 3
-
-static inline int Pdr_ManSimInfoNot( int Value )
-{
- if ( Value == PDR_ZER )
- return PDR_ONE;
- if ( Value == PDR_ONE )
- return PDR_ZER;
- return PDR_UND;
-}
-
-static inline int Pdr_ManSimInfoAnd( int Value0, int Value1 )
-{
- if ( Value0 == PDR_ZER || Value1 == PDR_ZER )
- return PDR_ZER;
- if ( Value0 == PDR_ONE && Value1 == PDR_ONE )
- return PDR_ONE;
- return PDR_UND;
-}
-
-static inline int Pdr_ManSimInfoGet( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-static inline void Pdr_ManSimInfoSet( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
-{
- assert( Value >= PDR_ZER && Value <= PDR_UND );
- Value ^= Pdr_ManSimInfoGet( p, pObj );
- p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Marks the TFI cone and collects CIs and nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
-{
- assert( !Aig_IsComplement(pObj) );
- if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(pAig, pObj);
- if ( Aig_ObjIsPi(pObj) )
- {
- Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
- return;
- }
- Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
- if ( Aig_ObjIsPo(pObj) )
- return;
- Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
- Vec_IntPush( vNodes, Aig_ObjId(pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Marks the TFI cone and collects CIs and nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
-{
- Aig_Obj_t * pObj;
- int i;
- Vec_IntClear( vCiObjs );
- Vec_IntClear( vNodes );
- Aig_ManIncrementTravId( pAig );
- Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
- Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
- Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs ternary simulation for one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
- int Value0, Value1, Value;
- Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
- if ( Aig_ObjFaninC0(pObj) )
- Value0 = Pdr_ManSimInfoNot( Value0 );
- if ( Aig_ObjIsPo(pObj) )
- {
- Pdr_ManSimInfoSet( pAig, pObj, Value0 );
- return Value0;
- }
- assert( Aig_ObjIsNode(pObj) );
- Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) );
- if ( Aig_ObjFaninC1(pObj) )
- Value1 = Pdr_ManSimInfoNot( Value1 );
- Value = Pdr_ManSimInfoAnd( Value0, Value1 );
- Pdr_ManSimInfoSet( pAig, pObj, Value );
- return Value;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs ternary simulation for one design.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManSimDataInit( Aig_Man_t * pAig,
- Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
- Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
-{
- Aig_Obj_t * pObj;
- int i;
- // set the CI values
- Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
- Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
- Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
- // set the FOs to remove
- if ( vCi2Rem != NULL )
- Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
- Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
- // perform ternary simulation
- Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
- Pdr_ManExtendOneEval( pAig, pObj );
- // transfer results to the output
- Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
- Pdr_ManExtendOneEval( pAig, pObj );
- // check the results
- Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
- if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
- return 0;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Tries to assign ternary value to one of the CIs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis )
-{
- Aig_Obj_t * pFanout;
- int i, k, iFanout, Value, Value2;
- assert( Saig_ObjIsLo(pAig, pObj) );
- assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
- // save original value
- Value = Pdr_ManSimInfoGet( pAig, pObj );
- assert( Value == PDR_ZER || Value == PDR_ONE );
- Vec_IntPush( vUndo, Aig_ObjId(pObj) );
- Vec_IntPush( vUndo, Value );
- // update original value
- Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
- // traverse
- Vec_IntClear( vVis );
- Vec_IntPush( vVis, Aig_ObjId(pObj) );
- Aig_ManForEachObjVec( vVis, pAig, pObj, i )
- {
- Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
- {
- if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
- continue;
- assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
- Value = Pdr_ManSimInfoGet( pAig, pFanout );
- if ( Value == PDR_UND )
- continue;
- Value2 = Pdr_ManExtendOneEval( pAig, pFanout );
- if ( Value2 == Value )
- continue;
- assert( Value2 == PDR_UND );
- Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
- Vec_IntPush( vUndo, Value );
- if ( Aig_ObjIsPo(pFanout) )
- return 0;
- assert( Aig_ObjIsNode(pFanout) );
- Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
- }
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Undoes the partial results of ternary simulation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
-{
- Aig_Obj_t * pObj;
- int i, Value;
- Aig_ManForEachObjVec( vUndo, pAig, pObj, i )
- {
- Value = Vec_IntEntry(vUndo, ++i);
- assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
- Pdr_ManSimInfoSet( pAig, pObj, Value );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the resulting cube.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem, Vec_Int_t * vRes, Vec_Int_t * vPiLits )
-{
- Aig_Obj_t * pObj;
- int i, Lit;
- // mark removed flop outputs
- Aig_ManIncrementTravId( pAig );
- Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
- {
- assert( Saig_ObjIsLo( pAig, pObj ) );
- Aig_ObjSetTravIdCurrent(pAig, pObj);
- }
- // collect flop outputs that are not marked
- Vec_IntClear( vRes );
- Vec_IntClear( vPiLits );
- Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
- {
- if ( Saig_ObjIsPi(pAig, pObj) )
- {
- Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
- Vec_IntPush( vPiLits, Lit );
- continue;
- }
- assert( Saig_ObjIsLo(pAig, pObj) );
- if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
- continue;
- Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
- Vec_IntPush( vRes, Lit );
- }
- if ( Vec_IntSize(vRes) == 0 )
- Vec_IntPush(vRes, 0);
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the resulting cube.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem )
-{
- Aig_Obj_t * pObj;
- int i;
- char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 );
- for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
- pBuff[i] = '-';
- pBuff[i] = 0;
- Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
- pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
- if ( vCi2Rem )
- Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
- pBuff[Aig_ObjPioNum(pObj)] = 'x';
- printf( "%s\n", pBuff );
- ABC_FREE( pBuff );
-}
-
-/**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 []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
- 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;
- int clk = clock();
-
- // collect CO objects
- Vec_IntClear( vCoObjs );
- if ( pCube == NULL ) // the target is the property output
- Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
- 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 )
-{
-printf( "Trying to justify cube " );
-if ( pCube )
- Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
-else
- printf( "<prop=fail>" );
-printf( " 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 );
-
- // try removing high-priority flops
- Vec_IntClear( vCi2Rem );
- Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
- {
- if ( !Saig_ObjIsLo( p->pAig, pObj ) )
- continue;
- Entry = Aig_ObjPioNum(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_ObjPioNum(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 );
- }
-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 += clock() - clk;
- return Pdr_SetCreate( vRes, vPiLits );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/pdr/pdrUtil.c b/src/sat/pdr/pdrUtil.c
deleted file mode 100644
index 1107aec7..00000000
--- a/src/sat/pdr/pdrUtil.c
+++ /dev/null
@@ -1,719 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "pdrInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetAlloc( int nSize )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
-{
- 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 );
-/*
- for ( i = 0; i < p->nLits; i++ )
- printf( "%d ", p->Lits[i] );
- printf( "\n" );
-*/
- // remember PI literals
- for ( i = p->nLits; i < p->nTotal; i++ )
- p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p )
-{
- p->nRefs++;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_SetDeref( Pdr_Set_t * p )
-{
- if ( --p->nRefs == 0 )
- ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
-{
- 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 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Return 1 if pOld set-theoretically contains pNew.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis [Return 1 if pOld set-theoretically contains pNew.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis [Return 1 if the state cube contains init state (000...0).]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext )
-{
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p )
-{
- p->nRefs++;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_OblDeref( Pdr_Obl_t * p )
-{
- if ( --p->nRefs == 0 )
- {
- if ( p->pNext )
- Pdr_OblDeref( p->pNext );
- Pdr_SetDeref( p->pState );
- ABC_FREE( p );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_QueueIsEmpty( Pdr_Man_t * p )
-{
- return p->pQueue == NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p )
-{
- return p->pQueue;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
-{
- Pdr_Obl_t * pRes = p->pQueue;
- if ( p->pQueue == NULL )
- return NULL;
- p->pQueue = p->pQueue->pLink;
- Pdr_OblDeref( pRes );
- return pRes;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
-{
- Pdr_Obl_t * pTemp, ** ppPrev;
- p->nObligs++;
- 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;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_QueuePrint( Pdr_Man_t * p )
-{
- Pdr_Obl_t * pObl;
- for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
- printf( "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Pdr_QueueStop( Pdr_Man_t * p )
-{
- Pdr_Obl_t * pObl;
- while ( !Pdr_QueueIsEmpty(p) )
- {
- pObl = Pdr_QueuePop(p);
- Pdr_OblDeref( pObl );
- }
- p->pQueue = NULL;
-}
-
-
-#define PDR_VAL0 1
-#define PDR_VAL1 2
-#define PDR_VALX 3
-
-/**Function*************************************************************
-
- Synopsis [Returns value (0 or 1) or X if unassigned.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Pdr_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl )
-{
- if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
- return (pNode->fMarkA ^ fCompl) ? PDR_VAL1 : PDR_VAL0;
- return PDR_VALX;
-}
-
-/**Function*************************************************************
-
- Synopsis [Recursively searched for a satisfying assignment.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pdr_Set_t * pCube, int Heur )
-{
- int Value0, Value1;
- if ( Aig_ObjIsConst1(pNode) )
- return 1;
- if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
- return ((int)pNode->fMarkA == Value);
- Aig_ObjSetTravIdCurrent(pAig, pNode);
- pNode->fMarkA = Value;
- if ( Aig_ObjIsPi(pNode) )
- {
-// if ( vSuppLits )
-// Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
- if ( Saig_ObjIsLo(pAig, pNode) )
- {
-// pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value );
- pCube->Lits[pCube->nLits++] = Aig_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value );
- pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63));
- }
- return 1;
- }
- assert( Aig_ObjIsNode(pNode) );
- // propagation
- if ( Value )
- {
- if ( !Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), pCube, Heur) )
- return 0;
- return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), pCube, Heur);
- }
- // justification
- Value0 = Pdr_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
- if ( Value0 == PDR_VAL0 )
- return 1;
- Value1 = Pdr_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
- if ( Value1 == PDR_VAL0 )
- return 1;
- if ( Value0 == PDR_VAL1 && Value1 == PDR_VAL1 )
- return 0;
- if ( Value0 == PDR_VAL1 )
- return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
- if ( Value1 == PDR_VAL1 )
- return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
- assert( Value0 == PDR_VALX && Value1 == PDR_VALX );
- // decision making
-// if ( rand() % 10 == Heur )
- if ( Aig_ObjId(pNode) % 4 == Heur )
- return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), pCube, Heur);
- else
- return Pdr_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), pCube, Heur);
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
-{
- 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;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 15:17:04 +0000