diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
commit | 6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch) | |
tree | 0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/sat/bsat/satInterB.c | |
parent | f0e77f6797c0504b0da25a56152b707d3357f386 (diff) | |
download | abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2 abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip |
initial commit of public abc
Diffstat (limited to 'src/sat/bsat/satInterB.c')
-rw-r--r-- | src/sat/bsat/satInterB.c | 84 |
1 files changed, 72 insertions, 12 deletions
diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c index cb7f7828..1ffb0dc5 100644 --- a/src/sat/bsat/satInterB.c +++ b/src/sat/bsat/satInterB.c @@ -26,6 +26,9 @@ #include "satStore.h" #include "aig.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -188,6 +191,7 @@ int Intb_ManGlobalVars( Intb_Man_t * p ) ***********************************************************************/ void Intb_ManResize( Intb_Man_t * p ) { + p->Counter = 0; // check if resizing is needed if ( p->nVarsAlloc < p->pCnf->nVars ) { @@ -205,7 +209,7 @@ void Intb_ManResize( Intb_Man_t * p ) p->pWatches = ABC_REALLOC(Sto_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); } - // clean the ABC_FREE space + // clean the free space memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); @@ -232,7 +236,7 @@ void Intb_ManResize( Intb_Man_t * p ) if ( p->nIntersAlloc < p->pCnf->nClauses ) { p->nIntersAlloc = p->pCnf->nClauses; - p->pInters = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc ); + p->pInters = ABC_REALLOC( Aig_Obj_t *, p->pInters, p->nIntersAlloc ); } memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); } @@ -550,7 +554,6 @@ int Intb_ManGetGlobalVar( Intb_Man_t * p, int Var ) return VarAB; } - /**Function************************************************************* Synopsis [Traces the proof for one clause.] @@ -608,7 +611,6 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF for ( v = 1; v < (int)pReason->nLits; v++ ) p->pSeens[lit_var(pReason->pLits[v])] = 1; - // record the reason clause assert( Intb_ManProofGet(p, pReason) > 0 ); p->Counter++; @@ -677,7 +679,6 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); } } - // Vec_PtrPush( pFinal->pAntis, pReason ); } @@ -710,6 +711,27 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF Intb_ManPrintResolvent( p->pResLits, p->nResLits ); Intb_ManPrintClause( p, pFinal ); } + + // if there are literals in the clause that are not in the resolvent + // it means that the derived resolvent is stronger than the clause + // we can replace the clause with the resolvent by removing these literals + if ( p->nResLits != (int)pFinal->nLits ) + { + for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ ) + { + for ( v2 = 0; v2 < p->nResLits; v2++ ) + if ( pFinal->pLits[v1] == p->pResLits[v2] ) + break; + if ( v2 < p->nResLits ) + continue; + // remove literal v1 from the final clause + pFinal->nLits--; + for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ ) + pFinal->pLits[v2] = pFinal->pLits[v2+1]; + v1--; + } + assert( p->nResLits == (int)pFinal->nLits ); + } } p->timeTrace += clock() - clk; @@ -719,6 +741,10 @@ p->timeTrace += clock() - clk; // Intb_ManPrintInterOne( p, pFinal ); } Intb_ManProofSet( p, pFinal, p->Counter ); + // make sure the same proof ID is not asssigned to two consecutive clauses + assert( p->pProofNums[pFinal->Id-1] != p->Counter ); +// if ( p->pProofNums[pFinal->Id] == p->pProofNums[pFinal->Id-1] ) +// p->pProofNums[pFinal->Id] = p->pProofNums[pConflict->Id]; return p->Counter; } @@ -743,9 +769,16 @@ int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause ) if ( pClause->nLits == 0 ) printf( "Error: Empty clause is attempted.\n" ); - // add assumptions to the trail assert( !pClause->fRoot ); assert( p->nTrailSize == p->nRootSize ); + + // if any of the clause literals are already assumed + // it means that the clause is redundant and can be skipped + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] ) + return 1; + + // add assumptions to the trail for ( i = 0; i < (int)pClause->nLits; i++ ) if ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) { @@ -759,6 +792,27 @@ int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause ) { assert( 0 ); // cannot prove return 0; + } + + // skip the clause if it is weaker or the same as the conflict clause + if ( pClause->nLits >= pConflict->nLits ) + { + // check if every literal of conflict clause can be found in the given clause + int j; + for ( i = 0; i < (int)pConflict->nLits; i++ ) + { + for ( j = 0; j < (int)pClause->nLits; j++ ) + if ( pConflict->pLits[i] == pClause->pLits[j] ) + break; + if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found + break; + } + if ( i == (int)pConflict->nLits ) // all lits are found + { + // undo to the root level + Intb_ManCancelUntil( p, p->nRootSize ); + return 1; + } } // construct the proof @@ -846,8 +900,12 @@ int Intb_ManProcessRoots( Intb_Man_t * p ) if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) ) { // detected root level conflict - printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" ); - assert( 0 ); +// printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" ); +// assert( 0 ); + // detected root level conflict + Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); return 0; } } @@ -895,7 +953,6 @@ void Intb_ManPrepareInter( Intb_Man_t * p ) } // clause of A Intb_ManAigClear( p, Intb_ManAigRead(p, pClause) ); - for ( v = 0; v < (int)pClause->nLits; v++ ) { Var = lit_var(pClause->pLits[v]); @@ -909,7 +966,6 @@ void Intb_ManPrepareInter( Intb_Man_t * p ) Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB ); } } - // Intb_ManPrintInterOne( p, pClause ); } } @@ -940,7 +996,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); p->pCnf = pCnf; p->fVerbose = fVerbose; - p->vVarsAB = vVarsAB; + p->vVarsAB = (Vec_Int_t *)vVarsAB; p->pAig = pRes = Aig_ManStart( 10000 ); Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); @@ -980,8 +1036,9 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in // stop the proof if ( p->fProofWrite ) - { + { fclose( p->pFile ); +// Sat_ProofChecker( "proof.cnf_" ); p->pFile = NULL; } @@ -1004,6 +1061,7 @@ p->timeTotal += clock() - clkTotal; } + /**Function************************************************************* Synopsis [] @@ -1053,3 +1111,5 @@ Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fCla //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + |