abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dchSat.c
Go to the documentation of this file.
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 
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 ***********************************************************************/
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) )
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 
167 
int nSatVars
Definition: dchInt.h:64
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
void Dch_ManSatSolverRecycle(Dch_Man_t *p)
Definition: dchMan.c:153
int nSatCallsSat
Definition: dchInt.h:80
ABC_NAMESPACE_IMPL_START int Dch_NodesAreEquiv(Dch_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
DECLARATIONS ///.
Definition: dchSat.c:45
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Aig_Man_t * pAigFraig
Definition: dchInt.h:58
abctime timeSatUnsat
Definition: dchInt.h:91
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
#define l_True
Definition: SolverTypes.h:84
int nCallsSince
Definition: dchInt.h:68
static abctime Abc_Clock()
Definition: abc_global.h:279
static lit lit_neg(lit l)
Definition: satVec.h:144
int nSatProof
Definition: dchInt.h:77
static lit toLitCond(int v, int c)
Definition: satVec.h:143
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Definition: aig.h:69
abctime timeSat
Definition: dchInt.h:89
abctime timeSatSat
Definition: dchInt.h:90
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
sat_solver * pSat
Definition: dchInt.h:63
abctime timeSatUndec
Definition: dchInt.h:92
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
int nSatCalls
Definition: dchInt.h:76
unsigned int fPhase
Definition: aig.h:78
#define l_False
Definition: SolverTypes.h:85
int nSatCallsUnsat
Definition: dchInt.h:79
#define assert(ex)
Definition: util_old.h:213
Dch_Pars_t * pPars
Definition: dchInt.h:54
void Dch_CnfNodeAddToSolver(Dch_Man_t *p, Aig_Obj_t *pObj)
Definition: dchCnf.c:287
ABC_INT64_T abctime
Definition: abc_global.h:278
int nSatFailsReal
Definition: dchInt.h:78
static int Dch_ObjSatNum(Dch_Man_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: dchInt.h:102