abc/src/proof/fraig/fraigSat.c
/**Function*************************************************************

  Synopsis    [Checks whether two nodes are functinally equivalent.]

  Description [The flag (fComp) tells whether the nodes to be checked
  are in the opposite polarity. The second flag (fSkipZeros) tells whether
  the checking should be performed if the simulation vectors are zeros.
  Returns 1 if the nodes are equivalent; 0 othewise.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Checks whether two nodes are functinally equivalent.]

Description [The flag (fComp) tells whether the nodes to be checked
are in the opposite polarity. The second flag (fSkipZeros) tells whether
the checking should be performed if the simulation vectors are zeros.
Returns 1 if the nodes are equivalent; 0 othewise.]




Function Synopsis [ Checks whether two nodes are functinally equivalent . ] Description [ The flag ( fComp ) tells whether the nodes to be checked are in the opposite polarity . The second flag ( fSkipZeros ) tells whether the checking should be performed if the simulation vectors are zeros . Returns 1 if the nodes are equivalent ; 0 othewise . ]
int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit )
{
    int RetValue, RetValue1, i, fComp;
    abctime clk;
    int fVerbose = 0;
    int fSwitch = 0;
    assert( !Fraig_IsComplement(pNew) );
    assert( !Fraig_IsComplement(pOld) );
    assert( pNew != pOld );
    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
    {
        p->nSatFails++;
        if ( nBTLimit <= 10 )
            return 0;
        nBTLimit = (int)sqrt((double)nBTLimit);
    }
    p->nSatCalls++;
    if ( p->pSat == NULL )
        Fraig_ManCreateSolver( p );
    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
    nMuxes = 0;
clk = Abc_Clock();
    Fraig_OrderVariables( p, pOld, pNew );
p->timeTrav += Abc_Clock() - clk;
if ( fVerbose )
    printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
    Fraig_SetActivity( p, pOld, pNew );
    fComp = Fraig_NodeComparePhase( pOld, pNew );
    Msat_SolverPrepare( p->pSat, p->vVarsInt );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
clk = Abc_Clock();
    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == MSAT_FALSE )
    {
if ( fVerbose )
{
}
        Msat_IntVecClear( p->vProj );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
        assert( RetValue );
    }
    else if ( RetValue1 == MSAT_TRUE )
    {
if ( fVerbose )
{
}
        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
        if ( fSwitch )
             printf( "s(%d)", pNew->Level );
        p->nSatCounter++;
        return 0;
    }
    else 
    {
p->time3 += Abc_Clock() - clk;
        if ( pOld != p->pConst1 ) 
            pOld->fFailTfo = 1;
        pNew->fFailTfo = 1;
        if ( fSwitch )
             printf( "T(%d)", pNew->Level );
        p->nSatFailsReal++;
        return 0;
    }
    if ( pOld == p->pConst1 )
        return 1;
    Msat_SolverPrepare( p->pSat, p->vVarsInt );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
clk = Abc_Clock();
    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == MSAT_FALSE )
    {
if ( fVerbose )
{
}
        Msat_IntVecClear( p->vProj );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
        assert( RetValue );
    }
    else if ( RetValue1 == MSAT_TRUE )
    {
if ( fVerbose )
{
}
        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
        p->nSatCounter++;
        if ( fSwitch )
             printf( "s(%d)", pNew->Level );
        return 0;
    }
    else 
    {
p->time3 += Abc_Clock() - clk;
        if ( fSwitch )
             printf( "T(%d)", pNew->Level );
        pOld->fFailTfo = 1;
        pNew->fFailTfo = 1;
        p->nSatFailsReal++;
        return 0;
    }
    p->nSatProof++;
    if ( fSwitch )
         printf( "u(%d)", pNew->Level );
    return 1;
}
int Fraig_NodeIsEquivalent ( Fraig_Man_t * p , Fraig_Node_t * pOld , Fraig_Node_t * pNew , int nBTLimit , int nTimeLimit ) { int RetValue , RetValue1 , i , fComp ; abctime clk ; int fVerbose = 0 ; int fSwitch = 0 ; assert ( ! Fraig_IsComplement ( pNew ) ) ; assert ( ! Fraig_IsComplement ( pOld ) ) ; assert ( pNew != pOld ) ; if ( nBTLimit > 0 && ( pOld -> fFailTfo || pNew -> fFailTfo ) ) { p -> nSatFails ++ ; if ( nBTLimit <= 10 ) return 0 ; nBTLimit = ( int ) sqrt ( ( double ) nBTLimit ) ; } p -> nSatCalls ++ ; if ( p -> pSat == NULL ) Fraig_ManCreateSolver ( p ) ; for ( i = Msat_SolverReadVarNum ( p -> pSat ) ; i < p -> vNodes -> nSize ; i ++ ) Msat_SolverAddVar ( p -> pSat , p -> vNodes -> pArray [ i ] -> Level ) ; nMuxes = 0 ; clk = Abc_Clock ( ) ; Fraig_OrderVariables ( p , pOld , pNew ) ; p -> timeTrav += Abc_Clock ( ) - clk ; if ( fVerbose ) printf ( " " , Fraig_CountPis ( p , p -> vVarsInt ) , Msat_IntVecReadSize ( p -> vVarsInt ) ) ; Fraig_SetActivity ( p , pOld , pNew ) ; fComp = Fraig_NodeComparePhase ( pOld , pNew ) ; Msat_SolverPrepare ( p -> pSat , p -> vVarsInt ) ; Msat_IntVecClear ( p -> vProj ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pOld -> Num , 0 ) ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pNew -> Num , ! fComp ) ) ; clk = Abc_Clock ( ) ; RetValue1 = Msat_SolverSolve ( p -> pSat , p -> vProj , nBTLimit , nTimeLimit ) ; p -> timeSat += Abc_Clock ( ) - clk ; if ( RetValue1 == MSAT_FALSE ) { if ( fVerbose ) { } Msat_IntVecClear ( p -> vProj ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pOld -> Num , 1 ) ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pNew -> Num , fComp ) ) ; RetValue = Msat_SolverAddClause ( p -> pSat , p -> vProj ) ; assert ( RetValue ) ; } else if ( RetValue1 == MSAT_TRUE ) { if ( fVerbose ) { } Fraig_FeedBack ( p , Msat_SolverReadModelArray ( p -> pSat ) , p -> vVarsInt , pOld , pNew ) ; if ( fSwitch ) printf ( " " , pNew -> Level ) ; p -> nSatCounter ++ ; return 0 ; } else { p -> time3 += Abc_Clock ( ) - clk ; if ( pOld != p -> pConst1 ) pOld -> fFailTfo = 1 ; pNew -> fFailTfo = 1 ; if ( fSwitch ) printf ( " " , pNew -> Level ) ; p -> nSatFailsReal ++ ; return 0 ; } if ( pOld == p -> pConst1 ) return 1 ; Msat_SolverPrepare ( p -> pSat , p -> vVarsInt ) ; Msat_IntVecClear ( p -> vProj ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pOld -> Num , 1 ) ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pNew -> Num , fComp ) ) ; clk = Abc_Clock ( ) ; RetValue1 = Msat_SolverSolve ( p -> pSat , p -> vProj , nBTLimit , nTimeLimit ) ; p -> timeSat += Abc_Clock ( ) - clk ; if ( RetValue1 == MSAT_FALSE ) { if ( fVerbose ) { } Msat_IntVecClear ( p -> vProj ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pOld -> Num , 0 ) ) ; Msat_IntVecPush ( p -> vProj , MSAT_VAR2LIT ( pNew -> Num , ! fComp ) ) ; RetValue = Msat_SolverAddClause ( p -> pSat , p -> vProj ) ; assert ( RetValue ) ; } else if ( RetValue1 == MSAT_TRUE ) { if ( fVerbose ) { } Fraig_FeedBack ( p , Msat_SolverReadModelArray ( p -> pSat ) , p -> vVarsInt , pOld , pNew ) ; p -> nSatCounter ++ ; if ( fSwitch ) printf ( " " , pNew -> Level ) ; return 0 ; } else { p -> time3 += Abc_Clock ( ) - clk ; if ( fSwitch ) printf ( " " , pNew -> Level ) ; pOld -> fFailTfo = 1 ; pNew -> fFailTfo = 1 ; p -> nSatFailsReal ++ ; return 0 ; } p -> nSatProof ++ ; if ( fSwitch ) printf ( " " , pNew -> Level ) ; return 1 ; }
Function
Synopsis    [Checks whether two nodes are functinally equivalent.]
Function Synopsis [ Checks whether two nodes are functinally equivalent . ]
// make sure the nodes are not complemented // if at least one of the nodes is a failed node, perform adjustments: // if the backtrack limit is small, simply skip this node // if the backtrack limit is > 10, take the quare root of the limit //            return 0; //        if ( nBTLimit > 10 ) //            nBTLimit /= 10; //        fSwitch = 1; // make sure the solver is allocated and has enough variables // make sure the SAT solver has enough variables /*
    {
        Fraig_Node_t * ppNodes[2] = { pOld, pNew };
        extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
        Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
    }
*/ // get the logic cone //    Fraig_VarsStudy( p, pOld, pNew ); //    Fraig_PrepareCones( p, pOld, pNew ); //    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) ); //    ABC_PRT( "Time", Abc_Clock() - clk ); // prepare variable activity // get the complemented attribute //Msat_SolverPrintClauses( p->pSat ); //////////////////////////////////////////// // prepare the solver to run incrementally on these variables //clk = Abc_Clock(); //p->time3 += Abc_Clock() - clk; // solve under assumptions // A = 1; B = 0     OR     A = 1; B = 1  //Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); // run the solver //p->time1 += Abc_Clock() - clk; //    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) ); //ABC_PRT( "time", Abc_Clock() - clk ); // add the clause // continue solving the other implication //p->time2 += Abc_Clock() - clk; //    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) ); //ABC_PRT( "time", Abc_Clock() - clk ); // record the counter example //        if ( pOld->fFailTfo || pNew->fFailTfo ) //            printf( "*" ); //        printf( "s(%d)", pNew->Level ); // if ( RetValue1 == MSAT_UNKNOWN ) //        if ( pOld->fFailTfo || pNew->fFailTfo ) //            printf( "*" ); //        printf( "T(%d)", pNew->Level ); // mark the node as the failed node //        p->nSatFails++; // if the old node was constant 0, we already know the answer //////////////////////////////////////////// // prepare the solver to run incrementally  //clk = Abc_Clock(); //p->time3 += Abc_Clock() - clk; // solve under assumptions // A = 0; B = 1     OR     A = 0; B = 0  // run the solver //p->time1 += Abc_Clock() - clk; //    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) ); //ABC_PRT( "time", Abc_Clock() - clk ); // add the clause // continue solving the other implication //p->time2 += Abc_Clock() - clk; //    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) ); //ABC_PRT( "time", Abc_Clock() - clk ); // record the counter example //        if ( pOld->fFailTfo || pNew->fFailTfo ) //            printf( "*" ); //        printf( "s(%d)", pNew->Level ); // if ( RetValue1 == MSAT_UNKNOWN ) //        if ( pOld->fFailTfo || pNew->fFailTfo ) //            printf( "*" ); //        printf( "T(%d)", pNew->Level ); // mark the node as the failed node //        p->nSatFails++; // return SAT proof //    if ( pOld->fFailTfo || pNew->fFailTfo ) //        printf( "*" ); //    printf( "u(%d)", pNew->Level );