summaryrefslogtreecommitdiffstats
path: root/src/sat/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/proof')
-rw-r--r--src/sat/proof/pr.c1263
-rw-r--r--src/sat/proof/pr.h65
-rw-r--r--src/sat/proof/stats.txt66
3 files changed, 0 insertions, 1394 deletions
diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c
deleted file mode 100644
index 2d1ab2d1..00000000
--- a/src/sat/proof/pr.c
+++ /dev/null
@@ -1,1263 +0,0 @@
-/**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 ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/proof/pr.h b/src/sat/proof/pr.h
deleted file mode 100644
index 1e71a2d3..00000000
--- a/src/sat/proof/pr.h
+++ /dev/null
@@ -1,65 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pr.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Proof recording.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __PR_H__
-#define __PR_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#ifdef _WIN32
-#define inline __inline // compatible with MS VS 6.0
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Pr_Man_t_ Pr_Man_t;
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== pr.c ==========================================================*/
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/proof/stats.txt b/src/sat/proof/stats.txt
deleted file mode 100644
index 470b1630..00000000
--- a/src/sat/proof/stats.txt
+++ /dev/null
@@ -1,66 +0,0 @@
-UC Berkeley, ABC 1.01 (compiled Jan 20 2007 16:47:34)
-abc.rc: No such file or directory
-Loaded "abc.rc" from the parent directory.
-abc 01> test
-Found last conflict after adding unit clause number 10229!
-Roots = 7184. Learned = 3047. Total = 10231. Steps = 196361. Ave = 62.09. Used = 2224. Ratio = 0.73.
-Runtime stats:
-Reading = 0.03 sec
-BCP = 0.32 sec
-Trace = 0.06 sec
-TOTAL = 0.43 sec
-abc 01> test
-Found last conflict after adding unit clause number 7676!
-Roots = 6605. Learned = 1073. Total = 7678. Steps = 52402. Ave = 42.68. Used = 1011. Ratio = 0.94.
-Runtime stats:
-Reading = 0.01 sec
-BCP = 0.02 sec
-Trace = 0.02 sec
-TOTAL = 0.06 sec
-abc 01> test
-Found last conflict after adding unit clause number 37868!
-Roots = 15443. Learned = 22427. Total = 37870. Steps = 2365472. Ave = 104.79. Used = 19763. Ratio = 0.88.
-Runtime stats:
-Reading = 0.20 sec
-BCP = 14.67 sec
-Trace = 0.56 sec
-TOTAL = 15.74 sec
-abc 01>
-
-
-abc 05> wb ibm_bmc/len25u_renc.blif
-abc 05> ps
-(no name) : i/o = 348/ 1 lat = 0 nd = 3648 bdd = 15522 lev = 246
-abc 05> sat -v
-==================================[MINISAT]===================================
-| Conflicts | ORIGINAL | LEARNT | Progress |
-| | Clauses Literals | Limit Clauses Literals Lit/Cl | |
-==============================================================================
-| 0 | 17413 54996 | 5804 0 0 0.0 | 0.000 % |
-| 100 | 17413 54996 | 6384 100 606 6.1 | 0.417 % |
-| 250 | 17413 54996 | 7023 250 1586 6.3 | 0.417 % |
-| 476 | 17413 54996 | 7725 476 3288 6.9 | 0.417 % |
-| 813 | 17413 54996 | 8498 813 7586 9.3 | 0.417 % |
-| 1319 | 17403 54970 | 9347 1318 14848 11.3 | 0.442 % |
-| 2078 | 17403 54970 | 10282 2076 40186 19.4 | 0.466 % |
-| 3217 | 17397 54948 | 11310 3208 99402 31.0 | 0.466 % |
-| 4926 | 17392 54930 | 12441 4911 131848 26.8 | 0.491 % |
-| 7489 | 17392 54930 | 13686 7474 204217 27.3 | 0.491 % |
-| 11336 | 17357 54829 | 15054 11310 332863 29.4 | 0.638 % |
-| 17103 | 17346 54794 | 16559 9130 203029 22.2 | 0.687 % |
-| 25752 | 17288 54606 | 18215 9083 176982 19.5 | 0.834 % |
-| 38727 | 17266 54536 | 20037 12674 278949 22.0 | 0.883 % |
-| 58188 | 17240 54453 | 22041 11905 255255 21.4 | 0.957 % |
-==============================================================================
-Start = 15. Conf = 79435. Dec = 130967. Prop = 24083434. Insp = 136774586.
-Total runtime = 18.66 sec. Var select = 0.00 sec. Var update = 0.00 sec.
-UNSATISFIABLE Time = 18.69 sec
-abc 05>
-abc 05> test
-Found last conflict after adding unit clause number 96902!
-Roots = 17469. Learned = 79435. Total = 96904. Steps = 9700042. Ave = 121.89. Used = 57072. Ratio = 0.72.
-Runtime stats:
-Reading = 1.26 sec
-BCP = 204.99 sec
-Trace = 2.85 sec
-TOTAL = 209.85 sec \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 06:14:13 +0000