summaryrefslogtreecommitdiffstats
path: root/src/aig/int/intCheck.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/int/intCheck.c')
-rw-r--r--src/aig/int/intCheck.c305
1 files changed, 0 insertions, 305 deletions
diff --git a/src/aig/int/intCheck.c b/src/aig/int/intCheck.c
deleted file mode 100644
index 6b36fe30..00000000
--- a/src/aig/int/intCheck.c
+++ /dev/null
@@ -1,305 +0,0 @@
-/**CFile****************************************************************
-
- FileName [intCheck.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Interpolation engine.]
-
- Synopsis [Procedures to perform incremental inductive check.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 24, 2008.]
-
- Revision [$Id: intCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "intInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-// checking manager
-struct Inter_Check_t_
-{
- int nFramesK; // the number of timeframes (K=1 for simple induction)
- int nVars; // the current number of variables in the solver
- Aig_Man_t * pFrames; // unrolled timeframes
- Cnf_Dat_t * pCnf; // CNF of unrolled timeframes
- sat_solver * pSat; // SAT solver
- Vec_Int_t * vOrLits; // OR vars in each time frame (total number is the number nFrames)
- Vec_Int_t * vAndLits; // AND vars in the last timeframe (total number is the number of interpolants)
- Vec_Int_t * vAssLits; // assumptions (the union of the two)
-};
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Create timeframes of the manager for interpolation.]
-
- Description [The resulting manager is combinational. The primary inputs
- corresponding to register outputs are ordered first.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
-{
- Aig_Man_t * pFrames;
- Aig_Obj_t * pObj, * pObjLi, * pObjLo;
- int i, f;
- assert( Saig_ManRegNum(pAig) > 0 );
- pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
- // map the constant node
- Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
- // create variables for register outputs
- Saig_ManForEachLo( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
- // add timeframes
- for ( f = 0; f < nFrames; f++ )
- {
- // create PI nodes for this frame
- Saig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
- // add internal nodes of this frame
- Aig_ManForEachNode( pAig, pObj, i )
- pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- // save register inputs
- Saig_ManForEachLi( pAig, pObj, i )
- pObj->pData = Aig_ObjChild0Copy(pObj);
- // transfer to register outputs
- Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
- {
- pObjLo->pData = pObjLi->pData;
- Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObjLo->pData );
- }
- }
- Aig_ManCleanup( pFrames );
- return pFrames;
-}
-
-/**Function*************************************************************
-
- Synopsis [This procedure sets default values of interpolation parameters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK )
-{
- Inter_Check_t * p;
- // create solver
- p = ABC_CALLOC( Inter_Check_t, 1 );
- p->vOrLits = Vec_IntAlloc( 100 );
- p->vAndLits = Vec_IntAlloc( 100 );
- p->vAssLits = Vec_IntAlloc( 100 );
- // generate the timeframes
- p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
- assert( Aig_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
- assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
- // convert to CNF
- p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );
- p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
- // assign parameters
- p->nFramesK = nFramesK;
- p->nVars = p->pCnf->nVars;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [This procedure sets default values of interpolation parameters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Inter_CheckStop( Inter_Check_t * p )
-{
- if ( p == NULL )
- return;
- Vec_IntFree( p->vOrLits );
- Vec_IntFree( p->vAndLits );
- Vec_IntFree( p->vAssLits );
- Cnf_DataFree( p->pCnf );
- Aig_ManStop( p->pFrames );
- sat_solver_delete( p->pSat );
- ABC_FREE( p );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Creates one OR-gate: A + B = C.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Inter_CheckAddOrGate( Inter_Check_t * p, int iVarA, int iVarB, int iVarC )
-{
- int RetValue, pLits[3];
- // add A => C or !A + C
- pLits[0] = toLitCond(iVarA, 1);
- pLits[1] = toLitCond(iVarC, 0);
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
- // add B => C or !B + C
- pLits[0] = toLitCond(iVarB, 1);
- pLits[1] = toLitCond(iVarC, 0);
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
- // add !A & !B => !C or A + B + !C
- pLits[0] = toLitCond(iVarA, 0);
- pLits[1] = toLitCond(iVarB, 0);
- pLits[2] = toLitCond(iVarC, 1);
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates equality: A = B.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
-{
- int RetValue, pLits[3];
- // add A => B or !A + B
- pLits[0] = toLitCond(iVarA, 1);
- pLits[1] = toLitCond(iVarB, 0);
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
- // add B => A or !B + A
- pLits[0] = toLitCond(iVarB, 1);
- pLits[1] = toLitCond(iVarA, 0);
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
-}
-
-/**Function*************************************************************
-
- Synopsis [Perform the checking.]
-
- Description [Returns 1 if the check has passed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut )
-{
- Aig_Obj_t * pObj, * pObj2;
- int i, f, VarA, VarB, RetValue, Entry, status;
- int nRegs = Aig_ManPiNum(pCnfInt->pMan);
- assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
- assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
-
- // set runtime limit
- if ( nTimeNewOut )
- sat_solver_set_runtime_limit( p->pSat, nTimeNewOut );
-
- // add clauses to the SAT solver
- Cnf_DataLift( pCnfInt, p->nVars );
- for ( f = 0; f <= p->nFramesK; f++ )
- {
- // add clauses to the solver
- for ( i = 0; i < pCnfInt->nClauses; i++ )
- {
- RetValue = sat_solver_addclause( p->pSat, pCnfInt->pClauses[i], pCnfInt->pClauses[i+1] );
- assert( RetValue );
- }
- // add equality clauses for the flop variables
- Aig_ManForEachPi( pCnfInt->pMan, pObj, i )
- {
- pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
- Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
- }
- // add final clauses
- if ( f < p->nFramesK )
- {
- if ( f == Vec_IntSize(p->vOrLits) ) // find time here
- {
- // add literal to this frame
- VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
- Vec_IntPush( p->vOrLits, VarB );
- }
- else
- {
- // add OR gate for this frame
- VarA = Vec_IntEntry( p->vOrLits, f );
- VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
- Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
- Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
- }
- }
- else
- {
- // add AND gate for this frame
- VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
- Vec_IntPush( p->vAndLits, VarB );
- }
- // update variable IDs
- Cnf_DataLift( pCnfInt, pCnfInt->nVars + 1 );
- p->nVars += pCnfInt->nVars + 1;
- }
- Cnf_DataLift( pCnfInt, -p->nVars );
- assert( Vec_IntSize(p->vOrLits) == p->nFramesK );
-
- // collect the assumption literals
- Vec_IntClear( p->vAssLits );
- Vec_IntForEachEntry( p->vOrLits, Entry, i )
- Vec_IntPush( p->vAssLits, toLitCond(Entry, 0) );
- Vec_IntForEachEntry( p->vAndLits, Entry, i )
- Vec_IntPush( p->vAssLits, toLitCond(Entry, 1) );
-/*
- if ( pCnfInt->nLiterals == 3635 )
- {
- int s = 0;
- }
-*/
- // call the SAT solver
- status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssLits),
- Vec_IntArray(p->vAssLits) + Vec_IntSize(p->vAssLits),
- (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
- return status == l_False;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-ABC_NAMESPACE_IMPL_END
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 22:01:14 +0000