#include "gia.h"
#include "sat/bsat/satSolver.h"

Data Structures
struct	Ccf_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Ccf_Man_t_	Ccf_Man_t
	DECLARATIONS ///. More...

Functions
Ccf_Man_t *	Ccf_ManStart (Gia_Man_t *pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose)
	FUNCTION DEFINITIONS ///. More...

void	Ccf_ManStop (Ccf_Man_t *p)

void	Gia_ManCofExtendSolver (Ccf_Man_t *p)

static int	Gia_Obj0Copy (Vec_Int_t *vCopies, int Fan0, int fCompl0)

static int	Gia_Obj1Copy (Vec_Int_t *vCopies, int Fan1, int fCompl1)

void	Gia_ManCofOneDerive_rec (Ccf_Man_t *p, int Id)

int	Gia_ManCofOneDerive (Ccf_Man_t *p, int LitProp)

int	Gia_ManCofGetReachable (Ccf_Man_t *p, int Lit)

Gia_Man_t *	Gia_ManCofTest (Gia_Man_t *pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Ccf_Man_t_ Ccf_Man_t

DECLARATIONS ///.

CFile****************************************************************

FileName [giaCCof.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Backward reachability using circuit cofactoring.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:: giaCCof.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 31 of file giaCCof.c.

Function Documentation

Ccf_Man_t* Ccf_ManStart	(	Gia_Man_t *	pGia,
		int	nFrameMax,
		int	nConfMax,
		int	nTimeMax,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Create manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file giaCCof.c.

 {
     static Gia_ParFra_t Pars, * pPars = &Pars;
     Ccf_Man_t * p;
     assert( nFrameMax > 0 );
     p = ABC_CALLOC( Ccf_Man_t, 1 );
     p->pGia      = pGia;
     p->nFrameMax = nFrameMax;    
     p->nConfMax  = nConfMax;
     p->nTimeMax  = nTimeMax;
     p->fVerbose  = fVerbose;
     // create unrolling manager
     memset( pPars, 0, sizeof(Gia_ParFra_t) );
     pPars->fVerbose     = fVerbose;
     pPars->nFrames      = nFrameMax;
     pPars->fSaveLastLit = 1;
     p->pUnr = Gia_ManUnrollStart( pGia, pPars );
     p->vCopies = Vec_IntAlloc( 1000 );
     // internal data
     p->pSat = sat_solver_new();
 //    sat_solver_setnvars( p->pSat, 10000 );
     return p;
 }

void Ccf_ManStop ( Ccf_Man_t * p )

Function*************************************************************

Synopsis [Delete manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file giaCCof.c.

 {
     Vec_IntFree( p->vCopies );
     Gia_ManUnrollStop( p->pUnr );
     sat_solver_delete( p->pSat );
     Gia_ManStopP( &p->pFrames );
     ABC_FREE( p );
 }

void Gia_ManCofExtendSolver ( Ccf_Man_t * p )

Function*************************************************************

Synopsis [Extends the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file giaCCof.c.

 {
     Gia_Obj_t * pObj;
     int i;
     // add SAT clauses
     for ( i = sat_solver_nvars(p->pSat); i < Gia_ManObjNum(p->pFrames); i++ )
     {
         pObj = Gia_ManObj( p->pFrames, i );
         if ( Gia_ObjIsAnd(pObj) )
             sat_solver_add_and( p->pSat, i, 
                 Gia_ObjFaninId0(pObj, i), 
                 Gia_ObjFaninId1(pObj, i), 
                 Gia_ObjFaninC0(pObj), 
                 Gia_ObjFaninC1(pObj), 0 ); 
     }
     sat_solver_setnvars( p->pSat, Gia_ManObjNum(p->pFrames) );
 }

int Gia_ManCofGetReachable	(	Ccf_Man_t *	p,
		int	Lit
	)

Function*************************************************************

Synopsis [Enumerates backward reachable states.]

Description [Return -1 if resource limit is reached. Returns 1 if computation converged (there is no more reachable states). Returns 0 if no more states to enumerate.]

SideEffects []

SeeAlso []

Definition at line 220 of file giaCCof.c.

 {
     int ObjPrev = 0, ConfPrev = 0;
     int Count = 0, LitOut, RetValue;
     abctime clk;
     // try solving for the first time and quit if converged
     RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
     if ( RetValue == l_False )
         return 1;
     // iterate circuit cofactoring
     while ( RetValue == l_True )
     {
         clk = Abc_Clock();
         // derive cofactor
         LitOut = Gia_ManCofOneDerive( p, Lit );
         // add the blocking clause
         RetValue = sat_solver_addclause( p->pSat, &LitOut, &LitOut + 1 );
         assert( RetValue );
         // try solving again
         RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
         // derive cofactors
         if ( p->fVerbose ) 
         {
             printf( "%3d : AIG =%7d  Conf =%7d.  ", Count++, 
                 Gia_ManObjNum(p->pFrames) - ObjPrev, sat_solver_nconflicts(p->pSat) - ConfPrev );
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             ObjPrev = Gia_ManObjNum(p->pFrames);
             ConfPrev = sat_solver_nconflicts(p->pSat);
         }
     }
     if ( RetValue == l_Undef )
         return -1;
     return 0;
 }

int Gia_ManCofOneDerive	(	Ccf_Man_t *	p,
		int	LitProp
	)

Function*************************************************************

Synopsis [Cofactor the circuit w.r.t. the given assignment.]

Description [Assumes that the solver has just returned SAT.]

SideEffects []

SeeAlso []

Definition at line 191 of file giaCCof.c.

 {
     int LitOut;
     // derive the cofactor of the property node
     Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 );
     Gia_ManCofOneDerive_rec( p, Abc_Lit2Var(LitProp) );
     LitOut = Vec_IntEntry( p->vCopies, Abc_Lit2Var(LitProp) );
     LitOut = Abc_LitNotCond( LitOut, Abc_LitIsCompl(LitProp) );
     // add new PO for the cofactor
     Gia_ManAppendCo( p->pFrames, LitOut );
     // add SAT clauses
     Gia_ManCofExtendSolver( p );
     // return negative literal of the cofactor
     return Abc_LitNot(LitOut);
 } 

void Gia_ManCofOneDerive_rec	(	Ccf_Man_t *	p,
		int	Id
	)

Function*************************************************************

Synopsis [Cofactor the circuit w.r.t. the given assignment.]

Description [Assumes that the solver has just returned SAT.]

SideEffects []

SeeAlso []

Definition at line 153 of file giaCCof.c.

 {
     Gia_Obj_t * pObj;
     int Res;
     if ( Vec_IntEntry(p->vCopies, Id) != -1 )
         return;
     pObj = Gia_ManObj(p->pFrames, Id);
     assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
     if ( Gia_ObjIsAnd(pObj) )
     {
         int fCompl0 = Gia_ObjFaninC0(pObj);
         int fCompl1 = Gia_ObjFaninC1(pObj);
         int Fan0 = Gia_ObjFaninId0p(p->pFrames, pObj);
         int Fan1 = Gia_ObjFaninId1p(p->pFrames, pObj);
         Gia_ManCofOneDerive_rec( p, Fan0 );
         Gia_ManCofOneDerive_rec( p, Fan1 );
         Res = Gia_ManHashAnd( p->pFrames, 
             Gia_Obj0Copy(p->vCopies, Fan0, fCompl0), 
             Gia_Obj1Copy(p->vCopies, Fan1, fCompl1) );
     }
     else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI
         Res = sat_solver_var_value( p->pSat, Id );
     else
         Res = Abc_Var2Lit( Id, 0 );
     Vec_IntWriteEntry( p->vCopies, Id, Res );
 }

Gia_Man_t* Gia_ManCofTest	(	Gia_Man_t *	pGia,
		int	nFrameMax,
		int	nConfMax,
		int	nTimeMax,
		int	fVerbose
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file giaCCof.c.

 { 
     Gia_Man_t * pNew;
     Ccf_Man_t * p;
     Gia_Obj_t * pObj;
     int f, i, Lit, RetValue = -1, fFailed = 0;
     abctime nTimeToStop = Abc_Clock() + nTimeMax * CLOCKS_PER_SEC;
     abctime clk = Abc_Clock();
     assert( Gia_ManPoNum(pGia) == 1 );
 
     // create reachability manager
     p = Ccf_ManStart( pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
 
     // set runtime limit
     if ( nTimeMax )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
 
     // perform backward image computation
     for ( f = 0; f < nFrameMax; f++ )
     {
         if ( fVerbose ) 
             printf( "ITER %3d :\n", f );
         // add to the mapping of nodes
         p->pFrames = (Gia_Man_t *)Gia_ManUnrollAdd( p->pUnr, f+1 );
         // add SAT clauses
         Gia_ManCofExtendSolver( p );
         // return output literal
         Lit = Gia_ManUnrollLastLit( p->pUnr );
         // derives cofactors of the property literal till all states are blocked
         RetValue = Gia_ManCofGetReachable( p, Lit );
         if ( RetValue )
             break;
 
         // check the property output
         Gia_ManSetPhase( p->pFrames );
         Gia_ManForEachPo( p->pFrames, pObj, i )
             if ( pObj->fPhase )
             {
                 printf( "Property failed in frame %d.\n", f );
                 fFailed = 1;
                 break;
             }
         if ( i < Gia_ManPoNum(p->pFrames) )
             break;
     }
 
     // report the result
     if ( nTimeToStop && Abc_Clock() > nTimeToStop )
         printf( "Runtime limit (%d sec) is reached after %d frames.  ", nTimeMax, f );
     else if ( f == nFrameMax )
         printf( "Completed %d frames without converging.  ", f );
     else if ( RetValue == 1 )
         printf( "Backward reachability converged after %d iterations.  ", f-1 );
     else if ( RetValue == -1 )
         printf( "Conflict limit or timeout is reached after %d frames.  ", f-1 );
     Abc_PrintTime( 1, "Runtime", Abc_Clock() - clk );
 
     if ( !fFailed && RetValue == 1 )
         printf( "Property holds.\n" );
     else if ( !fFailed )
         printf( "Property is undecided.\n" );
 
     // get the resulting AIG manager
     Gia_ManHashStop( p->pFrames );
     pNew = p->pFrames;  p->pFrames = NULL;
     Ccf_ManStop( p );
 
     // cleanup
 //    if ( fVerbose )
 //        Gia_ManPrintStats( pNew, 0 );
     pNew = Gia_ManCleanup( pGia = pNew );
     Gia_ManStop( pGia );
 //    if ( fVerbose )
 //        Gia_ManPrintStats( pNew, 0 );
     return pNew;   
 }