diff options
Diffstat (limited to 'src/aig/int/intM114p.c')
| -rw-r--r-- | src/aig/int/intM114p.c | 442 |
1 files changed, 0 insertions, 442 deletions
diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c deleted file mode 100644 index 0ad0552f..00000000 --- a/src/aig/int/intM114p.c +++ /dev/null @@ -1,442 +0,0 @@ -/**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 "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 - - |