summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h4
-rw-r--r--src/aig/gia/giaSweeper.c48
2 files changed, 18 insertions, 34 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 1d170102..0aa6aa53 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1179,8 +1179,8 @@ extern void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConf
extern void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds );
extern Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p );
extern int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit );
-extern int Gia_SweeperProbeFind( Gia_Man_t * p, int iLit );
-extern void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId );
+extern int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId );
+extern int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLitNew );
extern int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId );
extern int Gia_SweeperCondPop( Gia_Man_t * p );
extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId );
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index a930b994..20a5297d 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -33,13 +33,9 @@ SAT sweeping/equivalence checking requires the following steps:
- nodes representing conditions to be used as constraints
- nodes representing functions to be equivalence checked
- nodes representing functions needed by the user at the end of SAT sweeping
- Creating new probe using Gia_SweeperProbeCreate(): int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit );
- Find existing probe using Gia_SweeperProbeFind(): int Gia_SweeperProbeFind( Gia_Man_t * p, int iLit );
- If probe with this literal (iLit) exists, this procedure increments its reference counter and returns it.
- If probe with this literal does not exist, it creates new probe and sets is reference counter to 1.
- Dereference probe using Gia_SweeperProbeDeref(): void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId );
- Dereferences probe with the given ID. If ref counter become 0, recycles the logic cone of the given probe.
- Recycling of probe IDs can be added later.
+ Creating new probe using Gia_SweeperProbeCreate(): int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit );
+ Delete existing probe using Gia_SweeperProbeDelete(): int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId );
+ Update existing probe using Gia_SweeperProbeUpdate(): int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLit );
Comments:
- a probe is identified by its 0-based ID, which is returned by above procedures
- GIA literal of the probe is returned by int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
@@ -265,37 +261,25 @@ int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit )
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
int ProbeId = Vec_IntSize(pSwp->vProbes);
Vec_IntPush( pSwp->vProbes, iLit );
- Vec_IntPush( pSwp->vProbRefs, 1 );
- Vec_IntSetEntryFull( pSwp->vLit2Prob, iLit, ProbeId ); // consider hash table in the future
-//printf( "Creating probe %d with literal %d.\n", ProbeId, iLit );
return ProbeId;
}
-// if probe with this literal (iLit) exists, this procedure increments its reference counter and returns it.
-// if probe with this literal does not exist, it creates new probe and sets is reference counter to 1.
-int Gia_SweeperProbeFind( Gia_Man_t * p, int iLit )
+// delete existing probe
+int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
- int ProbeId = -1;
- if ( iLit < Vec_IntSize(pSwp->vLit2Prob) && (ProbeId = Vec_IntEntry(pSwp->vLit2Prob, iLit)) >= 0 )
- {
- Vec_IntAddToEntry( pSwp->vProbRefs, ProbeId, 1 );
- return ProbeId;
- }
- return Gia_SweeperProbeCreate( p, iLit );
+ int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
+ assert( iLit >= 0 );
+ Vec_IntWriteEntry(pSwp->vProbes, ProbeId, -1);
+ return iLit;
}
-// dereferences the probe
-void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId )
+// update existing probe
+int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLitNew )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
- assert( Vec_IntEntry(pSwp->vProbRefs, ProbeId) > 0 );
- if ( Vec_IntAddToEntry( pSwp->vProbRefs, ProbeId, -1 ) == 0 )
- {
- int iLit = Gia_SweeperProbeLit( p, ProbeId );
- Vec_IntWriteEntry( pSwp->vLit2Prob, iLit, -1 );
- Vec_IntWriteEntry( pSwp->vProbes, ProbeId, 0 );
- // TODO: recycle probe ID
-//printf( "Deleteing probe %d with literal %d.\n", ProbeId, iLit );
- }
+ int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
+ assert( iLit >= 0 );
+ Vec_IntWriteEntry(pSwp->vProbes, ProbeId, iLitNew);
+ return iLit;
}
// returns literal associated with the probe
int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
@@ -1008,7 +992,7 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords,
/**Function*************************************************************
- Synopsis [Procedure to perform conditional fraig sweeping on separate logic cones..]
+ Synopsis [Procedure to perform conditional fraig sweeping on separate logic cones.]
Description [The procedure takes GIA with the sweeper defined. The sweeper
is assumed to have some conditions currently pushed, which will be used