fraigSat.c File Reference

#include <math.h>
#include "fraigInt.h"
#include "sat/msat/msatInt.h"

Include dependency graph for fraigSat.c:

Go to the source code of this file.

Functions
int	Fraig_NodesAreEqual (Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit, int nTimeLimit)
	FUNCTION DEFINITIONS ///.
void	Fraig_ManProveMiter (Fraig_Man_t *p)
int	Fraig_ManCheckMiter (Fraig_Man_t *p)
int	Fraig_MarkTfi_rec (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int	Fraig_MarkTfi2_rec (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
int	Fraig_MarkTfi3_rec (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
void	Fraig_VarsStudy (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int	Fraig_NodeIsEquivalent (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit, int nTimeLimit)
int	Fraig_NodeIsImplification (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit)
int	Fraig_ManCheckClauseUsingSat (Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit)
void	Fraig_DetectFanoutFreeCone_rec (Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper, Fraig_NodeVec_t *vInside, int fFirst)
void	Fraig_DetectFanoutFreeConeMux_rec (Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper, Fraig_NodeVec_t *vInside, int fFirst)

Function Documentation

Fraig_DetectFanoutFreeCone_rec()

void Fraig_DetectFanoutFreeCone_rec	(	Fraig_Node_t *	pNode,
		Fraig_NodeVec_t *	vSuper,
		Fraig_NodeVec_t *	vInside,
		int	fFirst )

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

Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 1308 of file fraigSat.c.

{
    // make the pointer regular
    pNode = Fraig_Regular(pNode);
    // if the new node is complemented or a PI, another gate begins
    if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) )
    {
        Fraig_NodeVecPushUnique( vSuper, pNode );
        return;
    }
    // go through the branches
    Fraig_DetectFanoutFreeCone_rec( pNode->p1, vSuper, vInside, 0 );
    Fraig_DetectFanoutFreeCone_rec( pNode->p2, vSuper, vInside, 0 );
    // add the node
    Fraig_NodeVecPushUnique( vInside, pNode );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_DetectFanoutFreeConeMux_rec()

void Fraig_DetectFanoutFreeConeMux_rec	(	Fraig_Node_t *	pNode,
		Fraig_NodeVec_t *	vSuper,
		Fraig_NodeVec_t *	vInside,
		int	fFirst )

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

Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]

Description []

SideEffects []

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

Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 1371 of file fraigSat.c.

{
    // make the pointer regular
    pNode = Fraig_Regular(pNode);
    // if the new node is complemented or a PI, another gate begins
    if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) || !Fraig_NodeIsMuxType(pNode) )
    {
        Fraig_NodeVecPushUnique( vSuper, pNode );
        return;
    }
    // go through the branches
    Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p1, vSuper, vInside, 0 );
    Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p2, vSuper, vInside, 0 );
    Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p1, vSuper, vInside, 0 );
    Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p2, vSuper, vInside, 0 );
    // add the node
    Fraig_NodeVecPushUnique( vInside, pNode );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManCheckClauseUsingSat()

int Fraig_ManCheckClauseUsingSat	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pNode1,
		Fraig_Node_t *	pNode2,
		int	nBTLimit )

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

