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