abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaProp.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaProp.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Constraint propagation on the AIG.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaProp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 #define GIA_SAT_SHIFT 12
31 #define GIA_ROOT_MASK
32 #define GIA_PATH00_MASK
33 #define GIA_PATH10_MASK
34 #define GIA_PATH20_MASK
35 #define GIA_PATH30_MASK
36 #define GIA_PATH00_MASK
37 #define GIA_PATH10_MASK
38 #define GIA_PATH20_MASK
39 #define GIA_PATH30_MASK
40 
41 static inline int Gia_SatObjIsRoot( Gia_Obj_t * p ) { return 0; }
42 static inline int Gia_SatObjXorRoot( Gia_Obj_t * p ) { return 0; }
43 
44 
45 static inline int Gia_SatObjIsAssigned( Gia_Obj_t * p ) { return 0; }
46 static inline int Gia_SatObjIsHeld( Gia_Obj_t * p ) { return 0; }
47 static inline int Gia_SatObjValue( Gia_Obj_t * p ) { return 0; }
48 
49 
50 ////////////////////////////////////////////////////////////////////////
51 /// FUNCTION DEFINITIONS ///
52 ////////////////////////////////////////////////////////////////////////
53 
54 /**Function*************************************************************
55 
56  Synopsis [Checks if the give cut is satisfied.]
57 
58  Description []
59 
60  SideEffects []
61 
62  SeeAlso []
63 
64 ***********************************************************************/
65 int Gia_SatPathCheckCutSat_rec( Gia_Obj_t * p, int fCompl )
66 {
67  if ( Gia_SatObjIsRoot(p) )
68  return Gia_ObjIsAssigned(p) && Gia_SatObjValue(p) == fCompl;
69  if ( Gia_SatObjPath0(p) && !Gia_SatPathCheckCutSat_rec( Gia_ObjFanin0(p), fCompl ^ Gia_ObjFaninC0(p) ) )
70  return 0;
71  if ( Gia_SatObjPath1(p) && !Gia_SatPathCheckCutSat_rec( Gia_ObjFanin1(p), fCompl ^ Gia_ObjFaninC1(p) ) )
72  return 0;
73  return 1;
74 }
75 
76 /**Function*************************************************************
77 
78  Synopsis [Checks if the give cut is satisfied.]
79 
80  Description []
81 
82  SideEffects []
83 
84  SeeAlso []
85 
86 ***********************************************************************/
87 int Gia_SatPathCheckCutSat( Gia_Obj_t * p )
88 {
89  int RetValue;
90  assert( Gia_SatObjIsRoot(p) );
91  Gia_SatObjXorRoot(p);
92  RetValue = Gia_SatPathCheckCutSat_rec( p );
93  Gia_SatObjXorRoot(p);
94  return RetValue;
95 }
96 
97 /**Function*************************************************************
98 
99  Synopsis [Unbinds literals on the path.]
100 
101  Description []
102 
103  SideEffects []
104 
105  SeeAlso []
106 
107 ***********************************************************************/
108 int Gia_SatPathUnbind_rec( Gia_Obj_t * p )
109 {
110 }
111 
112 /**Function*************************************************************
113 
114  Synopsis [Creates a feasible path from the node to a terminal.]
115 
116  Description []
117 
118  SideEffects []
119 
120  SeeAlso []
121 
122 ***********************************************************************/
123 int Gia_SatPathStart_rec( Gia_Obj_t * p, int fDiffs, int fCompl )
124 {
125  if ( Gia_SatObjIsRoot(p) )
126  return fDiffs && (!Gia_ObjIsAssigned(p) || Gia_SatObjValue(p) != fCompl);
127  if ( fCompl == 0 )
128  {
129  if ( Gia_SatPathStart_rec( Gia_ObjFanin0(p), fDiffs + !Gia_SatObjPath0(p), fCompl ^ Gia_ObjFaninC0(p) ) &&
130  Gia_SatPathStart_rec( Gia_ObjFanin1(p), fDiffs + !Gia_SatObjPath1(p), fCompl ^ Gia_ObjFaninC1(p) ) )
131  return Gia_ObjSetDraftPath0(p) + Gia_ObjSetDraftPath1(p);
132  }
133  else
134  {
135  if ( Gia_SatPathStart_rec( Gia_ObjFanin0(p), fDiffs + !Gia_SatObjPath0(p), fCompl ^ Gia_ObjFaninC0(p) ) )
136  {
137  Gia_ObjUnsetDraftPath1(p);
138  return Gia_ObjSetDraftPath0(p);
139  }
140  if ( Gia_SatPathStart_rec( Gia_ObjFanin1(p), fDiffs + !Gia_SatObjPath1(p), fCompl ^ Gia_ObjFaninC1(p) ) )
141  {
142  Gia_ObjUnsetDraftPath0(p);
143  return Gia_ObjSetDraftPath1(p);
144  }
145  }
146  return 0;
147 }
148 
149 /**Function*************************************************************
150 
151  Synopsis [Creates a feasible path from the node to a terminal.]
152 
153  Description []
154 
155  SideEffects []
156 
157  SeeAlso []
158 
159 ***********************************************************************/
160 int Gia_SatPathStart( Gia_Obj_t * p )
161 {
162  int RetValue;
163  assert( Gia_SatObjIsRoot(p) );
164  Gia_SatObjXorRoot(p);
165  RetValue = Gia_SatPathStart_rec( p, 0, 0 );
166  Gia_SatObjXorRoot(p);
167  return RetValue;
168 }
169 
170 ////////////////////////////////////////////////////////////////////////
171 /// END OF FILE ///
172 ////////////////////////////////////////////////////////////////////////
173 
174 
175 ABC_NAMESPACE_IMPL_END
176 
Gia_SatPathUnbind_rec
int Gia_SatPathUnbind_rec(Gia_Obj_t *p)
Definition: giaProp.c:108
Gia_SatObjIsRoot
static int Gia_SatObjIsRoot(Gia_Obj_t *p)
Definition: giaProp.c:41
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_SatPathCheckCutSat_rec
int Gia_SatPathCheckCutSat_rec(Gia_Obj_t *p, int fCompl)
FUNCTION DEFINITIONS ///.
Definition: giaProp.c:65
Gia_SatPathStart
int Gia_SatPathStart(Gia_Obj_t *p)
Definition: giaProp.c:160
Gia_Obj_t_
Definition: gia.h:75
Gia_SatObjIsHeld
static int Gia_SatObjIsHeld(Gia_Obj_t *p)
Definition: giaProp.c:46
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_SatPathStart_rec
int Gia_SatPathStart_rec(Gia_Obj_t *p, int fDiffs, int fCompl)
Definition: giaProp.c:123
Gia_SatPathCheckCutSat
int Gia_SatPathCheckCutSat(Gia_Obj_t *p)
Definition: giaProp.c:87
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_SatObjXorRoot
static int Gia_SatObjXorRoot(Gia_Obj_t *p)
Definition: giaProp.c:42
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_SatObjIsAssigned
static int Gia_SatObjIsAssigned(Gia_Obj_t *p)
Definition: giaProp.c:45
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_SatObjValue
static int Gia_SatObjValue(Gia_Obj_t *p)
Definition: giaProp.c:47