satInter.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "satStore.h"

Go to the source code of this file.

Data Structures
struct	Int_Man_t_

Functions
static unsigned *	Int_ManTruthRead (Int_Man_t *p, Sto_Cls_t *pCls)
static void	Int_ManTruthClear (unsigned *p, int nWords)
static void	Int_ManTruthFill (unsigned *p, int nWords)
static void	Int_ManTruthCopy (unsigned *p, unsigned *q, int nWords)
static void	Int_ManTruthAnd (unsigned *p, unsigned *q, int nWords)
static void	Int_ManTruthOr (unsigned *p, unsigned *q, int nWords)
static void	Int_ManTruthOrNot (unsigned *p, unsigned *q, int nWords)
static int	Int_ManProofGet (Int_Man_t *p, Sto_Cls_t *pCls)
static void	Int_ManProofSet (Int_Man_t *p, Sto_Cls_t *pCls, int n)
Int_Man_t *	Int_ManAlloc ()
	FUNCTION DEFINITIONS ///. More...
int *	Int_ManSetGlobalVars (Int_Man_t *p, int nGloVars)
int	Int_ManGlobalVars (Int_Man_t *p)
void	Int_ManResize (Int_Man_t *p)
void	Int_ManFree (Int_Man_t *p)
void	Int_ManPrintClause (Int_Man_t *p, Sto_Cls_t *pClause)
void	Int_ManPrintResolvent (lit *pResLits, int nResLits)
void	Extra_PrintBinary__ (FILE *pFile, unsigned Sign[], int nBits)
void	Int_ManPrintInterOne (Int_Man_t *p, Sto_Cls_t *pClause)
static void	Int_ManWatchClause (Int_Man_t *p, Sto_Cls_t *pClause, lit Lit)
static int	Int_ManEnqueue (Int_Man_t *p, lit Lit, Sto_Cls_t *pReason)
static void	Int_ManCancelUntil (Int_Man_t *p, int Level)
static Sto_Cls_t *	Int_ManPropagateOne (Int_Man_t *p, lit Lit)
Sto_Cls_t *	Int_ManPropagate (Int_Man_t *p, int Start)
void	Int_ManProofWriteOne (Int_Man_t *p, Sto_Cls_t *pClause)
int	Int_ManProofTraceOne (Int_Man_t *p, Sto_Cls_t *pConflict, Sto_Cls_t *pFinal)
int	Int_ManProofRecordOne (Int_Man_t *p, Sto_Cls_t *pClause)
int	Int_ManProcessRoots (Int_Man_t *p)
void	Int_ManPrepareInter (Int_Man_t *p)
int	Int_ManInterpolate (Int_Man_t *p, Sto_Man_t *pCnf, int fVerbose, unsigned **ppResult)

Variables
static ABC_NAMESPACE_IMPL_START const lit	LIT_UNDEF = 0xffffffff
	DECLARATIONS ///. More...

Function Documentation

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

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

Synopsis [Records the proof.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file satInter.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) );
}

Int_Man_t* Int_ManAlloc

