/**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 <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#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
clock_t timeBcp;
clock_t timeTrace;
clock_t timeRead;
clock_t 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<<i)) > 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;
clock_t clk = clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Pr_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
p->timeBcp += clock() - clk;
return pClause;
}
}
p->timeBcp += 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;
clock_t clk = 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 += 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;
clock_t clk, clkTotal = clock();
clk = clock();
p = Pr_ManProofRead( pFileName );
p->timeRead = 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 = clock() - clkTotal;
Pr_ManFree( p );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END