1 /**CFile****************************************************************
2 
3   FileName    [pdrSat.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Property driven reachability.]
8 
9   Synopsis    [SAT solver procedures.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - November 20, 2010.]
16 
17   Revision    [$Id: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "pdrInt.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    [Creates new SAT solver.]
37 
38   Description []
39 
40   SideEffects []
41 
42   SeeAlso     []
43 
44 ***********************************************************************/
Pdr_ManCreateSolver(Pdr_Man_t * p,int k)45 sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
46 {
47     sat_solver * pSat;
48     Aig_Obj_t * pObj;
49     int i;
50     assert( Vec_PtrSize(p->vSolvers) == k );
51     assert( Vec_VecSize(p->vClauses) == k );
52     assert( Vec_IntSize(p->vActVars) == k );
53     // create new solver
54 //    pSat = sat_solver_new();
55     pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
56     pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
57     Vec_PtrPush( p->vSolvers, pSat );
58     Vec_VecExpand( p->vClauses, k );
59     Vec_IntPush( p->vActVars, 0 );
60     // add property cone
61     Saig_ManForEachPo( p->pAig, pObj, i )
62         Pdr_ObjSatVar( p, k, 1, pObj );
63     return pSat;
64 }
65 
66 /**Function*************************************************************
67 
68   Synopsis    [Returns old or restarted solver.]
69 
70   Description []
71 
72   SideEffects []
73 
74   SeeAlso     []
75 
76 ***********************************************************************/
Pdr_ManFetchSolver(Pdr_Man_t * p,int k)77 sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
78 {
79     sat_solver * pSat;
80     Vec_Ptr_t * vArrayK;
81     Pdr_Set_t * pCube;
82     int i, j;
83     pSat = Pdr_ManSolver(p, k);
84     if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
85         return pSat;
86     assert( k < Vec_PtrSize(p->vSolvers) - 1 );
87     p->nStarts++;
88 //    sat_solver_delete( pSat );
89 //    pSat = sat_solver_new();
90 //    sat_solver_restart( pSat );
91     zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed );
92     // create new SAT solver
93     pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
94     // write new SAT solver
95     Vec_PtrWriteEntry( p->vSolvers, k, pSat );
96     Vec_IntWriteEntry( p->vActVars, k, 0 );
97     // set the property output
98     Pdr_ManSetPropertyOutput( p, k );
99     // add the clauses
100     Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
101         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
102             Pdr_ManSolverAddClause( p, k, pCube );
103     return pSat;
104 }
105 
106 /**Function*************************************************************
107 
108   Synopsis    [Converts SAT variables into register IDs.]
109 
110   Description []
111 
112   SideEffects []
113 
114   SeeAlso     []
115 
116 ***********************************************************************/
Pdr_ManLitsToCube(Pdr_Man_t * p,int k,int * pArray,int nArray)117 Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
118 {
119     int i, RegId;
120     Vec_IntClear( p->vLits );
121     for ( i = 0; i < nArray; i++ )
122     {
123         RegId = Pdr_ObjRegNum( p, k, Abc_Lit2Var(pArray[i]) );
124         if ( RegId == -1 )
125             continue;
126         assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
127         Vec_IntPush( p->vLits, Abc_Var2Lit(RegId, !Abc_LitIsCompl(pArray[i])) );
128     }
129     assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
130     return p->vLits;
131 }
132 
133 /**Function*************************************************************
134 
135   Synopsis    [Converts the cube in terms of RO numbers into array of CNF literals.]
136 
137   Description []
138 
139   SideEffects []
140 
141   SeeAlso     []
142 
143 ***********************************************************************/
Pdr_ManCubeToLits(Pdr_Man_t * p,int k,Pdr_Set_t * pCube,int fCompl,int fNext)144 Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )
145 {
146     Aig_Obj_t * pObj;
147     int i, iVar, iVarMax = 0;
148     abctime clk = Abc_Clock();
149     Vec_IntClear( p->vLits );
150 //    assert( !(fNext && fCompl) );
151     for ( i = 0; i < pCube->nLits; i++ )
152     {
153         if ( pCube->Lits[i] == -1 )
154             continue;
155         if ( fNext )
156             pObj = Saig_ManLi( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
157         else
158             pObj = Saig_ManLo( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
159         iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - Abc_LitIsCompl(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
160         iVarMax = Abc_MaxInt( iVarMax, iVar );
161         Vec_IntPush( p->vLits, Abc_Var2Lit( iVar, fCompl ^ Abc_LitIsCompl(pCube->Lits[i]) ) );
162     }
163 //    sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
164     p->tCnf += Abc_Clock() - clk;
165     return p->vLits;
166 }
167 
168 /**Function*************************************************************
169 
170   Synopsis    [Sets the property output to 0 (sat) forever.]
171 
172   Description []
173 
174   SideEffects []
175 
176   SeeAlso     []
177 
178 ***********************************************************************/
Pdr_ManSetPropertyOutput(Pdr_Man_t * p,int k)179 void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
180 {
181     sat_solver * pSat;
182     Aig_Obj_t * pObj;
183     int Lit, RetValue, i;
184     if ( !p->pPars->fUsePropOut )
185         return;
186     pSat = Pdr_ManSolver(p, k);
187     Saig_ManForEachPo( p->pAig, pObj, i )
188     {
189         // skip solved outputs
190         if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
191             continue;
192         // skip timedout outputs
193         if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
194             continue;
195         Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
196         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
197         assert( RetValue == 1 );
198     }
199     sat_solver_compress( pSat );
200 }
201 
202 /**Function*************************************************************
203 
204   Synopsis    [Adds one clause in terms of ROs to the k-th SAT solver.]
205 
206   Description []
207 
208   SideEffects []
209 
210   SeeAlso     []
211 
212 ***********************************************************************/
Pdr_ManSolverAddClause(Pdr_Man_t * p,int k,Pdr_Set_t * pCube)213 void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
214 {
215     sat_solver * pSat;
216     Vec_Int_t * vLits;
217     int RetValue;
218     pSat  = Pdr_ManSolver(p, k);
219     vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
220     RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
221     assert( RetValue == 1 );
222     sat_solver_compress( pSat );
223 }
224 
225 /**Function*************************************************************
226 
227   Synopsis    [Collects values of the RO/RI variables in k-th SAT solver.]
228 
229   Description []
230 
231   SideEffects []
232 
233   SeeAlso     []
234 
235 ***********************************************************************/
Pdr_ManCollectValues(Pdr_Man_t * p,int k,Vec_Int_t * vObjIds,Vec_Int_t * vValues)236 void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )
237 {
238     sat_solver * pSat;
239     Aig_Obj_t * pObj;
240     int iVar, i;
241     Vec_IntClear( vValues );
242     pSat = Pdr_ManSolver(p, k);
243     Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
244     {
245         iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
246         Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
247     }
248 }
249 
250 /**Function*************************************************************
251 
252   Synopsis    [Checks if the cube holds (UNSAT) in the given timeframe.]
253 
254   Description [Return 1/0 if cube or property are proved to hold/fail
255   in k-th timeframe.  Returns the predecessor bad state in ppPred.]
256 
257   SideEffects []
258 
259   SeeAlso     []
260 
261 ***********************************************************************/
Pdr_ManCheckCubeCs(Pdr_Man_t * p,int k,Pdr_Set_t * pCube)262 int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
263 {
264     sat_solver * pSat;
265     Vec_Int_t * vLits;
266     abctime Limit;
267     int RetValue;
268     pSat = Pdr_ManFetchSolver( p, k );
269     vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
270     Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
271     RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
272     sat_solver_set_runtime_limit( pSat, Limit );
273     if ( RetValue == l_Undef )
274         return -1;
275     return (RetValue == l_False);
276 }
277 
278 /**Function*************************************************************
279 
280   Synopsis    [Checks if the cube holds (UNSAT) in the given timeframe.]
281 
282   Description [Return 1/0 if cube or property are proved to hold/fail
283   in k-th timeframe.  Returns the predecessor bad state in ppPred.]
284 
285   SideEffects []
286 
287   SeeAlso     []
288 
289 ***********************************************************************/
Pdr_ManCheckCube(Pdr_Man_t * p,int k,Pdr_Set_t * pCube,Pdr_Set_t ** ppPred,int nConfLimit,int fTryConf,int fUseLit)290 int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit )
291 {
292     //int fUseLit = 0;
293     int fLitUsed = 0;
294     sat_solver * pSat;
295     Vec_Int_t * vLits;
296     int Lit, RetValue;
297     abctime clk, Limit;
298     p->nCalls++;
299     pSat = Pdr_ManFetchSolver( p, k );
300     if ( pCube == NULL ) // solve the property
301     {
302         clk = Abc_Clock();
303         Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
304         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
305         RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
306         sat_solver_set_runtime_limit( pSat, Limit );
307         if ( RetValue == l_Undef )
308             return -1;
309     }
310     else // check relative containment in terms of next states
311     {
312         if ( fUseLit )
313         {
314             fLitUsed = 1;
315             Vec_IntAddToEntry( p->vActVars, k, 1 );
316             // add the cube in terms of current state variables
317             vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
318             // add activation literal
319             Lit = Abc_Var2Lit( Pdr_ManFreeVar(p, k), 0 );
320             // add activation literal
321             Vec_IntPush( vLits, Lit );
322             RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
323             assert( RetValue == 1 );
324             sat_solver_compress( pSat );
325             // create assumptions
326             vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
327             // add activation literal
328             Vec_IntPush( vLits, Abc_LitNot(Lit) );
329         }
330         else
331             vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
332 
333         // solve
334         clk = Abc_Clock();
335         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
336         RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 );
337         sat_solver_set_runtime_limit( pSat, Limit );
338         if ( RetValue == l_Undef )
339         {
340             if ( fTryConf && p->pPars->nConfGenLimit )
341                 RetValue = l_True;
342             else
343                 return -1;
344         }
345     }
346     clk = Abc_Clock() - clk;
347     p->tSat += clk;
348     assert( RetValue != l_Undef );
349     if ( RetValue == l_False )
350     {
351         p->tSatUnsat += clk;
352         p->nCallsU++;
353         if ( ppPred )
354             *ppPred = NULL;
355         RetValue = 1;
356     }
357     else // if ( RetValue == l_True )
358     {
359         p->tSatSat += clk;
360         p->nCallsS++;
361         if ( ppPred )
362         {
363             abctime clk = Abc_Clock();
364             if ( p->pPars->fNewXSim )
365                 *ppPred = Txs3_ManTernarySim( p->pTxs3, k, pCube );
366             else
367                 *ppPred = Pdr_ManTernarySim( p, k, pCube );
368             p->tTsim += Abc_Clock() - clk;
369             p->nXsimLits += (*ppPred)->nLits;
370             p->nXsimRuns++;
371         }
372         RetValue = 0;
373     }
374 
375 /* // for some reason, it does not work...
376     if ( fLitUsed )
377     {
378         int RetValue;
379         Lit = Abc_LitNot(Lit);
380         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
381         assert( RetValue == 1 );
382         sat_solver_compress( pSat );
383     }
384 */
385     return RetValue;
386 }
387 
388 
389 ////////////////////////////////////////////////////////////////////////
390 ///                       END OF FILE                                ///
391 ////////////////////////////////////////////////////////////////////////
392 
393 
394 ABC_NAMESPACE_IMPL_END
395 
396