From 47afd0f4f4f258ddc9231b791e6149430240ba52 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 23 Oct 2013 16:26:13 -0700 Subject: Multi-output property solver. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaMan.c | 2 ++ src/aig/gia/giaUtil.c | 2 +- 3 files changed, 4 insertions(+), 1 deletion(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 122e5025..8d953273 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -133,6 +133,7 @@ struct Gia_Man_t_ Vec_Int_t * vLutConfigs; // LUT configurations Abc_Cex_t * pCexComb; // combinational counter-example Abc_Cex_t * pCexSeq; // sequential counter-example + Vec_Ptr_t * vSeqModelVec; // sequential counter-examples int * pCopies; // intermediate copies Vec_Int_t * vTruths; // used for truth table computation Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 2eaf8eee..eb728cd0 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -72,6 +72,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax ) ***********************************************************************/ void Gia_ManStop( Gia_Man_t * p ) { + if ( p->vSeqModelVec ) + Vec_PtrFreeFree( p->vSeqModelVec ); Gia_ManStaticFanoutStop( p ); Tim_ManStopP( (Tim_Man_t **)&p->pManTime ); assert( p->pManTime == NULL ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 08136e7d..f3edca36 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1716,7 +1716,7 @@ int Gia_ManHasChoices_very_old( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose ) +Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose ) { Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame(); Gia_Man_t * p = Gia_ManDup( pInit ); -- cgit v1.2.3