summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaFalse.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaFalse.c')
-rw-r--r--src/aig/gia/giaFalse.c46
1 files changed, 21 insertions, 25 deletions
diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c
index 0d609436..c3f26455 100644
--- a/src/aig/gia/giaFalse.c
+++ b/src/aig/gia/giaFalse.c
@@ -390,34 +390,30 @@ Gia_Man_t * Gia_ManCheckOne( Gia_Man_t * p, int iOut, int iObj, int nTimeOut, in
// add CNF for the path
Gia_ManForEachObjVec( vPath, p, pObj, i )
{
- if ( Gia_ObjIsAnd(pObj) )
+ if ( !Gia_ObjIsAnd(pObj) )
+ continue;
+ assert( i > 0 );
+ pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) );
+ if ( pFanin == Gia_ObjFanin0(pObj) )
{
- assert( i > 0 );
- pFanin = Gia_ManObj( p, Vec_IntEntry(vPath, i-1) );
- if ( pFanin == Gia_ObjFanin0(pObj) )
- {
- sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
- i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0],
- Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
- sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
- i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1],
- Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
- }
- else if ( pFanin == Gia_ObjFanin1(pObj) )
- {
- sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
- Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath),
- Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
- sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
- Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath),
- Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
- }
- else assert( 0 );
- sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 );
+ sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
+ i-1 + 1*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[0],
+ Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+ sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
+ i-1 + 2*Vec_IntSize(vPath), Gia_ObjFanin1(pObj)->Value + Shift[1],
+ Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+ }
+ else if ( pFanin == Gia_ObjFanin1(pObj) )
+ {
+ sat_solver_add_and( pSat, i + 1*Vec_IntSize(vPath),
+ Gia_ObjFanin0(pObj)->Value + Shift[0], i-1 + 1*Vec_IntSize(vPath),
+ Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+ sat_solver_add_and( pSat, i + 2*Vec_IntSize(vPath),
+ Gia_ObjFanin0(pObj)->Value + Shift[1], i-1 + 2*Vec_IntSize(vPath),
+ Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
}
- else if ( Gia_ObjIsCi(pObj) )
- sat_solver_add_xor( pSat, i, pObj->Value + Shift[0], pObj->Value + Shift[1], 0 );
else assert( 0 );
+ sat_solver_add_xor( pSat, i, i + 1*Vec_IntSize(vPath), i + 2*Vec_IntSize(vPath), 0 );
Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
}
// call the SAT solver