satProof.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "misc/vec/vecSet.h"
#include "aig/aig/aig.h"
#include "satTruth.h"

Go to the source code of this file.

Data Structures
struct	satset_t

Macros
#define	Proof_ForeachClauseVec(pVec, p, pNode, i)   for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ )
#define	Proof_ForeachNodeVec(pVec, p, pNode, i)   for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
#define	Proof_ForeachNodeVec1(pVec, p, pNode, i)   for ( i = 1; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
#define	Proof_NodeForeachFanin(pProof, pNode, pFanin, i)   for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ )

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct satset_t	satset

Functions
static satset *	Proof_NodeRead (Vec_Set_t *p, int h)
	DECLARATIONS ///. More...
static int	Proof_NodeWordNum (int nEnts)
void	Proof_ClauseSetEnts (Vec_Set_t *p, int h, int nEnts)
void	Proof_CleanCollected (Vec_Set_t *vProof, Vec_Int_t *vUsed)
	FUNCTION DEFINITIONS ///. More...
void	Proof_CollectUsed_iter (Vec_Set_t *vProof, int hNode, Vec_Int_t *vUsed, Vec_Int_t *vStack)
Vec_Int_t *	Proof_CollectUsedIter (Vec_Set_t *vProof, Vec_Int_t *vRoots, int fSort)
void	Proof_CollectUsed_rec (Vec_Set_t *vProof, int hNode, Vec_Int_t *vUsed)
Vec_Int_t *	Proof_CollectUsedRec (Vec_Set_t *vProof, Vec_Int_t *vRoots)
int	Proof_MarkUsed_rec (Vec_Set_t *vProof, int hNode)
int	Proof_MarkUsedRec (Vec_Set_t *vProof, Vec_Int_t *vRoots)
void	Sat_ProofCheck0 (Vec_Set_t *vProof)
int	Sat_ProofReduce (Vec_Set_t *vProof, void *pRoots, int hProofPivot)
Vec_Int_t *	Sat_ProofCollectCore (Vec_Set_t *vProof, Vec_Int_t *vUsed)
void *	Proof_DeriveCore (Vec_Set_t *vProof, int hRoot)

Macro Definition Documentation

#define Proof_ForeachClauseVec	(		pVec,
			p,
			pNode,
			i
	)		for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ )

Definition at line 64 of file satProof.c.

#define Proof_ForeachNodeVec	(		pVec,
			p,
			pNode,
			i
	)		for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )

Definition at line 66 of file satProof.c.

#define Proof_ForeachNodeVec1	(		pVec,
			p,
			pNode,
			i
	)		for ( i = 1; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )

Definition at line 68 of file satProof.c.

#define Proof_NodeForeachFanin	(		pProof,
			pNode,
			pFanin,
			i
	)		for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ )

Definition at line 72 of file satProof.c.

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct satset_t satset

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

FileName [satProof.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver.]

