simSymSat.c File Reference

#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "sim.h"

Include dependency graph for simSymSat.c:

Go to the source code of this file.

Functions
int	Sim_SymmsGetPatternUsingSat (Sym_Man_t *p, unsigned *pPattern)
	FUNCTION DEFINITIONS ///.

Function Documentation

Sim_SymmsGetPatternUsingSat()

int Sim_SymmsGetPatternUsingSat	(	Sym_Man_t *	p,
		unsigned *	pPattern )

FUNCTION DEFINITIONS ///.

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

Synopsis [Tries to prove the remaining pairs using SAT.]

Description [Continues to prove as long as it encounters symmetric pairs. Returns 1 if a non-symmetric pair is found (which gives a counter-example). Returns 0 if it finishes considering all pairs for all outputs.]

SideEffects []

SeeAlso []

Definition at line 51 of file simSymSat.c.

{
    Vec_Int_t * vSupport;
    Extra_BitMat_t * pMatSym, * pMatNonSym;
    int Index1, Index2, Index3, IndexU, IndexV;
    int v, u, i, k, b, out;
 
    // iterate through outputs
    for ( out = p->iOutput; out < p->nOutputs; out++ )
    {
        pMatSym    = (Extra_BitMat_t *)Vec_PtrEntry( p->vMatrSymms,    out );
        pMatNonSym = (Extra_BitMat_t *)Vec_PtrEntry( p->vMatrNonSymms, out );
 
        // go through the remaining variable pairs
        vSupport = Vec_VecEntryInt( p->vSupports, out );
        Vec_IntForEachEntry( vSupport, v, Index1 )
        Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
        {
            if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
                continue;
            p->nSatRuns++;
 
            // collect the support variables that are symmetric with u and v
            Vec_IntClear( p->vVarsU );
            Vec_IntClear( p->vVarsV );
            Vec_IntForEachEntry( vSupport, b, Index3 )
            {
                if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
                    Vec_IntPush( p->vVarsU, b );
                if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
                    Vec_IntPush( p->vVarsV, b );
            }
 
            if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
            { // update the symmetric variable info            
                p->nSatRunsUnsat++;
                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
                {
                    Extra_BitMatrixInsert1( pMatSym,  i, k );  // Theorem 1
                    Extra_BitMatrixInsert2( pMatSym,  i, k );  // Theorem 1
                    Extra_BitMatrixOrTwo( pMatNonSym, i, k );  // Theorem 2
                }
            }
            else
            { // update the assymmetric variable info
                p->nSatRunsSat++;
                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
                {
                    Extra_BitMatrixInsert1( pMatNonSym, i, k );   // Theorem 3
                    Extra_BitMatrixInsert2( pMatNonSym, i, k );   // Theorem 3
                }
 
                // remember the out
                p->iOutput = out;
                p->iVar1Old = p->iVar1;
                p->iVar2Old = p->iVar2;
                p->iVar1 = v;
                p->iVar2 = u;
                return 1;
 
            }
        }
        // make sure that the symmetry matrix contains only cliques
        assert( Extra_BitMatrixIsClique( pMatSym ) );
    }
 
    // mark that we finished all outputs
    p->iOutput = p->nOutputs;
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function: