/**CFile**************************************************************** FileName [pr.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Proof recording.] Synopsis [Core procedures of the package.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: pr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include #include #include #include #include "misc/util/abc_global.h" #include "pr.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef unsigned lit; typedef struct Pr_Cls_t_ Pr_Cls_t; struct Pr_Cls_t_ { unsigned uTruth; // interpolant void * pProof; // the proof node // void * pAntis; // the anticedents Pr_Cls_t * pNext; // the next clause Pr_Cls_t * pNext0; // the next 0-watch Pr_Cls_t * pNext1; // the next 0-watch int Id; // the clause ID unsigned fA : 1; // belongs to A unsigned fRoot : 1; // original clause unsigned fVisit : 1; // visited clause unsigned nLits : 24; // the number of literals lit pLits[0]; // literals of this clause }; struct Pr_Man_t_ { // general data int fProofWrite; // writes the proof file int fProofVerif; // verifies the proof int nVars; // the number of variables int nVarsAB; // the number of global variables int nRoots; // the number of root clauses int nClauses; // the number of all clauses int nClausesA; // the number of clauses of A Pr_Cls_t * pHead; // the head clause Pr_Cls_t * pTail; // the tail clause Pr_Cls_t * pLearnt; // the tail clause Pr_Cls_t * pEmpty; // the empty clause // internal BCP int nRootSize; // the number of root level assignments int nTrailSize; // the number of assignments made lit * pTrail; // chronological order of assignments (size nVars) lit * pAssigns; // assignments by variable (size nVars) char * pSeens; // temporary mark (size nVars) char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] Pr_Cls_t ** pReasons; // reasons for each assignment (size nVars) Pr_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) int nVarsAlloc; // the allocated size of arrays // proof recording void * pManProof; // proof manager int Counter; // counter of resolved clauses // memory management int nChunkSize; // the number of bytes in a chunk int nChunkUsed; // the number of bytes used in the last chunk char * pChunkLast; // the last memory chunk // internal verification lit * pResLits; // the literals of the resolvent int nResLits; // the number of literals of the resolvent int nResLitsAlloc;// the number of literals of the resolvent // runtime stats abctime timeBcp; abctime timeTrace; abctime timeRead; abctime timeTotal; }; // variable assignments static const lit LIT_UNDEF = 0xffffffff; // variable/literal conversions (taken from MiniSat) static inline lit toLit (int v) { return v + v; } static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } static inline lit lit_neg (lit l) { return l ^ 1; } static inline int lit_var (lit l) { return l >> 1; } static inline int lit_sign (lit l) { return l & 1; } static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } // iterators through the clauses #define Pr_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext ) #define Pr_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls != p->pLearnt; pCls = pCls->pNext ) #define Pr_ManForEachClauseLearnt( p, pCls ) for( pCls = p->pLearnt; pCls; pCls = pCls->pNext ) // static procedures static char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes ); static void Pr_ManMemoryStop( Pr_Man_t * p ); static void Pr_ManResize( Pr_Man_t * p, int nVarsNew ); // exported procedures extern Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ); extern void Pr_ManFree( Pr_Man_t * p ); extern int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA ); extern int Pr_ManProofWrite( Pr_Man_t * p ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Allocate proof manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ) { Pr_Man_t * p; // allocate the manager p = (Pr_Man_t *)ABC_ALLOC( char, sizeof(Pr_Man_t) ); memset( p, 0, sizeof(Pr_Man_t) ); // allocate internal arrays Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 ); // set the starting number of variables p->nVars = 0; // memory management p->nChunkSize = (1<<16); // use 64K chunks // verification p->nResLitsAlloc = (1<<16); p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc ); // parameters p->fProofWrite = 0; p->fProofVerif = 0; return p; } /**Function************************************************************* Synopsis [Resize proof manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManResize( Pr_Man_t * p, int nVarsNew ) { // check if resizing is needed if ( p->nVarsAlloc < nVarsNew ) { int nVarsAllocOld = p->nVarsAlloc; // find the new size if ( p->nVarsAlloc == 0 ) p->nVarsAlloc = 1; while ( p->nVarsAlloc < nVarsNew ) p->nVarsAlloc *= 2; // resize the arrays p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); p->pVarTypes = ABC_REALLOC(char, p->pVarTypes, p->nVarsAlloc ); p->pReasons = ABC_REALLOC(Pr_Cls_t *, p->pReasons, p->nVarsAlloc ); p->pWatches = ABC_REALLOC(Pr_Cls_t *, p->pWatches, p->nVarsAlloc*2 ); // clean the free space memset( p->pAssigns + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) ); memset( p->pSeens + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) ); memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) ); memset( p->pReasons + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld) ); memset( p->pWatches + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld)*2 ); } // adjust the number of variables if ( p->nVars < nVarsNew ) p->nVars = nVarsNew; } /**Function************************************************************* Synopsis [Deallocate proof manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManFree( Pr_Man_t * p ) { printf( "Runtime stats:\n" ); ABC_PRT( "Reading ", p->timeRead ); ABC_PRT( "BCP ", p->timeBcp ); ABC_PRT( "Trace ", p->timeTrace ); ABC_PRT( "TOTAL ", p->timeTotal ); Pr_ManMemoryStop( p ); ABC_FREE( p->pTrail ); ABC_FREE( p->pAssigns ); ABC_FREE( p->pSeens ); ABC_FREE( p->pVarTypes ); ABC_FREE( p->pReasons ); ABC_FREE( p->pWatches ); ABC_FREE( p->pResLits ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Adds one clause to the watcher list.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline void Pr_ManWatchClause( Pr_Man_t * p, Pr_Cls_t * pClause, lit Lit ) { assert( lit_check(Lit, p->nVars) ); if ( pClause->pLits[0] == Lit ) pClause->pNext0 = p->pWatches[lit_neg(Lit)]; else { assert( pClause->pLits[1] == Lit ); pClause->pNext1 = p->pWatches[lit_neg(Lit)]; } p->pWatches[lit_neg(Lit)] = pClause; } /**Function************************************************************* Synopsis [Adds one clause to the manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA ) { Pr_Cls_t * pClause; lit Lit, * i, * j; int nSize, VarMax; // process the literals if ( pBeg < pEnd ) { // insertion sort VarMax = lit_var( *pBeg ); for ( i = pBeg + 1; i < pEnd; i++ ) { Lit = *i; VarMax = lit_var(Lit) > VarMax ? lit_var(Lit) : VarMax; for ( j = i; j > pBeg && *(j-1) > Lit; j-- ) *j = *(j-1); *j = Lit; } // make sure there is no duplicated variables for ( i = pBeg + 1; i < pEnd; i++ ) assert( lit_var(*(i-1)) != lit_var(*i) ); // resize the manager Pr_ManResize( p, VarMax+1 ); } // get memory for the clause nSize = sizeof(Pr_Cls_t) + sizeof(lit) * (pEnd - pBeg); pClause = (Pr_Cls_t *)Pr_ManMemoryFetch( p, nSize ); memset( pClause, 0, sizeof(Pr_Cls_t) ); // assign the clause assert( !fClauseA || fRoot ); // clause of A is always a root clause p->nRoots += fRoot; p->nClausesA += fClauseA; pClause->Id = p->nClauses++; pClause->fA = fClauseA; pClause->fRoot = fRoot; pClause->nLits = pEnd - pBeg; memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) ); // add the clause to the list if ( p->pHead == NULL ) p->pHead = pClause; if ( p->pTail == NULL ) p->pTail = pClause; else { p->pTail->pNext = pClause; p->pTail = pClause; } // mark the first learnt clause if ( p->pLearnt == NULL && !pClause->fRoot ) p->pLearnt = pClause; // add the empty clause if ( pClause->nLits == 0 ) { if ( p->pEmpty ) printf( "More than one empty clause!\n" ); p->pEmpty = pClause; } return 1; } /**Function************************************************************* Synopsis [Fetches memory.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes ) { char * pMem; if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed ) { pMem = (char *)ABC_ALLOC( char, p->nChunkSize ); *(char **)pMem = p->pChunkLast; p->pChunkLast = pMem; p->nChunkUsed = sizeof(char *); } pMem = p->pChunkLast + p->nChunkUsed; p->nChunkUsed += nBytes; return pMem; } /**Function************************************************************* Synopsis [Frees memory manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManMemoryStop( Pr_Man_t * p ) { char * pMem, * pNext; if ( p->pChunkLast == NULL ) return; for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext ) ABC_FREE( pMem ); ABC_FREE( pMem ); } /**Function************************************************************* Synopsis [Reports memory usage in bytes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Pr_ManMemoryReport( Pr_Man_t * p ) { int Total; char * pMem, * pNext; if ( p->pChunkLast == NULL ) return 0; Total = p->nChunkUsed; for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext ) Total += p->nChunkSize; return Total; } /**Function************************************************************* Synopsis [Records the proof.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Extra_PrintBinary_( FILE * pFile, unsigned Sign[], int nBits ) { int Remainder, nWords; int w, i; Remainder = (nBits%(sizeof(unsigned)*8)); nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0); for ( w = nWords-1; w >= 0; w-- ) for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- ) fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1< 0) ); } /**Function************************************************************* Synopsis [Prints the interpolant for one clause.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManPrintInterOne( Pr_Man_t * p, Pr_Cls_t * pClause ) { printf( "Clause %2d : ", pClause->Id ); Extra_PrintBinary_( stdout, &pClause->uTruth, (1 << p->nVarsAB) ); printf( "\n" ); } /**Function************************************************************* Synopsis [Records implication.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Pr_ManEnqueue( Pr_Man_t * p, lit Lit, Pr_Cls_t * pReason ) { int Var = lit_var(Lit); if ( p->pAssigns[Var] != LIT_UNDEF ) return p->pAssigns[Var] == Lit; p->pAssigns[Var] = Lit; p->pReasons[Var] = pReason; p->pTrail[p->nTrailSize++] = Lit; //printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); return 1; } /**Function************************************************************* Synopsis [Records implication.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline void Pr_ManCancelUntil( Pr_Man_t * p, int Level ) { lit Lit; int i, Var; for ( i = p->nTrailSize - 1; i >= Level; i-- ) { Lit = p->pTrail[i]; Var = lit_var( Lit ); p->pReasons[Var] = NULL; p->pAssigns[Var] = LIT_UNDEF; //printf( "cancelling var %d\n", Var ); } p->nTrailSize = Level; } /**Function************************************************************* Synopsis [Propagate one assignment.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Pr_Cls_t * Pr_ManPropagateOne( Pr_Man_t * p, lit Lit ) { Pr_Cls_t ** ppPrev, * pCur, * pTemp; lit LitF = lit_neg(Lit); int i; // iterate through the literals ppPrev = p->pWatches + Lit; for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) { // make sure the false literal is in the second literal of the clause if ( pCur->pLits[0] == LitF ) { pCur->pLits[0] = pCur->pLits[1]; pCur->pLits[1] = LitF; pTemp = pCur->pNext0; pCur->pNext0 = pCur->pNext1; pCur->pNext1 = pTemp; } assert( pCur->pLits[1] == LitF ); // if the first literal is true, the clause is satisfied if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) { ppPrev = &pCur->pNext1; continue; } // look for a new literal to watch for ( i = 2; i < (int)pCur->nLits; i++ ) { // skip the case when the literal is false if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) continue; // the literal is either true or unassigned - watch it pCur->pLits[1] = pCur->pLits[i]; pCur->pLits[i] = LitF; // remove this clause from the watch list of Lit *ppPrev = pCur->pNext1; // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) Pr_ManWatchClause( p, pCur, pCur->pLits[1] ); break; } if ( i < (int)pCur->nLits ) // found new watch continue; // clause is unit - enqueue new implication if ( Pr_ManEnqueue(p, pCur->pLits[0], pCur) ) { ppPrev = &pCur->pNext1; continue; } // conflict detected - return the conflict clause return pCur; } return NULL; } /**Function************************************************************* Synopsis [Propagate the current assignments.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Pr_Cls_t * Pr_ManPropagate( Pr_Man_t * p, int Start ) { Pr_Cls_t * pClause; int i; abctime clk = Abc_Clock(); for ( i = Start; i < p->nTrailSize; i++ ) { pClause = Pr_ManPropagateOne( p, p->pTrail[i] ); if ( pClause ) { p->timeBcp += Abc_Clock() - clk; return pClause; } } p->timeBcp += Abc_Clock() - clk; return NULL; } /**Function************************************************************* Synopsis [Prints the clause.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManPrintClause( Pr_Cls_t * pClause ) { int i; printf( "Clause ID = %d. Proof = %d. {", pClause->Id, (int)pClause->pProof ); for ( i = 0; i < (int)pClause->nLits; i++ ) printf( " %d", pClause->pLits[i] ); printf( " }\n" ); } /**Function************************************************************* Synopsis [Prints the resolvent.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManPrintResolvent( lit * pResLits, int nResLits ) { int i; printf( "Resolvent: {" ); for ( i = 0; i < nResLits; i++ ) printf( " %d", pResLits[i] ); printf( " }\n" ); } /**Function************************************************************* Synopsis [Writes one root clause into a file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManProofWriteOne( Pr_Man_t * p, Pr_Cls_t * pClause ) { pClause->pProof = (void *)++p->Counter; if ( p->fProofWrite ) { int v; fprintf( (FILE *)p->pManProof, "%d", (int)pClause->pProof ); for ( v = 0; v < (int)pClause->nLits; v++ ) fprintf( (FILE *)p->pManProof, " %d", lit_print(pClause->pLits[v]) ); fprintf( (FILE *)p->pManProof, " 0 0\n" ); } } /**Function************************************************************* Synopsis [Traces the proof for one clause.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal ) { Pr_Cls_t * pReason; int i, v, Var, PrevId; int fPrint = 0; abctime clk = Abc_Clock(); // collect resolvent literals if ( p->fProofVerif ) { assert( (int)pConflict->nLits <= p->nResLitsAlloc ); memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); p->nResLits = pConflict->nLits; } // mark all the variables in the conflict as seen for ( v = 0; v < (int)pConflict->nLits; v++ ) p->pSeens[lit_var(pConflict->pLits[v])] = 1; // start the anticedents // pFinal->pAntis = Vec_PtrAlloc( 32 ); // Vec_PtrPush( pFinal->pAntis, pConflict ); if ( p->nClausesA ) pFinal->uTruth = pConflict->uTruth; // follow the trail backwards PrevId = (int)pConflict->pProof; for ( i = p->nTrailSize - 1; i >= 0; i-- ) { // skip literals that are not involved Var = lit_var(p->pTrail[i]); if ( !p->pSeens[Var] ) continue; p->pSeens[Var] = 0; // skip literals of the resulting clause pReason = p->pReasons[Var]; if ( pReason == NULL ) continue; assert( p->pTrail[i] == pReason->pLits[0] ); // add the variables to seen for ( v = 1; v < (int)pReason->nLits; v++ ) p->pSeens[lit_var(pReason->pLits[v])] = 1; // record the reason clause assert( pReason->pProof > 0 ); p->Counter++; if ( p->fProofWrite ) fprintf( (FILE *)p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof ); PrevId = p->Counter; if ( p->nClausesA ) { if ( p->pVarTypes[Var] == 1 ) // var of A pFinal->uTruth |= pReason->uTruth; else pFinal->uTruth &= pReason->uTruth; } // resolve the temporary resolvent with the reason clause if ( p->fProofVerif ) { int v1, v2; if ( fPrint ) Pr_ManPrintResolvent( p->pResLits, p->nResLits ); // check that the var is present in the resolvent for ( v1 = 0; v1 < p->nResLits; v1++ ) if ( lit_var(p->pResLits[v1]) == Var ) break; if ( v1 == p->nResLits ) printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); // remove this variable from the resolvent assert( lit_var(p->pResLits[v1]) == Var ); p->nResLits--; for ( ; v1 < p->nResLits; v1++ ) p->pResLits[v1] = p->pResLits[v1+1]; // add variables of the reason clause for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) { for ( v1 = 0; v1 < p->nResLits; v1++ ) if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) break; // if it is a new variable, add it to the resolvent if ( v1 == p->nResLits ) { if ( p->nResLits == p->nResLitsAlloc ) printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n, pFinal->Id" ); p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; continue; } // if the variable is the same, the literal should be the same too if ( p->pResLits[v1] == pReason->pLits[v2] ) continue; // the literal is different printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); } } // Vec_PtrPush( pFinal->pAntis, pReason ); } // unmark all seen variables // for ( i = p->nTrailSize - 1; i >= 0; i-- ) // p->pSeens[lit_var(p->pTrail[i])] = 0; // check that the literals are unmarked // for ( i = p->nTrailSize - 1; i >= 0; i-- ) // assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); // use the resulting clause to check the correctness of resolution if ( p->fProofVerif ) { int v1, v2; if ( fPrint ) Pr_ManPrintResolvent( p->pResLits, p->nResLits ); for ( v1 = 0; v1 < p->nResLits; v1++ ) { for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) if ( pFinal->pLits[v2] == p->pResLits[v1] ) break; if ( v2 < (int)pFinal->nLits ) continue; break; } if ( v1 < p->nResLits ) { printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); Pr_ManPrintClause( pConflict ); Pr_ManPrintResolvent( p->pResLits, p->nResLits ); Pr_ManPrintClause( pFinal ); } } p->timeTrace += Abc_Clock() - clk; // return the proof pointer if ( p->nClausesA ) { Pr_ManPrintInterOne( p, pFinal ); } return p->Counter; } /**Function************************************************************* Synopsis [Records the proof for one clause.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Pr_ManProofRecordOne( Pr_Man_t * p, Pr_Cls_t * pClause ) { Pr_Cls_t * pConflict; int i; // empty clause never ends up there assert( pClause->nLits > 0 ); if ( pClause->nLits == 0 ) printf( "Error: Empty clause is attempted.\n" ); // add assumptions to the trail assert( !pClause->fRoot ); assert( p->nTrailSize == p->nRootSize ); for ( i = 0; i < (int)pClause->nLits; i++ ) if ( !Pr_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) { assert( 0 ); // impossible return 0; } // propagate the assumptions pConflict = Pr_ManPropagate( p, p->nRootSize ); if ( pConflict == NULL ) { assert( 0 ); // cannot prove return 0; } // construct the proof pClause->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, pClause ); // undo to the root level Pr_ManCancelUntil( p, p->nRootSize ); // add large clauses to the watched lists if ( pClause->nLits > 1 ) { Pr_ManWatchClause( p, pClause, pClause->pLits[0] ); Pr_ManWatchClause( p, pClause, pClause->pLits[1] ); return 1; } assert( pClause->nLits == 1 ); // if the clause proved is unit, add it and propagate if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) ) { assert( 0 ); // impossible return 0; } // propagate the assumption pConflict = Pr_ManPropagate( p, p->nRootSize ); if ( pConflict ) { // construct the proof p->pEmpty->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, p->pEmpty ); printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); return 0; } // update the root level p->nRootSize = p->nTrailSize; return 1; } /**Function************************************************************* Synopsis [Propagate the root clauses.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Pr_ManProcessRoots( Pr_Man_t * p ) { Pr_Cls_t * pClause; int Counter; // make sure the root clauses are preceeding the learnt clauses Counter = 0; Pr_ManForEachClause( p, pClause ) { assert( (int)pClause->fA == (Counter < (int)p->nClausesA) ); assert( (int)pClause->fRoot == (Counter < (int)p->nRoots) ); Counter++; } assert( p->nClauses == Counter ); // make sure the last clause if empty assert( p->pTail->nLits == 0 ); // go through the root unit clauses p->nTrailSize = 0; Pr_ManForEachClauseRoot( p, pClause ) { // create watcher lists for the root clauses if ( pClause->nLits > 1 ) { Pr_ManWatchClause( p, pClause, pClause->pLits[0] ); Pr_ManWatchClause( p, pClause, pClause->pLits[1] ); } // empty clause and large clauses if ( pClause->nLits != 1 ) continue; // unit clause assert( lit_check(pClause->pLits[0], p->nVars) ); if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) ) { // detected root level conflict printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" ); assert( 0 ); return 0; } } // propagate the root unit clauses pClause = Pr_ManPropagate( p, 0 ); if ( pClause ) { // detected root level conflict printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" ); assert( 0 ); return 0; } // set the root level p->nRootSize = p->nTrailSize; return 1; } /**Function************************************************************* Synopsis [Records the proof.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Pr_ManPrepareInter( Pr_Man_t * p ) { unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; Pr_Cls_t * pClause; int Var, v; // mark the variable encountered in the clauses of A Pr_ManForEachClauseRoot( p, pClause ) { if ( !pClause->fA ) break; for ( v = 0; v < (int)pClause->nLits; v++ ) p->pVarTypes[lit_var(pClause->pLits[v])] = 1; } // check variables that appear in clauses of B p->nVarsAB = 0; Pr_ManForEachClauseRoot( p, pClause ) { if ( pClause->fA ) continue; for ( v = 0; v < (int)pClause->nLits; v++ ) { Var = lit_var(pClause->pLits[v]); if ( p->pVarTypes[Var] == 1 ) // var of A { // change it into a global variable p->nVarsAB++; p->pVarTypes[Var] = -1; } } } // order global variables p->nVarsAB = 0; for ( v = 0; v < p->nVars; v++ ) if ( p->pVarTypes[v] == -1 ) p->pVarTypes[v] -= p->nVarsAB++; printf( "There are %d global variables.\n", p->nVarsAB ); // set interpolants for root clauses Pr_ManForEachClauseRoot( p, pClause ) { if ( !pClause->fA ) // clause of B { pClause->uTruth = ~0; Pr_ManPrintInterOne( p, pClause ); continue; } // clause of A pClause->uTruth = 0; for ( v = 0; v < (int)pClause->nLits; v++ ) { Var = lit_var(pClause->pLits[v]); if ( p->pVarTypes[Var] < 0 ) // global var { if ( lit_sign(pClause->pLits[v]) ) // negative var pClause->uTruth |= ~uTruths[ -p->pVarTypes[Var]-1 ]; else pClause->uTruth |= uTruths[ -p->pVarTypes[Var]-1 ]; } } Pr_ManPrintInterOne( p, pClause ); } } /**Function************************************************************* Synopsis [Records the proof.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Pr_ManProofWrite( Pr_Man_t * p ) { Pr_Cls_t * pClause; int RetValue = 1; // propagate root level assignments Pr_ManProcessRoots( p ); // prepare the interpolant computation if ( p->nClausesA ) Pr_ManPrepareInter( p ); // construct proof for each clause // start the proof if ( p->fProofWrite ) p->pManProof = fopen( "proof.cnf_", "w" ); p->Counter = 0; // write the root clauses Pr_ManForEachClauseRoot( p, pClause ) Pr_ManProofWriteOne( p, pClause ); // consider each learned clause Pr_ManForEachClauseLearnt( p, pClause ) { if ( !Pr_ManProofRecordOne( p, pClause ) ) { RetValue = 0; break; } } if ( p->nClausesA ) { printf( "Interpolant: " ); } // stop the proof if ( p->fProofWrite ) { fclose( (FILE *)p->pManProof ); p->pManProof = NULL; } return RetValue; } /**Function************************************************************* Synopsis [Reads clauses from file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Pr_Man_t * Pr_ManProofRead( char * pFileName ) { Pr_Man_t * p = NULL; char * pCur, * pBuffer = NULL; int * pArray = NULL; FILE * pFile; int RetValue, Counter, nNumbers, Temp; int nClauses, nClausesA, nRoots, nVars; // open the file pFile = fopen( pFileName, "r" ); if ( pFile == NULL ) { printf( "Count not open input file \"%s\".\n", pFileName ); return NULL; } // read the file pBuffer = (char *)ABC_ALLOC( char, (1<<16) ); for ( Counter = 0; fgets( pBuffer, (1<<16), pFile ); ) { if ( pBuffer[0] == 'c' ) continue; if ( pBuffer[0] == 'p' ) { assert( p == NULL ); nClausesA = 0; RetValue = sscanf( pBuffer + 1, "%d %d %d %d", &nVars, &nClauses, &nRoots, &nClausesA ); if ( RetValue != 3 && RetValue != 4 ) { printf( "Wrong input file format.\n" ); } p = Pr_ManAlloc( nVars ); pArray = (int *)ABC_ALLOC( char, sizeof(int) * (nVars + 10) ); continue; } // skip empty lines for ( pCur = pBuffer; *pCur; pCur++ ) if ( !(*pCur == ' ' || *pCur == '\t' || *pCur == '\r' || *pCur == '\n') ) break; if ( *pCur == 0 ) continue; // scan the numbers from file nNumbers = 0; pCur = pBuffer; while ( *pCur ) { // skip spaces for ( ; *pCur && *pCur == ' '; pCur++ ); // read next number Temp = 0; sscanf( pCur, "%d", &Temp ); if ( Temp == 0 ) break; pArray[ nNumbers++ ] = lit_read( Temp ); // skip non-spaces for ( ; *pCur && *pCur != ' '; pCur++ ); } // add the clause if ( !Pr_ManAddClause( p, (unsigned *)pArray, (unsigned *)pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) ) { printf( "Bad clause number %d.\n", Counter ); return NULL; } // count the clauses Counter++; } // check the number of clauses if ( Counter != nClauses ) printf( "Expected %d clauses but read %d.\n", nClauses, Counter ); // finish if ( pArray ) ABC_FREE( pArray ); if ( pBuffer ) ABC_FREE( pBuffer ); fclose( pFile ); return p; } /**Function************************************************************* Synopsis [Records the proof.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ /* int Pr_ManProofCount_rec( Pr_Cls_t * pClause ) { Pr_Cls_t * pNext; int i, Counter; if ( pClause->fRoot ) return 0; if ( pClause->fVisit ) return 0; pClause->fVisit = 1; // count the number of visited clauses Counter = 1; Vec_PtrForEachEntry( Pr_Cls_t *, pClause->pAntis, pNext, i ) Counter += Pr_ManProofCount_rec( pNext ); return Counter; } */ /**Function************************************************************* Synopsis [Records the proof.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Pr_ManProofTest( char * pFileName ) { Pr_Man_t * p; abctime clk, clkTotal = Abc_Clock(); clk = Abc_Clock(); p = Pr_ManProofRead( pFileName ); p->timeRead = Abc_Clock() - clk; if ( p == NULL ) return 0; Pr_ManProofWrite( p ); // print stats /* nUsed = Pr_ManProofCount_rec( p->pEmpty ); printf( "Roots = %d. Learned = %d. Total = %d. Steps = %d. Ave = %.2f. Used = %d. Ratio = %.2f. \n", p->nRoots, p->nClauses-p->nRoots, p->nClauses, p->Counter, 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), nUsed, 1.0*nUsed/(p->nClauses-p->nRoots) ); */ printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter, 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), 1.0*Pr_ManMemoryReport(p)/(1<<20) ); p->timeTotal = Abc_Clock() - clkTotal; Pr_ManFree( p ); return 1; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END