1 /**CFile****************************************************************
2 
3   FileName    [intM114.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Interpolation engine.]
8 
9   Synopsis    [Intepolation using ABC's proof generator added to MiniSat-1.14c.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 24, 2008.]
16 
17   Revision    [$Id: intM114.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    [Returns the SAT solver for one interpolation run.]
37 
38   Description [pInter is the previous interpolant. pAig is one time frame.
39   pFrames is the unrolled time frames.]
40 
41   SideEffects []
42 
43   SeeAlso     []
44 
45 ***********************************************************************/
Inter_ManDeriveSatSolver(Aig_Man_t * pInter,Cnf_Dat_t * pCnfInter,Aig_Man_t * pAig,Cnf_Dat_t * pCnfAig,Aig_Man_t * pFrames,Cnf_Dat_t * pCnfFrames,Vec_Int_t * vVarsAB,int fUseBackward)46 sat_solver * Inter_ManDeriveSatSolver(
47     Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter,
48     Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig,
49     Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames,
50     Vec_Int_t * vVarsAB, int fUseBackward )
51 {
52     sat_solver * pSat;
53     Aig_Obj_t * pObj, * pObj2;
54     int i, Lits[2];
55 
56 //Aig_ManDumpBlif( pInter,  "out_inter.blif", NULL, NULL );
57 //Aig_ManDumpBlif( pAig,    "out_aig.blif", NULL, NULL );
58 //Aig_ManDumpBlif( pFrames, "out_frames.blif", NULL, NULL );
59 
60     // sanity checks
61     assert( Aig_ManRegNum(pInter) == 0 );
62     assert( Aig_ManRegNum(pAig) > 0 );
63     assert( Aig_ManRegNum(pFrames) == 0 );
64     assert( Aig_ManCoNum(pInter) == 1 );
65     assert( Aig_ManCoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
66     assert( fUseBackward || Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
67 //    assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
68 
69     // prepare CNFs
70     Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
71     Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
72 
73     // start the solver
74     pSat = sat_solver_new();
75     sat_solver_store_alloc( pSat );
76     sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
77 
78     // add clauses of A
79     // interpolant
80     for ( i = 0; i < pCnfInter->nClauses; i++ )
81     {
82         if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
83         {
84             sat_solver_delete( pSat );
85             // return clauses to the original state
86             Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
87             Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
88             return NULL;
89         }
90     }
91     // connector clauses
92     if ( fUseBackward )
93     {
94         Saig_ManForEachLi( pAig, pObj2, i )
95         {
96             if ( Saig_ManRegNum(pAig) == Aig_ManCiNum(pInter) )
97                 pObj = Aig_ManCi( pInter, i );
98             else
99             {
100                 assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pInter) );
101                 pObj = Aig_ManCi( pInter, Aig_ManCiNum(pAig)-Saig_ManRegNum(pAig) + i );
102             }
103 
104             Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
105             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
106             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
107                 assert( 0 );
108             Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
109             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
110             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
111                 assert( 0 );
112         }
113     }
114     else
115     {
116         Aig_ManForEachCi( pInter, pObj, i )
117         {
118             pObj2 = Saig_ManLo( pAig, i );
119 
120             Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
121             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
122             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
123                 assert( 0 );
124             Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
125             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
126             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
127                 assert( 0 );
128         }
129     }
130     // one timeframe
131     for ( i = 0; i < pCnfAig->nClauses; i++ )
132     {
133         if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
134             assert( 0 );
135     }
136     // connector clauses
137     Vec_IntClear( vVarsAB );
138     if ( fUseBackward )
139     {
140         Aig_ManForEachCo( pFrames, pObj, i )
141         {
142             assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
143             Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
144 
145             pObj2 = Saig_ManLo( pAig, i );
146             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
147             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
148             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
149                 assert( 0 );
150             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
151             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
152             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
153                 assert( 0 );
154         }
155     }
156     else
157     {
158         Aig_ManForEachCi( pFrames, pObj, i )
159         {
160             if ( i == Aig_ManRegNum(pAig) )
161                 break;
162             Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
163 
164             pObj2 = Saig_ManLi( pAig, i );
165             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
166             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
167             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
168                 assert( 0 );
169             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
170             Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
171             if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
172                 assert( 0 );
173         }
174     }
175     // add clauses of B
176     sat_solver_store_mark_clauses_a( pSat );
177     for ( i = 0; i < pCnfFrames->nClauses; i++ )
178     {
179         if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
180         {
181             pSat->fSolved = 1;
182             break;
183         }
184     }
185     sat_solver_store_mark_roots( pSat );
186     // return clauses to the original state
187     Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
188     Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
189     return pSat;
190 }
191 
192 /**Function*************************************************************
193 
194   Synopsis    [Performs one SAT run with interpolation.]
195 
196   Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
197 
198   SideEffects []
199 
200   SeeAlso     []
201 
202 ***********************************************************************/
Inter_ManPerformOneStep(Inter_Man_t * p,int fUseBias,int fUseBackward,abctime nTimeNewOut)203 int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, abctime nTimeNewOut )
204 {
205     sat_solver * pSat;
206     void * pSatCnf = NULL;
207     Inta_Man_t * pManInterA;
208 //    Intb_Man_t * pManInterB;
209     int * pGlobalVars;
210     int status, RetValue;
211     int i, Var;
212     abctime clk;
213 //    assert( p->pInterNew == NULL );
214 
215     // derive the SAT solver
216     pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward );
217     if ( pSat == NULL )
218     {
219         p->pInterNew = NULL;
220         return 1;
221     }
222 
223     // set runtime limit
224     if ( nTimeNewOut )
225         sat_solver_set_runtime_limit( pSat, nTimeNewOut );
226 
227     // collect global variables
228     pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) );
229     Vec_IntForEachEntry( p->vVarsAB, Var, i )
230         pGlobalVars[Var] = 1;
231     pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;
232 
233     // solve the problem
234 clk = Abc_Clock();
235     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
236     p->nConfCur = pSat->stats.conflicts;
237 p->timeSat += Abc_Clock() - clk;
238 
239     pSat->pGlobalVars = NULL;
240     ABC_FREE( pGlobalVars );
241     if ( status == l_False )
242     {
243         pSatCnf = sat_solver_store_release( pSat );
244         RetValue = 1;
245     }
246     else if ( status == l_True )
247     {
248         RetValue = 0;
249     }
250     else
251     {
252         RetValue = -1;
253     }
254     sat_solver_delete( pSat );
255     if ( pSatCnf == NULL )
256         return RetValue;
257 
258     // create the resulting manager
259 clk = Abc_Clock();
260 /*
261     if ( !fUseIp )
262     {
263         pManInterA = Inta_ManAlloc();
264         p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
265         Inta_ManFree( pManInterA );
266     }
267     else
268     {
269         Aig_Man_t * pInterNew2;
270         int RetValue;
271 
272         pManInterA = Inta_ManAlloc();
273         p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
274 //        Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
275         Inta_ManFree( pManInterA );
276 
277         pManInterB = Intb_ManAlloc();
278         pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
279         Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
280         Intb_ManFree( pManInterB );
281 
282         // check relationship
283         RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew );
284         if ( RetValue )
285             printf( "Equivalence \"Ip == Im\" holds\n" );
286         else
287         {
288 //            printf( "Equivalence \"Ip == Im\" does not hold\n" );
289             RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew );
290             if ( RetValue )
291                 printf( "Containment \"Ip -> Im\" holds\n" );
292             else
293                 printf( "Containment \"Ip -> Im\" does not hold\n" );
294 
295             RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 );
296             if ( RetValue )
297                 printf( "Containment \"Im -> Ip\" holds\n" );
298             else
299                 printf( "Containment \"Im -> Ip\" does not hold\n" );
300         }
301 
302         Aig_ManStop( pInterNew2 );
303     }
304 */
305 
306     pManInterA = Inta_ManAlloc();
307     p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, nTimeNewOut, p->vVarsAB, 0 );
308     Inta_ManFree( pManInterA );
309 
310 p->timeInt += Abc_Clock() - clk;
311     Sto_ManFree( (Sto_Man_t *)pSatCnf );
312     if ( p->pInterNew == NULL )
313         RetValue = -1;
314     return RetValue;
315 }
316 
317 ////////////////////////////////////////////////////////////////////////
318 ///                       END OF FILE                                ///
319 ////////////////////////////////////////////////////////////////////////
320 
321 
322 ABC_NAMESPACE_IMPL_END
323 
324