abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cgtSat.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cgtSat.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Clock gating package.]
8 
9  Synopsis [Checking implications using SAT.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: cgtSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cgtInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 
35 /**Function*************************************************************
36 
37  Synopsis [Runs equivalence test for the two nodes.]
38 
39  Description [Both nodes should be regular and different from each other.]
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter )
47 {
48  int nBTLimit = p->pPars->nConfMax;
49  int pLits[2], RetValue;
50  abctime clk;
51  p->nCalls++;
52 
53  // sanity checks
54  assert( p->pSat && p->pCnf );
55  assert( !Aig_IsComplement(pMiter) );
56  assert( Aig_Regular(pGate) != pMiter );
57 
58  // solve under assumptions
59  // G => !M -- true G & M -- false
60  pLits[0] = toLitCond( p->pCnf->pVarNums[Aig_Regular(pGate)->Id], Aig_IsComplement(pGate) );
61  pLits[1] = toLitCond( p->pCnf->pVarNums[pMiter->Id], 0 );
62 
63 clk = Abc_Clock();
64  RetValue = sat_solver_solve( p->pSat, pLits, pLits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
65 p->timeSat += Abc_Clock() - clk;
66  if ( RetValue == l_False )
67  {
68 p->timeSatUnsat += Abc_Clock() - clk;
69  pLits[0] = lit_neg( pLits[0] );
70  pLits[1] = lit_neg( pLits[1] );
71  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
72  assert( RetValue );
73  sat_solver_compress( p->pSat );
74  p->nCallsUnsat++;
75  return 1;
76  }
77  else if ( RetValue == l_True )
78  {
79 p->timeSatSat += Abc_Clock() - clk;
80  p->nCallsSat++;
81  return 0;
82  }
83  else // if ( RetValue1 == l_Undef )
84  {
85 p->timeSatUndec += Abc_Clock() - clk;
86  p->nCallsUndec++;
87  return -1;
88  }
89  return -2;
90 }
91 
92 ////////////////////////////////////////////////////////////////////////
93 /// END OF FILE ///
94 ////////////////////////////////////////////////////////////////////////
95 
96 
98 
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
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
static void sat_solver_compress(sat_solver *s)
Definition: satSolver.h:217
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
#define l_True
Definition: SolverTypes.h:84
static abctime Abc_Clock()
Definition: abc_global.h:279
static lit lit_neg(lit l)
Definition: satVec.h:144
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
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
ABC_NAMESPACE_IMPL_START int Cgt_CheckImplication(Cgt_Man_t *p, Aig_Obj_t *pGate, Aig_Obj_t *pMiter)
DECLARATIONS ///.
Definition: cgtSat.c:46
#define l_False
Definition: SolverTypes.h:85
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int Id
Definition: aig.h:85
typedefABC_NAMESPACE_HEADER_START struct Cgt_Man_t_ Cgt_Man_t
INCLUDES ///.
Definition: cgtInt.h:47