(

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file satInter.c.

{
    Int_Man_t * p;
    // allocate the manager
    p = (Int_Man_t *)ABC_ALLOC( char, sizeof(Int_Man_t) );
    memset( p, 0, sizeof(Int_Man_t) );
    // verification
    p->nResLitsAlloc = (1<<16);
    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
    // parameters
    p->fProofWrite = 0;
    p->fProofVerif = 1;
    return p;    
}

static void Int_ManCancelUntil ( Int_Man_t *  p, int  Level  )

inlinestatic

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

Synopsis [Records implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file satInter.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 Int_ManEnqueue ( Int_Man_t *  p, lit  Lit, Sto_Cls_t *  pReason  )

inlinestatic

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

Synopsis [Records implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 416 of file satInter.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 Int_ManFree

(

Int_Man_t *

p

)

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file satInter.c.

{
/*
    printf( "Runtime stats:\n" );
ABC_PRT( "BCP     ", p->timeBcp   );
ABC_PRT( "Trace   ", p->timeTrace );
ABC_PRT( "TOTAL   ", p->timeTotal );
*/
    ABC_FREE( p->pInters );
    ABC_FREE( p->pProofNums );
    ABC_FREE( p->pTrail );
    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pSeens );
    ABC_FREE( p->pVarTypes );
    ABC_FREE( p->pReasons );
    ABC_FREE( p->pWatches );
    ABC_FREE( p->pResLits );
    ABC_FREE( p );
}

int Int_ManGlobalVars

(

Int_Man_t *

p

)

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

Synopsis [Count common variables in the clauses of A and B.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file satInter.c.

{
    Sto_Cls_t * pClause;
    int Var, nVarsAB, v;

    // mark the variable encountered in the clauses of A
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
    {
        if ( !pClause->fA )
            break;
        for ( v = 0; v < (int)pClause->nLits; v++ )
            p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
    }

    if ( p->nGloVars )
    {
        for ( v = 0; v < p->nGloVars; v++ )
            p->pVarTypes[ p->pGloVars[v] ] = - v - 1;
        return p->nGloVars;
    }

    // check variables that appear in clauses of B
    nVarsAB = 0;
    Sto_ManForEachClauseRoot( p->pCnf, 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
                nVarsAB++;
                p->pVarTypes[Var] = -1;
            }
        }
    }

    // order global variables
    nVarsAB = 0;
    for ( v = 0; v < p->pCnf->nVars; v++ )
        if ( p->pVarTypes[v] == -1 )
            p->pVarTypes[v] -= nVarsAB++;
//printf( "There are %d global variables.\n", nVarsAB );
    return nVarsAB;
}

int Int_ManInterpolate	(	Int_Man_t *	p,
		Sto_Man_t *	pCnf,
		int	fVerbose,
		unsigned **	ppResult
	)

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

Synopsis [Computes interpolant for the given CNF.]

Description [Returns the number of common variable found and interpolant. Returns 0, if something did not work.]

SideEffects []

SeeAlso []

Definition at line 1005 of file satInter.c.

{
    Sto_Cls_t * pClause;
    int RetValue = 1;
    abctime clkTotal = Abc_Clock();

    // check that the CNF makes sense
    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
    p->pCnf = pCnf;
    p->fVerbose = fVerbose;
    *ppResult = NULL;

    // adjust the manager
    Int_ManResize( p );

    // prepare the interpolant computation
    Int_ManPrepareInter( p );

    // construct proof for each clause
    // start the proof
    if ( p->fProofWrite )
    {
        p->pFile = fopen( "proof.cnf_", "w" );
        p->Counter = 0;
    }

    // write the root clauses
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
        Int_ManProofWriteOne( p, pClause );

    // propagate root level assignments
    if ( Int_ManProcessRoots( p ) )
    {
        // if there is no conflict, consider learned clauses
        Sto_ManForEachClause( p->pCnf, pClause )
        {
            if ( pClause->fRoot )
                continue;
            if ( !Int_ManProofRecordOne( p, pClause ) )
            {
                RetValue = 0;
                break;
            }
        }
    }

    // stop the proof
    if ( p->fProofWrite )
    {
        fclose( p->pFile );
        p->pFile = NULL;    
    }

    if ( fVerbose )
    {
    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n", 
        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += Abc_Clock() - clkTotal;
    }

    *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
    return p->nVarsAB;
}

void Int_ManPrepareInter

(

Int_Man_t *

p

)

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

Synopsis [Records the proof.]

Description []

SideEffects []

SeeAlso []

Definition at line 948 of file satInter.c.

{
    // elementary truth tables
    unsigned uTruths[8][8] = {
        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
    };
    Sto_Cls_t * pClause;
    int Var, VarAB, v;
    assert( p->nVarsAB <= 8 );

    // set interpolants for root clauses
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
    {
        if ( !pClause->fA ) // clause of B
        {
            Int_ManTruthFill( Int_ManTruthRead(p, pClause), p->nWords );
//            Int_ManPrintInterOne( p, pClause );
            continue;
        }
        // clause of A
        Int_ManTruthClear( Int_ManTruthRead(p, pClause), p->nWords );
        for ( v = 0; v < (int)pClause->nLits; v++ )
        {
            Var = lit_var(pClause->pLits[v]);
            if ( p->pVarTypes[Var] < 0 ) // global var
            {
                VarAB = -p->pVarTypes[Var]-1;
                assert( VarAB >= 0 && VarAB < p->nVarsAB );
                if ( lit_sign(pClause->pLits[v]) ) // negative var
                    Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
                else
                    Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
            }
        }
//        Int_ManPrintInterOne( p, pClause );
    }
}

void Int_ManPrintClause	(	Int_Man_t *	p,
		Sto_Cls_t *	pClause
	)

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

Synopsis [Prints the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file satInter.c.

{
    int i;
    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofGet(p, pClause) );
    for ( i = 0; i < (int)pClause->nLits; i++ )
        printf( " %d", pClause->pLits[i] );
    printf( " }\n" );
}

void Int_ManPrintInterOne	(	Int_Man_t *	p,
		Sto_Cls_t *	pClause
	)

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

Synopsis [Prints the interpolant for one clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 371 of file satInter.c.

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

void Int_ManPrintResolvent	(	lit *	pResLits,
		int	nResLits
	)

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

Synopsis [Prints the resolvent.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file satInter.c.

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

int Int_ManProcessRoots

(

Int_Man_t *

p

)

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

Synopsis [Propagate the root clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 875 of file satInter.c.

{
    Sto_Cls_t * pClause;
    int Counter;

    // make sure the root clauses are preceeding the learnt clauses
    Counter = 0;
    Sto_ManForEachClause( p->pCnf, pClause )
    {
        assert( (int)pClause->fA    == (Counter < (int)p->pCnf->nClausesA) );
        assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots)    );
        Counter++;
    }
    assert( p->pCnf->nClauses == Counter );

    // make sure the last clause if empty
    assert( p->pCnf->pTail->nLits == 0 );

    // go through the root unit clauses
    p->nTrailSize = 0;
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
    {
        // create watcher lists for the root clauses
        if ( pClause->nLits > 1 )
        {
            Int_ManWatchClause( p, pClause, pClause->pLits[0] );
            Int_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->pCnf->nVars) );
        if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
        {
            // detected root level conflict
//            printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
//            assert( 0 );
            // detected root level conflict
            Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
            if ( p->fVerbose )
                printf( "Found root level conflict!\n" );
            return 0;
        }
    }

    // propagate the root unit clauses
    pClause = Int_ManPropagate( p, 0 );
    if ( pClause )
    {
        // detected root level conflict
        Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
        if ( p->fVerbose )
            printf( "Found root level conflict!\n" );
        return 0;
    }

    // set the root level
    p->nRootSize = p->nTrailSize;
    return 1;
}

static int Int_ManProofGet ( Int_Man_t *  p, Sto_Cls_t *  pCls  )

inlinestatic

Definition at line 89 of file satInter.c.

{ return p->pProofNums[pCls->Id];  }

int Int_ManProofRecordOne	(	Int_Man_t *	p,
		Sto_Cls_t *	pClause
	)

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

Synopsis [Records the proof for one clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 770 of file satInter.c.

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

    // if any of the clause literals are already assumed
    // it means that the clause is redundant and can be skipped
    for ( i = 0; i < (int)pClause->nLits; i++ )
        if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
            return 1;

    for ( i = 0; i < (int)pClause->nLits; i++ )
        if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
        {
            assert( 0 ); // impossible
            return 0;
        }

    // propagate the assumptions
    pConflict = Int_ManPropagate( p, p->nRootSize );
    if ( pConflict == NULL )
    {
        assert( 0 ); // cannot prove
        return 0;
    }

    // skip the clause if it is weaker or the same as the conflict clause
    if ( pClause->nLits >= pConflict->nLits )
    {
        // check if every literal of conflict clause can be found in the given clause
        int j;
        for ( i = 0; i < (int)pConflict->nLits; i++ )
        {
            for ( j = 0; j < (int)pClause->nLits; j++ )
                if ( pConflict->pLits[i] == pClause->pLits[j] )
                    break;
            if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found
                break;
        }
        if ( i == (int)pConflict->nLits ) // all lits are found
        {
            // undo to the root level
            Int_ManCancelUntil( p, p->nRootSize );
            return 1;
        }
    }

    // construct the proof
    Int_ManProofTraceOne( p, pConflict, pClause );

    // undo to the root level
    Int_ManCancelUntil( p, p->nRootSize );

    // add large clauses to the watched lists
    if ( pClause->nLits > 1 )
    {
        Int_ManWatchClause( p, pClause, pClause->pLits[0] );
        Int_ManWatchClause( p, pClause, pClause->pLits[1] );
        return 1;
    }
    assert( pClause->nLits == 1 );

    // if the clause proved is unit, add it and propagate
    if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
    {
        assert( 0 ); // impossible
        return 0;
    }

    // propagate the assumption
    pConflict = Int_ManPropagate( p, p->nRootSize );
    if ( pConflict )
    {
        // construct the proof
        Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
        if ( p->fVerbose )
            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;
}

static void Int_ManProofSet ( Int_Man_t *  p, Sto_Cls_t *  pCls, int  n  )

inlinestatic

Definition at line 90 of file satInter.c.

{ p->pProofNums[pCls->Id] = n;     }

int Int_ManProofTraceOne	(	Int_Man_t *	p,
		Sto_Cls_t *	pConflict,
		Sto_Cls_t *	pFinal
	)

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

Synopsis [Traces the proof for one clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 589 of file satInter.c.

{
    Sto_Cls_t * pReason;
    int i, v, Var, PrevId;
    int fPrint = 0;
    abctime clk = Abc_Clock();

    // collect resolvent literals
    if ( p->fProofVerif )
    {
        assert( (int)pConflict->nLits <= p->nResLitsAlloc );
        memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
        p->nResLits = pConflict->nLits;
    }

    // mark all the variables in the conflict as seen
    for ( v = 0; v < (int)pConflict->nLits; v++ )
        p->pSeens[lit_var(pConflict->pLits[v])] = 1;

    // start the anticedents
//    pFinal->pAntis = Vec_PtrAlloc( 32 );
//    Vec_PtrPush( pFinal->pAntis, pConflict );

    if ( p->pCnf->nClausesA )
        Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords );

    // follow the trail backwards
    PrevId = Int_ManProofGet(p, pConflict);
    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( Int_ManProofGet(p, pReason) > 0 );
        p->Counter++;
        if ( p->fProofWrite )
            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) );
        PrevId = p->Counter;

        if ( p->pCnf->nClausesA )
        {
            if ( p->pVarTypes[Var] == 1 ) // var of A
                Int_ManTruthOr( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
            else
                Int_ManTruthAnd( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
        }
 
        // resolve the temporary resolvent with the reason clause
        if ( p->fProofVerif )
        {
            int v1, v2; 
            if ( fPrint )
                Int_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 )
            Int_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 );
            Int_ManPrintClause( p, pConflict );
            Int_ManPrintResolvent( p->pResLits, p->nResLits );
            Int_ManPrintClause( p, pFinal );
        }

        // if there are literals in the clause that are not in the resolvent
        // it means that the derived resolvent is stronger than the clause
        // we can replace the clause with the resolvent by removing these literals
        if ( p->nResLits != (int)pFinal->nLits )
        {
            for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
            {
                for ( v2 = 0; v2 < p->nResLits; v2++ )
                    if ( pFinal->pLits[v1] == p->pResLits[v2] )
                        break;
                if ( v2 < p->nResLits )
                    continue;
                // remove literal v1 from the final clause
                pFinal->nLits--;
                for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
                    pFinal->pLits[v2] = pFinal->pLits[v2+1];
                v1--;
            }
            assert( p->nResLits == (int)pFinal->nLits );
        }
    }