Synopsis [Prepares the SAT solver to run on the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 653 of file fraigSat.c.

{
    Fraig_Node_t * pNode1R, * pNode2R;
    int RetValue, RetValue1, i;
    abctime clk;
    int fVerbose = 0;
 
    pNode1R = Fraig_Regular(pNode1);
    pNode2R = Fraig_Regular(pNode2);
    assert( pNode1R != pNode2R );
 
    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
        Fraig_ManCreateSolver( p );
    // make sure the SAT solver has enough variables
    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
   // get the logic cone
clk = Abc_Clock();
    Fraig_OrderVariables( p, pNode1R, pNode2R );
//    Fraig_PrepareCones( p, pNode1R, pNode2R );
p->timeTrav += Abc_Clock() - clk;

    // prepare the solver to run incrementally on these variables
//clk = Abc_Clock();
    Msat_SolverPrepare( p->pSat, p->vVarsInt );
//p->time3 += Abc_Clock() - clk;
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
    // run the solver
clk = Abc_Clock();
    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
p->timeSat += Abc_Clock() - clk;
 
    if ( RetValue1 == MSAT_FALSE )
    {
//p->time1 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
 
        // add the clause
        Msat_IntVecClear( p->vProj );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
        assert( RetValue );
//        p->nSatProofImp++;
        return 1;
    }
    else if ( RetValue1 == MSAT_TRUE )
    {
//p->time2 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
        // record the counter example
//        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
        p->nSatCounterImp++;
        return 0;
    }
    else // if ( RetValue1 == MSAT_UNKNOWN )
    {
p->time3 += Abc_Clock() - clk;
        p->nSatFailsImp++;
        return 0;
    }
}

Here is the call graph for this function:

Fraig_ManCheckMiter()

int Fraig_ManCheckMiter

(

Fraig_Man_t *

p

)

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

Synopsis [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file fraigSat.c.

{
    Fraig_Node_t * pNode;
    int i;
    ABC_FREE( p->pModel );
    for ( i = 0; i < p->vOutputs->nSize; i++ )
    {
        // get the output node (it can be complemented!)
        pNode = p->vOutputs->pArray[i];
        // if the miter is constant 0, the problem is UNSAT
        if ( pNode == Fraig_Not(p->pConst1) )
            continue;
        // consider the special case when the miter is constant 1
        if ( pNode == p->pConst1 )
        {
            // in this case, any counter example will do to distinquish it from constant 0
            // here we pick the counter example composed of all zeros
            p->pModel = Fraig_ManAllocCounterExample( p );
            return 0;
        }
        // save the counter example
        p->pModel = Fraig_ManSaveCounterExample( p, pNode );
        // if the model is not found, return undecided
        if ( p->pModel == NULL )
            return -1;
        else
            return 0;
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManProveMiter()

void Fraig_ManProveMiter

(

Fraig_Man_t *

p

)

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

Synopsis [Tries to prove the final miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file fraigSat.c.

{
    Fraig_Node_t * pNode;
    int i;
    abctime clk;
 
    if ( !p->fTryProve )
        return;
 
    clk = Abc_Clock();
    // consider all outputs of the multi-output miter
    for ( i = 0; i < p->vOutputs->nSize; i++ )
    {
        pNode = Fraig_Regular(p->vOutputs->pArray[i]);
        // skip already constant nodes
        if ( pNode == p->pConst1 )
            continue;
        // skip nodes that are different according to simulation
        if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
            continue;
        if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
        {
            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
                p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
            else
                p->vOutputs->pArray[i] = p->pConst1;
        }
    }
    if ( p->fVerboseP ) 
    {
//        ABC_PRT( "Final miter proof time", Abc_Clock() - clk );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_MarkTfi2_rec()

int Fraig_MarkTfi2_rec	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode )

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

Synopsis [Returns 1 if pOld is in the TFI of pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file fraigSat.c.

{
    // skip the visited node
    if ( pNode->TravId == pMan->nTravIds )
        return 0;
    // skip the boundary node
    if ( pNode->TravId == pMan->nTravIds-1 )
    {
        pNode->TravId = pMan->nTravIds;
        return 1;
    }
    pNode->TravId = pMan->nTravIds;
    // skip the PI node
    if ( pNode->NumPi >= 0 )
        return 1;
    // check the children
    return Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p1) ) +
           Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p2) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_MarkTfi3_rec()

int Fraig_MarkTfi3_rec	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode )

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

Synopsis [Returns 1 if pOld is in the TFI of pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file fraigSat.c.

{
    // skip the visited node
    if ( pNode->TravId == pMan->nTravIds )
        return 1;
    // skip the boundary node
    if ( pNode->TravId == pMan->nTravIds-1 )
    {
        pNode->TravId = pMan->nTravIds;
        return 1;
    }
    pNode->TravId = pMan->nTravIds;
    // skip the PI node
    if ( pNode->NumPi >= 0 )
        return 0;
    // check the children
    return Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p1) ) *
           Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p2) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_MarkTfi_rec()

int Fraig_MarkTfi_rec	(	Fraig_Man_t *	pMan,
		Fraig_Node_t *	pNode )

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

Synopsis [Returns 1 if pOld is in the TFI of pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file fraigSat.c.

{
    // skip the visited node
    if ( pNode->TravId == pMan->nTravIds )
        return 0;
    pNode->TravId = pMan->nTravIds;
    // skip the PI node
    if ( pNode->NumPi >= 0 )
        return 1;
    // check the children
    return Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p1) ) +
           Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p2) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeIsEquivalent()

int Fraig_NodeIsEquivalent	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew,
		int	nBTLimit,
		int	nTimeLimit )

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 []

Definition at line 302 of file fraigSat.c.

{
    int RetValue, RetValue1, i, fComp;
    abctime clk;
    int fVerbose = 0;
    int fSwitch = 0;
 
    // make sure the nodes are not complemented
    assert( !Fraig_IsComplement(pNew) );
    assert( !Fraig_IsComplement(pOld) );
    assert( pNew != pOld );
 
    // 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
    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
    {
        p->nSatFails++;
//            return 0;
//        if ( nBTLimit > 10 )
//            nBTLimit /= 10;
        if ( nBTLimit <= 10 )
            return 0;
        nBTLimit = (int)sqrt((double)nBTLimit);
//        fSwitch = 1;
    }
 
    p->nSatCalls++;
 
    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
        Fraig_ManCreateSolver( p );
    // make sure the SAT solver has enough variables
    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
 
 
/*
    {
        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" );
    }
*/
 
    nMuxes = 0;
 
 
    // get the logic cone
clk = Abc_Clock();
//    Fraig_VarsStudy( p, pOld, pNew );
    Fraig_OrderVariables( p, pOld, pNew );
//    Fraig_PrepareCones( p, pOld, pNew );
p->timeTrav += Abc_Clock() - clk;
 
//    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 );
 
    if ( fVerbose )
        printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
 
 
    // prepare variable activity
    Fraig_SetActivity( p, pOld, pNew );
 
    // get the complemented attribute
    fComp = Fraig_NodeComparePhase( pOld, pNew );
//Msat_SolverPrintClauses( p->pSat );

    // prepare the solver to run incrementally on these variables
//clk = Abc_Clock();
    Msat_SolverPrepare( p->pSat, p->vVarsInt );
//p->time3 += Abc_Clock() - clk;
 
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
 
//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
 
    // run the solver
clk = Abc_Clock();
    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += Abc_Clock() - clk;
 
    if ( RetValue1 == MSAT_FALSE )
    {
//p->time1 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
 
        // add the clause
        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 );
        // continue solving the other implication
    }
    else if ( RetValue1 == MSAT_TRUE )
    {
//p->time2 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
 
        // record the counter example
        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
 
//        if ( pOld->fFailTfo || pNew->fFailTfo )
//            printf( "*" );
//        printf( "s(%d)", pNew->Level );
        if ( fSwitch )
             printf( "s(%d)", pNew->Level );
        p->nSatCounter++;
        return 0;
    }
    else // if ( RetValue1 == MSAT_UNKNOWN )
    {
p->time3 += Abc_Clock() - clk;
 
//        if ( pOld->fFailTfo || pNew->fFailTfo )
//            printf( "*" );
//        printf( "T(%d)", pNew->Level );
 
        // mark the node as the failed node
        if ( pOld != p->pConst1 ) 
            pOld->fFailTfo = 1;
        pNew->fFailTfo = 1;
//        p->nSatFails++;
        if ( fSwitch )
             printf( "T(%d)", pNew->Level );
        p->nSatFailsReal++;
        return 0;
    }
 
    // if the old node was constant 0, we already know the answer
    if ( pOld == p->pConst1 )
        return 1;

    // prepare the solver to run incrementally 
//clk = Abc_Clock();
    Msat_SolverPrepare( p->pSat, p->vVarsInt );
//p->time3 += Abc_Clock() - clk;
    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
    // run the solver
clk = Abc_Clock();
    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += Abc_Clock() - clk;
 
    if ( RetValue1 == MSAT_FALSE )
    {
//p->time1 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
 
        // add the clause
        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 );
        // continue solving the other implication
    }
    else if ( RetValue1 == MSAT_TRUE )
    {
//p->time2 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
 
        // record the counter example
        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
        p->nSatCounter++;
 
//        if ( pOld->fFailTfo || pNew->fFailTfo )
//            printf( "*" );
//        printf( "s(%d)", pNew->Level );
        if ( fSwitch )
             printf( "s(%d)", pNew->Level );
        return 0;
    }
    else // if ( RetValue1 == MSAT_UNKNOWN )
    {
p->time3 += Abc_Clock() - clk;
 
//        if ( pOld->fFailTfo || pNew->fFailTfo )
//            printf( "*" );
//        printf( "T(%d)", pNew->Level );
        if ( fSwitch )
             printf( "T(%d)", pNew->Level );
 
        // mark the node as the failed node
        pOld->fFailTfo = 1;
        pNew->fFailTfo = 1;
//        p->nSatFails++;
        p->nSatFailsReal++;
        return 0;
    }
 
    // return SAT proof
    p->nSatProof++;
 
