summaryrefslogtreecommitdiffstats
path: root/src/proof/int/intCheck.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/int/intCheck.c')
-rw-r--r--src/proof/int/intCheck.c305
1 files changed, 305 insertions, 0 deletions
diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
new file mode 100644
index 00000000..6b36fe30
--- /dev/null
+++ b/src/proof/int/intCheck.c
@@ -0,0 +1,305 @@
+/**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-06-30 18:55:53 +0000