p->timeTrace += Abc_Clock() - clk;

    // return the proof pointer 
    if ( p->pCnf->nClausesA )
    {
//        Int_ManPrintInterOne( p, pFinal );
    }
    Int_ManProofSet( p, pFinal, p->Counter );
    // make sure the same proof ID is not asssigned to two consecutive clauses
    assert( p->pProofNums[pFinal->Id-1] != p->Counter );
    return p->Counter;
}

void Int_ManProofWriteOne	(	Int_Man_t *	p,
		Sto_Cls_t *	pClause
	)

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

Synopsis [Writes one root clause into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 564 of file satInter.c.

{
    Int_ManProofSet( p, pClause, ++p->Counter );

    if ( p->fProofWrite )
    {
        int v;
        fprintf( p->pFile, "%d", Int_ManProofGet(p, pClause) );
        for ( v = 0; v < (int)pClause->nLits; v++ )
            fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
        fprintf( p->pFile, " 0 0\n" );
    }
}

Sto_Cls_t* Int_ManPropagate	(	Int_Man_t *	p,
		int	Start
	)

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

Synopsis [Propagate the current assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 534 of file satInter.c.

{
    Sto_Cls_t * pClause;
    int i;
    abctime clk = Abc_Clock();
    for ( i = Start; i < p->nTrailSize; i++ )
    {
        pClause = Int_ManPropagateOne( p, p->pTrail[i] );
        if ( pClause )
        {
p->timeBcp += Abc_Clock() - clk;
            return pClause;
        }
    }
p->timeBcp += Abc_Clock() - clk;
    return NULL;
}

static Sto_Cls_t* Int_ManPropagateOne ( Int_Man_t *  p, lit  Lit  )

inlinestatic

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

Synopsis [Propagate one assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 465 of file satInter.c.

{
    Sto_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])
            Int_ManWatchClause( p, pCur, pCur->pLits[1] );
            break;
        }
        if ( i < (int)pCur->nLits ) // found new watch
            continue;

        // clause is unit - enqueue new implication
        if ( Int_ManEnqueue(p, pCur->pLits[0], pCur) )
        {
            ppPrev = &pCur->pNext1;
            continue;
        }

        // conflict detected - return the conflict clause
        return pCur;
    }
    return NULL;
}

