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