abc/src/proof/fra/fraClau.c
/**Function*************************************************************

  Synopsis    [Reduces the counter-example by removing complemented literals.]

  Description [Removes literals from vMain that differ from those in the  
  counter-example (vNew). Relies on the fact that the PI variables are
  assigned in the increasing order.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Reduces the counter-example by removing complemented literals.]

Description [Removes literals from vMain that differ from those in the
counter-example (vNew). Relies on the fact that the PI variables are
assigned in the increasing order.]




Function Synopsis [ Reduces the counter - example by removing complemented literals . ] Description [ Removes literals from vMain that differ from those in the counter - example ( vNew ) . Relies on the fact that the PI variables are assigned in the increasing order . ]
void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew )
{
    int LitM, LitN, VarM, VarN, i, j, k;
    assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) );
    for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); )
    {
        LitM = Vec_IntEntry( vMain, i );
        LitN = Vec_IntEntry( vNew, j );
        VarM = lit_var( LitM );
        VarN = lit_var( LitN );
        if ( VarM < VarN )
        {
            assert( 0 );
        }
        else if ( VarM > VarN )
        {
            j++;
        }
        else 
        {
            i++;
            j++;
            if ( LitM == LitN )
                Vec_IntWriteEntry( vMain, k++, LitM );
        }
    }
    assert( i == Vec_IntSize(vMain) );
    Vec_IntShrink( vMain, k );
}
void Fra_ClauReduceClause ( Vec_Int_t * vMain , Vec_Int_t * vNew ) { int LitM , LitN , VarM , VarN , i , j , k ; assert ( Vec_IntSize ( vMain ) <= Vec_IntSize ( vNew ) ) ; for ( i = j = k = 0 ; i < Vec_IntSize ( vMain ) && j < Vec_IntSize ( vNew ) ; ) { LitM = Vec_IntEntry ( vMain , i ) ; LitN = Vec_IntEntry ( vNew , j ) ; VarM = lit_var ( LitM ) ; VarN = lit_var ( LitN ) ; if ( VarM < VarN ) { assert ( 0 ) ; } else if ( VarM > VarN ) { j ++ ; } else { i ++ ; j ++ ; if ( LitM == LitN ) Vec_IntWriteEntry ( vMain , k ++ , LitM ) ; } } assert ( i == Vec_IntSize ( vMain ) ) ; Vec_IntShrink ( vMain , k ) ; }
Function
Synopsis    [Reduces the counter-example by removing complemented literals.]
Function Synopsis [ Reduces the counter - example by removing complemented literals . ]
// if ( VarM == VarN )