1 /**CFile****************************************************************
2
3 FileName [abcQbf.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Implementation of a simple QBF solver.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcQbf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "sat/cnf/cnf.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 /*
28 Implementation of a simple QBF solver along the lines of
29 A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia,
30 "Combinatorial sketching for finite programs", 12th International
31 Conference on Architectural Support for Programming Languages and
32 Operating Systems (ASPLOS 2006), San Jose, CA, October 2006.
33 */
34
35 ////////////////////////////////////////////////////////////////////////
36 /// DECLARATIONS ///
37 ////////////////////////////////////////////////////////////////////////
38
39 static void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
40 static void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars );
41 static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
42 static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
43 static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
44
45 extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
46
47 ////////////////////////////////////////////////////////////////////////
48 /// FUNCTION DEFINITIONS ///
49 ////////////////////////////////////////////////////////////////////////
50
51 /**Function*************************************************************
52
53 Synopsis [Solve the QBF problem EpAx[M(p,x)].]
54
55 Description [Variables p go first, followed by variable x.
56 The number of parameters is nPars. The miter is in pNtk.
57 The miter expresses EQUALITY of the implementation and spec.]
58
59 SideEffects []
60
61 SeeAlso []
62
63 ***********************************************************************/
Abc_NtkQbf(Abc_Ntk_t * pNtk,int nPars,int nItersMax,int fDumpCnf,int fVerbose)64 void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fDumpCnf, int fVerbose )
65 {
66 Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
67 Vec_Int_t * vPiValues;
68 abctime clkTotal = Abc_Clock(), clkS, clkV;
69 int nIters, nInputs, RetValue, fFound = 0;
70
71 assert( Abc_NtkIsStrash(pNtk) );
72 assert( Abc_NtkIsComb(pNtk) );
73 assert( Abc_NtkPoNum(pNtk) == 1 );
74 assert( nPars > 0 && nPars < Abc_NtkPiNum(pNtk) );
75 // assert( Abc_NtkPiNum(pNtk)-nPars < 32 );
76 nInputs = Abc_NtkPiNum(pNtk) - nPars;
77
78 if ( fDumpCnf )
79 {
80 // original problem: \exists p \forall x \exists y. M(p,x,y)
81 // negated problem: \forall p \exists x \exists y. !M(p,x,y)
82 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
83 Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 0 );
84 Cnf_Dat_t * pCnf = Cnf_Derive( pMan, 0 );
85 Vec_Int_t * vVarMap, * vForAlls, * vExists;
86 Aig_Obj_t * pObj;
87 char * pFileName;
88 int i, Entry;
89 // create var map
90 vVarMap = Vec_IntStart( pCnf->nVars );
91 Aig_ManForEachCi( pMan, pObj, i )
92 if ( i < nPars )
93 Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
94 // create various maps
95 vForAlls = Vec_IntAlloc( nPars );
96 vExists = Vec_IntAlloc( Abc_NtkPiNum(pNtk) - nPars );
97 Vec_IntForEachEntry( vVarMap, Entry, i )
98 if ( Entry )
99 Vec_IntPush( vForAlls, i );
100 else
101 Vec_IntPush( vExists, i );
102 // generate CNF
103 pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".qdimacs" );
104 Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists );
105 Aig_ManStop( pMan );
106 Cnf_DataFree( pCnf );
107 Vec_IntFree( vForAlls );
108 Vec_IntFree( vExists );
109 Vec_IntFree( vVarMap );
110 printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
111 return;
112 }
113
114 // initialize the synthesized network with 0000-combination
115 vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );
116
117 // create random init value
118 {
119 int i;
120 srand( time(NULL) );
121 for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
122 Vec_IntWriteEntry( vPiValues, i, rand() & 1 );
123 }
124
125 Abc_NtkVectorClearPars( vPiValues, nPars );
126 pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues );
127 if ( fVerbose )
128 {
129 printf( "Iter %2d : ", 0 );
130 printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
131 Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
132 printf( "\n" );
133 }
134
135 // iteratively solve
136 for ( nIters = 0; nIters < nItersMax; nIters++ )
137 {
138 // solve the synthesis instance
139 clkS = Abc_Clock();
140 // RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
141 RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
142 clkS = Abc_Clock() - clkS;
143 if ( RetValue == 0 )
144 Abc_NtkModelToVector( pNtkSyn, vPiValues );
145 if ( RetValue == 1 )
146 {
147 break;
148 }
149 if ( RetValue == -1 )
150 {
151 printf( "Synthesis timed out.\n" );
152 break;
153 }
154 // there is a counter-example
155
156 // construct the verification instance
157 Abc_NtkVectorClearVars( pNtk, vPiValues, nPars );
158 pNtkVer = Abc_NtkMiterCofactor( pNtk, vPiValues );
159 // complement the output
160 Abc_ObjXorFaninC( Abc_NtkPo(pNtkVer,0), 0 );
161
162 // solve the verification instance
163 clkV = Abc_Clock();
164 RetValue = Abc_NtkMiterSat( pNtkVer, 0, 0, 0, NULL, NULL );
165 clkV = Abc_Clock() - clkV;
166 if ( RetValue == 0 )
167 Abc_NtkModelToVector( pNtkVer, vPiValues );
168 Abc_NtkDelete( pNtkVer );
169 if ( RetValue == 1 )
170 {
171 fFound = 1;
172 break;
173 }
174 if ( RetValue == -1 )
175 {
176 printf( "Verification timed out.\n" );
177 break;
178 }
179 // there is a counter-example
180
181 // create a new synthesis network
182 Abc_NtkVectorClearPars( vPiValues, nPars );
183 pNtkSyn2 = Abc_NtkMiterCofactor( pNtk, vPiValues );
184 // add to the synthesis instance
185 pNtkSyn = Abc_NtkMiterAnd( pNtkTemp = pNtkSyn, pNtkSyn2, 0, 0 );
186 Abc_NtkDelete( pNtkSyn2 );
187 Abc_NtkDelete( pNtkTemp );
188
189 if ( fVerbose )
190 {
191 printf( "Iter %2d : ", nIters+1 );
192 printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
193 Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
194 printf( " " );
195 ABC_PRT( "Syn", clkS );
196 // ABC_PRT( "Ver", clkV );
197 }
198 }
199 Abc_NtkDelete( pNtkSyn );
200 // report the results
201 if ( fFound )
202 {
203 int nZeros = Vec_IntCountZero( vPiValues );
204 printf( "Parameters: " );
205 Abc_NtkVectorPrintPars( vPiValues, nPars );
206 printf( " Statistics: 0=%d 1=%d\n", nZeros, Vec_IntSize(vPiValues) - nZeros );
207 printf( "Solved after %d iterations. ", nIters );
208 }
209 else if ( nIters == nItersMax )
210 printf( "Quit after %d iterations. ", nItersMax );
211 else
212 printf( "Implementation does not exist. " );
213 ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
214 Vec_IntFree( vPiValues );
215 }
216
217
218 /**Function*************************************************************
219
220 Synopsis [Translates model into the vector of values.]
221
222 Description []
223
224 SideEffects []
225
226 SeeAlso []
227
228 ***********************************************************************/
Abc_NtkModelToVector(Abc_Ntk_t * pNtk,Vec_Int_t * vPiValues)229 void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
230 {
231 int * pModel, i;
232 pModel = pNtk->pModel;
233 for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )
234 Vec_IntWriteEntry( vPiValues, i, pModel[i] );
235 }
236
237 /**Function*************************************************************
238
239 Synopsis [Clears parameters.]
240
241 Description []
242
243 SideEffects []
244
245 SeeAlso []
246
247 ***********************************************************************/
Abc_NtkVectorClearPars(Vec_Int_t * vPiValues,int nPars)248 void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars )
249 {
250 int i;
251 for ( i = 0; i < nPars; i++ )
252 Vec_IntWriteEntry( vPiValues, i, -1 );
253 }
254
255 /**Function*************************************************************
256
257 Synopsis [Clears variables.]
258
259 Description []
260
261 SideEffects []
262
263 SeeAlso []
264
265 ***********************************************************************/
Abc_NtkVectorClearVars(Abc_Ntk_t * pNtk,Vec_Int_t * vPiValues,int nPars)266 void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
267 {
268 int i;
269 for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
270 Vec_IntWriteEntry( vPiValues, i, -1 );
271 }
272
273 /**Function*************************************************************
274
275 Synopsis [Clears variables.]
276
277 Description []
278
279 SideEffects []
280
281 SeeAlso []
282
283 ***********************************************************************/
Abc_NtkVectorPrintPars(Vec_Int_t * vPiValues,int nPars)284 void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars )
285 {
286 int i;
287 for ( i = 0; i < nPars; i++ )
288 printf( "%d", Vec_IntEntry(vPiValues,i) );
289 }
290
291 /**Function*************************************************************
292
293 Synopsis [Clears variables.]
294
295 Description []
296
297 SideEffects []
298
299 SeeAlso []
300
301 ***********************************************************************/
Abc_NtkVectorPrintVars(Abc_Ntk_t * pNtk,Vec_Int_t * vPiValues,int nPars)302 void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
303 {
304 int i;
305 for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
306 printf( "%d", Vec_IntEntry(vPiValues,i) );
307 }
308
309 ////////////////////////////////////////////////////////////////////////
310 /// END OF FILE ///
311 ////////////////////////////////////////////////////////////////////////
312
313
314 ABC_NAMESPACE_IMPL_END
315
316