abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
intInter.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [intInter.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Interpolation engine.]
8 
9  Synopsis [Experimental procedures to derive and compare interpolants.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 24, 2008.]
16 
17  Revision [$Id: intInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "intInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis []
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
46 {
47  Aig_Man_t * pInterC;
48  assert( Aig_ManCiNum(pInter) <= Aig_ManCiNum(pOther) );
49  pInterC = Aig_ManDupSimple( pInter );
50  Aig_IthVar( pInterC, Aig_ManCiNum(pOther)-1 );
51  assert( Aig_ManCiNum(pInterC) == Aig_ManCiNum(pOther) );
52  return pInterC;
53 }
54 
55 /**Function*************************************************************
56 
57  Synopsis []
58 
59  Description []
60 
61  SideEffects []
62 
63  SeeAlso []
64 
65 ***********************************************************************/
66 void Inter_ManVerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
67 {
68  extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
69  Aig_Man_t * pLower, * pUpper, * pInterC;
70  int RetValue1, RetValue2;
71 
72  pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 );
73  pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 );
74  Aig_ManFlipFirstPo( pUpper );
75 
76  pInterC = Inter_ManDupExpand( pInter, pLower );
77  RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
78  Aig_ManStop( pInterC );
79 
80  pInterC = Inter_ManDupExpand( pInter, pUpper );
81  RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
82  Aig_ManStop( pInterC );
83 
84  if ( RetValue1 && RetValue2 )
85  printf( "Im is correct.\n" );
86  if ( !RetValue1 )
87  printf( "Property A => Im fails.\n" );
88  if ( !RetValue2 )
89  printf( "Property Im => !B fails.\n" );
90 
91  Aig_ManStop( pLower );
92  Aig_ManStop( pUpper );
93 }
94 
95 /**Function*************************************************************
96 
97  Synopsis []
98 
99  Description []
100 
101  SideEffects []
102 
103  SeeAlso []
104 
105 ***********************************************************************/
106 void Inter_ManVerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
107 {
108  extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
109  Aig_Man_t * pLower, * pUpper, * pInterC;
110  int RetValue1, RetValue2;
111 
112  pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 );
113  pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 );
114  Aig_ManFlipFirstPo( pUpper );
115 
116  pInterC = Inter_ManDupExpand( pInter, pLower );
117 //Aig_ManPrintStats( pLower );
118 //Aig_ManPrintStats( pUpper );
119 //Aig_ManPrintStats( pInterC );
120 //Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL );
121  RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
122  Aig_ManStop( pInterC );
123 
124  pInterC = Inter_ManDupExpand( pInter, pUpper );
125  RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
126  Aig_ManStop( pInterC );
127 
128  if ( RetValue1 && RetValue2 )
129  printf( "Ip is correct.\n" );
130  if ( !RetValue1 )
131  printf( "Property A => Ip fails.\n" );
132  if ( !RetValue2 )
133  printf( "Property Ip => !B fails.\n" );
134 
135  Aig_ManStop( pLower );
136  Aig_ManStop( pUpper );
137 }
138 
139 ////////////////////////////////////////////////////////////////////////
140 /// END OF FILE ///
141 ////////////////////////////////////////////////////////////////////////
142 
143 
144 ABC_NAMESPACE_IMPL_END
145 
Inter_ManVerifyInterpolant1
void Inter_ManVerifyInterpolant1(Inta_Man_t *pMan, Sto_Man_t *pCnf, Aig_Man_t *pInter)
Definition: intInter.c:66
Sto_Man_t_
Definition: satStore.h:82
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Intb_Man_t_
Definition: satInterB.c:40
Inter_Check_t_::pCnf
Cnf_Dat_t * pCnf
Definition: intCheck.c:36
Inter_ManVerifyInterpolant2
void Inter_ManVerifyInterpolant2(Intb_Man_t *pMan, Sto_Man_t *pCnf, Aig_Man_t *pInter)
Definition: intInter.c:106
Aig_ManFlipFirstPo
void Aig_ManFlipFirstPo(Aig_Man_t *p)
Definition: aigMan.c:457
Inta_ManDeriveClauses
Aig_Man_t * Inta_ManDeriveClauses(Inta_Man_t *pMan, Sto_Man_t *pCnf, int fClausesA)
Definition: satInterA.c:1050
Aig_IthVar
Aig_Obj_t * Aig_IthVar(Aig_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition: aigOper.c:63
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Intb_ManDeriveClauses
Aig_Man_t * Intb_ManDeriveClauses(Intb_Man_t *pMan, Sto_Man_t *pCnf, int fClausesA)
Definition: satInterB.c:1076
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Inter_ManDupExpand
ABC_NAMESPACE_IMPL_START Aig_Man_t * Inter_ManDupExpand(Aig_Man_t *pInter, Aig_Man_t *pOther)
DECLARATIONS ///.
Definition: intInter.c:45
Inta_Man_t_
Definition: satInterA.c:40
assert
#define assert(ex)
Definition: util_old.h:213
Inter_ManCheckContainment
int Inter_ManCheckContainment(Aig_Man_t *pNew, Aig_Man_t *pOld)
FUNCTION DEFINITIONS ///.
Definition: intContain.c:47
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigDup.c:46