//    if ( pOld->fFailTfo || pNew->fFailTfo )
//        printf( "*" );
//    printf( "u(%d)", pNew->Level );
 
    if ( fSwitch )
         printf( "u(%d)", pNew->Level );
 
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeIsImplification()

int Fraig_NodeIsImplification	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew,
		int	nBTLimit )

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

Synopsis [Checks whether pOld => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 551 of file fraigSat.c.

{
    int RetValue, RetValue1, i, fComp;
    abctime clk;
    int fVerbose = 0;
 
    // make sure the nodes are not complemented
    assert( !Fraig_IsComplement(pNew) );
    assert( !Fraig_IsComplement(pOld) );
    assert( pNew != pOld );
 
    p->nSatCallsImp++;
 
    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
        Fraig_ManCreateSolver( p );
    // make sure the SAT solver has enough variables
    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
        Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
   // get the logic cone
clk = Abc_Clock();
    Fraig_OrderVariables( p, pOld, pNew );
//    Fraig_PrepareCones( p, pOld, pNew );
p->timeTrav += Abc_Clock() - clk;
 
    if ( fVerbose )
        printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
 
 
    // get the complemented attribute
    fComp = Fraig_NodeComparePhase( pOld, pNew );
//Msat_SolverPrintClauses( p->pSat );

    // prepare the solver to run incrementally on these variables
//clk = Abc_Clock();
    Msat_SolverPrepare( p->pSat, p->vVarsInt );
//p->time3 += Abc_Clock() - clk;
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
    // run the solver
clk = Abc_Clock();
    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
p->timeSat += Abc_Clock() - clk;
 
    if ( RetValue1 == MSAT_FALSE )
    {
//p->time1 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
 
        // add the clause
        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 );
//        p->nSatProofImp++;
        return 1;
    }
    else if ( RetValue1 == MSAT_TRUE )
    {
//p->time2 += Abc_Clock() - clk;
 
if ( fVerbose )
{
//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
//ABC_PRT( "time", Abc_Clock() - clk );
}
        // record the counter example
        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
        p->nSatCounterImp++;
        return 0;
    }
    else // if ( RetValue1 == MSAT_UNKNOWN )
    {
p->time3 += Abc_Clock() - clk;
        p->nSatFailsImp++;
        return 0;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodesAreEqual()

int Fraig_NodesAreEqual	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pNode1,
		Fraig_Node_t *	pNode2,
		int	nBTLimit,
		int	nTimeLimit )

FUNCTION DEFINITIONS ///.

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

Synopsis [Checks equivalence of two nodes.]

Description [Returns 1 iff the nodes are equivalent.]

SideEffects []

SeeAlso []

Definition at line 65 of file fraigSat.c.

{
    if ( pNode1 == pNode2 )
        return 1;
    if ( pNode1 == Fraig_Not(pNode2) )
        return 0;
    return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
}

Here is the call graph for this function:

Fraig_VarsStudy()

void Fraig_VarsStudy	(	Fraig_Man_t *	p,
		Fraig_Node_t *	pOld,
		Fraig_Node_t *	pNew )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 260 of file fraigSat.c.

{
    int NumPis, NumCut, fContain;
 
    // mark the TFI of pNew
    p->nTravIds++;
    NumPis = Fraig_MarkTfi_rec( p, pNew );
    printf( "(%d)(%d,%d):", NumPis, pOld->Level, pNew->Level );
 
    // check if the old is in the TFI
    if ( pOld->TravId == p->nTravIds )
    {
        printf( "* " );
        return;
    }
 
    // count the boundary of nodes in pOld
    p->nTravIds++;
    NumCut = Fraig_MarkTfi2_rec( p, pOld );
    printf( "%d", NumCut );
 
    // check if the new is contained in the old's support
    p->nTravIds++;
    fContain = Fraig_MarkTfi3_rec( p, pNew );
    printf( "%c ", fContain? '+':'-' );
}

Here is the call graph for this function: