1 /**CFile****************************************************************
2 
3   FileName    [sswSat.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Inductive prover with constraints.]
8 
9   Synopsis    [Calls to the SAT solver.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - September 1, 2008.]
16 
17   Revision    [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.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    [Runs equivalence test for the two nodes.]
37 
38   Description [Both nodes should be regular and different from each other.]
39 
40   SideEffects []
41 
42   SeeAlso     []
43 
44 ***********************************************************************/
Ssw_NodesAreEquiv(Ssw_Man_t * p,Aig_Obj_t * pOld,Aig_Obj_t * pNew)45 int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
46 {
47     int nBTLimit = p->pPars->nBTLimit;
48     int pLits[3], nLits, RetValue, RetValue1;
49     abctime clk;//, status;
50     p->nSatCalls++;
51     p->pMSat->nSolverCalls++;
52 
53     // sanity checks
54     assert( !Aig_IsComplement(pOld) );
55     assert( !Aig_IsComplement(pNew) );
56     assert( pOld != pNew );
57     assert( p->pMSat != NULL );
58 
59     // if the nodes do not have SAT variables, allocate them
60     Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
61     Ssw_CnfNodeAddToSolver( p->pMSat, pNew );
62 
63     // solve under assumptions
64     // A = 1; B = 0     OR     A = 1; B = 1
65     nLits = 2;
66     pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
67     pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase == pNew->fPhase );
68     if ( p->iOutputLit > -1 )
69         pLits[nLits++] = p->iOutputLit;
70     if ( p->pPars->fPolarFlip )
71     {
72         if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
73         if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
74     }
75 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
76 
77     if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
78     {
79         RetValue = sat_solver_simplify(p->pMSat->pSat);
80         //assert( RetValue != 0 );
81     }
82 
83 clk = Abc_Clock();
84     RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
85         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
86 p->timeSat += Abc_Clock() - clk;
87     if ( RetValue1 == l_False )
88     {
89 p->timeSatUnsat += Abc_Clock() - clk;
90         if ( nLits == 2 )
91         {
92             pLits[0] = lit_neg( pLits[0] );
93             pLits[1] = lit_neg( pLits[1] );
94             RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
95             assert( RetValue );
96 /*
97             if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
98             {
99                 RetValue = sat_solver_simplify(p->pMSat->pSat);
100                 assert( RetValue != 0 );
101             }
102 */
103         }
104         p->nSatCallsUnsat++;
105     }
106     else if ( RetValue1 == l_True )
107     {
108 p->timeSatSat += Abc_Clock() - clk;
109         p->nSatCallsSat++;
110         return 0;
111     }
112     else // if ( RetValue1 == l_Undef )
113     {
114 p->timeSatUndec += Abc_Clock() - clk;
115         p->nSatFailsReal++;
116         return -1;
117     }
118 
119     // if the old node was constant 0, we already know the answer
120     if ( pOld == Aig_ManConst1(p->pFrames) )
121     {
122         p->nSatProof++;
123         return 1;
124     }
125 
126     // solve under assumptions
127     // A = 0; B = 1     OR     A = 0; B = 0
128     nLits = 2;
129     pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
130     pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase );
131     if ( p->iOutputLit > -1 )
132         pLits[nLits++] = p->iOutputLit;
133     if ( p->pPars->fPolarFlip )
134     {
135         if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
136         if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
137     }
138 
139     if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
140     {
141         RetValue = sat_solver_simplify(p->pMSat->pSat);
142         //assert( RetValue != 0 );
143     }
144 
145 clk = Abc_Clock();
146     RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
147         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
148 p->timeSat += Abc_Clock() - clk;
149     if ( RetValue1 == l_False )
150     {
151 p->timeSatUnsat += Abc_Clock() - clk;
152         if ( nLits == 2 )
153         {
154             pLits[0] = lit_neg( pLits[0] );
155             pLits[1] = lit_neg( pLits[1] );
156             RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
157             assert( RetValue );
158 /*
159             if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
160             {
161                 RetValue = sat_solver_simplify(p->pMSat->pSat);
162                 assert( RetValue != 0 );
163             }
164 */
165         }
166         p->nSatCallsUnsat++;
167     }
168     else if ( RetValue1 == l_True )
169     {
170 p->timeSatSat += Abc_Clock() - clk;
171         p->nSatCallsSat++;
172         return 0;
173     }
174     else // if ( RetValue1 == l_Undef )
175     {
176 p->timeSatUndec += Abc_Clock() - clk;
177         p->nSatFailsReal++;
178         return -1;
179     }
180     // return SAT proof
181     p->nSatProof++;
182     return 1;
183 }
184 
185 /**Function*************************************************************
186 
187   Synopsis    [Constrains two nodes to be equivalent in the SAT solver.]
188 
189   Description []
190 
191   SideEffects []
192 
193   SeeAlso     []
194 
195 ***********************************************************************/
Ssw_NodesAreConstrained(Ssw_Man_t * p,Aig_Obj_t * pOld,Aig_Obj_t * pNew)196 int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
197 {
198     int pLits[2], RetValue, fComplNew;
199     Aig_Obj_t * pTemp;
200 
201     // sanity checks
202     assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
203     assert( p->pPars->fConstrs || Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) );
204 
205     // move constant to the old node
206     if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
207     {
208         assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
209         pTemp = pOld;
210         pOld  = pNew;
211         pNew  = pTemp;
212     }
213 
214     // move complement to the new node
215     if ( Aig_IsComplement(pOld) )
216     {
217         pOld = Aig_Regular(pOld);
218         pNew = Aig_Not(pNew);
219     }
220     assert( p->pMSat != NULL );
221 
222     // if the nodes do not have SAT variables, allocate them
223     Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
224     Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pNew) );
225 
226     // transform the new node
227     fComplNew = Aig_IsComplement( pNew );
228     pNew = Aig_Regular( pNew );
229 
230     // consider the constant 1 case
231     if ( pOld == Aig_ManConst1(p->pFrames) )
232     {
233         // add constraint A = 1  ---->  A
234         pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
235         if ( p->pPars->fPolarFlip )
236         {
237             if ( pNew->fPhase )  pLits[0] = lit_neg( pLits[0] );
238         }
239         RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 1 );
240         assert( RetValue );
241     }
242     else
243     {
244         // add constraint A = B  ---->  (A v !B)(!A v B)
245 
246         // (A v !B)
247         pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
248         pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew );
249         if ( p->pPars->fPolarFlip )
250         {
251             if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
252             if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
253         }
254         pLits[0] = lit_neg( pLits[0] );
255         pLits[1] = lit_neg( pLits[1] );
256         RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
257         assert( RetValue );
258 
259         // (!A v B)
260         pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
261         pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew);
262         if ( p->pPars->fPolarFlip )
263         {
264             if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
265             if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
266         }
267         pLits[0] = lit_neg( pLits[0] );
268         pLits[1] = lit_neg( pLits[1] );
269         RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
270         assert( RetValue );
271     }
272     return 1;
273 }
274 
275 /**Function*************************************************************
276 
277   Synopsis    [Constrains one node in the SAT solver.]
278 
279   Description []
280 
281   SideEffects []
282 
283   SeeAlso     []
284 
285 ***********************************************************************/
Ssw_NodeIsConstrained(Ssw_Man_t * p,Aig_Obj_t * pPoObj)286 int Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj )
287 {
288     int RetValue, Lit;
289     Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pPoObj) );
290     // add constraint A = 1  ---->  A
291     Lit = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_ObjFanin0(pPoObj)), !Aig_ObjFaninC0(pPoObj) );
292     if ( p->pPars->fPolarFlip )
293     {
294         if ( Aig_ObjFanin0(pPoObj)->fPhase )  Lit = lit_neg( Lit );
295     }
296     RetValue = sat_solver_addclause( p->pMSat->pSat, &Lit, &Lit + 1 );
297     assert( RetValue );
298     return 1;
299 }
300 
301 ////////////////////////////////////////////////////////////////////////
302 ///                       END OF FILE                                ///
303 ////////////////////////////////////////////////////////////////////////
304 
305 
306 ABC_NAMESPACE_IMPL_END
307 
308