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 ***********************************************************************/
Inter_ManDupExpand(Aig_Man_t * pInter,Aig_Man_t * pOther)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 ***********************************************************************/
Inter_ManVerifyInterpolant1(Inta_Man_t * pMan,Sto_Man_t * pCnf,Aig_Man_t * pInter)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 ***********************************************************************/
Inter_ManVerifyInterpolant2(Intb_Man_t * pMan,Sto_Man_t * pCnf,Aig_Man_t * pInter)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
146