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