abc/src/opt/sim/simSymSat.c
/**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     []

***********************************************************************/
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.]




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 . ]
int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
{
    Vec_Int_t * vSupport;
    Extra_BitMat_t * pMatSym, * pMatNonSym;
    int Index1, Index2, Index3, IndexU, IndexV;
    int v, u, i, k, b, out;
    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 );
        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++;
            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 ) )
            { 
                p->nSatRunsUnsat++;
                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
                {
                    Extra_BitMatrixInsert1( pMatSym,  i, k );  
                    Extra_BitMatrixInsert2( pMatSym,  i, k );  
                    Extra_BitMatrixOrTwo( pMatNonSym, i, k );  
                }
            }
            else
            { 
                p->nSatRunsSat++;
                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
                {
                    Extra_BitMatrixInsert1( pMatNonSym, i, k );   
                    Extra_BitMatrixInsert2( pMatNonSym, i, k );   
                }
                p->iOutput = out;
                p->iVar1Old = p->iVar1;
                p->iVar2Old = p->iVar2;
                p->iVar1 = v;
                p->iVar2 = u;
                return 1;
            }
        }
        assert( Extra_BitMatrixIsClique( pMatSym ) );
    }
    p->iOutput = p->nOutputs;
    return 0;
}
int Sim_SymmsGetPatternUsingSat ( Sym_Man_t * p , unsigned * pPattern ) { Vec_Int_t * vSupport ; Extra_BitMat_t * pMatSym , * pMatNonSym ; int Index1 , Index2 , Index3 , IndexU , IndexV ; int v , u , i , k , b , out ; 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 ) ; 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 ++ ; 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 ) ) { p -> nSatRunsUnsat ++ ; Vec_IntForEachEntry ( p -> vVarsU , i , IndexU ) Vec_IntForEachEntry ( p -> vVarsV , k , IndexV ) { Extra_BitMatrixInsert1 ( pMatSym , i , k ) ; Extra_BitMatrixInsert2 ( pMatSym , i , k ) ; Extra_BitMatrixOrTwo ( pMatNonSym , i , k ) ; } } else { p -> nSatRunsSat ++ ; Vec_IntForEachEntry ( p -> vVarsU , i , IndexU ) Vec_IntForEachEntry ( p -> vVarsV , k , IndexV ) { Extra_BitMatrixInsert1 ( pMatNonSym , i , k ) ; Extra_BitMatrixInsert2 ( pMatNonSym , i , k ) ; } p -> iOutput = out ; p -> iVar1Old = p -> iVar1 ; p -> iVar2Old = p -> iVar2 ; p -> iVar1 = v ; p -> iVar2 = u ; return 1 ; } } assert ( Extra_BitMatrixIsClique ( pMatSym ) ) ; } p -> iOutput = p -> nOutputs ; return 0 ; }
Function
Synopsis    [Tries to prove the remaining pairs using SAT.]
Function Synopsis [ Tries to prove the remaining pairs using SAT . ]
// iterate through outputs // go through the remaining variable pairs // collect the support variables that are symmetric with u and v // update the symmetric variable info             // Theorem 1 // Theorem 1 // Theorem 2 // update the assymmetric variable info // Theorem 3 // Theorem 3 // remember the out // make sure that the symmetry matrix contains only cliques // mark that we finished all outputs