1 /**CFile****************************************************************
2
3 FileName [dchSat.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Choice computation for tech-mapping.]
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 - June 29, 2008.]
16
17 Revision [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "dchInt.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 []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Dch_NodesAreEquiv(Dch_Man_t * p,Aig_Obj_t * pOld,Aig_Obj_t * pNew)45 int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
46 {
47 int nBTLimit = p->pPars->nBTLimit;
48 int pLits[2], RetValue, RetValue1, status;
49 abctime clk;
50 p->nSatCalls++;
51
52 // sanity checks
53 assert( !Aig_IsComplement(pNew) );
54 assert( !Aig_IsComplement(pOld) );
55 assert( pNew != pOld );
56
57 p->nCallsSince++; // experiment with this!!!
58
59 // check if SAT solver needs recycling
60 if ( p->pSat == NULL ||
61 (p->pPars->nSatVarMax &&
62 p->nSatVars > p->pPars->nSatVarMax &&
63 p->nCallsSince > p->pPars->nCallsRecycle) )
64 Dch_ManSatSolverRecycle( p );
65
66 // if the nodes do not have SAT variables, allocate them
67 Dch_CnfNodeAddToSolver( p, pOld );
68 Dch_CnfNodeAddToSolver( p, pNew );
69
70 // propage unit clauses
71 if ( p->pSat->qtail != p->pSat->qhead )
72 {
73 status = sat_solver_simplify(p->pSat);
74 assert( status != 0 );
75 assert( p->pSat->qtail == p->pSat->qhead );
76 }
77
78 // solve under assumptions
79 // A = 1; B = 0 OR A = 1; B = 1
80 pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 );
81 pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
82 if ( p->pPars->fPolarFlip )
83 {
84 if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
85 if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
86 }
87 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
88 clk = Abc_Clock();
89 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
90 (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
91 p->timeSat += Abc_Clock() - clk;
92 if ( RetValue1 == l_False )
93 {
94 p->timeSatUnsat += Abc_Clock() - clk;
95 pLits[0] = lit_neg( pLits[0] );
96 pLits[1] = lit_neg( pLits[1] );
97 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
98 assert( RetValue );
99 p->nSatCallsUnsat++;
100 }
101 else if ( RetValue1 == l_True )
102 {
103 p->timeSatSat += Abc_Clock() - clk;
104 p->nSatCallsSat++;
105 return 0;
106 }
107 else // if ( RetValue1 == l_Undef )
108 {
109 p->timeSatUndec += Abc_Clock() - clk;
110 p->nSatFailsReal++;
111 return -1;
112 }
113
114 // if the old node was constant 0, we already know the answer
115 if ( pOld == Aig_ManConst1(p->pAigFraig) )
116 {
117 p->nSatProof++;
118 return 1;
119 }
120
121 // solve under assumptions
122 // A = 0; B = 1 OR A = 0; B = 0
123 pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 );
124 pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
125 if ( p->pPars->fPolarFlip )
126 {
127 if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
128 if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
129 }
130 clk = Abc_Clock();
131 RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
132 (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
133 p->timeSat += Abc_Clock() - clk;
134 if ( RetValue1 == l_False )
135 {
136 p->timeSatUnsat += Abc_Clock() - clk;
137 pLits[0] = lit_neg( pLits[0] );
138 pLits[1] = lit_neg( pLits[1] );
139 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
140 assert( RetValue );
141 p->nSatCallsUnsat++;
142 }
143 else if ( RetValue1 == l_True )
144 {
145 p->timeSatSat += Abc_Clock() - clk;
146 p->nSatCallsSat++;
147 return 0;
148 }
149 else // if ( RetValue1 == l_Undef )
150 {
151 p->timeSatUndec += Abc_Clock() - clk;
152 p->nSatFailsReal++;
153 return -1;
154 }
155 // return SAT proof
156 p->nSatProof++;
157 return 1;
158 }
159
160
161 ////////////////////////////////////////////////////////////////////////
162 /// END OF FILE ///
163 ////////////////////////////////////////////////////////////////////////
164
165
166 ABC_NAMESPACE_IMPL_END
167
168