ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaProp.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
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
41static inline int Gia_SatObjIsRoot( Gia_Obj_t * p ) { return 0; }
42static inline int Gia_SatObjXorRoot( Gia_Obj_t * p ) { return 0; }
43
44
45static inline int Gia_SatObjIsAssigned( Gia_Obj_t * p ) { return 0; }
46static inline int Gia_SatObjIsHeld( Gia_Obj_t * p ) { return 0; }
47static inline int Gia_SatObjValue( Gia_Obj_t * p ) { return 0; }
48
49
53
65int 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
87int 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
111
123int 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
160int 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
173
174
175ABC_NAMESPACE_IMPL_END
176
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
p
Cube * p
Definition exorList.c:222
Gia_SatPathUnbind_rec
int Gia_SatPathUnbind_rec(Gia_Obj_t *p)
Definition giaProp.c:108
Gia_SatPathStart
int Gia_SatPathStart(Gia_Obj_t *p)
Definition giaProp.c:160
Gia_SatPathCheckCutSat_rec
int Gia_SatPathCheckCutSat_rec(Gia_Obj_t *p, int fCompl)
FUNCTION DEFINITIONS ///.
Definition giaProp.c:65
Gia_SatPathCheckCutSat
int Gia_SatPathCheckCutSat(Gia_Obj_t *p)
Definition giaProp.c:87
Gia_SatPathStart_rec
int Gia_SatPathStart_rec(Gia_Obj_t *p, int fDiffs, int fCompl)
Definition giaProp.c:123
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
assert
#define assert(ex)
Definition util_old.h:213