abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sfmCnf.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sfmCnf.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based optimization using internal don't-cares.]
8 
9  Synopsis [CNF computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: sfmCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sfmInt.h"
22 #include "bool/kit/kit.h"
23 
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis []
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 void Sfm_PrintCnf( Vec_Str_t * vCnf )
47 {
48  char Entry;
49  int i, Lit;
50  Vec_StrForEachEntry( vCnf, Entry, i )
51  {
52  Lit = (int)Entry;
53  if ( Lit == -1 )
54  printf( "\n" );
55  else
56  printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
57  }
58 }
59 
60 /**Function*************************************************************
61 
62  Synopsis []
63 
64  Description []
65 
66  SideEffects []
67 
68  SeeAlso []
69 
70 ***********************************************************************/
71 int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
72 {
73  Vec_StrClear( vCnf );
74  if ( Truth == 0 || ~Truth == 0 )
75  {
76 // assert( nVars == 0 );
77  Vec_StrPush( vCnf, (char)(Truth == 0) );
78  Vec_StrPush( vCnf, (char)-1 );
79  return 1;
80  }
81  else
82  {
83  int i, k, c, RetValue, Literal, Cube, nCubes = 0;
84  assert( nVars > 0 );
85  for ( c = 0; c < 2; c ++ )
86  {
87  Truth = c ? ~Truth : Truth;
88  RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
89  assert( RetValue == 0 );
90  nCubes += Vec_IntSize( vCover );
91  Vec_IntForEachEntry( vCover, Cube, i )
92  {
93  for ( k = 0; k < nVars; k++ )
94  {
95  Literal = 3 & (Cube >> (k << 1));
96  if ( Literal == 1 ) // '0' -> pos lit
97  Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
98  else if ( Literal == 2 ) // '1' -> neg lit
99  Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
100  else if ( Literal != 0 )
101  assert( 0 );
102  }
103  Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
104  Vec_StrPush( vCnf, (char)-1 );
105  }
106  }
107  return nCubes;
108  }
109 }
110 
111 /**Function*************************************************************
112 
113  Synopsis []
114 
115  Description []
116 
117  SideEffects []
118 
119  SeeAlso []
120 
121 ***********************************************************************/
123 {
124  Vec_Wec_t * vCnfs;
125  Vec_Str_t * vCnf, * vCnfBase;
126  word uTruth;
127  int i, nCubes;
128  vCnf = Vec_StrAlloc( 100 );
129  vCnfs = Vec_WecStart( p->nObjs );
130  Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
131  {
132  nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
133  vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
134  Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
135  memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
136  vCnfBase->nSize = Vec_StrSize(vCnf);
137  }
138  Vec_StrFree( vCnf );
139  return vCnfs;
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis []
145 
146  Description []
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
153 void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
154 {
155  Vec_Int_t * vClause;
156  char Entry;
157  int i, Lit;
158  Vec_WecClear( vRes );
159  vClause = Vec_WecPushLevel( vRes );
160  Vec_StrForEachEntry( vCnf, Entry, i )
161  {
162  if ( (int)Entry == -1 )
163  {
164  vClause = Vec_WecPushLevel( vRes );
165  continue;
166  }
167  Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
168  Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
169  Vec_IntPush( vClause, Lit );
170  }
171 }
172 
173 ////////////////////////////////////////////////////////////////////////
174 /// END OF FILE ///
175 ////////////////////////////////////////////////////////////////////////
176 
177 
179 
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static int Abc_Lit2LitV(int *pMap, int Lit)
Definition: abc_global.h:269
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition: vecWec.h:42
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static char * Vec_StrArray(Vec_Str_t *p)
Definition: vecStr.h:272
static Vec_Wec_t * Vec_WecStart(int nSize)
Definition: vecWec.h:98
#define Vec_StrForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecStr.h:54
static Vec_Int_t * Vec_WecPushLevel(Vec_Wec_t *p)
Definition: vecWec.h:284
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static int Sfm_ObjFaninNum(Sfm_Ntk_t *p, int i)
Definition: sfmInt.h:139
static void Vec_StrClear(Vec_Str_t *p)
Definition: vecStr.h:519
char * memcpy()
typedefABC_NAMESPACE_HEADER_START struct Sfm_Ntk_t_ Sfm_Ntk_t
INCLUDES ///.
Definition: sfm.h:41
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
ABC_NAMESPACE_IMPL_START void Sfm_PrintCnf(Vec_Str_t *vCnf)
DECLARATIONS ///.
Definition: sfmCnf.c:46
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
static void Vec_WecClear(Vec_Wec_t *p)
Definition: vecWec.h:255
static void Vec_StrGrow(Vec_Str_t *p, int nCapMin)
Definition: vecStr.h:404
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
#define Vec_WrdForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition: vecWrd.h:60
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_Wec_t * Sfm_CreateCnf(Sfm_Ntk_t *p)
Definition: sfmCnf.c:122
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static Vec_Int_t * Vec_WecEntry(Vec_Wec_t *p, int i)
Definition: vecWec.h:142
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int Sfm_TruthToCnf(word Truth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vCnf)
Definition: sfmCnf.c:71
void Sfm_TranslateCnf(Vec_Wec_t *vRes, Vec_Str_t *vCnf, Vec_Int_t *vFaninMap, int iPivotVar)
Definition: sfmCnf.c:153
int nSize
Definition: bblif.c:50
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54