diff options
Diffstat (limited to 'src/proof/int')
| -rw-r--r-- | src/proof/int/int.h | 94 | ||||
| -rw-r--r-- | src/proof/int/intCheck.c | 305 | ||||
| -rw-r--r-- | src/proof/int/intContain.c | 341 | ||||
| -rw-r--r-- | src/proof/int/intCore.c | 389 | ||||
| -rw-r--r-- | src/proof/int/intCtrex.c | 167 | ||||
| -rw-r--r-- | src/proof/int/intDup.c | 184 | ||||
| -rw-r--r-- | src/proof/int/intFrames.c | 115 | ||||
| -rw-r--r-- | src/proof/int/intInt.h | 142 | ||||
| -rw-r--r-- | src/proof/int/intInter.c | 145 | ||||
| -rw-r--r-- | src/proof/int/intM114.c | 320 | ||||
| -rw-r--r-- | src/proof/int/intM114p.c | 442 | ||||
| -rw-r--r-- | src/proof/int/intMan.c | 163 | ||||
| -rw-r--r-- | src/proof/int/intUtil.c | 108 | ||||
| -rw-r--r-- | src/proof/int/module.make | 11 |
14 files changed, 2926 insertions, 0 deletions
diff --git a/src/proof/int/int.h b/src/proof/int/int.h new file mode 100644 index 00000000..a93e3c93 --- /dev/null +++ b/src/proof/int/int.h @@ -0,0 +1,94 @@ +/**CFile**************************************************************** + + FileName [int.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: int.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__int__int_h +#define ABC__aig__int__int_h + + +/* + The interpolation algorithm implemented here was introduced in the paper: + K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13. +*/ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// simulation manager +typedef struct Inter_ManParams_t_ Inter_ManParams_t; +struct Inter_ManParams_t_ +{ + int nBTLimit; // limit on the number of conflicts + int nFramesMax; // the max number timeframes to unroll + int nSecLimit; // time limit in seconds + int nFramesK; // the number of timeframes to use in induction + int fRewrite; // use additional rewriting to simplify timeframes + int fTransLoop; // add transition into the init state under new PI var + int fUsePudlak; // use Pudluk interpolation procedure + int fUseOther; // use other undisclosed option + int fUseMiniSat; // use MiniSat-1.14p instead of internal proof engine + int fCheckKstep; // check using K-step induction + int fUseBias; // bias decisions to global variables + int fUseBackward; // perform backward interpolation + int fUseSeparate; // solve each output separately + int fDropSatOuts; // replace by 1 the solved outputs + int fDropInvar; // dump inductive invariant into file + int fVerbose; // print verbose statistics + int iFrameMax; // the time frame reached +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== intCore.c ==========================================================*/ +extern void Inter_ManSetDefaultParams( Inter_ManParams_t * p ); +extern int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame ); + + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + 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 + diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c new file mode 100644 index 00000000..58b408d7 --- /dev/null +++ b/src/proof/int/intContain.c @@ -0,0 +1,341 @@ +/**CFile**************************************************************** + + FileName [intContain.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Interpolant containment checking.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intContain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" +#include "src/proof/fra/fra.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks constainment of two interpolants.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) +{ + Aig_Man_t * pMiter, * pAigTemp; + int RetValue; + pMiter = Aig_ManCreateMiter( pNew, pOld, 1 ); +// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); +// Aig_ManStop( pAigTemp ); + RetValue = Fra_FraigMiterStatus( pMiter ); + if ( RetValue == -1 ) + { + pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); + RetValue = Fra_FraigMiterStatus( pAigTemp ); + Aig_ManStop( pAigTemp ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 ); + } + assert( RetValue != -1 ); + Aig_ManStop( pMiter ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Checks constainment of two interpolants.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ) +{ + Aig_Man_t * pMiter, * pAigTemp; + int RetValue; + pMiter = Aig_ManCreateMiter( pNew, pOld, 0 ); +// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); +// Aig_ManStop( pAigTemp ); + RetValue = Fra_FraigMiterStatus( pMiter ); + if ( RetValue == -1 ) + { + pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); + RetValue = Fra_FraigMiterStatus( pAigTemp ); + Aig_ManStop( pAigTemp ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 ); + } + assert( RetValue != -1 ); + Aig_ManStop( pMiter ); + return RetValue; +} + + +/**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_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg ) +{ + 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 + *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) ); + Saig_ManForEachLo( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreatePi( pFrames ); + Vec_PtrPush( *pvMapReg, pObj->pData ); + } + // 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; + Vec_PtrPush( *pvMapReg, pObjLo->pData ); + } + } + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while mapping PIs into the given array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl ) +{ + Aig_Obj_t * pObj; + int i; + assert( Aig_ManPoNum(pOld) == 1 ); + // create the PIs + Aig_ManCleanData( pOld ); + Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( pOld, pObj, i ) + pObj->pData = ppNewPis[i]; + // duplicate internal nodes + Aig_ManForEachNode( pOld, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add one PO to new + pObj = Aig_ManPo( pOld, 0 ); + Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); +} + + +/**Function************************************************************* + + Synopsis [Checks constainment of two interpolants inductively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t ** ppNodes; + Vec_Ptr_t * vMapRegs; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int f, nRegs, status; + nRegs = Saig_ManRegNum(pTrans); + assert( nRegs > 0 ); + // generate the timeframes + pFrames = Inter_ManFramesLatches( pTrans, nSteps, &vMapRegs ); + assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs ); + // add main constraints to the timeframes + ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs); + if ( !fBackward ) + { + // forward inductive check: p -> p -> ... -> !p + for ( f = 0; f < nSteps; f++ ) + Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 ); + Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 ); + } + else + { + // backward inductive check: p -> !p -> ... -> !p + Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 ); + for ( f = 1; f <= nSteps; f++ ) + Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 ); + } + Vec_PtrFree( vMapRegs ); + Aig_ManCleanup( pFrames ); + + // convert to CNF + pCnf = Cnf_Derive( pFrames, 0 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); +// Cnf_DataFree( pCnf ); +// Aig_ManStop( pFrames ); + + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + return 1; + } + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + +// Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps ); + + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + + sat_solver_delete( pSat ); + return status == l_False; +} +ABC_NAMESPACE_IMPL_END + +#include "src/proof/fra/fra.h" + +ABC_NAMESPACE_IMPL_START + + +/**Function************************************************************* + + Synopsis [Check if cex satisfies uniqueness constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames ) +{ + extern int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 ); + extern void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ); + extern void Fra_SmlSimulateOne( Fra_Sml_t * p ); + + Fra_Sml_t * pSml; + Vec_Int_t * vPis; + Aig_Obj_t * pObj, * pObj0; + int i, k, v, iBit, * pCounterEx; + int Counter; + if ( nFrames == 1 ) + return 1; +// if ( pSat->model.size == 0 ) + + // possible consequences here!!! + assert( 0 ); + + if ( sat_solver_nvars(pSat) == 0 ) + return 1; +// assert( Saig_ManPoNum(p) == 1 ); + assert( Aig_ManRegNum(p) > 0 ); + assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) ); + + // get the counter-example + vPis = Vec_IntAlloc( 100 ); + Aig_ManForEachPi( pCnf->pMan, pObj, k ) + Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] ); + assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) ); + pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize ); + Vec_IntFree( vPis ); + + // start a new sequential simulator + pSml = Fra_SmlStart( p, 0, nFrames, 1 ); + // assign simulation info for the registers + iBit = 0; + Aig_ManForEachLoSeq( p, pObj, i ) + Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], 0 ); + // assign simulation info for the primary inputs + for ( i = 0; i < nFrames; i++ ) + Aig_ManForEachPiSeq( p, pObj, k ) + Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i ); + assert( iBit == Aig_ManPiNum(pCnf->pMan) ); + // run simulation + Fra_SmlSimulateOne( pSml ); + + // check if the given output has failed +// RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) ); +// assert( RetValue ); + + // check values at the internal nodes + Counter = 0; + for ( i = 0; i < nFrames; i++ ) + for ( k = i+1; k < nFrames; k++ ) + { + for ( v = 0; v < Aig_ManRegNum(p); v++ ) + { + pObj0 = Aig_ManLo(p, v); + if ( !Fra_SmlNodesCompareInFrame( pSml, pObj0, pObj0, i, k ) ) + break; + } + if ( v == Aig_ManRegNum(p) ) + Counter++; + } + printf( "Uniquness does not hold in %d frames.\n", Counter ); + + Fra_SmlStop( pSml ); + ABC_FREE( pCounterEx ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c new file mode 100644 index 00000000..3bd111be --- /dev/null +++ b/src/proof/int/intCore.c @@ -0,0 +1,389 @@ +/**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" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// 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->nSecLimit = 0; // time limit in seconds + p->nFramesK = 1; // the number of timeframes to use in induction + p->fRewrite = 0; // use additional rewriting to simplify timeframes + p->fTransLoop = 0; // 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->fUseSeparate = 0; // solve each output separately + p->fDropSatOuts = 0; // replace by 1 the solved outputs + p->fVerbose = 0; // print verbose statistics + p->iFrameMax =-1; +} + +/**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 * piFrame ) +{ + extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ); + Inter_Man_t * p; + Inter_Check_t * pCheck = NULL; + Aig_Man_t * pAigTemp; + int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp; + int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0; + + // sanity checks + assert( Saig_ManRegNum(pAig) > 0 ); + assert( Saig_ManPiNum(pAig) > 0 ); + assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 ); + if ( pPars->fVerbose && Saig_ManConstrNum(pAig) ) + printf( "Performing interpolation with %d constraints...\n", Saig_ManConstrNum(pAig) ); + + if ( Inter_ManCheckInitialState(pAig) ) + { + *piFrame = 0; + 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 + *piFrame = -1; + p->nFrames = 1; + for ( s = 0; ; s++ ) + { + Cnf_Dat_t * pCnfInter2; + +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->pCnfFrames = Cnf_DeriveSimple( 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) ); + ABC_PRT( "Time", clock() - clk2 ); + } + + + ////////////////////////////////////////// + // start containment checking + if ( !(pPars->fTransLoop || pPars->fUseBackward) ) + { + pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK ); + // try new containment check for the initial state +clk = clock(); + pCnfInter2 = Cnf_Derive( p->pInter, 1 ); +p->timeCnf += clock() - clk; + RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut ); +// assert( RetValue == 0 ); + Cnf_DataFree( pCnfInter2 ); + if ( p->vInters ) + Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) ); + } + ////////////////////////////////////////// + + // 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, 0 ); + Inter_CheckStop( pCheck ); + 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, nTimeNewOut ); + + 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 ); + ABC_PRT( "Time", clock() - clk ); + } + // remember the number of timeframes completed + pPars->iFrameMax = i + 1 + p->nFrames; + if ( RetValue == 0 ) // found a (spurious?) counter-example + { + if ( i == 0 ) // real counterexample + { + if ( pPars->fVerbose ) + printf( "Found a real counterexample in frame %d.\n", p->nFrames ); + p->timeTotal = clock() - clkTotal; + *piFrame = p->nFrames; +// pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose ); + { + int RetValue; + Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc; + Saig_ParBmcSetDefaultParams( pParsBmc ); + pParsBmc->nConfLimit = 100000000; + pParsBmc->nStart = p->nFrames; + pParsBmc->fVerbose = pPars->fVerbose; + RetValue = Saig_ManBmcScalable( pAig, pParsBmc ); + if ( RetValue == 1 ) + printf( "Error: The problem should be SAT but it is UNSAT.\n" ); + else if ( RetValue == -1 ) + printf( "Error: The problem timed out.\n" ); + } + Inter_ManStop( p, 0 ); + Inter_CheckStop( pCheck ); + return 0; + } + // likely spurious counter-example + p->nFrames += i; + Inter_ManClean( p ); + break; + } + else if ( RetValue == -1 ) + { + if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out + { + if ( pPars->fVerbose ) + printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit ); + } + else + { + assert( p->nConfCur >= p->nConfLimit ); + if ( pPars->fVerbose ) + printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit ); + } + p->timeTotal = clock() - clkTotal; + Inter_ManStop( p, 0 ); + Inter_CheckStop( pCheck ); + return -1; + } + assert( RetValue == 1 ); // found new interpolant + // compress the interpolant +clk = clock(); + if ( p->pInterNew ) + { +// Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 ); + p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 ); +// p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 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, 1 ); + Inter_CheckStop( pCheck ); + 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) ) + { + if ( pPars->fTransLoop || pPars->fUseBackward ) + Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward ); + else + { // new containment check +clk2 = clock(); + pCnfInter2 = Cnf_Derive( p->pInterNew, 1 ); +p->timeCnf += clock() - clk2; +timeTemp = clock() - clk2; + + Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut ); + Cnf_DataFree( pCnfInter2 ); + if ( p->vInters ) + Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) ); + } + } + 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 - timeTemp; + if ( Status ) // contained + { + if ( pPars->fVerbose ) + printf( "Proved containment of interpolants.\n" ); + p->timeTotal = clock() - clkTotal; + Inter_ManStop( p, 1 ); + Inter_CheckStop( pCheck ); + return 1; + } + if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) + { + printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit ); + p->timeTotal = clock() - clkTotal; + Inter_ManStop( p, 1 ); + Inter_CheckStop( pCheck ); + return -1; + } + // save interpolant and convert it into CNF + if ( pPars->fTransLoop ) + { + Aig_ManStop( p->pInter ); + p->pInter = p->pInterNew; + } + else + { + if ( pPars->fUseBackward ) + { + 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; + } + else // forward with the new containment checking (using only the frontier) + { + Aig_ManStop( p->pInter ); + p->pInter = p->pInterNew; + } + } + p->pInterNew = NULL; + Cnf_DataFree( p->pCnfInter ); +clk = clock(); + p->pCnfInter = Cnf_Derive( p->pInter, 0 ); +p->timeCnf += clock() - clk; + } + + // start containment checking + Inter_CheckStop( pCheck ); + } + assert( 0 ); + return RetValue; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c new file mode 100644 index 00000000..9ba8c9df --- /dev/null +++ b/src/proof/int/intCtrex.c @@ -0,0 +1,167 @@ +/**CFile**************************************************************** + + FileName [intCtrex.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Counter-example generation after disproving the property.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intCtrex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" +#include "src/proof/ssw/ssw.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Unroll the circuit the given number of timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + assert( Saig_ManPoNum(pAig) == 1 ); + 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_ManConst0( 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) ); + if ( f == nFrames - 1 ) + break; + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLi->pData = Aig_ObjChild0Copy(pObjLi); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + // create POs for the output of the last frame + pObj = Aig_ManPo( pAig, 0 ); + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Run the SAT solver on the unrolled instance.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) +{ + int nConfLimit = 1000000; + Abc_Cex_t * pCtrex = NULL; + Aig_Man_t * pFrames; + sat_solver * pSat; + Cnf_Dat_t * pCnf; + int status, clk = clock(); + Vec_Int_t * vCiIds; + // create timeframes + assert( Saig_ManPoNum(pAig) == 1 ); + pFrames = Inter_ManFramesBmc( pAig, nFrames ); + // derive CNF + pCnf = Cnf_Derive( pFrames, 0 ); + Cnf_DataTranformPolarity( pCnf, 0 ); + vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); + Aig_ManStop( pFrames ); + // convert into SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Cnf_DataFree( pCnf ); + if ( pSat == NULL ) + { + printf( "Counter-example generation in command \"int\" has failed.\n" ); + printf( "Use command \"bmc2\" to produce a valid counter-example.\n" ); + Vec_IntFree( vCiIds ); + return NULL; + } + // simplify the problem + status = sat_solver_simplify(pSat); + if ( status == 0 ) + { + Vec_IntFree( vCiIds ); + sat_solver_delete( pSat ); + return NULL; + } + // solve the miter + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); + pCtrex->iFrame = nFrames - 1; + pCtrex->iPo = 0; + for ( i = 0; i < Vec_IntSize(vCiIds); i++ ) + if ( pModel[i] ) + Abc_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i ); + ABC_FREE( pModel ); + } + // free the sat_solver + sat_solver_delete( pSat ); + Vec_IntFree( vCiIds ); + // verify counter-example + status = Saig_ManVerifyCex( pAig, pCtrex ); + if ( status == 0 ) + printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" ); + // report the results + if ( fVerbose ) + { + ABC_PRT( "Total ctrex generation time", clock() - clk ); + } + return pCtrex; + +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intDup.c b/src/proof/int/intDup.c new file mode 100644 index 00000000..551473ef --- /dev/null +++ b/src/proof/int/intDup.c @@ -0,0 +1,184 @@ +/**CFile**************************************************************** + + FileName [intDup.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Specialized AIG duplication procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create trivial AIG manager for the init state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManStartInitState( int nRegs ) +{ + Aig_Man_t * p; + Aig_Obj_t * pRes; + Aig_Obj_t ** ppInputs; + int i; + assert( nRegs > 0 ); + ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs ); + p = Aig_ManStart( nRegs ); + for ( i = 0; i < nRegs; i++ ) + ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) ); + pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND ); + Aig_ObjCreatePo( p, pRes ); + ABC_FREE( ppInputs ); + return p; +} + +/**Function************************************************************* + + Synopsis [Duplicate the AIG w/o POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( Aig_ManRegNum(p) > 0 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // set registers + pNew->nTruePis = p->nTruePis; + pNew->nTruePos = Saig_ManConstrNum(p); + pNew->nRegs = p->nRegs; + // duplicate internal nodes + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + + // create constraint outputs + Saig_ManForEachPo( p, pObj, i ) + { + if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) ) + continue; + Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); + } + + // create register inputs with MUXes + Saig_ManForEachLi( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ManCleanup( pNew ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicate the AIG w/o POs and transforms to transit into init state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized" + int i; + assert( Aig_ManRegNum(p) > 0 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + { + if ( i == Saig_ManPiNum(p) ) + pCtrl = Aig_ObjCreatePi( pNew ); + pObj->pData = Aig_ObjCreatePi( pNew ); + } + // set registers + pNew->nRegs = fAddFirstPo? 0 : p->nRegs; + pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1; + pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p); + // duplicate internal nodes + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + + // create constraint outputs + Saig_ManForEachPo( p, pObj, i ) + { + if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) ) + continue; + Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); + } + + // add the PO + if ( fAddFirstPo ) + { + pObj = Aig_ManPo( p, 0 ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + else + { + // create register inputs with MUXes + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + { + pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); + // pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) ); + Aig_ObjCreatePo( pNew, pObj ); + } + } + Aig_ManCleanup( pNew ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c new file mode 100644 index 00000000..0fbab6cb --- /dev/null +++ b/src/proof/int/intFrames.c @@ -0,0 +1,115 @@ +/**CFile**************************************************************** + + FileName [intFrames.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Sequential AIG unrolling for interpolation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intFrames.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// 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. The only POs of the + manager is the property output of the last timeframe.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 ); + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + if ( fAddRegOuts ) + { + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + } + else + { + 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) ); + // add outputs for constraints + Saig_ManForEachPo( pAig, pObj, i ) + { + if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) ) + continue; + Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); + } + if ( f == nFrames - 1 ) + break; + // 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; + } + // create POs for each register output + if ( fAddRegOuts ) + { + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + } + // create the only PO of the manager + else + { + pObj = Aig_ManPo( pAig, 0 ); + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intInt.h b/src/proof/int/intInt.h new file mode 100644 index 00000000..6a033d85 --- /dev/null +++ b/src/proof/int/intInt.h @@ -0,0 +1,142 @@ +/**CFile**************************************************************** + + FileName [intInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__int__intInt_h +#define ABC__aig__int__intInt_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "src/aig/saig/saig.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/sat/bsat/satStore.h" +#include "int.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// interpolation manager +typedef struct Inter_Man_t_ Inter_Man_t; +struct Inter_Man_t_ +{ + // AIG manager + Aig_Man_t * pAig; // the original AIG manager + Aig_Man_t * pAigTrans; // the transformed original AIG manager + Cnf_Dat_t * pCnfAig; // CNF for the original manager + // interpolant + Aig_Man_t * pInter; // the current interpolant + Cnf_Dat_t * pCnfInter; // CNF for the current interplant + // timeframes + Aig_Man_t * pFrames; // the timeframes + Cnf_Dat_t * pCnfFrames; // CNF for the timeframes + // other data + Vec_Int_t * vVarsAB; // the variables participating in + // temporary place for the new interpolant + Aig_Man_t * pInterNew; + Vec_Ptr_t * vInters; + // parameters + int nFrames; // the number of timeframes + int nConfCur; // the current number of conflicts + int nConfLimit; // the limit on the number of conflicts + int fVerbose; // the verbosiness flag + // runtime + int timeRwr; + int timeCnf; + int timeSat; + int timeInt; + int timeEqu; + int timeOther; + int timeTotal; +}; + +// containment checking manager +typedef struct Inter_Check_t_ Inter_Check_t; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== intCheck.c ============================================================*/ +extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK ); +extern void Inter_CheckStop( Inter_Check_t * p ); +extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, int nTimeNewOut ); + +/*=== intContain.c ============================================================*/ +extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ); +extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ); +extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ); + +/*=== intCtrex.c ============================================================*/ +extern void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ); + +/*=== intDup.c ============================================================*/ +extern Aig_Man_t * Inter_ManStartInitState( int nRegs ); +extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ); +extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ); + +/*=== intFrames.c ============================================================*/ +extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts ); + +/*=== intMan.c ============================================================*/ +extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars ); +extern void Inter_ManClean( Inter_Man_t * p ); +extern void Inter_ManStop( Inter_Man_t * p, int fProved ); + +/*=== intM114.c ============================================================*/ +extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut ); + +/*=== intM114p.c ============================================================*/ +#ifdef ABC_USE_LIBRARIES +extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther ); +#endif + +/*=== intUtil.c ============================================================*/ +extern int Inter_ManCheckInitialState( Aig_Man_t * p ); +extern int Inter_ManCheckAllStates( Aig_Man_t * p ); + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/int/intInter.c b/src/proof/int/intInter.c new file mode 100644 index 00000000..ef32294b --- /dev/null +++ b/src/proof/int/intInter.c @@ -0,0 +1,145 @@ +/**CFile**************************************************************** + + FileName [intInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Experimental procedures to derive and compare interpolants.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther ) +{ + Aig_Man_t * pInterC; + assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) ); + pInterC = Aig_ManDupSimple( pInter ); + Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 ); + assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) ); + return pInterC; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManVerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) +{ + extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); + Aig_Man_t * pLower, * pUpper, * pInterC; + int RetValue1, RetValue2; + + pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 ); + pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 ); + Aig_ManFlipFirstPo( pUpper ); + + pInterC = Inter_ManDupExpand( pInter, pLower ); + RetValue1 = Inter_ManCheckContainment( pLower, pInterC ); + Aig_ManStop( pInterC ); + + pInterC = Inter_ManDupExpand( pInter, pUpper ); + RetValue2 = Inter_ManCheckContainment( pInterC, pUpper ); + Aig_ManStop( pInterC ); + + if ( RetValue1 && RetValue2 ) + printf( "Im is correct.\n" ); + if ( !RetValue1 ) + printf( "Property A => Im fails.\n" ); + if ( !RetValue2 ) + printf( "Property Im => !B fails.\n" ); + + Aig_ManStop( pLower ); + Aig_ManStop( pUpper ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManVerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) +{ + extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); + Aig_Man_t * pLower, * pUpper, * pInterC; + int RetValue1, RetValue2; + + pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 ); + pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 ); + Aig_ManFlipFirstPo( pUpper ); + + pInterC = Inter_ManDupExpand( pInter, pLower ); +//Aig_ManPrintStats( pLower ); +//Aig_ManPrintStats( pUpper ); +//Aig_ManPrintStats( pInterC ); +//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL ); + RetValue1 = Inter_ManCheckContainment( pLower, pInterC ); + Aig_ManStop( pInterC ); + + pInterC = Inter_ManDupExpand( pInter, pUpper ); + RetValue2 = Inter_ManCheckContainment( pInterC, pUpper ); + Aig_ManStop( pInterC ); + + if ( RetValue1 && RetValue2 ) + printf( "Ip is correct.\n" ); + if ( !RetValue1 ) + printf( "Property A => Ip fails.\n" ); + if ( !RetValue2 ) + printf( "Property Ip => !B fails.\n" ); + + Aig_ManStop( pLower ); + Aig_ManStop( pUpper ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c new file mode 100644 index 00000000..139c9bbd --- /dev/null +++ b/src/proof/int/intM114.c @@ -0,0 +1,320 @@ +/**CFile**************************************************************** + + FileName [intM114.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Intepolation using ABC's proof generator added to MiniSat-1.14c.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intM114.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the SAT solver for one interpolation run.] + + Description [pInter is the previous interpolant. pAig is one time frame. + pFrames is the unrolled time frames.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Inter_ManDeriveSatSolver( + Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, + Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, + Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, + Vec_Int_t * vVarsAB, int fUseBackward ) +{ + sat_solver * pSat; + Aig_Obj_t * pObj, * pObj2; + int i, Lits[2]; + +//Aig_ManDumpBlif( pInter, "out_inter.blif", NULL, NULL ); +//Aig_ManDumpBlif( pAig, "out_aig.blif", NULL, NULL ); +//Aig_ManDumpBlif( pFrames, "out_frames.blif", NULL, NULL ); + + // sanity checks + assert( Aig_ManRegNum(pInter) == 0 ); + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pFrames) == 0 ); + assert( Aig_ManPoNum(pInter) == 1 ); + assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 ); + assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); +// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); + + // prepare CNFs + Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); + + // start the solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars ); + + // add clauses of A + // interpolant + for ( i = 0; i < pCnfInter->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) ) + { + sat_solver_delete( pSat ); + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); + return NULL; + } + } + // connector clauses + if ( fUseBackward ) + { + Saig_ManForEachLi( pAig, pObj2, i ) + { + if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) ) + pObj = Aig_ManPi( pInter, i ); + else + { + assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) ); + pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i ); + } + + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + else + { + Aig_ManForEachPi( pInter, pObj, i ) + { + pObj2 = Saig_ManLo( pAig, i ); + + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + // one timeframe + for ( i = 0; i < pCnfAig->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Vec_IntClear( vVarsAB ); + if ( fUseBackward ) + { + Aig_ManForEachPo( pFrames, pObj, i ) + { + assert( pCnfFrames->pVarNums[pObj->Id] >= 0 ); + Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); + + pObj2 = Saig_ManLo( pAig, i ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + else + { + Aig_ManForEachPi( pFrames, pObj, i ) + { + if ( i == Aig_ManRegNum(pAig) ) + break; + Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); + + pObj2 = Saig_ManLi( pAig, i ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + // add clauses of B + sat_solver_store_mark_clauses_a( pSat ); + for ( i = 0; i < pCnfFrames->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) + { + pSat->fSolved = 1; + break; + } + } + sat_solver_store_mark_roots( pSat ); + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Performs one SAT run with interpolation.] + + Description [Returns 1 if proven. 0 if failed. -1 if undecided.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut ) +{ + sat_solver * pSat; + void * pSatCnf = NULL; + Inta_Man_t * pManInterA; +// Intb_Man_t * pManInterB; + int * pGlobalVars; + int clk, status, RetValue; + int i, Var; +// assert( p->pInterNew == NULL ); + + // derive the SAT solver + pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward ); + if ( pSat == NULL ) + { + p->pInterNew = NULL; + return 1; + } + + // set runtime limit + if ( nTimeNewOut ) + sat_solver_set_runtime_limit( pSat, nTimeNewOut ); + + // collect global variables + pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) ); + Vec_IntForEachEntry( p->vVarsAB, Var, i ) + pGlobalVars[Var] = 1; + pSat->pGlobalVars = fUseBias? pGlobalVars : NULL; + + // solve the problem +clk = clock(); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + p->nConfCur = pSat->stats.conflicts; +p->timeSat += clock() - clk; + + pSat->pGlobalVars = NULL; + ABC_FREE( pGlobalVars ); + if ( status == l_False ) + { + pSatCnf = sat_solver_store_release( pSat ); + RetValue = 1; + } + else if ( status == l_True ) + { + RetValue = 0; + } + else + { + RetValue = -1; + } + sat_solver_delete( pSat ); + if ( pSatCnf == NULL ) + return RetValue; + + // create the resulting manager +clk = clock(); +/* + if ( !fUseIp ) + { + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); + Inta_ManFree( pManInterA ); + } + else + { + Aig_Man_t * pInterNew2; + int RetValue; + + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); +// Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew ); + Inta_ManFree( pManInterA ); + + pManInterB = Intb_ManAlloc(); + pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 ); + Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 ); + Intb_ManFree( pManInterB ); + + // check relationship + RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew ); + if ( RetValue ) + printf( "Equivalence \"Ip == Im\" holds\n" ); + else + { +// printf( "Equivalence \"Ip == Im\" does not hold\n" ); + RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew ); + if ( RetValue ) + printf( "Containment \"Ip -> Im\" holds\n" ); + else + printf( "Containment \"Ip -> Im\" does not hold\n" ); + + RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 ); + if ( RetValue ) + printf( "Containment \"Im -> Ip\" holds\n" ); + else + printf( "Containment \"Im -> Ip\" does not hold\n" ); + } + + Aig_ManStop( pInterNew2 ); + } +*/ + + pManInterA = Inta_ManAlloc(); + p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, p->vVarsAB, 0 ); + Inta_ManFree( pManInterA ); + +p->timeInt += clock() - clk; + Sto_ManFree( (Sto_Man_t *)pSatCnf ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c new file mode 100644 index 00000000..7c011426 --- /dev/null +++ b/src/proof/int/intM114p.c @@ -0,0 +1,442 @@ +/**CFile**************************************************************** + + FileName [intM114p.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Intepolation using interfaced to MiniSat-1.14p.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intM114p.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" +#include "src/sat/psat/m114p.h" + +#ifdef ABC_USE_LIBRARIES + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the SAT solver for one interpolation run.] + + Description [pInter is the previous interpolant. pAig is one time frame. + pFrames is the unrolled time frames.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +M114p_Solver_t Inter_ManDeriveSatSolverM114p( + Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, + Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, + Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, + Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars ) +{ + M114p_Solver_t pSat; + Aig_Obj_t * pObj, * pObj2; + int i, Lits[2]; + + // sanity checks + assert( Aig_ManRegNum(pInter) == 0 ); + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pFrames) == 0 ); + assert( Aig_ManPoNum(pInter) == 1 ); + assert( Aig_ManPoNum(pFrames) == 1 ); + assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); +// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); + + // prepare CNFs + Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); + + *pvMapRoots = Vec_IntAlloc( 10000 ); + *pvMapVars = Vec_IntAlloc( 0 ); + Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 ); + for ( i = 0; i < pCnfFrames->nVars; i++ ) + Vec_IntWriteEntry( *pvMapVars, i, -2 ); + + // start the solver + pSat = M114p_SolverNew( 1 ); + M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars ); + + // add clauses of A + // interpolant + for ( i = 0; i < pCnfInter->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Aig_ManForEachPi( pInter, pObj, i ) + { + pObj2 = Saig_ManLo( pAig, i ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // one timeframe + for ( i = 0; i < pCnfAig->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Aig_ManForEachPi( pFrames, pObj, i ) + { + if ( i == Aig_ManRegNum(pAig) ) + break; +// Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); + Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i ); + + pObj2 = Saig_ManLi( pAig, i ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // add clauses of B + for ( i = 0; i < pCnfFrames->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 1 ); + if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) + { +// assert( 0 ); + break; + } + } + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); + return pSat; +} + + +/**Function************************************************************* + + Synopsis [Performs one resolution step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManResolveM114p( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar ) +{ + int i, k, iLit = -1, fFound = 0; + // find the variable in the clause + for ( i = 0; i < vResolvent->nSize; i++ ) + if ( lit_var(vResolvent->pArray[i]) == iVar ) + { + iLit = vResolvent->pArray[i]; + vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize]; + break; + } + assert( iLit != -1 ); + // add other variables + for ( i = 0; i < nLits; i++ ) + { + if ( lit_var(pLits[i]) == iVar ) + { + assert( iLit == lit_neg(pLits[i]) ); + fFound = 1; + continue; + } + // check if this literal appears + for ( k = 0; k < vResolvent->nSize; k++ ) + if ( vResolvent->pArray[k] == pLits[i] ) + break; + if ( k < vResolvent->nSize ) + continue; + // add this literal + Vec_IntPush( vResolvent, pLits[i] ); + } + assert( fFound ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + Vec_Int_t * vLiterals, * vClauses, * vResolvent; + int * pLitsNext, nLitsNext, nOffset, iLit; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, v, iVar; + assert( M114p_SolverProofIsReady(s) ); + vInters = Vec_PtrAlloc( 1000 ); + + vLiterals = Vec_IntAlloc( 10000 ); + vClauses = Vec_IntAlloc( 1000 ); + vResolvent = Vec_IntAlloc( 100 ); + + // create elementary variables + p = Aig_ManStart( 10000 ); + Vec_IntForEachEntry( vMapVars, iVar, i ) + if ( iVar >= 0 ) + Aig_IthVar(p, iVar); + // process root clauses + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + pInter = Aig_ManConst1(p); + else // clause of A + pInter = Aig_ManConst0(p); + Vec_PtrPush( vInters, pInter ); + + // save the root clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, nLits ); + for ( v = 0; v < nLits; v++ ) + Vec_IntPush( vLiterals, pLits[v] ); + } + assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + pInter = Vec_PtrEntry( vInters, pClauses[0] ); + + // initialize the resolvent + nOffset = Vec_IntEntry( vClauses, pClauses[0] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Vec_IntClear( vResolvent ); + for ( v = 0; v < nLitsNext; v++ ) + Vec_IntPush( vResolvent, pLitsNext[v] ); + + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + + // resolve it with the next clause + nOffset = Vec_IntEntry( vClauses, pClauses[k+1] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Inter_ManResolveM114p( vResolvent, pLitsNext, nLitsNext, pVars[k] ); + + if ( iVar == -1 ) // var of A + pInter = Aig_Or( p, pInter, pInter2 ); + else if ( iVar == -2 ) // var of B + pInter = Aig_And( p, pInter, pInter2 ); + else // var of C + { + // check polarity of the pivot variable in the clause + for ( v = 0; v < nLitsNext; v++ ) + if ( lit_var(pLitsNext[v]) == pVars[k] ) + break; + assert( v < nLitsNext ); + pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) ); + pInter = Aig_Mux( p, pVar, pInter, pInter2 ); + } + } + Vec_PtrPush( vInters, pInter ); + + // store the resulting clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) ); + Vec_IntForEachEntry( vResolvent, iLit, v ) + Vec_IntPush( vLiterals, iLit ); + } + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause + Vec_PtrFree( vInters ); + Vec_IntFree( vLiterals ); + Vec_IntFree( vClauses ); + Vec_IntFree( vResolvent ); + Aig_ObjCreatePo( p, pInter ); + Aig_ManCleanup( p ); + return p; +} + + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, iVar; + int nClauses; + + nClauses = M114p_SolverProofClauseNum(s); + + assert( M114p_SolverProofIsReady(s) ); + + vInters = Vec_PtrAlloc( 1000 ); + // process root clauses + p = Aig_ManStart( 10000 ); + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + pInter = Aig_ManConst1(p); + else // clause of A + { + pInter = Aig_ManConst0(p); + for ( k = 0; k < nLits; k++ ) + { + iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) ); + if ( iVar < 0 ) // var of A or B + continue; + // this is a variable of C + pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) ); + pInter = Aig_Or( p, pInter, pVar ); + } + } + Vec_PtrPush( vInters, pInter ); + } +// assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + pInter = Vec_PtrEntry( vInters, pClauses[0] ); + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + if ( iVar == -1 ) // var of A + pInter = Aig_Or( p, pInter, pInter2 ); + else // var of B or C + pInter = Aig_And( p, pInter, pInter2 ); + } + Vec_PtrPush( vInters, pInter ); + } + + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + Vec_PtrFree( vInters ); + Aig_ObjCreatePo( p, pInter ); + Aig_ManCleanup( p ); + assert( Aig_ManCheck(p) ); + return p; +} + + +/**Function************************************************************* + + Synopsis [Performs one SAT run with interpolation.] + + Description [Returns 1 if proven. 0 if failed. -1 if undecided.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther ) +{ + M114p_Solver_t pSat; + Vec_Int_t * vMapRoots, * vMapVars; + int clk, status, RetValue; + assert( p->pInterNew == NULL ); + // derive the SAT solver + pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter, + p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, + &vMapRoots, &vMapVars ); + // solve the problem +clk = clock(); + status = M114p_SolverSolve( pSat, NULL, NULL, 0 ); + p->nConfCur = M114p_SolverGetConflictNum( pSat ); +p->timeSat += clock() - clk; + if ( status == 0 ) + { + RetValue = 1; +// Inter_ManpInterpolateM114Report( pSat, vMapRoots, vMapVars ); + +clk = clock(); + if ( fUsePudlak ) + p->pInterNew = Inter_ManInterpolateM114pPudlak( pSat, vMapRoots, vMapVars ); + else + p->pInterNew = Inter_ManpInterpolateM114( pSat, vMapRoots, vMapVars ); +p->timeInt += clock() - clk; + } + else if ( status == 1 ) + { + RetValue = 0; + } + else + { + RetValue = -1; + } + M114p_SolverDelete( pSat ); + Vec_IntFree( vMapRoots ); + Vec_IntFree( vMapVars ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END + +#endif + + diff --git a/src/proof/int/intMan.c b/src/proof/int/intMan.c new file mode 100644 index 00000000..6fd81d7a --- /dev/null +++ b/src/proof/int/intMan.c @@ -0,0 +1,163 @@ +/**CFile**************************************************************** + + FileName [intMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Interpolation manager procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" +#include "src/aig/ioa/ioa.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars ) +{ + Inter_Man_t * p; + // create interpolation manager + p = ABC_ALLOC( Inter_Man_t, 1 ); + memset( p, 0, sizeof(Inter_Man_t) ); + p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) ); + p->nConfLimit = pPars->nBTLimit; + p->fVerbose = pPars->fVerbose; + p->pAig = pAig; + if ( pPars->fDropInvar ) + p->vInters = Vec_PtrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Cleans the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManClean( Inter_Man_t * p ) +{ + if ( p->vInters ) + { + Aig_Man_t * pMan; + int i; + Vec_PtrForEachEntry( Aig_Man_t *, p->vInters, pMan, i ) + Aig_ManStop( pMan ); + Vec_PtrClear( p->vInters ); + } + if ( p->pCnfInter ) + Cnf_DataFree( p->pCnfInter ); + if ( p->pCnfFrames ) + Cnf_DataFree( p->pCnfFrames ); + if ( p->pInter ) + Aig_ManStop( p->pInter ); + if ( p->pFrames ) + Aig_ManStop( p->pFrames ); +} + +/**Function************************************************************* + + Synopsis [Writes interpolant into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManInterDump( Inter_Man_t * p, int fProved ) +{ + Aig_Man_t * pMan; + pMan = Aig_ManDupArray( p->vInters ); + Ioa_WriteAiger( pMan, "invar.aig", 0, 0 ); + Aig_ManStop( pMan ); + if ( fProved ) + printf( "Inductive invariant is dumped into file \"invar.aig\".\n" ); + else + printf( "Interpolants are dumped into file \"inter.aig\".\n" ); +} + +/**Function************************************************************* + + Synopsis [Frees the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManStop( Inter_Man_t * p, int fProved ) +{ + if ( p->fVerbose ) + { + p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu; + printf( "Runtime statistics:\n" ); + ABC_PRTP( "Rewriting ", p->timeRwr, p->timeTotal ); + ABC_PRTP( "CNF mapping", p->timeCnf, p->timeTotal ); + ABC_PRTP( "SAT solving", p->timeSat, p->timeTotal ); + ABC_PRTP( "Interpol ", p->timeInt, p->timeTotal ); + ABC_PRTP( "Containment", p->timeEqu, p->timeTotal ); + ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); + ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + } + + if ( p->vInters ) + Inter_ManInterDump( p, fProved ); + + if ( p->pCnfAig ) + Cnf_DataFree( p->pCnfAig ); + if ( p->pAigTrans ) + Aig_ManStop( p->pAigTrans ); + if ( p->pInterNew ) + Aig_ManStop( p->pInterNew ); + Inter_ManClean( p ); + Vec_PtrFreeP( &p->vInters ); + Vec_IntFreeP( &p->vVarsAB ); + ABC_FREE( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/intUtil.c b/src/proof/int/intUtil.c new file mode 100644 index 00000000..8027bdef --- /dev/null +++ b/src/proof/int/intUtil.c @@ -0,0 +1,108 @@ +/**CFile**************************************************************** + + FileName [intUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Various interpolation utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Returns 1 if the property fails in the initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckInitialState( Aig_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + Aig_Obj_t * pObj; + sat_solver * pSat; + int i, status; + int clk = clock(); + pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 ); + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + return 0; + } + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + ABC_PRT( "Time", clock() - clk ); + if ( status == l_True ) + { + p->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), 1 ); + Saig_ManForEachPi( p, pObj, i ) + if ( sat_solver_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pObj)] ) ) + Abc_InfoSetBit( p->pSeqModel->pData, Aig_ManRegNum(p) + i ); + } + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + return status == l_True; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the property holds in all states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckAllStates( Aig_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int status; + int clk = clock(); + pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Cnf_DataFree( pCnf ); + if ( pSat == NULL ) + return 1; + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + sat_solver_delete( pSat ); + ABC_PRT( "Time", clock() - clk ); + return status == l_False; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int/module.make b/src/proof/int/module.make new file mode 100644 index 00000000..4a66b6ca --- /dev/null +++ b/src/proof/int/module.make @@ -0,0 +1,11 @@ +SRC += src/proof/int/intCheck.c \ + src/proof/int/intContain.c \ + src/proof/int/intCore.c \ + src/proof/int/intCtrex.c \ + src/proof/int/intDup.c \ + src/proof/int/intFrames.c \ + src/proof/int/intInter.c \ + src/proof/int/intM114.c \ + src/proof/int/intM114p.c \ + src/proof/int/intMan.c \ + src/proof/int/intUtil.c |