src/sat/proof/pr.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "pr.h"

Include dependency graph for pr.c:

Go to the source code of this file.

Data Structures
struct	Pr_Cls_t_
struct	Pr_Man_t_
Defines
#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 )
Typedefs
typedef unsigned	lit
typedef struct Pr_Cls_t_	Pr_Cls_t
Functions
static lit	toLit (int v)
static lit	toLitCond (int v, int c)
static lit	lit_neg (lit l)
static int	lit_var (lit l)
static int	lit_sign (lit l)
static int	lit_print (lit l)
static lit	lit_read (int s)
static int	lit_check (lit l, int n)
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)
Pr_Man_t *	Pr_ManAlloc (int nVarsAlloc)
void	Pr_ManFree (Pr_Man_t *p)
int	Pr_ManAddClause (Pr_Man_t *p, lit *pBeg, lit *pEnd, int fRoot, int fClauseA)
int	Pr_ManProofWrite (Pr_Man_t *p)
static void	Pr_ManWatchClause (Pr_Man_t *p, Pr_Cls_t *pClause, lit Lit)
int	Pr_ManMemoryReport (Pr_Man_t *p)
void	Extra_PrintBinary_ (FILE *pFile, unsigned Sign[], int nBits)
void	Pr_ManPrintInterOne (Pr_Man_t *p, Pr_Cls_t *pClause)
static int	Pr_ManEnqueue (Pr_Man_t *p, lit Lit, Pr_Cls_t *pReason)
static void	Pr_ManCancelUntil (Pr_Man_t *p, int Level)
static Pr_Cls_t *	Pr_ManPropagateOne (Pr_Man_t *p, lit Lit)
Pr_Cls_t *	Pr_ManPropagate (Pr_Man_t *p, int Start)
void	Pr_ManPrintClause (Pr_Cls_t *pClause)
void	Pr_ManPrintResolvent (lit *pResLits, int nResLits)
void	Pr_ManProofWriteOne (Pr_Man_t *p, Pr_Cls_t *pClause)
int	Pr_ManProofTraceOne (Pr_Man_t *p, Pr_Cls_t *pConflict, Pr_Cls_t *pFinal)
int	Pr_ManProofRecordOne (Pr_Man_t *p, Pr_Cls_t *pClause)
int	Pr_ManProcessRoots (Pr_Man_t *p)
void	Pr_ManPrepareInter (Pr_Man_t *p)
Pr_Man_t *	Pr_ManProofRead (char *pFileName)
int	Pr_ManProofTest (char *pFileName)
Variables
static const lit	LIT_UNDEF = 0xffffffff

---

Define Documentation

#define Pr_ManForEachClause	(	p,
		pCls		)	for( pCls = p->pHead; pCls; pCls = pCls->pNext )

Definition at line 112 of file pr.c.

#define Pr_ManForEachClauseLearnt	(	p,
		pCls		)	for( pCls = p->pLearnt; pCls; pCls = pCls->pNext )

Definition at line 114 of file pr.c.

#define Pr_ManForEachClauseRoot	(	p,
		pCls		)	for( pCls = p->pHead; pCls != p->pLearnt; pCls = pCls->pNext )

Definition at line 113 of file pr.c.

---

Typedef Documentation

typedef unsigned lit

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

] DECLARATIONS ///

Definition at line 33 of file pr.c.

typedef struct Pr_Cls_t_ Pr_Cls_t

Definition at line 35 of file pr.c.

---

Function Documentation

void Extra_PrintBinary_	(	FILE *	pFile,
		unsigned	Sign[],
		int	nBits
	)

Function*************************************************************

Synopsis [Records the proof.]

Description []

SideEffects []

SeeAlso []

Definition at line 416 of file pr.c.

{
    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) );
}

static int lit_check	(	lit	l,
		int	n
	)			[inline, static]

Definition at line 109 of file pr.c.

{ return l >= 0 && lit_var(l) < n;                  }

static lit lit_neg

(

lit

l

)

[inline, static]

Definition at line 104 of file pr.c.

{ return l ^ 1;  }

static int lit_print

(

lit

l

)

[inline, static]

Definition at line 107 of file pr.c.

{ return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }

static lit lit_read

(

int

s

)

[inline, static]

Definition at line 108 of file pr.c.

{ return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }

static int lit_sign

(

lit

l

)

[inline, static]

Definition at line 106 of file pr.c.

{ return l & 1;  }

static int lit_var

(

lit

l

)

[inline, static]

Definition at line 105 of file pr.c.

{ return l >> 1; }

int Pr_ManAddClause	(	Pr_Man_t *	p,
		lit *	pBeg,
		lit *	pEnd,
		int	fRoot,
		int	fClauseA
	)

Function*************************************************************

