abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sswMan.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sswMan.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Inductive prover with constraints.]
8 
9  Synopsis [Calls to the SAT solver.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - September 1, 2008.]
16 
17  Revision [$Id: sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Creates the manager.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
46 {
47  Ssw_Man_t * p;
48  // prepare the sequential AIG
49  assert( Saig_ManRegNum(pAig) > 0 );
50  Aig_ManFanoutStart( pAig );
51  Aig_ManSetCioIds( pAig );
52  // create interpolation manager
53  p = ABC_ALLOC( Ssw_Man_t, 1 );
54  memset( p, 0, sizeof(Ssw_Man_t) );
55  p->pPars = pPars;
56  p->pAig = pAig;
57  p->nFrames = pPars->nFramesK + 1;
58  p->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
59  p->vCommon = Vec_PtrAlloc( 100 );
60  p->iOutputLit = -1;
61  // allocate storage for sim pattern
62  p->nPatWords = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
63  p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords );
64  // other
65  p->vNewLos = Vec_PtrAlloc( 100 );
66  p->vNewPos = Vec_IntAlloc( 100 );
67  p->vResimConsts = Vec_PtrAlloc( 100 );
68  p->vResimClasses = Vec_PtrAlloc( 100 );
69 // p->pPars->fVerbose = 1;
70  return p;
71 }
72 
73 /**Function*************************************************************
74 
75  Synopsis [Prints stats of the manager.]
76 
77  Description []
78 
79  SideEffects []
80 
81  SeeAlso []
82 
83 ***********************************************************************/
85 {
86  Aig_Obj_t * pObj;
87  int i, nEquivs = 0;
88  Aig_ManForEachObj( p->pAig, pObj, i )
89  nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL );
90  return nEquivs;
91 }
92 
93 /**Function*************************************************************
94 
95  Synopsis [Prints stats of the manager.]
96 
97  Description []
98 
99  SideEffects []
100 
101  SeeAlso []
102 
103 ***********************************************************************/
105 {
106  double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
107 
108  Abc_Print( 1, "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f MB.\n",
109  p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, Saig_ManConstrNum(p->pAig), p->pPars->nMaxLevs, nMemory );
110  Abc_Print( 1, "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
111  Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
112  0/(p->pPars->nIters+1) );
113  Abc_Print( 1, "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
114  p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) );
115  Abc_Print( 1, "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n",
116  p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds );
117  Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
118  p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
119  p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
120 
121  p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
122  ABC_PRTP( "BMC ", p->timeBmc, p->timeTotal );
123  ABC_PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
124  ABC_PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
125  ABC_PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
126  ABC_PRTP( "SAT solving", p->timeSat, p->timeTotal );
127  ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
128  ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal );
129  ABC_PRTP( " undecided", p->timeSatUndec, p->timeTotal );
130  ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
131  ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
132 
133  // report the reductions
134  if ( p->pAig->nConstrs )
135  {
136  Abc_Print( 1, "Statistics reflecting the use of constraints:\n" );
137  Abc_Print( 1, "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n",
138  p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal );
139  Abc_Print( 1, "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n",
140  p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal );
141  Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
142  p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1),
143  p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) );
144  }
145 }
146 
147 /**Function*************************************************************
148 
149  Synopsis [Frees the manager.]
150 
151  Description []
152 
153  SideEffects []
154 
155  SeeAlso []
156 
157 ***********************************************************************/
159 {
160 // Aig_ManCleanMarkAB( p->pAig );
161  assert( p->pMSat == NULL );
162  if ( p->pFrames )
163  {
164  Aig_ManCleanMarkAB( p->pFrames );
165  Aig_ManStop( p->pFrames );
166  p->pFrames = NULL;
167  memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
168  }
169  if ( p->vSimInfo )
170  {
171  Vec_PtrFree( p->vSimInfo );
172  p->vSimInfo = NULL;
173  }
174  p->nConstrTotal = 0;
175  p->nConstrReduced = 0;
176 }
177 
178 /**Function*************************************************************
179 
180  Synopsis [Frees the manager.]
181 
182  Description []
183 
184  SideEffects []
185 
186  SeeAlso []
187 
188 ***********************************************************************/
190 {
191  ABC_FREE( p->pVisited );
192  if ( p->pPars->fVerbose )//&& p->pPars->nStepsMax == -1 )
193  Ssw_ManPrintStats( p );
194  if ( p->ppClasses )
195  Ssw_ClassesStop( p->ppClasses );
196  if ( p->pSml )
197  Ssw_SmlStop( p->pSml );
198  if ( p->vDiffPairs )
199  Vec_IntFree( p->vDiffPairs );
200  if ( p->vInits )
201  Vec_IntFree( p->vInits );
202  Vec_PtrFree( p->vResimConsts );
203  Vec_PtrFree( p->vResimClasses );
204  Vec_PtrFree( p->vNewLos );
205  Vec_IntFree( p->vNewPos );
206  Vec_PtrFree( p->vCommon );
207  ABC_FREE( p->pNodeToFrames );
208  ABC_FREE( p->pPatWords );
209  ABC_FREE( p );
210 }
211 
212 ////////////////////////////////////////////////////////////////////////
213 /// END OF FILE ///
214 ////////////////////////////////////////////////////////////////////////
215 
216 
char * memset()
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:330
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
typedefABC_NAMESPACE_HEADER_START struct Ssw_Pars_t_ Ssw_Pars_t
INCLUDES ///.
Definition: ssw.h:40
void Ssw_ManPrintStats(Ssw_Man_t *p)
Definition: sswMan.c:104
void Ssw_ClassesStop(Ssw_Cla_t *p)
Definition: sswClass.c:189
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t
INCLUDES ///.
Definition: sswInt.h:47
ABC_NAMESPACE_IMPL_START Ssw_Man_t * Ssw_ManCreate(Aig_Man_t *pAig, Ssw_Pars_t *pPars)
DECLARATIONS ///.
Definition: sswMan.c:45
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: aigFanout.c:56
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
static int Saig_ManConstrNum(Aig_Man_t *p)
Definition: saig.h:78
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Ssw_ManStop(Ssw_Man_t *p)
Definition: sswMan.c:189
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Definition: aig.h:69
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition: aigUtil.c:965
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
void Ssw_SmlStop(Ssw_Sml_t *p)
Definition: sswSim.c:1211
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition: aigUtil.c:186
#define ABC_FREE(obj)
Definition: abc_global.h:232
void Ssw_ManCleanup(Ssw_Man_t *p)
Definition: sswMan.c:158
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
int Ssw_ManCountEquivs(Ssw_Man_t *p)
Definition: sswMan.c:84
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223