void Int_ManResize

(

Int_Man_t *

p

)

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

Synopsis [Resize proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file satInter.c.

{
    // check if resizing is needed
    if ( p->nVarsAlloc < p->pCnf->nVars )
    {
        // find the new size
        if ( p->nVarsAlloc == 0 )
            p->nVarsAlloc = 1;
        while ( p->nVarsAlloc < p->pCnf->nVars ) 
            p->nVarsAlloc *= 2;
        // resize the arrays
        p->pTrail    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
    }

    // clean the free space
    memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
    memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
    memset( p->pVarTypes, 0,    sizeof(int) * p->pCnf->nVars );
    memset( p->pReasons , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars );
    memset( p->pWatches , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );

    // compute the number of common variables
    p->nVarsAB = Int_ManGlobalVars( p );
    // compute the number of words in the truth table
    p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5)));

    // check if resizing of clauses is needed
    if ( p->nClosAlloc < p->pCnf->nClauses )
    {
        // find the new size
        if ( p->nClosAlloc == 0 )
            p->nClosAlloc = 1;
        while ( p->nClosAlloc < p->pCnf->nClauses ) 
            p->nClosAlloc *= 2;
        // resize the arrays
        p->pProofNums = ABC_REALLOC(int, p->pProofNums,  p->nClosAlloc );
    }
    memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );

    // check if resizing of truth tables is needed
    if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses )
    {
        p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
        p->pInters = ABC_REALLOC(unsigned, p->pInters, p->nIntersAlloc );
    }
