summaryrefslogtreecommitdiffstats
path: root/src/sat/proof/pr.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/proof/pr.c')
-rw-r--r--src/sat/proof/pr.c1263
1 files changed, 1263 insertions, 0 deletions
diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c
new file mode 100644
index 00000000..2d1ab2d1
--- /dev/null
+++ b/src/sat/proof/pr.c
@@ -0,0 +1,1263 @@
+/**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 <time.h>
+//#include "vec.h"
+#include "pr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// 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
+ int timeBcp;
+ int timeTrace;
+ int timeRead;
+ int timeTotal;
+};
+
+#ifndef PRT
+#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
+// 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 *)malloc( 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 = malloc( sizeof(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 = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc );
+ p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc );
+ p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc );
+ p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
+ p->pReasons = (Pr_Cls_t **)realloc( p->pReasons, sizeof(Pr_Cls_t *) * p->nVarsAlloc );
+ p->pWatches = (Pr_Cls_t **)realloc( p->pWatches, sizeof(Pr_Cls_t *) * 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" );
+PRT( "Reading ", p->timeRead );
+PRT( "BCP ", p->timeBcp );
+PRT( "Trace ", p->timeTrace );
+PRT( "TOTAL ", p->timeTotal );
+
+ Pr_ManMemoryStop( p );
+ free( p->pTrail );
+ free( p->pAssigns );
+ free( p->pSeens );
+ free( p->pVarTypes );
+ free( p->pReasons );
+ free( p->pWatches );
+ free( p->pResLits );
+ 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 *)malloc( 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 )
+ free( pMem );
+ 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;
+ int 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( p->pManProof, "%d", (int)pClause->pProof );
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ fprintf( p->pManProof, " %d", lit_print(pClause->pLits[v]) );
+ fprintf( 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;
+ int 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( 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( 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 *)malloc( (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 *)malloc( 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, pArray, 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 ) free( pArray );
+ if ( pBuffer ) 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( 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;
+ int 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 ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 19:27:02 +0000