1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
/**CFile****************************************************************
FileName [dchMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation of equivalence classes using simulation.]
Synopsis [Calls to the SAT solver.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dchInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates the interpolation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
{
Dch_Man_t * p;
// create interpolation manager
p = ALLOC( Dch_Man_t, 1 );
memset( p, 0, sizeof(Dch_Man_t) );
p->pPars = pPars;
// AIGs
p->vAigs = vAigs;
p->pAigTotal = Dch_DeriveTotalAig( vAigs );
// equivalence classes
Aig_ManReprStart( p->pAigTotal, Aig_ManObjNumMax(p->pAigTotal) );
// SAT solving
p->ppSatVars = CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAigTotal) );
p->vUsedNodes = Vec_PtrAlloc( 1000 );
return p;
}
/**Function*************************************************************
Synopsis [Frees the interpolation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManStop( Dch_Man_t * p )
{
if ( p->pPars->fVerbose )
{
/*
p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
printf( "Runtime statistics:\n" );
PRTP( "Rewriting ", p->timeRwr, p->timeTotal );
PRTP( "CNF mapping", p->timeCnf, p->timeTotal );
PRTP( "SAT solving", p->timeSat, p->timeTotal );
PRTP( "Interpol ", p->timeInt, p->timeTotal );
PRTP( "Containment", p->timeEqu, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
*/
}
if ( p->pAigTotal )
Aig_ManStop( p->pAigTotal );
if ( p->pAigFraig )
Aig_ManStop( p->pAigFraig );
FREE( p->ppClasses );
FREE( p->ppSatVars );
Vec_PtrFree( p->vUsedNodes );
free( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