Synopsis [Proof manipulation procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 41 of file satProof.c.

Function Documentation

void Proof_ClauseSetEnts	(	Vec_Set_t *	p,
		int	h,
		int	nEnts
	)

Definition at line 61 of file satProof.c.

{ Proof_NodeRead(p, h)->nEnts = nEnts;             }

void Proof_CleanCollected	(	Vec_Set_t *	vProof,
		Vec_Int_t *	vUsed
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Cleans collected resultion nodes belonging to the proof.]

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file satProof.c.

{
    satset * pNode;
    int hNode;
    Proof_ForeachNodeVec( vUsed, vProof, pNode, hNode )
        pNode->Id = 0;
}

void Proof_CollectUsed_iter	(	Vec_Set_t *	vProof,
		int	hNode,
		Vec_Int_t *	vUsed,
		Vec_Int_t *	vStack
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file satProof.c.

{
    satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
    int i;
    if ( pNode->Id )
        return;
    // start with node
    pNode->Id = 1;
    Vec_IntPush( vStack, hNode << 1 );
    // perform DFS search
    while ( Vec_IntSize(vStack) )
    {
        hNode = Vec_IntPop( vStack );
        if ( hNode & 1 ) // extracted second time
        {
            Vec_IntPush( vUsed, hNode >> 1 );
            continue;
        }
        // extracted first time        
        Vec_IntPush( vStack, hNode ^ 1 ); // add second time
        // add its anticedents        ;
        pNode = Proof_NodeRead( vProof, hNode >> 1 );
        Proof_NodeForeachFanin( vProof, pNode, pNext, i )
            if ( pNext && !pNext->Id )
            {
                pNext->Id = 1;
                Vec_IntPush( vStack, (pNode->pEnts[i] >> 2) << 1 ); // add first time
            }
    }
}

void Proof_CollectUsed_rec	(	Vec_Set_t *	vProof,
		int	hNode,
		Vec_Int_t *	vUsed
	)

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

Synopsis [Recursively collects useful proof nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file satProof.c.

{
    satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
    int i;
    if ( pNode->Id )
        return;
    pNode->Id = 1;
    Proof_NodeForeachFanin( vProof, pNode, pNext, i )
        if ( pNext && !pNext->Id )
            Proof_CollectUsed_rec( vProof, pNode->pEnts[i] >> 2, vUsed );
    Vec_IntPush( vUsed, hNode );
}

Vec_Int_t* Proof_CollectUsedIter	(	Vec_Set_t *	vProof,
		Vec_Int_t *	vRoots,
		int	fSort
	)

Definition at line 145 of file satProof.c.

{
    int fVerify = 0;
    Vec_Int_t * vUsed, * vStack;
    abctime clk = Abc_Clock();
    int i, Entry, iPrev = 0;
    vUsed = Vec_IntAlloc( 1000 );
    vStack = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntry( vRoots, Entry, i )
        if ( Entry >= 0 )
            Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
    Vec_IntFree( vStack );
//    Abc_PrintTime( 1, "Iterative clause collection time", Abc_Clock() - clk );
    clk = Abc_Clock();
    Abc_MergeSort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
//    Abc_PrintTime( 1, "Postprocessing with sorting time", Abc_Clock() - clk );
    // verify topological order
    if ( fVerify )
    {
        iPrev = 0;
        Vec_IntForEachEntry( vUsed, Entry, i )
        {
            if ( iPrev >= Entry )
                printf( "Out of topological order!!!\n" );
            assert( iPrev < Entry );
            iPrev = Entry;
        }
    }
    return vUsed;
}

Vec_Int_t* Proof_CollectUsedRec	(	Vec_Set_t *	vProof,
		Vec_Int_t *	vRoots
	)

Definition at line 199 of file satProof.c.

{
    Vec_Int_t * vUsed;
    int i, Entry;
    vUsed = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntry( vRoots, Entry, i )
        if ( Entry >= 0 )
            Proof_CollectUsed_rec( vProof, Entry, vUsed );
    return vUsed;
}

void* Proof_DeriveCore	(	Vec_Set_t *	vProof,
		int	hRoot
	)

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

Synopsis [Computes UNSAT core.]

Description [The result is the array of root clause indexes.]

SideEffects []

SeeAlso []

Definition at line 913 of file satProof.c.

{
    Vec_Int_t Roots = { 1, 1, &hRoot }, * vRoots = &Roots;
    Vec_Int_t * vCore, * vUsed;
    if ( hRoot == -1 )
        return NULL;
    // collect visited clauses
    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
    // collect core clauses 
    vCore = Sat_ProofCollectCore( vProof, vUsed );
    Vec_IntFree( vUsed );
    Vec_IntSort( vCore, 1 );
    return vCore;
}

int Proof_MarkUsed_rec	(	Vec_Set_t *	vProof,
		int	hNode
	)

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

Synopsis [Recursively visits useful proof nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 221 of file satProof.c.

{
    satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
    int i, Counter = 1;
    if ( pNode->Id )
        return 0;
    pNode->Id = 1;
    Proof_NodeForeachFanin( vProof, pNode, pNext, i )
        if ( pNext && !pNext->Id )
            Counter += Proof_MarkUsed_rec( vProof, pNode->pEnts[i] >> 2 );
    return Counter;
}

int Proof_MarkUsedRec	(	Vec_Set_t *	vProof,
		Vec_Int_t *	vRoots
	)

Definition at line 233 of file satProof.c.

{
    int i, Entry, Counter = 0;
    Vec_IntForEachEntry( vRoots, Entry, i )
        if ( Entry >= 0 )
            Counter += Proof_MarkUsed_rec( vProof, Entry );
    return Counter;
}

static satset* Proof_NodeRead ( Vec_Set_t *  p, int  h  )

inlinestatic

DECLARATIONS ///.

Definition at line 58 of file satProof.c.

{ assert( h > 0 );     return (satset*)Vec_SetEntry( p, h );  }

static int Proof_NodeWordNum ( int  nEnts )

inlinestatic

Definition at line 59 of file satProof.c.

{ assert( nEnts > 0 ); return 1 + ((nEnts + 1) >> 1);         }

void Sat_ProofCheck0

(

Vec_Set_t *

vProof

)

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

Synopsis [Checks the validity of the check point.]

Description []

SideEffects []

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

Synopsis [Reduces the proof to contain only roots and their children.]

Description [The result is updated proof and updated roots.]

SideEffects []

SeeAlso []

Definition at line 371 of file satProof.c.

{
    satset * pNode, * pFanin;
    int i, j, k, nSize;
    Vec_SetForEachEntry( satset *, vProof, nSize, pNode, i, j )
    {
        nSize = Vec_SetWordNum( 2 + pNode->nEnts );
        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
            assert( (pNode->pEnts[k] >> 2) );
    }
}

Vec_Int_t* Sat_ProofCollectCore	(	Vec_Set_t *	vProof,
		Vec_Int_t *	vUsed
	)

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

Synopsis [Collects nodes belonging to the UNSAT core.]

Description [The resulting array contains 1-based IDs of root clauses.]

SideEffects []

SeeAlso []

Definition at line 607 of file satProof.c.

{
    Vec_Int_t * vCore;
    satset * pNode, * pFanin;
    unsigned * pBitMap;
    int i, k, MaxCla = 0;
    // find the largest number
    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
            if ( pFanin == NULL )
                MaxCla = Abc_MaxInt( MaxCla, pNode->pEnts[k] >> 2 );
    // allocate bitmap
    pBitMap = ABC_CALLOC( unsigned, Abc_BitWordNum(MaxCla) + 1 );
    // collect leaves
    vCore = Vec_IntAlloc( 1000 );
    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
            if ( pFanin == NULL )
            {
                int Entry = (pNode->pEnts[k] >> 2);
                if ( Abc_InfoHasBit(pBitMap, Entry) )
                    continue;
                Abc_InfoSetBit(pBitMap, Entry);
                Vec_IntPush( vCore, Entry );
            }
    ABC_FREE( pBitMap );
//    Vec_IntUniqify( vCore );
    return vCore;
}

int Sat_ProofReduce	(	Vec_Set_t *	vProof,
		void *	pRoots,
		int	hProofPivot
	)

Definition at line 383 of file satProof.c.

{
//    Vec_Set_t * vProof   = (Vec_Set_t *)&s->Proofs;
//    Vec_Int_t * vRoots   = (Vec_Int_t *)&s->claProofs;
    Vec_Int_t * vRoots   = (Vec_Int_t *)pRoots;
//    Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
    int fVerbose = 0;
    Vec_Ptr_t * vUsed;
    satset * pNode, * pFanin, * pPivot;
    int i, j, k, hTemp, nSize;
    abctime clk = Abc_Clock();
    static abctime TimeTotal = 0;
    int RetValue;
//Sat_ProofCheck0( vProof );

    // collect visited nodes
    nSize = Proof_MarkUsedRec( vProof, vRoots );
    vUsed = Vec_PtrAlloc( nSize );
//Sat_ProofCheck0( vProof );

    // relabel nodes to use smaller space
    Vec_SetShrinkS( vProof, 2 );
    Vec_SetForEachEntry( satset *, vProof, nSize, pNode, i, j )
    {
        nSize = Vec_SetWordNum( 2 + pNode->nEnts );
        if ( pNode->Id == 0 ) 
            continue;
        pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
        assert( pNode->Id > 0 );
        Vec_PtrPush( vUsed, pNode );
        // update fanins
        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
            if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
            {
                assert( pFanin->Id > 0 );
                pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
            }
//            else // problem clause
//                assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
    }
    // update roots
    Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
        Vec_IntWriteEntry( vRoots, i, pNode->Id );
    // determine new pivot
    assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) );
    pPivot = Proof_NodeRead( vProof, hProofPivot );
    RetValue = Vec_SetHandCurrentS(vProof);
    // compact the nodes
    Vec_PtrForEachEntry( satset *, vUsed, pNode, i )
    {
        hTemp = pNode->Id; pNode->Id = 0;
        memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
        if ( pPivot && pPivot <= pNode )
        {
            RetValue = hTemp;
            pPivot = NULL;
        }
    }
    Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) );
    Vec_PtrFree( vUsed );

    // report the result
    if ( fVerbose )
    {
        printf( "\n" );
        printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%)  ", 
            1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20), 
            100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
        TimeTotal += Abc_Clock() - clk;
        Abc_PrintTime( 1, "Time", TimeTotal );
    }
    Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
    Vec_SetShrinkLimits( vProof );
//    Sat_ProofReduceCheck( s );
//Sat_ProofCheck0( vProof );

    return RetValue;
}