summaryrefslogtreecommitdiffstats
path: root/src/aig/int/intCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/int/intCore.c')
-rw-r--r--src/aig/int/intCore.c286
1 files changed, 286 insertions, 0 deletions
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
new file mode 100644
index 00000000..d959ff07
--- /dev/null
+++ b/src/aig/int/intCore.c
@@ -0,0 +1,286 @@
+/**CFile****************************************************************
+
+ FileName [intCore.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Interpolation engine.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 24, 2008.]
+
+ Revision [$Id: intCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [This procedure sets default values of interpolation parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
+{
+ memset( p, 0, sizeof(Inter_ManParams_t) );
+ p->nBTLimit = 10000; // limit on the number of conflicts
+ p->nFramesMax = 40; // the max number timeframes to unroll
+ p->nFramesK = 1; // the number of timeframes to use in induction
+ p->fRewrite = 0; // use additional rewriting to simplify timeframes
+ p->fTransLoop = 1; // add transition into the init state under new PI var
+ p->fUsePudlak = 0; // use Pudluk interpolation procedure
+ p->fUseOther = 0; // use other undisclosed option
+ p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine
+ p->fCheckKstep = 1; // check using K-step induction
+ p->fUseBias = 0; // bias decisions to global variables
+ p->fUseBackward = 0; // perform backward interpolation
+ p->fVerbose = 0; // print verbose statistics
+}
+
+/**Function*************************************************************
+
+ Synopsis [Interplates while the number of conflicts is not exceeded.]
+
+ Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+
+ SideEffects [Does not check the property in 0-th frame.]
+
+ SeeAlso []
+
+***********************************************************************/
+int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth )
+{
+ extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
+ Inter_Man_t * p;
+ Aig_Man_t * pAigTemp;
+ int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
+ // sanity checks
+ assert( Saig_ManRegNum(pAig) > 0 );
+ assert( Saig_ManPiNum(pAig) > 0 );
+ assert( Saig_ManPoNum(pAig) == 1 );
+/*
+ if ( Inter_ManCheckInitialState(pAig) )
+ {
+ printf( "Property trivially fails in the initial state.\n" );
+ return 0;
+ }
+ if ( Inter_ManCheckAllStates(pAig) )
+ {
+ printf( "Property trivially holds in all states.\n" );
+ return 1;
+ }
+*/
+ // create interpolation manager
+ // can perform SAT sweeping and/or rewriting of this AIG...
+ p = Inter_ManCreate( pAig, pPars );
+ if ( pPars->fTransLoop )
+ p->pAigTrans = Inter_ManStartOneOutput( pAig, 0 );
+ else
+ p->pAigTrans = Inter_ManStartDuplicated( pAig );
+ // derive CNF for the transformed AIG
+clk = clock();
+ p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) );
+p->timeCnf += clock() - clk;
+ if ( pPars->fVerbose )
+ {
+ printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d. CNF: Var/Cla = %d/%d.\n",
+ Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
+ Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
+ p->pCnfAig->nVars, p->pCnfAig->nClauses );
+ }
+
+ // derive interpolant
+ *pDepth = -1;
+ p->nFrames = 1;
+ for ( s = 0; ; s++ )
+ {
+clk2 = clock();
+ // initial state
+ if ( pPars->fUseBackward )
+ p->pInter = Inter_ManStartOneOutput( pAig, 1 );
+ else
+ p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
+ assert( Aig_ManPoNum(p->pInter) == 1 );
+clk = clock();
+ p->pCnfInter = Cnf_Derive( p->pInter, 0 );
+p->timeCnf += clock() - clk;
+ // timeframes
+ p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward );
+clk = clock();
+ if ( pPars->fRewrite )
+ {
+ p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
+ Aig_ManStop( pAigTemp );
+// p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
+// Aig_ManStop( pAigTemp );
+ }
+p->timeRwr += clock() - clk;
+ // can also do SAT sweeping on the timeframes...
+clk = clock();
+ if ( pPars->fUseBackward )
+ p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );
+ else
+ p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );
+p->timeCnf += clock() - clk;
+ // report statistics
+ if ( pPars->fVerbose )
+ {
+ printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d. ",
+ s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
+ PRT( "Time", clock() - clk2 );
+ }
+ // iterate the interpolation procedure
+ for ( i = 0; ; i++ )
+ {
+ if ( p->nFrames + i >= pPars->nFramesMax )
+ {
+ if ( pPars->fVerbose )
+ printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
+ p->timeTotal = clock() - clkTotal;
+ Inter_ManStop( p );
+ return -1;
+ }
+
+ // perform interpolation
+ clk = clock();
+#ifdef ABC_USE_LIBRARIES
+ if ( pPars->fUseMiniSat )
+ {
+ assert( !pPars->fUseBackward );
+ RetValue = Inter_ManPerformOneStepM114p( p, pPars->fUsePudlak, pPars->fUseOther );
+ }
+ else
+#endif
+ RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward );
+
+ if ( pPars->fVerbose )
+ {
+ printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ",
+ i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
+ PRT( "Time", clock() - clk );
+ }
+ if ( RetValue == 0 ) // found a (spurious?) counter-example
+ {
+ if ( i == 0 ) // real counterexample
+ {
+ if ( pPars->fVerbose )
+ printf( "Found a real counterexample in the first frame.\n" );
+ p->timeTotal = clock() - clkTotal;
+ *pDepth = p->nFrames + 1;
+ Inter_ManStop( p );
+ return 0;
+ }
+ // likely spurious counter-example
+ p->nFrames += i;
+ Inter_ManClean( p );
+ break;
+ }
+ else if ( RetValue == -1 ) // timed out
+ {
+ if ( pPars->fVerbose )
+ printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
+ assert( p->nConfCur >= p->nConfLimit );
+ p->timeTotal = clock() - clkTotal;
+ Inter_ManStop( p );
+ return -1;
+ }
+ assert( RetValue == 1 ); // found new interpolant
+ // compress the interpolant
+clk = clock();
+ if ( p->pInterNew )
+ {
+ p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
+ Aig_ManStop( pAigTemp );
+ }
+p->timeRwr += clock() - clk;
+
+ // check if interpolant is trivial
+ if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
+ {
+// printf( "interpolant is constant 0\n" );
+ if ( pPars->fVerbose )
+ printf( "The problem is trivially true for all states.\n" );
+ p->timeTotal = clock() - clkTotal;
+ Inter_ManStop( p );
+ return 1;
+ }
+
+ // check containment of interpolants
+clk = clock();
+ if ( pPars->fCheckKstep ) // k-step unique-state induction
+ {
+ if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+ Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
+ else
+ Status = 0;
+ }
+ else // combinational containment
+ {
+ if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+ Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
+ else
+ Status = 0;
+ }
+p->timeEqu += clock() - clk;
+ if ( Status ) // contained
+ {
+ if ( pPars->fVerbose )
+ printf( "Proved containment of interpolants.\n" );
+ p->timeTotal = clock() - clkTotal;
+ Inter_ManStop( p );
+ return 1;
+ }
+ // save interpolant and convert it into CNF
+ if ( pPars->fTransLoop )
+ {
+ Aig_ManStop( p->pInter );
+ p->pInter = p->pInterNew;
+ }
+ else
+ {
+ p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
+ Aig_ManStop( pAigTemp );
+ Aig_ManStop( p->pInterNew );
+ // compress the interpolant
+clk = clock();
+ p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
+ Aig_ManStop( pAigTemp );
+p->timeRwr += clock() - clk;
+ }
+ p->pInterNew = NULL;
+ Cnf_DataFree( p->pCnfInter );
+clk = clock();
+ p->pCnfInter = Cnf_Derive( p->pInter, 0 );
+p->timeCnf += clock() - clk;
+ }
+ }
+ assert( 0 );
+ return RetValue;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 14:36:02 +0000