summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw/sswInt.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw/sswInt.h')
-rw-r--r--src/aig/ssw/sswInt.h164
1 files changed, 164 insertions, 0 deletions
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
new file mode 100644
index 00000000..0e54af32
--- /dev/null
+++ b/src/aig/ssw/sswInt.h
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+ FileName [sswInt.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __SSW_INT_H__
+#define __SSW_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "saig.h"
+#include "satSolver.h"
+#include "ssw.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// equivalence classes
+typedef struct Ssw_Cla_t_ Ssw_Cla_t;
+
+// manager
+typedef struct Ssw_Man_t_ Ssw_Man_t;
+struct Ssw_Man_t_
+{
+ // parameters
+ Ssw_Pars_t * pPars; // parameters
+ int nFrames; // for quick lookup
+ // AIGs used in the package
+ Aig_Man_t * pAig; // user-given AIG
+ Aig_Man_t * pFrames; // final AIG
+ Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes
+ int nFrameNodes; // the number of nodes in the timeframes
+ // equivalence classes
+ Ssw_Cla_t * ppClasses; // equivalence classes of nodes
+// Aig_Obj_t ** pReprsProved; // equivalences proved
+ int fRefined; // is set to 1 when refinement happens
+ // SAT solving
+ sat_solver * pSat; // recyclable SAT solver
+ int nSatVars; // the counter of SAT variables
+ int * pSatVars; // mapping of each node into its SAT var
+ Vec_Ptr_t * vFanins; // fanins of the CNF node
+ Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
+ Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
+ // constraints
+ int nConstrTotal; // the number of total constraints
+ int nConstrReduced; // the number of reduced constraints
+ // SAT calls statistics
+ int nSatCalls; // the number of SAT calls
+ int nSatProof; // the number of proofs
+ int nSatFailsReal; // the number of timeouts
+ int nSatCallsUnsat; // the number of unsat SAT calls
+ int nSatCallsSat; // the number of sat SAT calls
+ // runtime stats
+ int timeBmc; // bounded model checking
+ int timeReduce; // speculative reduction
+ int timeSimSat; // simulation of the counter-examples
+ int timeSat; // solving SAT
+ int timeSatSat; // sat
+ int timeSatUnsat; // unsat
+ int timeSatUndec; // undecided
+ int timeOther; // other runtime
+ int timeTotal; // total runtime
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
+static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
+
+static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
+{
+ return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
+}
+static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
+{
+ assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) );
+ Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
+}
+
+static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFraig[p->nFrames*pObj->Id + i]; }
+static inline void Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; }
+
+static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
+static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sswAig.c ===================================================*/
+extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p );
+/*=== sswClass.c =================================================*/
+extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig );
+extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
+ unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
+ int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
+ int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
+extern void Ssw_ClassesStop( Ssw_Cla_t * p );
+extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p );
+extern int Ssw_ClassesClassNum( Ssw_Cla_t * p );
+extern int Ssw_ClassesLitNum( Ssw_Cla_t * p );
+extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
+extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
+extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
+extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
+extern void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs );
+extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
+extern int Ssw_ClassesRefine( Ssw_Cla_t * p );
+extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
+extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
+/*=== sswCnf.c ===================================================*/
+extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
+/*=== sswMan.c ===================================================*/
+extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
+extern void Ssw_ManCleanup( Ssw_Man_t * p );
+extern void Ssw_ManStop( Ssw_Man_t * p );
+extern void Ssw_ManStartSolver( Ssw_Man_t * p );
+/*=== sswSat.c ===================================================*/
+extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+/*=== sswSimSat.c ===================================================*/
+extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
+/*=== sswSweep.c ===================================================*/
+extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
+extern int Ssw_ManSweep( Ssw_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 11:42:14 +0000