summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigDup.c37
-rw-r--r--src/aig/fra/fraSec.c1
-rw-r--r--src/aig/saig/module.make4
-rw-r--r--src/aig/saig/saig.h1
-rw-r--r--src/aig/saig/saigAbs.c311
-rw-r--r--src/aig/saig/saigBmc.c6
-rw-r--r--src/aig/saig/saigDup.c60
-rw-r--r--src/aig/saig/saigLoc.c169
-rw-r--r--src/aig/ssw/module.make3
-rw-r--r--src/aig/ssw/ssw.h5
-rw-r--r--src/aig/ssw/sswCore.c10
-rw-r--r--src/aig/ssw/sswInt.h9
-rw-r--r--src/aig/ssw/sswMan.c3
-rw-r--r--src/aig/ssw/sswSat.c34
-rw-r--r--src/aig/ssw/sswSweep.c32
-rw-r--r--src/aig/ssw/sswUnique.c254
-rw-r--r--src/base/abci/abc.c117
-rw-r--r--src/base/abci/abcDar.c59
-rw-r--r--src/base/abci/abcStrash.c8
-rw-r--r--src/map/pcm/module.make0
-rw-r--r--src/map/ply/module.make0
-rw-r--r--src/opt/mfs/mfs.h1
-rw-r--r--src/opt/mfs/mfsCore.c4
-rw-r--r--src/opt/mfs/mfsInt.h1
-rw-r--r--src/opt/mfs/mfsInter.c17
-rw-r--r--src/opt/mfs/mfsSat.c32
-rw-r--r--src/sat/bsat/satInterA_yu_hu.c1048
-rw-r--r--src/sat/bsat/satInterP.c2
29 files changed, 2198 insertions, 31 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index fcaf41fa..503985b7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -480,6 +480,7 @@ extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
/*=== aigDup.c ==========================================================*/
extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p );
+extern Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos );
extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index c6a4d19a..9fb19b36 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -194,6 +194,43 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Duplicates part of the AIG manager.]
+
+ Description [Orders nodes as follows: PIs, ANDs, POs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ // create the PIs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
+ Vec_PtrForEachEntry( vPis, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ // duplicate internal nodes
+ Vec_PtrForEachEntry( vPos, pObj, i )
+ {
+ pObjNew = Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
+ Aig_ObjCreatePo( pNew, pObjNew );
+ }
+ Aig_ManSetRegNum( pNew, 0 );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupSimple(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates the AIG manager.]
Description [Assumes topological ordering of the nodes.]
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 232a789e..dce34600 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -56,6 +56,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fInterpolation = 1; // enables interpolation
p->fReachability = 1; // enables BDD based reachability
p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
+ p->fUseNewProver = 0; // enables new prover
p->fSilent = 0; // disables all output
p->fVerbose = 0; // enables verbose reporting of statistics
p->fVeryVerbose = 0; // enables very verbose reporting
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index b09091fb..c3c0a1b6 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,8 +1,10 @@
-SRC += src/aig/saig/saigBmc.c \
+SRC += src/aig/saig/saigAbs.c \
+ src/aig/saig/saigBmc.c \
src/aig/saig/saigCone.c \
src/aig/saig/saigDup.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigIoa.c \
+ src/aig/saig/saigLoc.c \
src/aig/saig/saigMiter.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetFwd.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 81f0fcf5..c7a40f96 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -84,6 +84,7 @@ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int n
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigDup.c ==========================================================*/
extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p );
+extern Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigIoa.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
new file mode 100644
index 00000000..48a26a3c
--- /dev/null
+++ b/src/aig/saig/saigAbs.c
@@ -0,0 +1,311 @@
+/**CFile****************************************************************
+
+ FileName [saigAbs.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Proof-based abstraction.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+#include "cnf.h"
+#include "satSolver.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Saig_ObjFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { return ppMap[nFrames*pObj->Id + i]; }
+static inline void Saig_ObjSetFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + i] = pNode; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Create timeframes of the manager for BMC.]
+
+ Description [The resulting manager is combinational. The only PO is
+ the output of the last frame.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** pppMap )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t ** ppMap;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, f;
+ assert( Saig_ManRegNum(pAig) > 0 );
+ // start the mapping
+ ppMap = *pppMap = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) * nFrames );
+ // start the manager
+ pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+ // create variables for register outputs
+ Saig_ManForEachLo( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ManConst0( pFrames );
+ Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData );
+ }
+ // add timeframes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+ Saig_ObjSetFrame( ppMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pAig)->pData );
+ // create PI nodes for this frame
+ Saig_ManForEachPi( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+ }
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ {
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+ }
+ // create POs for this frame
+ if ( f == nFrames - 1 )
+ {
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+ }
+ break;
+ }
+ // save register inputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+ }
+ // transfer to register outputs
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ {
+ pObjLo->pData = pObjLi->pData;
+ Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData );
+ }
+ }
+ Aig_ManCleanup( pFrames );
+ // remove mapping for the nodes that are no longer there
+ for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ )
+ if ( ppMap[i] && Aig_ObjIsNone( Aig_Regular(ppMap[i]) ) )
+ ppMap[i] = NULL;
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds the set of variables involved in the UNSAT core.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose )
+{
+ void * pSatCnf;
+ Intp_Man_t * pManProof;
+ sat_solver * pSat;
+ Vec_Int_t * vCore;
+ int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars;
+ int i, RetValue;
+ // create the SAT solver
+ pSat = sat_solver_new();
+ sat_solver_store_alloc( pSat );
+ sat_solver_setnvars( pSat, pCnf->nVars );
+ for ( i = 0; i < pCnf->nClauses; i++ )
+ {
+ if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+ {
+ printf( "The BMC problem is trivially UNSAT.\n" );
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+ sat_solver_store_mark_roots( pSat );
+ // solve the problem
+ RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue == l_Undef )
+ {
+ printf( "Conflict limit is reached.\n" );
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ if ( RetValue == l_True )
+ {
+ printf( "The BMC problem is SAT.\n" );
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
+ assert( RetValue == l_False );
+ pSatCnf = sat_solver_store_release( pSat );
+ sat_solver_delete( pSat );
+ // derive the UNSAT core
+ pManProof = Intp_ManAlloc();
+ vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
+ Intp_ManFree( pManProof );
+ Sto_ManFree( pSatCnf );
+ // derive the set of variables on which the core depends
+ // collect the variable numbers
+ nVars = 0;
+ pVars = ALLOC( int, pCnf->nVars );
+ memset( pVars, 0, sizeof(int) * pCnf->nVars );
+ Vec_IntForEachEntry( vCore, iClause, i )
+ {
+ pClause1 = pCnf->pClauses[iClause];
+ pClause2 = pCnf->pClauses[iClause+1];
+ for ( pLit = pClause1; pLit < pClause2; pLit++ )
+ {
+ if ( pVars[ (*pLit) >> 1 ] == 0 )
+ nVars++;
+ pVars[ (*pLit) >> 1 ] = 1;
+ if ( fVerbose )
+ printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
+ }
+ if ( fVerbose )
+ printf( "\n" );
+ }
+ Vec_IntFree( vCore );
+ return pVars;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Labels nodes with the given CNF variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iVar )
+{
+ int iVarThis = pCnf->pVarNums[pObj->Id];
+ if ( iVarThis >= 0 && iVarThis != iVar )
+ return;
+ assert( Aig_ObjIsNode(pObj) );
+ Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin0(pObj), pCnf, iVar );
+ Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin1(pObj), pCnf, iVar );
+ pCnf->pVarNums[pObj->Id] = iVar;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs proof-based abstraction using BMC of the given depth.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
+{
+ Cnf_Dat_t * pCnf;
+ Vec_Int_t * vFlops;
+ Aig_Man_t * pFrames, * pResult;
+ Aig_Obj_t ** ppAigToFrames;
+ Aig_Obj_t * pObj, * pObjFrame;
+ int f, i, * pUnsatCoreVars, clk = clock();
+ assert( Saig_ManPoNum(p) == 1 );
+ Aig_ManSetPioNumbers( p );
+ if ( fVerbose )
+ printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
+ // create the timeframes
+ pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames );
+ // convert them into CNF
+// pCnf = Cnf_Derive( pFrames, 0 );
+ pCnf = Cnf_DeriveSimple( pFrames, 0 );
+ // collect CNF variables involved in UNSAT core
+ pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, nConfMax, 0 );
+ if ( pUnsatCoreVars == NULL )
+ {
+ Aig_ManStop( pFrames );
+ Cnf_DataFree( pCnf );
+ return NULL;
+ }
+ if ( fVerbose )
+ {
+ int Counter = 0;
+ for ( i = 0; i < pCnf->nVars; i++ )
+ Counter += pUnsatCoreVars[i];
+ printf( "The number of variables in the UNSAT core is %d (out of %d).\n", Counter, pCnf->nVars );
+ }
+ // map other nodes into existing CNF variables
+ Aig_ManForEachNode( pFrames, pObj, i )
+ if ( pCnf->pVarNums[pObj->Id] >= 0 )
+ Saig_ManMarkIntoPresentVars_rec( pObj, pCnf, pCnf->pVarNums[pObj->Id] );
+ // collect relevant registers
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Saig_ManForEachLo( p, pObj, i )
+ {
+ pObjFrame = Saig_ObjFrame( ppAigToFrames, nFrames, pObj, f );
+ if ( pObjFrame == NULL )
+ continue;
+ pObjFrame = Aig_Regular(pObjFrame);
+ if ( Aig_ObjIsConst1( pObjFrame ) )
+ continue;
+ assert( pCnf->pVarNums[pObjFrame->Id] >= 0 );
+ if ( pUnsatCoreVars[ pCnf->pVarNums[pObjFrame->Id] ] )
+ pObj->fMarkA = 1;
+ }
+ }
+ // collect the flops
+ vFlops = Vec_IntAlloc( 1000 );
+ Saig_ManForEachLo( p, pObj, i )
+ if ( pObj->fMarkA )
+ {
+ pObj->fMarkA = 0;
+ Vec_IntPush( vFlops, i );
+ }
+ if ( fVerbose )
+ {
+ printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
+ PRT( "Time", clock() - clk );
+ }
+ // create the resulting AIG
+ pResult = Saig_ManAbstraction( p, vFlops );
+ // cleanup
+ Aig_ManStop( pFrames );
+ Cnf_DataFree( pCnf );
+ free( ppAigToFrames );
+ free( pUnsatCoreVars );
+ Vec_IntFree( vFlops );
+ return pResult;
+
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index f03364a4..baf00241 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -34,8 +34,7 @@
Synopsis [Create timeframes of the manager for BMC.]
- Description [The resulting manager is combinational. The primary inputs
- corresponding to register outputs are ordered first. POs correspond to \
+ Description [The resulting manager is combinational. POs correspond to \
the property outputs in each time-frame.]
SideEffects []
@@ -106,8 +105,7 @@ int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
Synopsis [Create timeframes of the manager for BMC.]
- Description [The resulting manager is combinational. The primary inputs
- corresponding to register outputs are ordered first. POs correspond to
+ Description [The resulting manager is combinational. POs correspond to
the property outputs in each time-frame.
The unrolling is stopped as soon as the number of nodes in the frames
exceeds the given maximum size.]
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 1a050741..165a08f2 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -67,6 +67,66 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
return pAigNew;
}
+/**Function*************************************************************
+
+ Synopsis [Numbers of flops included in the abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
+{
+ Aig_Man_t * pAigNew;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, Entry;
+ // start the new manager
+ pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ // label included flops
+ Vec_IntForEachEntry( vFlops, Entry, i )
+ {
+ pObjLi = Saig_ManLi( pAig, Entry );
+ assert( pObjLi->fMarkA == 0 );
+ pObjLi->fMarkA = 1;
+ pObjLo = Saig_ManLo( pAig, Entry );
+ assert( pObjLo->fMarkA == 0 );
+ pObjLo->fMarkA = 1;
+ }
+ // create variables for PIs
+ Aig_ManForEachPi( pAig, pObj, i )
+ if ( !pObj->fMarkA )
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+ // create variables for LOs
+ Aig_ManForEachPi( pAig, pObj, i )
+ if ( pObj->fMarkA )
+ {
+ pObj->fMarkA = 0;
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+ }
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create POs
+ Aig_ManForEachPo( pAig, pObj, i )
+ if ( !pObj->fMarkA )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ // create LIs
+ Aig_ManForEachPo( pAig, pObj, i )
+ if ( pObj->fMarkA )
+ {
+ pObj->fMarkA = 0;
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ }
+ Aig_ManCleanup( pAigNew );
+ Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
+ return pAigNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigLoc.c b/src/aig/saig/saigLoc.c
new file mode 100644
index 00000000..60c547dd
--- /dev/null
+++ b/src/aig/saig/saigLoc.c
@@ -0,0 +1,169 @@
+/**CFile****************************************************************
+
+ FileName [saigLoc.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Localization package.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigLoc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs localization by unrolling timeframes backward.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose )
+{
+ sat_solver * pSat;
+ Vec_Int_t * vTopVarNums;
+ Vec_Ptr_t * vTop, * vBot;
+ Cnf_Dat_t * pCnfTop, * pCnfBot;
+ Aig_Man_t * pPartTop, * pPartBot;
+ Aig_Obj_t * pObj, * pObjBot;
+ int i, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
+ assert( Saig_ManPoNum(p) == 1 );
+ Aig_ManSetPioNumbers( p );
+
+ // start the top by including the PO
+ vBot = Vec_PtrAlloc( 100 );
+ vTop = Vec_PtrAlloc( 100 );
+ Vec_PtrPush( vTop, Aig_ManPo(p, 0) );
+ // create the manager composed of one PI/PO pair
+ pPartTop = Aig_ManStart( 10 );
+ Aig_ObjCreatePo( pPartTop, Aig_ObjCreatePi(pPartTop) );
+ pCnfTop = Cnf_Derive( pPartTop, 0 );
+ // start the array of CNF variables
+ vTopVarNums = Vec_IntAlloc( 100 );
+ Vec_IntPush( vTopVarNums, pCnfTop->pVarNums[Aig_ManPi(pPartTop,0)->Id] );
+ // start the solver
+ pSat = Cnf_DataWriteIntoSolver( pCnfTop, 1, 0 );
+
+ // iterate backward unrolling
+ RetValue = -1;
+ nSatVarNum = pCnfTop->nVars;
+ if ( fVerbose )
+ printf( "Localization parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
+ for ( f = 0; ; f++ )
+ {
+ clk = clock();
+ // get the bottom
+ Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
+ // derive AIG for the part between top and bottom
+ pPartBot = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
+ // convert it into CNF
+ pCnfBot = Cnf_Derive( pPartBot, Aig_ManPoNum(pPartBot) );
+ Cnf_DataLift( pCnfBot, nSatVarNum );
+ nSatVarNum += pCnfBot->nVars;
+ // stitch variables of top and bot
+ assert( Aig_ManPoNum(pPartBot) == Vec_IntSize(vTopVarNums) );
+ Aig_ManForEachPo( pPartBot, pObjBot, i )
+ {
+ Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 0 );
+ Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 1 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 1 );
+ Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 0 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ }
+ // add CNF to the SAT solver
+ for ( i = 0; i < pCnfBot->nClauses; i++ )
+ if ( !sat_solver_addclause( pSat, pCnfBot->pClauses[i], pCnfBot->pClauses[i+1] ) )
+ break;
+ if ( i < pCnfBot->nClauses )
+ {
+// printf( "SAT solver became UNSAT after adding clauses.\n" );
+ RetValue = 1;
+ break;
+ }
+ // run the SAT solver
+ nConfPrev = pSat->stats.conflicts;
+ status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 );
+ if ( fVerbose )
+ {
+ printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ",
+ f+1, Aig_ManPiNum(pPartBot), Aig_ManPoNum(pPartBot), Aig_ManNodeNum(pPartBot),
+ nSatVarNum, pSat->stats.conflicts-nConfPrev );
+ PRT( "Time", clock() - clk );
+ }
+ if ( status == l_Undef )
+ break;
+ if ( status == l_False )
+ {
+ RetValue = 1;
+ break;
+ }
+ assert( status == l_True );
+ if ( f == nFramesMax - 1 )
+ break;
+ // the problem is SAT - add more clauses
+ // create new set of POs to derive new top
+ Vec_PtrClear( vTop );
+ Vec_IntClear( vTopVarNums );
+ Vec_PtrForEachEntry( vBot, pObj, i )
+ {
+ assert( Aig_ObjIsPi(pObj) );
+ if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pObjBot = pObj->pData;
+ assert( pObjBot != NULL );
+ Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObj) );
+ Vec_IntPush( vTopVarNums, pCnfBot->pVarNums[pObjBot->Id] );
+ }
+ }
+ // remove old top and replace it by bottom
+ Aig_ManStop( pPartTop );
+ pPartTop = pPartBot;
+ pPartBot = NULL;
+ Cnf_DataFree( pCnfTop );
+ pCnfTop = pCnfBot;
+ pCnfBot = NULL;
+ }
+// printf( "Completed %d interations.\n", f+1 );
+ // cleanup
+ sat_solver_delete( pSat );
+ Aig_ManStop( pPartTop );
+ Cnf_DataFree( pCnfTop );
+ Aig_ManStop( pPartBot );
+ Cnf_DataFree( pCnfBot );
+ Vec_IntFree( vTopVarNums );
+ Vec_PtrFree( vTop );
+ Vec_PtrFree( vBot );
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 6b748598..625d72d1 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -10,4 +10,5 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswSat.c \
src/aig/ssw/sswSim.c \
src/aig/ssw/sswSimSat.c \
- src/aig/ssw/sswSweep.c
+ src/aig/ssw/sswSweep.c \
+ src/aig/ssw/sswUnique.c
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 98e8c9d7..766407d4 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -53,6 +53,7 @@ struct Ssw_Pars_t_
int fSkipCheck; // do not run equivalence check for unaffected cones
int fLatchCorr; // perform register correspondence
int fSemiFormal; // enable semiformal filtering
+ int fUniqueness; // enable uniqueness constraints
int fVerbose; // verbose stats
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
@@ -82,11 +83,15 @@ struct Ssw_Cex_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*=== sswAbs.c ==========================================================*/
+extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
+/*=== sswLoc.c ==========================================================*/
+extern int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 424e3531..8052ffcd 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -45,7 +45,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nPartSize = 0; // size of the partition
p->nOverSize = 0; // size of the overlap between partitions
p->nFramesK = 1; // the induction depth
- p->nFramesAddSim = 2; // additional frames to simulate
+ p->nFramesAddSim = 0; // additional frames to simulate
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node
p->nMinDomSize = 100; // min clock domain considered for optimization
@@ -53,6 +53,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fSkipCheck = 0; // do not run equivalence check for unaffected cones
p->fLatchCorr = 0; // performs register correspondence
p->fSemiFormal = 0; // enable semiformal filtering
+ p->fUniqueness = 0; // enable uniqueness constraints
p->fVerbose = 0; // verbose stats
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
@@ -153,9 +154,9 @@ clk = clock();
RetValue = Ssw_ManSweep( p );
if ( p->pPars->fVerbose )
{
- printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
+ printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
- p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
+ p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal );
if ( p->pPars->fSkipCheck )
printf( "Use = %5d. Skip = %5d. ",
p->nRefUse, p->nRefSkip );
@@ -165,7 +166,7 @@ clk = clock();
Ssw_ManCleanup( p );
if ( !RetValue )
break;
-
+/*
{
static int Flag = 0;
if ( Flag++ == 4 && nIter == 4 )
@@ -176,6 +177,7 @@ clk = clock();
Aig_ManStop( pSRed );
}
}
+*/
}
p->pPars->nIters = nIter + 1;
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 5daffc75..636bd139 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -78,6 +78,10 @@ struct Ssw_Man_t_
int nRecycleCalls; // the number of calls since last recycling
int nRecycles; // the number of time SAT solver was recycled
int nConeMax; // the maximum cone size
+ // uniqueness
+ Vec_Ptr_t * vCommon; // the set of common variables in the logic cones
+ int iOutputLit; // the output literal of the uniqueness constaint
+ int nUniques; // the number of uniqueness constaints used
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
@@ -205,10 +209,13 @@ extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrame
extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
+extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc );
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
-
+/*=== sswUnique.c ===================================================*/
+extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
+extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
#ifdef __cplusplus
}
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index ba19d46e..d4a26f64 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -59,6 +59,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 );
p->vUsedPis = Vec_PtrAlloc( 1000 );
+ p->vCommon = Vec_PtrAlloc( 100 );
+ p->iOutputLit = -1;
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
@@ -190,6 +192,7 @@ void Ssw_ManStop( Ssw_Man_t * p )
Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vUsedPis );
Vec_IntFree( p->vSatVars );
+ Vec_PtrFree( p->vCommon );
FREE( p->pNodeToFrames );
FREE( p->pPatWords );
free( p );
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index 264b39d1..af3bf80e 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -42,7 +42,7 @@
int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int nBTLimit = p->pPars->nBTLimit;
- int pLits[2], RetValue, RetValue1, clk;//, status;
+ int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
p->nSatCalls++;
// sanity checks
@@ -59,8 +59,11 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
+ nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+ if ( p->iOutputLit > -1 )
+ pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
@@ -75,16 +78,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
clk = clock();
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
- pLits[0] = lit_neg( pLits[0] );
- pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
+ if ( nLits == 2 )
+ {
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ }
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
@@ -109,8 +115,11 @@ p->timeSatUndec += clock() - clk;
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
+ nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+ if ( p->iOutputLit > -1 )
+ pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
@@ -124,16 +133,19 @@ p->timeSatUndec += clock() - clk;
}
clk = clock();
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
- pLits[0] = lit_neg( pLits[0] );
- pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
+ if ( nLits == 2 )
+ {
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ }
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index add00a88..b971a13a 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -87,14 +87,15 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
SeeAlso []
***********************************************************************/
-int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
{
Aig_Obj_t * pObjFraig;
int nVarNum, Value;
- assert( Aig_ObjIsPi(pObj) );
+// assert( Aig_ObjIsPi(pObj) );
pObjFraig = Ssw_ObjFrame( p, pObj, f );
nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+// Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum )));
// Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
if ( p->pPars->fPolarFlip )
{
@@ -120,7 +121,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pAig, pObj, i )
- if ( Ssw_ManOriginalPiValue( p, pObj, f ) )
+ if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
Aig_InfoSetBit( p->pPatWords, i );
}
@@ -179,7 +180,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
{
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
- return 0;
+ return 0;
// count the number of skipped calls
if ( !pObj->fMarkA && !pObjRepr->fMarkA )
p->nRefSkip++;
@@ -212,6 +213,18 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
// disproved the equivalence
Ssw_SmlSavePatternAig( p, f );
}
+ if ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 &&
+ Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 )
+ {
+ if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
+ {
+ int RetValue;
+ assert( p->iOutputLit > -1 );
+ RetValue = Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->iOutputLit = -1;
+ return RetValue;
+ }
+ }
if ( p->pPars->nConstrs == 0 )
Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
else
@@ -300,6 +313,7 @@ int Ssw_ManSweep( Ssw_Man_t * p )
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, clk, i, f;
+ int v;
// perform speculative reduction
clk = clock();
@@ -330,6 +344,8 @@ clk = clock();
Ssw_ManSweepMarkRefinement( p );
p->timeMarkCones += clock() - clk;
+//Ssw_ManUnique( p );
+
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
@@ -338,10 +354,18 @@ p->timeMarkCones += clock() - clk;
// make sure LOs are assigned
Saig_ManForEachLo( p->pAig, pObj, i )
assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
+////
+ // bring up the previous frames
+ if ( p->pPars->fUniqueness )
+ for ( v = 0; v < f; v++ )
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ Ssw_CnfNodeAddToSolver( p, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) );
+////
// sweep internal nodes
p->fRefined = 0;
p->nSatFailsReal = 0;
p->nRefUse = p->nRefSkip = 0;
+ p->nUniques = 0;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
new file mode 100644
index 00000000..888ed3da
--- /dev/null
+++ b/src/aig/ssw/sswUnique.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+ FileName [sswSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [On-demand uniqueness constraints.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns the result of merging the two vectors.]
+
+ Description [Assumes that the vectors are sorted in the increasing order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
+{
+ Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
+ Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
+ Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
+ Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
+ Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
+ Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
+ pBeg = (Aig_Obj_t **)vArr->pArray;
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( (*pBeg1)->Id == (*pBeg2)->Id )
+ *pBeg++ = *pBeg1++, pBeg2++;
+ else if ( (*pBeg1)->Id < (*pBeg2)->Id )
+ *pBeg++ = *pBeg1++;
+ else
+ *pBeg++ = *pBeg2++;
+ }
+ while ( pBeg1 < pEnd1 )
+ *pBeg++ = *pBeg1++;
+ while ( pBeg2 < pEnd2 )
+ *pBeg++ = *pBeg2++;
+ vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
+ assert( vArr->nSize <= vArr->nCap );
+ assert( vArr->nSize >= vArr1->nSize );
+ assert( vArr->nSize >= vArr2->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the result of merging the two vectors.]
+
+ Description [Assumes that the vectors are sorted in the increasing order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
+{
+ Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
+ Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
+ Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
+ Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
+ Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
+ Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
+ pBeg = (Aig_Obj_t **)vArr->pArray;
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( (*pBeg1)->Id == (*pBeg2)->Id )
+ *pBeg++ = *pBeg1++, pBeg2++;
+ else if ( (*pBeg1)->Id < (*pBeg2)->Id )
+// *pBeg++ = *pBeg1++;
+ pBeg1++;
+ else
+// *pBeg++ = *pBeg2++;
+ pBeg2++;
+ }
+// while ( pBeg1 < pEnd1 )
+// *pBeg++ = *pBeg1++;
+// while ( pBeg2 < pEnd2 )
+// *pBeg++ = *pBeg2++;
+ vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
+ assert( vArr->nSize <= vArr->nCap );
+ assert( vArr->nSize <= vArr1->nSize );
+ assert( vArr->nSize <= vArr2->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if uniqueness constraints can be added.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
+{
+ int fVerbose = 0;
+ Aig_Obj_t * ppObjs[2], * pTemp;
+ Vec_Ptr_t * vSupp, * vSupp2;
+ int i, k, Value0, Value1, RetValue;
+ assert( p->pPars->nFramesK > 1 );
+
+ vSupp = Vec_PtrAlloc( 100 );
+ vSupp2 = Vec_PtrAlloc( 100 );
+ Vec_PtrClear( p->vCommon );
+
+ // compute the first support in terms of LOs
+ ppObjs[0] = pRepr;
+ ppObjs[1] = pObj;
+ Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp );
+ // modify support to be in terms of LIs
+ k = 0;
+ Vec_PtrForEachEntry( vSupp, pTemp, i )
+ if ( Saig_ObjIsLo(p->pAig, pTemp) )
+ Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) );
+ Vec_PtrShrink( vSupp, k );
+ // compute the support of support
+ Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 );
+ // return support to LO
+ Vec_PtrForEachEntry( vSupp, pTemp, i )
+ Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) );
+ // find the number of common vars
+ Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease );
+ Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease );
+ Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon );
+/*
+ {
+ Vec_Ptr_t * vNew = Vec_PtrDup(vSupp);
+ Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
+ if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) )
+ printf( "Not unique!\n" );
+ }
+ {
+ Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2);
+ Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
+ if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) )
+ printf( "Not unique!\n" );
+ }
+ {
+ Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon);
+ Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
+ if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) )
+ printf( "Not unique!\n" );
+ }
+*/
+ if ( fVerbose )
+ printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ",
+ Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) );
+
+ // check the current values
+ RetValue = 1;
+ Vec_PtrForEachEntry( p->vCommon, pTemp, i )
+ {
+ Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 );
+ Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 );
+ if ( Value0 != Value1 )
+ RetValue = 0;
+ if ( fVerbose )
+ printf( "%d", Value0 ^ Value1 );
+ }
+ if ( Vec_PtrSize(p->vCommon) == 0 )
+ RetValue = 0;
+ if ( fVerbose )
+ printf( "\n" );
+
+ Vec_PtrFree( vSupp );
+ Vec_PtrFree( vSupp2 );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the output of the uniqueness constraint.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 )
+{
+ Aig_Obj_t * pObj, * pObj1New, * pObj2New, * pMiter, * pTotal;
+ int i, pLits[2];
+// int RetValue;
+ assert( Vec_PtrSize(vCommon) > 0 );
+ // generate the constraint
+ pTotal = Aig_ManConst0(p->pFrames);
+ Vec_PtrForEachEntry( vCommon, pObj, i )
+ {
+ assert( Saig_ObjIsLo(p->pAig, pObj) );
+ pObj1New = Ssw_ObjFrame( p, pObj, f1 );
+ pObj2New = Ssw_ObjFrame( p, pObj, f2 );
+ pMiter = Aig_Exor( p->pFrames, pObj1New, pObj2New );
+ pTotal = Aig_Or( p->pFrames, pTotal, pMiter );
+ }
+ if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
+ {
+// printf( "Skipped\n" );
+ return 0;
+ }
+ p->nUniques++;
+ // create CNF
+ Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) );
+ // add output constraint
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
+/*
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+ assert( RetValue );
+ // simplify the solver
+ if ( p->pSat->qtail != p->pSat->qhead )
+ {
+ RetValue = sat_solver_simplify(p->pSat);
+ assert( RetValue != 0 );
+ }
+*/
+ assert( p->iOutputLit == -1 );
+ p->iOutputLit = pLits[0];
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5d5ccb46..4f46f3a2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -215,6 +215,7 @@ static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandLocalize ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -481,6 +482,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "int", Abc_CommandBmcInter, 0 );
Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 );
Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 );
+ Cmd_CommandAdd( pAbc, "Verification", "loc", Abc_CommandLocalize, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 );
@@ -3671,7 +3673,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Abc_NtkMfsParsDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraesvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraestvwh" ) ) != EOF )
{
switch ( c )
{
@@ -3753,6 +3755,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fSwapEdge ^= 1;
break;
+ case 't':
+ pPars->fOneHotness ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -3786,7 +3791,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raesvh]\n" );
+ fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raestvh]\n" );
fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" );
fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
@@ -3798,6 +3803,7 @@ usage:
fprintf( pErr, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
fprintf( pErr, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
fprintf( pErr, "\t-s : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" );
+ fprintf( pErr, "\t-t : toggle using artificial one-hotness conditions [default = %s]\n", pPars->fOneHotness? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -13535,7 +13541,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfuvh" ) ) != EOF )
{
switch ( c )
{
@@ -13628,6 +13634,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pPars->fSemiFormal ^= 1;
break;
+ case 'u':
+ pPars->fUniqueness ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -13680,7 +13689,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfvh]\n" );
+ fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfuvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -13693,6 +13702,7 @@ usage:
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( pErr, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" );
fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
+ fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -16475,6 +16485,105 @@ usage:
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int nFramesMax;
+ int nConfMax;
+ int fVerbose;
+ int c;
+ extern void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFramesMax = 50;
+ nConfMax = 500;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFramesMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFramesMax < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfMax < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsComb(pNtk) )
+ {
+ fprintf( pErr, "The network is combinational.\n" );
+ return 0;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ {
+ fprintf( pErr, "Currently this command works only for single-output miter.\n" );
+ return 0;
+ }
+
+ // modify the current network
+ Abc_NtkDarLocalize( pNtk, nFramesMax, nConfMax, fVerbose );
+ return 0;
+usage:
+ fprintf( pErr, "usage: loc [-FC num] [-vh]\n" );
+ fprintf( pErr, "\t performs localization for single-output miter\n" );
+ fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
+ fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+ fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
/**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 71443265..98228c56 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1974,6 +1974,44 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
Aig_ManStop( pMan );
return pNtkAig;
}
+/**Function*************************************************************
+
+ Synopsis [Performs targe enlargement.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
+{
+ Aig_Man_t * pMan, * pTemp;
+ int clkTotal = clock();
+ int RetValue;
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return;
+ RetValue = Saig_ManLocalization( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
+ Aig_ManStop( pTemp );
+ if ( RetValue == 1 )
+ {
+ printf( "Networks are equivalent. " );
+PRT( "Time", clock() - clkTotal );
+ }
+ else if ( RetValue == 0 )
+ {
+ printf( "Networks are NOT EQUIVALENT. " );
+PRT( "Time", clock() - clkTotal );
+ }
+ else
+ {
+ printf( "Networks are UNDECIDED. " );
+PRT( "Time", clock() - clkTotal );
+ }
+}
+
/**Function*************************************************************
@@ -2453,6 +2491,7 @@ Aig_ManPrintStats( pMan );
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
{
+/*
extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
Abc_Ntk_t * pNtkAig;
@@ -2471,6 +2510,26 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
+*/
+ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
+
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan, * pTemp;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return NULL;
+
+ Aig_ManSetRegNum( pMan, pMan->nRegs );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, 10, 1000, 1 );
+ Aig_ManStop( pTemp );
+
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+ Aig_ManStop( pMan );
+ return pNtkAig;
+
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index ad09f084..463846b9 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -122,7 +122,15 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
// complement the 1-valued registers
Abc_NtkForEachLatch( pNtkAig, pObj, i )
if ( Abc_LatchIsInit1(pObj) )
+ {
Abc_ObjXorFaninC( Abc_ObjFanin0(pObj), 0 );
+ // if latch has PO as one of its fanouts change latch name
+ if ( Abc_NodeFindCoFanout( Abc_ObjFanout0(pObj) ) )
+ {
+ Nm_ManDeleteIdName( pObj->pNtk->pManName, Abc_ObjFanout0(pObj)->Id );
+ Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjName(Abc_ObjFanout0(pObj)), "_inv" );
+ }
+ }
// set all constant-0 values
Abc_NtkForEachLatch( pNtkAig, pObj, i )
Abc_LatchSetInit0( pObj );
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 989cd718..9550a31b 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -52,6 +52,7 @@ struct Mfs_Par_t_
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
int fSwapEdge; // performs edge swapping
+ int fOneHotness; // adds one-hotness conditions
int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 0b2ba47d..3444bab1 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -41,6 +41,7 @@
***********************************************************************/
void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
{
+ memset( pPars, 0, sizeof(Mfs_Par_t) );
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nDepthMax = 20;
@@ -52,6 +53,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
pPars->fArea = 0;
pPars->fMoreEffort = 0;
pPars->fSwapEdge = 0;
+ pPars->fOneHotness = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
}
@@ -155,6 +157,8 @@ p->timeCnf += clock() - clk;
// create the SAT problem
clk = clock();
p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+ if ( p->pSat && p->pPars->fOneHotness )
+ Abc_NtkAddOneHotness( p );
if ( p->pSat == NULL )
return 0;
// solve the SAT problem
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 37521189..df8a4848 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -141,6 +141,7 @@ extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsSat.c ==========================================================*/
extern int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int Abc_NtkAddOneHotness( Mfs_Man_t * p );
/*=== mfsStrash.c ==========================================================*/
extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 5944fd5b..6e50d444 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -123,6 +123,15 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
return NULL;
}
+ // add one-hotness constraints
+ if ( p->pPars->fOneHotness )
+ {
+ p->pSat = pSat;
+ if ( !Abc_NtkAddOneHotness( p ) )
+ return NULL;
+ p->pSat = NULL;
+ }
+
// bookmark the clauses of A
if ( pCands )
sat_solver_store_mark_clauses_a( pSat );
@@ -139,6 +148,14 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
return NULL;
}
}
+ // add one-hotness constraints
+ if ( p->pPars->fOneHotness )
+ {
+ p->pSat = pSat;
+ if ( !Abc_NtkAddOneHotness( p ) )
+ return NULL;
+ p->pSat = NULL;
+ }
// transform the literals
for ( i = 0; i < p->pCnf->nLiterals; i++ )
p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index 5023bf62..6cc0f0fd 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -133,6 +133,38 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Adds one-hotness constraints for the window inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkAddOneHotness( Mfs_Man_t * p )
+{
+ Aig_Obj_t * pObj1, * pObj2;
+ int i, k, Lits[2];
+ for ( i = 0; i < Vec_PtrSize(p->pAigWin->vPis); i++ )
+ for ( k = i+1; k < Vec_PtrSize(p->pAigWin->vPis); k++ )
+ {
+ pObj1 = Aig_ManPi( p->pAigWin, i );
+ pObj2 = Aig_ManPi( p->pAigWin, k );
+ Lits[0] = toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 );
+ Lits[1] = toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 );
+ if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
+ {
+ sat_solver_delete( p->pSat );
+ p->pSat = NULL;
+ return 0;
+ }
+ }
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satInterA_yu_hu.c b/src/sat/bsat/satInterA_yu_hu.c
new file mode 100644
index 00000000..2005e558
--- /dev/null
+++ b/src/sat/bsat/satInterA_yu_hu.c
@@ -0,0 +1,1048 @@
+/**CFile****************************************************************
+
+ FileName [satInter.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT sat_solver.]
+
+ Synopsis [Interpolation package.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "satStore.h"
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// variable assignments
+static const lit LIT_UNDEF = 0xffffffff;
+
+// interpolation manager
+struct Inta_Man_t_
+{
+ // clauses of the problems
+ Sto_Man_t * pCnf; // the set of CNF clauses for A and B
+ Vec_Int_t * vVarsAB; // the array of global variables
+ // various parameters
+ int fVerbose; // verbosiness flag
+ int fProofVerif; // verifies the proof
+ int fProofWrite; // writes the proof file
+ int nVarsAlloc; // the allocated size of var arrays
+ int nClosAlloc; // the allocated size of clause arrays
+ // internal BCP
+ int nRootSize; // the number of root level assignments
+ int nTrailSize; // the number of assignments made
+ lit * pTrail; // chronological order of assignments (size nVars)
+ lit * pAssigns; // assignments by variable (size nVars)
+ char * pSeens; // temporary mark (size nVars)
+ Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars)
+ Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars)
+ // interpolation data
+ Aig_Man_t * pAig; // the AIG manager for recording the interpolant
+ int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB]
+ Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses)
+ int nIntersAlloc; // the allocated size of truth table array
+ // proof recording
+ int Counter; // counter of resolved clauses
+ int * pProofNums; // the proof numbers for each clause (size nClauses)
+ FILE * pFile; // the file for proof recording
+ // internal verification
+ lit * pResLits; // the literals of the resolvent
+ int nResLits; // the number of literals of the resolvent
+ int nResLitsAlloc;// the number of literals of the resolvent
+ // runtime stats
+ int timeBcp; // the runtime for BCP
+ int timeTrace; // the runtime of trace construction
+ int timeTotal; // the total runtime of interpolation
+};
+
+// procedure to get hold of the clauses' truth table
+static inline Aig_Obj_t ** Inta_ManAigRead( Inta_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; }
+static inline void Inta_ManAigClear( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); }
+static inline void Inta_ManAigFill( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); }
+static inline void Inta_ManAigCopy( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; }
+static inline void Inta_ManAigAnd( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); }
+static inline void Inta_ManAigOr( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); }
+static inline void Inta_ManAigOrNot( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); }
+static inline void Inta_ManAigOrVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); }
+static inline void Inta_ManAigOrNotVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); }
+
+// reading/writing the proof for a clause
+static inline int Inta_ManProofGet( Inta_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; }
+static inline void Inta_ManProofSet( Inta_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocate proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Inta_Man_t * Inta_ManAlloc()
+{
+ Inta_Man_t * p;
+ // allocate the manager
+ p = (Inta_Man_t *)malloc( sizeof(Inta_Man_t) );
+ memset( p, 0, sizeof(Inta_Man_t) );
+ // verification
+ p->nResLitsAlloc = (1<<16);
+ p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+ // parameters
+ p->fProofWrite = 1;
+ p->fProofVerif = 1;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count common variables in the clauses of A and B.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Inta_ManGlobalVars( Inta_Man_t * p )
+{
+ Sto_Cls_t * pClause;
+ int LargeNum = -100000000;
+ int Var, nVarsAB, v;
+
+ // mark the variable encountered in the clauses of A
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ if ( !pClause->fA )
+ break;
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
+ }
+
+ // check variables that appear in clauses of B
+ nVarsAB = 0;
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ if ( pClause->fA )
+ continue;
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ {
+ Var = lit_var(pClause->pLits[v]);
+ if ( p->pVarTypes[Var] == 1 ) // var of A
+ {
+ // change it into a global variable
+ nVarsAB++;
+ p->pVarTypes[Var] = LargeNum;
+ }
+ }
+ }
+ assert( nVarsAB <= Vec_IntSize(p->vVarsAB) );
+
+ // order global variables
+ nVarsAB = 0;
+ Vec_IntForEachEntry( p->vVarsAB, Var, v )
+ p->pVarTypes[Var] = -(1+nVarsAB++);
+
+ // check that there is no extra global variables
+ for ( v = 0; v < p->pCnf->nVars; v++ )
+ assert( p->pVarTypes[v] != LargeNum );
+ return nVarsAB;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resize proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inta_ManResize( Inta_Man_t * p )
+{
+ // check if resizing is needed
+ if ( p->nVarsAlloc < p->pCnf->nVars )
+ {
+ // find the new size
+ if ( p->nVarsAlloc == 0 )
+ p->nVarsAlloc = 1;
+ while ( p->nVarsAlloc < p->pCnf->nVars )
+ p->nVarsAlloc *= 2;
+ // resize the arrays
+ p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc );
+ p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc );
+ p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc );
+ p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc );
+ p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc );
+ p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+ }
+
+ // clean the free space
+ memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
+ memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars );
+ memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars );
+ memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars );
+ memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
+
+ // compute the number of common variables
+ Inta_ManGlobalVars( p );
+
+ // check if resizing of clauses is needed
+ if ( p->nClosAlloc < p->pCnf->nClauses )
+ {
+ // find the new size
+ if ( p->nClosAlloc == 0 )
+ p->nClosAlloc = 1;
+ while ( p->nClosAlloc < p->pCnf->nClauses )
+ p->nClosAlloc *= 2;
+ // resize the arrays
+ p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc );
+ }
+ memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
+
+ // check if resizing of truth tables is needed
+ if ( p->nIntersAlloc < p->pCnf->nClauses )
+ {
+ p->nIntersAlloc = p->pCnf->nClauses;
+ p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc );
+ }
+ memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocate proof manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inta_ManFree( Inta_Man_t * p )
+{
+/*
+ printf( "Runtime stats:\n" );
+PRT( "BCP ", p->timeBcp );
+PRT( "Trace ", p->timeTrace );
+PRT( "TOTAL ", p->timeTotal );
+*/
+ free( p->pInters );
+ free( p->pProofNums );
+ free( p->pTrail );
+ free( p->pAssigns );
+ free( p->pSeens );
+ free( p->pVarTypes );
+ free( p->pReasons );
+ free( p->pWatches );
+ free( p->pResLits );
+ free( p );
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Prints the clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inta_ManPrintClause( Inta_Man_t * p, Sto_Cls_t * pClause )
+{
+ int i;
+ printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Inta_ManProofGet(p, pClause) );
+ for ( i = 0; i < (int)pClause->nLits; i++ )
+ printf( " %d", pClause->pLits[i] );
+ printf( " }\n" );
+}
+
+// Yu Hu
+void Inta_ManPrintClauseEx( lit * pResLits, int nResLits )
+{
+ int i;
+ printf( " {" );
+ for ( i = 0; i < nResLits; i++ )
+ printf( " %d", lit_print(pResLits[i]) );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the resolvent.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inta_ManPrintResolvent( lit * pResLits, int nResLits )
+{
+ int i;
+ printf( "Resolvent: {" );
+ for ( i = 0; i < nResLits; i++ )
+ printf( " %d", lit_print(pResLits[i]) );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the interpolant for one clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inta_ManPrintInterOne( Inta_Man_t * p, Sto_Cls_t * pClause )
+{
+ printf( "Clause %2d : ", pClause->Id );
+// Extra_PrintBinary___( stdout, Inta_ManAigRead(p, pClause), (1 << p->nVarsAB) );
+ printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Adds one clause to the watcher list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Inta_ManWatchClause( Inta_Man_t * p, Sto_Cls_t * pClause, lit Lit )
+{
+ assert( lit_check(Lit, p->pCnf->nVars) );
+ if ( pClause->pLits[0] == Lit )
+ pClause->pNext0 = p->pWatches[lit_neg(Lit)];
+ else
+ {
+ assert( pClause->pLits[1] == Lit );
+ pClause->pNext1 = p->pWatches[lit_neg(Lit)];
+ }
+ p->pWatches[lit_neg(Lit)] = pClause;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Records implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Inta_ManEnqueue( Inta_Man_t * p, lit Lit, Sto_Cls_t * pReason )
+{
+ int Var = lit_var(Lit);
+ if ( p->pAssigns[Var] != LIT_UNDEF )
+ return p->pAssigns[Var] == Lit;
+ p->pAssigns[Var] = Lit;
+ p->pReasons[Var] = pReason;
+ p->pTrail[p->nTrailSize++] = Lit;
+//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Records implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Inta_ManCancelUntil( Inta_Man_t * p, int Level )
+{
+ lit Lit;
+ int i, Var;
+ for ( i = p->nTrailSize - 1; i >= Level; i-- )
+ {
+ Lit = p->pTrail[i];
+ Var = lit_var( Lit );
+ p->pReasons[Var] = NULL;
+ p->pAssigns[Var] = LIT_UNDEF;
+//printf( "cancelling var %d\n", Var );
+ }
+ p->nTrailSize = Level;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate one assignment.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Sto_Cls_t * Inta_ManPropagateOne( Inta_Man_t * p, lit Lit )
+{
+ Sto_Cls_t ** ppPrev, * pCur, * pTemp;
+ lit LitF = lit_neg(Lit);
+ int i;
+ // iterate through the literals
+ ppPrev = p->pWatches + Lit;
+ for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
+ {
+ // make sure the false literal is in the second literal of the clause
+ if ( pCur->pLits[0] == LitF )
+ {
+ pCur->pLits[0] = pCur->pLits[1];
+ pCur->pLits[1] = LitF;
+ pTemp = pCur->pNext0;
+ pCur->pNext0 = pCur->pNext1;
+ pCur->pNext1 = pTemp;
+ }
+ assert( pCur->pLits[1] == LitF );
+
+ // if the first literal is true, the clause is satisfied
+ if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
+ {
+ ppPrev = &pCur->pNext1;
+ continue;
+ }
+
+ // look for a new literal to watch
+ for ( i = 2; i < (int)pCur->nLits; i++ )
+ {
+ // skip the case when the literal is false
+ if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
+ continue;
+ // the literal is either true or unassigned - watch it
+ pCur->pLits[1] = pCur->pLits[i];
+ pCur->pLits[i] = LitF;
+ // remove this clause from the watch list of Lit
+ *ppPrev = pCur->pNext1;
+ // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
+ Inta_ManWatchClause( p, pCur, pCur->pLits[1] );
+ break;
+ }
+ if ( i < (int)pCur->nLits ) // found new watch
+ continue;
+
+ // clause is unit - enqueue new implication
+ if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) )
+ {
+ ppPrev = &pCur->pNext1;
+ continue;
+ }
+
+ // conflict detected - return the conflict clause
+ return pCur;
+ }
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate the current assignments.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start )
+{
+ Sto_Cls_t * pClause;
+ int i;
+ int clk = clock();
+ for ( i = Start; i < p->nTrailSize; i++ )
+ {
+ pClause = Inta_ManPropagateOne( p, p->pTrail[i] );
+ if ( pClause )
+ {
+p->timeBcp += clock() - clk;
+ return pClause;
+ }
+ }
+p->timeBcp += clock() - clk;
+ return NULL;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes one root clause into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inta_ManProofWriteOne( Inta_Man_t * p, Sto_Cls_t * pClause )
+{
+ Inta_ManProofSet( p, pClause, ++p->Counter );
+
+ if ( p->fProofWrite )
+ {
+ int v;
+ fprintf( p->pFile, "%d", Inta_ManProofGet(p, pClause) );
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
+ fprintf( p->pFile, " 0 0\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Traces the proof for one clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal )
+{
+ Sto_Cls_t * pReason;
+ int i, v, Var, PrevId;
+ int fPrint = 1; // Yu Hu
+ int clk = clock();
+
+ // collect resolvent literals
+ if ( p->fProofVerif )
+ {
+ assert( (int)pConflict->nLits <= p->nResLitsAlloc );
+ memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
+ p->nResLits = pConflict->nLits;
+ }
+
+ // mark all the variables in the conflict as seen
+ for ( v = 0; v < (int)pConflict->nLits; v++ )
+ p->pSeens[lit_var(pConflict->pLits[v])] = 1;
+
+ // start the anticedents
+// pFinal->pAntis = Vec_PtrAlloc( 32 );
+// Vec_PtrPush( pFinal->pAntis, pConflict );
+
+ if ( p->pCnf->nClausesA )
+ Inta_ManAigCopy( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pConflict) );
+
+ // follow the trail backwards
+ PrevId = Inta_ManProofGet(p, pConflict);
+ for ( i = p->nTrailSize - 1; i >= 0; i-- )
+ {
+ // skip literals that are not involved
+ Var = lit_var(p->pTrail[i]);
+ if ( !p->pSeens[Var] )
+ continue;
+ p->pSeens[Var] = 0;
+
+ // skip literals of the resulting clause
+ pReason = p->pReasons[Var];
+ if ( pReason == NULL )
+ continue;
+ assert( p->pTrail[i] == pReason->pLits[0] );
+
+ // add the variables to seen
+ for ( v = 1; v < (int)pReason->nLits; v++ )
+ p->pSeens[lit_var(pReason->pLits[v])] = 1;
+
+
+ // record the reason clause
+ assert( Inta_ManProofGet(p, pReason) > 0 );
+ p->Counter++;
+ if ( p->fProofWrite ) {
+ fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) );
+ // Yu Hu
+ printf( "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) );
+ }
+ PrevId = p->Counter;
+
+ if ( p->pCnf->nClausesA )
+ {
+ if ( p->pVarTypes[Var] == 1 ) // var of A
+ Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
+ else
+ Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
+ }
+
+ // resolve the temporary resolvent with the reason clause
+ if ( p->fProofVerif )
+ {
+ int v1, v2;
+ // Yu Hu
+// if ( fPrint )
+// Inta_ManPrintResolvent( p->pResLits, p->nResLits );
+ if ( fPrint ) {
+ printf("pivot = %d,\n", lit_print(p->pTrail[i]));
+ Inta_ManPrintClauseEx( p->pResLits, p->nResLits);
+ }
+
+ // check that the var is present in the resolvent
+ for ( v1 = 0; v1 < p->nResLits; v1++ )
+ if ( lit_var(p->pResLits[v1]) == Var )
+ break;
+ if ( v1 == p->nResLits )
+ printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
+ if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
+ printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
+ // remove this variable from the resolvent
+ assert( lit_var(p->pResLits[v1]) == Var );
+ p->nResLits--;
+ for ( ; v1 < p->nResLits; v1++ )
+ p->pResLits[v1] = p->pResLits[v1+1];
+ // add variables of the reason clause
+ for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
+ {
+ for ( v1 = 0; v1 < p->nResLits; v1++ )
+ if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
+ break;
+ // if it is a new variable, add it to the resolvent
+ if ( v1 == p->nResLits )
+ {
+ if ( p->nResLits == p->nResLitsAlloc )
+ printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id );
+ p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
+ continue;
+ }
+ // if the variable is the same, the literal should be the same too
+ if ( p->pResLits[v1] == pReason->pLits[v2] )
+ continue;
+ // the literal is different
+ printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
+ }
+
+ // Yu Hu
+ if ( fPrint ) {
+ Inta_ManPrintClauseEx( pReason->pLits, pReason->nLits);
+ Inta_ManPrintResolvent( p->pResLits, p->nResLits );
+ }
+ }
+
+// Vec_PtrPush( pFinal->pAntis, pReason );
+ }
+
+ // unmark all seen variables
+// for ( i = p->nTrailSize - 1; i >= 0; i-- )
+// p->pSeens[lit_var(p->pTrail[i])] = 0;
+ // check that the literals are unmarked
+// for ( i = p->nTrailSize - 1; i >= 0; i-- )
+// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
+
+ // use the resulting clause to check the correctness of resolution
+ if ( p->fProofVerif )
+ {
+ int v1, v2;
+ if ( fPrint ){
+ // Yu Hu
+// Inta_ManPrintResolvent( p->pResLits, p->nResLits );
+ }
+ for ( v1 = 0; v1 < p->nResLits; v1++ )
+ {
+ for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
+ if ( pFinal->pLits[v2] == p->pResLits[v1] )
+ break;
+ if ( v2 < (int)pFinal->nLits )
+ continue;
+ break;
+ }
+ if ( v1 < p->nResLits )
+ {
+ printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
+ Inta_ManPrintClause( p, pConflict );
+ Inta_ManPrintResolvent( p->pResLits, p->nResLits );
+ Inta_ManPrintClause( p, pFinal );
+ }
+ }
+p->timeTrace += clock() - clk;
+
+ // return the proof pointer
+ if ( p->pCnf->nClausesA )
+ {
+// Inta_ManPrintInterOne( p, pFinal );
+ }
+ Inta_ManProofSet( p, pFinal, p->Counter );
+ return p->Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Records the proof for one clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause )
+{
+ Sto_Cls_t * pConflict;
+ int i;
+
+ // empty clause never ends up there
+ assert( pClause->nLits > 0 );
+ if ( pClause->nLits == 0 )
+ printf( "Error: Empty clause is attempted.\n" );
+
+ // add assumptions to the trail
+ assert( !pClause->fRoot );
+ assert( p->nTrailSize == p->nRootSize );
+ for ( i = 0; i < (int)pClause->nLits; i++ )
+ if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+ {
+ assert( 0 ); // impossible
+ return 0;
+ }
+
+ // propagate the assumptions
+ pConflict = Inta_ManPropagate( p, p->nRootSize );
+ if ( pConflict == NULL )
+ {
+ assert( 0 ); // cannot prove
+ return 0;
+ }
+
+ // construct the proof
+ Inta_ManProofTraceOne( p, pConflict, pClause );
+
+ // undo to the root level
+ Inta_ManCancelUntil( p, p->nRootSize );
+
+ // add large clauses to the watched lists
+ if ( pClause->nLits > 1 )
+ {
+ Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
+ Inta_ManWatchClause( p, pClause, pClause->pLits[1] );
+ return 1;
+ }
+ assert( pClause->nLits == 1 );
+
+ // if the clause proved is unit, add it and propagate
+ if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
+ {
+ assert( 0 ); // impossible
+ return 0;
+ }
+
+ // propagate the assumption
+ pConflict = Inta_ManPropagate( p, p->nRootSize );
+ if ( pConflict )
+ {
+ // construct the proof
+ Inta_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
+// if ( p->fVerbose )
+// printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
+ return 0;
+ }
+
+ // update the root level
+ p->nRootSize = p->nTrailSize;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagate the root clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Inta_ManProcessRoots( Inta_Man_t * p )
+{
+ Sto_Cls_t * pClause;
+ int Counter;
+
+ // make sure the root clauses are preceeding the learnt clauses
+ Counter = 0;
+ Sto_ManForEachClause( p->pCnf, pClause )
+ {
+ assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) );
+ assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) );
+ Counter++;
+ }
+ assert( p->pCnf->nClauses == Counter );
+
+ // make sure the last clause if empty
+ assert( p->pCnf->pTail->nLits == 0 );
+
+ // go through the root unit clauses
+ p->nTrailSize = 0;
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ // create watcher lists for the root clauses
+ if ( pClause->nLits > 1 )
+ {
+ Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
+ Inta_ManWatchClause( p, pClause, pClause->pLits[1] );
+ }
+ // empty clause and large clauses
+ if ( pClause->nLits != 1 )
+ continue;
+ // unit clause
+ assert( lit_check(pClause->pLits[0], p->pCnf->nVars) );
+ if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
+ {
+ // detected root level conflict
+// printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+// assert( 0 );
+ // detected root level conflict
+ Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+ if ( p->fVerbose )
+ printf( "Found root level conflict!\n" );
+ return 0;
+ }
+ }
+
+ // propagate the root unit clauses
+ pClause = Inta_ManPropagate( p, 0 );
+ if ( pClause )
+ {
+ // detected root level conflict
+ Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+ if ( p->fVerbose )
+ printf( "Found root level conflict!\n" );
+ return 0;
+ }
+
+ // set the root level
+ p->nRootSize = p->nTrailSize;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Records the proof.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inta_ManPrepareInter( Inta_Man_t * p )
+{
+ Sto_Cls_t * pClause;
+ int Var, VarAB, v;
+
+ // set interpolants for root clauses
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ {
+ if ( !pClause->fA ) // clause of B
+ {
+ Inta_ManAigFill( p, Inta_ManAigRead(p, pClause) );
+// Inta_ManPrintInterOne( p, pClause );
+ continue;
+ }
+ // clause of A
+ Inta_ManAigClear( p, Inta_ManAigRead(p, pClause) );
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ {
+ Var = lit_var(pClause->pLits[v]);
+ if ( p->pVarTypes[Var] < 0 ) // global var
+ {
+ VarAB = -p->pVarTypes[Var]-1;
+ assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) );
+ if ( lit_sign(pClause->pLits[v]) ) // negative var
+ Inta_ManAigOrNotVar( p, Inta_ManAigRead(p, pClause), VarAB );
+ else
+ Inta_ManAigOrVar( p, Inta_ManAigRead(p, pClause), VarAB );
+ }
+ }
+// Inta_ManPrintInterOne( p, pClause );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes interpolant for the given CNF.]
+
+ Description [Takes the interpolation manager, the CNF deriving by the SAT
+ solver, which includes ClausesA, ClausesB, and learned clauses. Additional
+ arguments are the vector of variables common to AB and the verbosiness flag.
+ Returns the AIG manager with a single output, containing the interpolant.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
+{
+ Aig_Man_t * pRes;
+ Aig_Obj_t * pObj;
+ Sto_Cls_t * pClause;
+ int RetValue = 1;
+ int clkTotal = clock();
+
+ // check that the CNF makes sense
+ assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
+ p->pCnf = pCnf;
+ p->fVerbose = fVerbose;
+ p->vVarsAB = vVarsAB;
+ p->pAig = pRes = Aig_ManStart( 10000 );
+ Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
+
+ // adjust the manager
+ Inta_ManResize( p );
+
+ // prepare the interpolant computation
+ Inta_ManPrepareInter( p );
+
+ // construct proof for each clause
+ // start the proof
+ if ( p->fProofWrite )
+ {
+ p->pFile = fopen( "proof.cnf_", "w" );
+ p->Counter = 0;
+ }
+
+ // write the root clauses
+ Sto_ManForEachClauseRoot( p->pCnf, pClause )
+ Inta_ManProofWriteOne( p, pClause );
+
+ // propagate root level assignments
+ if ( Inta_ManProcessRoots( p ) )
+ {
+ // if there is no conflict, consider learned clauses
+ Sto_ManForEachClause( p->pCnf, pClause )
+ {
+ if ( pClause->fRoot )
+ continue;
+ if ( !Inta_ManProofRecordOne( p, pClause ) )
+ {
+ RetValue = 0;
+ break;
+ }
+ }
+ }
+
+ // stop the proof
+ if ( p->fProofWrite )
+ {
+ fclose( p->pFile );
+ p->pFile = NULL;
+ }
+
+ if ( fVerbose )
+ {
+// PRT( "Interpo", clock() - clkTotal );
+ printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n",
+ p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
+ 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
+ 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
+p->timeTotal += clock() - clkTotal;
+ }
+
+ pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
+ Aig_ObjCreatePo( pRes, pObj );
+ Aig_ManCleanup( pRes );
+
+ p->pAig = NULL;
+ return pRes;
+
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA )
+{
+ Aig_Man_t * p;
+ Aig_Obj_t * pMiter, * pSum, * pLit;
+ Sto_Cls_t * pClause;
+ int Var, VarAB, v;
+ p = Aig_ManStart( 10000 );
+ pMiter = Aig_ManConst1(p);
+ Sto_ManForEachClauseRoot( pCnf, pClause )
+ {
+ if ( fClausesA ^ pClause->fA ) // clause of B
+ continue;
+ // clause of A
+ pSum = Aig_ManConst0(p);
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ {
+ Var = lit_var(pClause->pLits[v]);
+ if ( pMan->pVarTypes[Var] < 0 ) // global var
+ {
+ VarAB = -pMan->pVarTypes[Var]-1;
+ assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) );
+ pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) );
+ }
+ else
+ pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) );
+ pSum = Aig_Or( p, pSum, pLit );
+ }
+ pMiter = Aig_And( p, pMiter, pSum );
+ }
+ Aig_ObjCreatePo( p, pMiter );
+ return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index 9559b39f..686774fa 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -796,7 +796,7 @@ void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis,
Synopsis [Computes UNSAT core of the satisfiablity problem.]
- Description [Takes the interpolation manager, the CNF deriving by the SAT
+ Description [Takes the interpolation manager, the CNF derived by the SAT
solver, which includes the root clauses and the learned clauses. Returns
the array of integers representing the number of root clauses that are in
the UNSAT core.]
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 08:06:55 +0000