Synopsis [Adds one clause to the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file pr.c.

{
    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;
}

Pr_Man_t * Pr_ManAlloc

(

int

nVarsAlloc

)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file pr.c.

{
    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;    
}

static void Pr_ManCancelUntil	(	Pr_Man_t *	p,
		int	Level
	)			[inline, static]

Function*************************************************************

Synopsis [Records implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 483 of file pr.c.

{
    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;
}

static int Pr_ManEnqueue	(	Pr_Man_t *	p,
		lit	Lit,
		Pr_Cls_t *	pReason
	)			[inline, static]

Function*************************************************************

Synopsis [Records implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 460 of file pr.c.

{
    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;
}

void Pr_ManFree

(

Pr_Man_t *

p

)

Function*************************************************************

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 215 of file pr.c.

{
    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 );
}

char * Pr_ManMemoryFetch	(	Pr_Man_t *	p,
		int	nBytes
	)			[static]

Function*************************************************************

Synopsis [Fetches memory.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file pr.c.

{
    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;
}

int Pr_ManMemoryReport

(

Pr_Man_t *

p

)

Function*************************************************************

Synopsis [Reports memory usage in bytes.]

Description []

SideEffects []

SeeAlso []

Definition at line 393 of file pr.c.

{
    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;
}

void Pr_ManMemoryStop

(

Pr_Man_t *

p

)

[static]

Function*************************************************************

Synopsis [Frees memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 372 of file pr.c.

{
    char * pMem, * pNext;
    if ( p->pChunkLast == NULL )
        return;
    for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
        free( pMem );
    free( pMem );
}

void Pr_ManPrepareInter

(

Pr_Man_t *

p

)

Function*************************************************************

Synopsis [Records the proof.]

Description []

SideEffects []

SeeAlso []

Definition at line 974 of file pr.c.

{
    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 );
    }
}

void Pr_ManPrintClause

(

Pr_Cls_t *

pClause

)

Function*************************************************************

Synopsis [Prints the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 608 of file pr.c.

{
    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" );
}

void Pr_ManPrintInterOne	(	Pr_Man_t *	p,
		Pr_Cls_t *	pClause
	)

Function*************************************************************

Synopsis [Prints the interpolant for one clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file pr.c.

{
    printf( "Clause %2d :  ", pClause->Id );
    Extra_PrintBinary_( stdout, &pClause->uTruth, (1 << p->nVarsAB) );
    printf( "\n" );
}

void Pr_ManPrintResolvent	(	lit *	pResLits,
		int	nResLits
	)

Function*************************************************************

Synopsis [Prints the resolvent.]

Description []

SideEffects []

SeeAlso []

Definition at line 628 of file pr.c.

{
    int i;
    printf( "Resolvent: {" );
    for ( i = 0; i < nResLits; i++ )
        printf( " %d", pResLits[i] );
    printf( " }\n" );
}

int Pr_ManProcessRoots

(

Pr_Man_t *

p

)

Function*************************************************************

Synopsis [Propagate the root clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 906 of file pr.c.

{
    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;
}

Pr_Man_t* Pr_ManProofRead

(

char *

pFileName

)

Function*************************************************************

Synopsis [Reads clauses from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 1109 of file pr.c.

{
    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;
}

int Pr_ManProofRecordOne	(	Pr_Man_t *	p,
		Pr_Cls_t *	pClause
	)

Function*************************************************************

Synopsis [Records the proof for one clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 830 of file pr.c.

{
    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;
}

int Pr_ManProofTest

(

char *

pFileName

)

Function*************************************************************

Synopsis [Records the proof.]

Description []

SideEffects []

SeeAlso []Function*************************************************************

Synopsis [Records the proof.]

Description []

SideEffects []

SeeAlso []

Definition at line 1227 of file pr.c.

{
    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;
}

int Pr_ManProofTraceOne	(	Pr_Man_t *	p,
		Pr_Cls_t *	pConflict,
		Pr_Cls_t *	pFinal
	)

Function*************************************************************

Synopsis [Traces the proof for one clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 673 of file pr.c.

{
    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;
}

int Pr_ManProofWrite

(

Pr_Man_t *

p

)

Function*************************************************************

Synopsis [Records the proof.]

Description []

SideEffects []

SeeAlso []

Definition at line 1051 of file pr.c.

{
    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;
}

void Pr_ManProofWriteOne	(	Pr_Man_t *	p,
		Pr_Cls_t *	pClause
	)

Function*************************************************************

Synopsis [Writes one root clause into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 648 of file pr.c.

{
    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" );
    }
}

Pr_Cls_t* Pr_ManPropagate	(	Pr_Man_t *	p,
		int	Start
	)

Function*************************************************************

Synopsis [Propagate the current assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 578 of file pr.c.

{
    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;
}

static Pr_Cls_t* Pr_ManPropagateOne	(	Pr_Man_t *	p,
		lit	Lit
	)			[inline, static]

Function*************************************************************

Synopsis [Propagate one assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 509 of file pr.c.

{
    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;
}

void Pr_ManResize	(	Pr_Man_t *	p,
		int	nVarsNew
	)			[static]

Function*************************************************************

Synopsis [Resize proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file pr.c.

{
    // 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;
}

static void Pr_ManWatchClause	(	Pr_Man_t *	p,
		Pr_Cls_t *	pClause,
		lit	Lit
	)			[inline, static]

Function*************************************************************

Synopsis [Adds one clause to the watcher list.]

Description []

SideEffects []

SeeAlso []

Definition at line 245 of file pr.c.

{
    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;
}

static lit toLit

(

int

v

)

[inline, static]

Definition at line 102 of file pr.c.

{ return v + v;  }

static lit toLitCond	(	int	v,
		int	c
	)			[inline, static]

Definition at line 103 of file pr.c.

{ return v + v + (c != 0); }

---

Variable Documentation

const lit LIT_UNDEF = 0xffffffff [static]

Definition at line 99 of file pr.c.