//    memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses );
}

int* Int_ManSetGlobalVars	(	Int_Man_t *	p,
		int	nGloVars
	)

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file satInter.c.

{
    p->nGloVars = nGloVars;
    return p->pGloVars;
}

static void Int_ManTruthAnd ( unsigned *  p, unsigned *  q, int  nWords  )

inlinestatic

Definition at line 84 of file satInter.c.

{ int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &=  q[i]; }

static void Int_ManTruthClear ( unsigned *  p, int  nWords  )

inlinestatic

Definition at line 81 of file satInter.c.

{ int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  0;    }

static void Int_ManTruthCopy ( unsigned *  p, unsigned *  q, int  nWords  )

inlinestatic

Definition at line 83 of file satInter.c.

{ int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  q[i]; }

static void Int_ManTruthFill ( unsigned *  p, int  nWords  )

inlinestatic

Definition at line 82 of file satInter.c.

{ int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  = ~0;    }

static void Int_ManTruthOr ( unsigned *  p, unsigned *  q, int  nWords  )

inlinestatic

Definition at line 85 of file satInter.c.

{ int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |=  q[i]; }

static void Int_ManTruthOrNot ( unsigned *  p, unsigned *  q, int  nWords  )

inlinestatic

Definition at line 86 of file satInter.c.

{ int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; }

static unsigned* Int_ManTruthRead ( Int_Man_t *  p, Sto_Cls_t *  pCls  )

inlinestatic

Definition at line 80 of file satInter.c.

{ return p->pInters + pCls->Id * p->nWords;                 }

static void Int_ManWatchClause ( Int_Man_t *  p, Sto_Cls_t *  pClause, lit  Lit  )

inlinestatic

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

Synopsis [Adds one clause to the watcher list.]

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file satInter.c.

{
    assert( lit_check(Lit, p->pCnf->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;
}

Variable Documentation

ABC_NAMESPACE_IMPL_START const lit LIT_UNDEF = 0xffffffff

static

DECLARATIONS ///.

CFile****************************************************************

FileName [satInter.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT sat_solver.]

Synopsis [Interpolation package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp

]

Definition at line 36 of file satInter.c.