fraigSat.c File Reference

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

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START void	Fraig_OrderVariables (Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
	DECLARATIONS ///. More...
static void	Fraig_SetupAdjacent (Fraig_Man_t *pMan, Msat_IntVec_t *vConeVars)
static void	Fraig_SetupAdjacentMark (Fraig_Man_t *pMan, Msat_IntVec_t *vConeVars)
static void	Fraig_PrepareCones (Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
static void	Fraig_PrepareCones_rec (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
static void	Fraig_SupergateAddClauses (Fraig_Man_t *pMan, Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper)
static void	Fraig_SupergateAddClausesExor (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
static void	Fraig_SupergateAddClausesMux (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
static void	Fraig_DetectFanoutFreeConeMux (Fraig_Man_t *pMan, Fraig_Node_t *pNode)
static void	Fraig_SetActivity (Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int	Fraig_NodesAreEqual (Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit, int nTimeLimit)
	FUNCTION DEFINITIONS ///. More...
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_NodeIsImplication (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)

Variables
static int	nMuxes

Function Documentation

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 );
}

void Fraig_DetectFanoutFreeConeMux ( Fraig_Man_t *  pMan, Fraig_Node_t *  pNode  )

static

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1401 of file fraigSat.c.

{
    Fraig_NodeVec_t * vFanins;
    Fraig_NodeVec_t * vInside;
    int nCubes;
    extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside );

    vFanins = Fraig_NodeVecAlloc( 8 );
    vInside = Fraig_NodeVecAlloc( 8 );

    Fraig_DetectFanoutFreeConeMux_rec( pNode, vFanins, vInside, 1 );
    assert( vInside->pArray[vInside->nSize-1] == pNode );

//    nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside );
    nCubes = 0;

printf( "%d(%d)", vFanins->nSize, nCubes );
    Fraig_NodeVecFree( vFanins );
    Fraig_NodeVecFree( vInside );
}

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 );
}

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;
    }
}

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;
}

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 );
    }
}

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) );
}

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) );
}

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) );
}

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;
}

int Fraig_NodeIsImplication	(	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;
    }
}

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 );
}

void Fraig_OrderVariables ( Fraig_Man_t *  pMan, Fraig_Node_t *  pOld, Fraig_Node_t *  pNew  )

static

DECLARATIONS ///.

CFile****************************************************************

FileName [fraigSat.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Proving functional equivalence using SAT.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id:

fraigSat.c,v 1.10 2005/07/08 01:01:32 alanmi Exp

]

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

Synopsis [Collect variables using their proximity from the nodes.]

Description [This procedure creates a variable order based on collecting first the nodes that are the closest to the given two target nodes.]

SideEffects []

SeeAlso []

Definition at line 875 of file fraigSat.c.

{
    Fraig_Node_t * pNode, * pFanin;
    int i, k, Number, fUseMuxes = 1;
    int nVarsAlloc;

    assert( pOld != pNew );
    assert( !Fraig_IsComplement(pOld) );
    assert( !Fraig_IsComplement(pNew) );

    pMan->nTravIds++;

    // clean the variables
    nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed);
    Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 );
    Msat_IntVecClear( pMan->vVarsInt );

    // add the first node
    Msat_IntVecPush( pMan->vVarsInt, pOld->Num );
    Msat_IntVecWriteEntry( pMan->vVarsUsed, pOld->Num, 1 );
    pOld->TravId = pMan->nTravIds;

    // add the second node
    Msat_IntVecPush( pMan->vVarsInt, pNew->Num );
    Msat_IntVecWriteEntry( pMan->vVarsUsed, pNew->Num, 1 );
    pNew->TravId = pMan->nTravIds;

    // create the variable order
    for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
    {
        // get the new node on the frontier
        Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
        pNode = pMan->vNodes->pArray[Number];
        if ( !Fraig_NodeIsAnd(pNode) )
            continue;

        // if the node does not have fanins, create them
        if ( pNode->vFanins == NULL )
        {
            // create the fanins of the supergate
            assert( pNode->fClauses == 0 );
            // detecting a fanout-free cone (experiment only)
//            Fraig_DetectFanoutFreeCone( pMan, pNode );

            if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
            {
                pNode->vFanins = Fraig_NodeVecAlloc( 4 );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
                Fraig_SupergateAddClausesMux( pMan, pNode );
//                Fraig_DetectFanoutFreeConeMux( pMan, pNode );

                nMuxes++;
            }
            else
            {
                pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes );
                Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins );
            }
            assert( pNode->vFanins->nSize > 1 );
            pNode->fClauses = 1;
            pMan->nVarsClauses++;

            pNode->fMark2 = 1; // goes together with Fraig_SetupAdjacentMark()
        }

        // explore the implication fanins of pNode
        for ( k = 0; k < pNode->vFanins->nSize; k++ )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
            if ( pFanin->TravId == pMan->nTravIds ) // already collected
                continue;
            // collect and mark
            Msat_IntVecPush( pMan->vVarsInt, pFanin->Num );
            Msat_IntVecWriteEntry( pMan->vVarsUsed, pFanin->Num, 1 );
            pFanin->TravId = pMan->nTravIds;
        }
    }

    // set up the adjacent variable information
//    Fraig_SetupAdjacent( pMan, pMan->vVarsInt );
    Fraig_SetupAdjacentMark( pMan, pMan->vVarsInt );
}

void Fraig_PrepareCones ( Fraig_Man_t *  pMan, Fraig_Node_t *  pOld, Fraig_Node_t *  pNew  )

static

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 746 of file fraigSat.c.

{
//    Msat_IntVec_t * vAdjs;
//    int * pVars, nVars, i, k;
    int nVarsAlloc;

    assert( pOld != pNew );
    assert( !Fraig_IsComplement(pOld) );
    assert( !Fraig_IsComplement(pNew) );
    // clean the variables
    nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed);
    Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 );
    Msat_IntVecClear( pMan->vVarsInt );

    pMan->nTravIds++;
    Fraig_PrepareCones_rec( pMan, pNew );
    Fraig_PrepareCones_rec( pMan, pOld );


/*
    nVars = Msat_IntVecReadSize( pMan->vVarsInt );
    pVars = Msat_IntVecReadArray( pMan->vVarsInt );
    for ( i = 0; i < nVars; i++ )
    {
        // process its connections
        vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
        printf( "%d=%d { ", pVars[i], Msat_IntVecReadSize(vAdjs) );
        for ( k = 0; k < Msat_IntVecReadSize(vAdjs); k++ )
            printf( "%d ", Msat_IntVecReadEntry(vAdjs,k) );
        printf( "}\n" );

    }
    i = 0;
*/
}

void Fraig_PrepareCones_rec ( Fraig_Man_t *  pMan, Fraig_Node_t *  pNode  )

static

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

Synopsis [Traverses the cone, collects the numbers and adds the clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file fraigSat.c.

{
    Fraig_Node_t * pFanin;
    Msat_IntVec_t * vAdjs;
    int fUseMuxes = 1, i;
    int fItIsTime;

    // skip if the node is aleady visited
    assert( !Fraig_IsComplement(pNode) );
    if ( pNode->TravId == pMan->nTravIds )
        return;
    pNode->TravId = pMan->nTravIds;

    // collect the node's number (closer to reverse topological order)
    Msat_IntVecPush( pMan->vVarsInt, pNode->Num );
    Msat_IntVecWriteEntry( pMan->vVarsUsed, pNode->Num, 1 );
    if ( !Fraig_NodeIsAnd( pNode ) )
        return;

    // if the node does not have fanins, create them
    fItIsTime = 0;
    if ( pNode->vFanins == NULL )
    {
        fItIsTime = 1;
        // create the fanins of the supergate
        assert( pNode->fClauses == 0 );
        if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
        {
            pNode->vFanins = Fraig_NodeVecAlloc( 4 );
            Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) );
            Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) );
            Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) );
            Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
            Fraig_SupergateAddClausesMux( pMan, pNode );
        }
        else
        {
            pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes );
            Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins );
        }
        assert( pNode->vFanins->nSize > 1 );
        pNode->fClauses = 1;
        pMan->nVarsClauses++;

        // add fanins
        vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pNode->Num );
        assert( Msat_IntVecReadSize( vAdjs ) == 0 );
        for ( i = 0; i < pNode->vFanins->nSize; i++ )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[i]);
            Msat_IntVecPush( vAdjs, pFanin->Num );
        }
    }

    // recursively visit the fanins
    for ( i = 0; i < pNode->vFanins->nSize; i++ )
        Fraig_PrepareCones_rec( pMan, Fraig_Regular(pNode->vFanins->pArray[i]) );

    if ( fItIsTime )
    {
        // recursively visit the fanins
        for ( i = 0; i < pNode->vFanins->nSize; i++ )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[i]);
            vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
            Msat_IntVecPush( vAdjs, pNode->Num );
        }
    }
}

void Fraig_SetActivity ( Fraig_Man_t *  pMan, Fraig_Node_t *  pOld, Fraig_Node_t *  pNew  )

static

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

Synopsis [Collect variables using their proximity from the nodes.]

Description [This procedure creates a variable order based on collecting first the nodes that are the closest to the given two target nodes.]

SideEffects []

SeeAlso []

Definition at line 1436 of file fraigSat.c.

{
    Fraig_Node_t * pNode;
    int i, Number, MaxLevel;
    float * pFactors = Msat_SolverReadFactors(pMan->pSat);
    if ( pFactors == NULL )
        return;
    MaxLevel = Abc_MaxInt( pOld->Level, pNew->Level );
    // create the variable order
    for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
    {
        // get the new node on the frontier
        Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
        pNode = pMan->vNodes->pArray[Number];
        pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level );
//        if ( pNode->Num % 50 == 0 )
//        printf( "(%d) %.2f  ", MaxLevel - pNode->Level, pFactors[pNode->Num] );
    }
//    printf( "\n" );
}

void Fraig_SetupAdjacent ( Fraig_Man_t *  pMan, Msat_IntVec_t *  vConeVars  )

static

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

Synopsis [Set up the adjacent variable information.]

Description []

SideEffects []

SeeAlso []

Definition at line 974 of file fraigSat.c.

{
    Fraig_Node_t * pNode, * pFanin;
    Msat_IntVec_t * vAdjs;
    int * pVars, nVars, i, k;

    // clean the adjacents for the variables
    nVars = Msat_IntVecReadSize( vConeVars );
    pVars = Msat_IntVecReadArray( vConeVars );
    for ( i = 0; i < nVars; i++ )
    {
        // process its connections
        vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
        Msat_IntVecClear( vAdjs );

        pNode = pMan->vNodes->pArray[pVars[i]];
        if ( !Fraig_NodeIsAnd(pNode) )
            continue;

        // add fanins
        vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
        for ( k = 0; k < pNode->vFanins->nSize; k++ )
//        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
            Msat_IntVecPush( vAdjs, pFanin->Num );
//            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
        }
    }
    // add the fanouts
    for ( i = 0; i < nVars; i++ )
    {
        pNode = pMan->vNodes->pArray[pVars[i]];
        if ( !Fraig_NodeIsAnd(pNode) )
            continue;

        // add the edges
        for ( k = 0; k < pNode->vFanins->nSize; k++ )
//        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
            vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
            Msat_IntVecPush( vAdjs, pNode->Num );
//            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
        }
    }
}

void Fraig_SetupAdjacentMark ( Fraig_Man_t *  pMan, Msat_IntVec_t *  vConeVars  )

static

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

Synopsis [Set up the adjacent variable information.]

Description []

SideEffects []

SeeAlso []

Definition at line 1034 of file fraigSat.c.

{
    Fraig_Node_t * pNode, * pFanin;
    Msat_IntVec_t * vAdjs;
    int * pVars, nVars, i, k;

    // clean the adjacents for the variables
    nVars = Msat_IntVecReadSize( vConeVars );
    pVars = Msat_IntVecReadArray( vConeVars );
    for ( i = 0; i < nVars; i++ )
    {
        pNode = pMan->vNodes->pArray[pVars[i]];
        if ( pNode->fMark2 == 0 )
            continue;
//        pNode->fMark2 = 0;

        // process its connections
//        vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
//        Msat_IntVecClear( vAdjs );

        if ( !Fraig_NodeIsAnd(pNode) )
            continue;

        // add fanins
        vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
        for ( k = 0; k < pNode->vFanins->nSize; k++ )
//        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
            Msat_IntVecPush( vAdjs, pFanin->Num );
//            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
        }
    }
    // add the fanouts
    for ( i = 0; i < nVars; i++ )
    {
        pNode = pMan->vNodes->pArray[pVars[i]];
        if ( pNode->fMark2 == 0 )
            continue;
        pNode->fMark2 = 0;

        if ( !Fraig_NodeIsAnd(pNode) )
            continue;

        // add the edges
        for ( k = 0; k < pNode->vFanins->nSize; k++ )
//        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
            vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
            Msat_IntVecPush( vAdjs, pNode->Num );
//            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
        }
    }
}

void Fraig_SupergateAddClauses ( Fraig_Man_t *  p, Fraig_Node_t *  pNode, Fraig_NodeVec_t *  vSuper  )

static

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

Synopsis [Adds clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1104 of file fraigSat.c.

{
    int fComp1, RetValue, nVars, Var, Var1, i;

    assert( Fraig_NodeIsAnd( pNode ) );
    nVars = Msat_SolverReadVarNum(p->pSat);

    Var = pNode->Num;
    assert( Var  < nVars ); 
    for ( i = 0; i < vSuper->nSize; i++ )
    {
        // get the predecessor nodes
        // get the complemented attributes of the nodes
        fComp1 = Fraig_IsComplement(vSuper->pArray[i]);
        // determine the variable numbers
        Var1 = Fraig_Regular(vSuper->pArray[i])->Num;
        // check that the variables are in the SAT manager
        assert( Var1 < nVars );

        // suppose the AND-gate is A * B = C
        // add !A => !C   or   A + !C
    //  fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
        Msat_IntVecClear( p->vProj );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, fComp1) );
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var,  1) );
        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
        assert( RetValue );
    }

    // add A & B => C   or   !A + !B + C
//  fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
    Msat_IntVecClear( p->vProj );
    for ( i = 0; i < vSuper->nSize; i++ )
    {
        // get the predecessor nodes
        // get the complemented attributes of the nodes
        fComp1 = Fraig_IsComplement(vSuper->pArray[i]);
        // determine the variable numbers
        Var1 = Fraig_Regular(vSuper->pArray[i])->Num;

        // add this variable to the array
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, !fComp1) );
    }
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 0) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
}

void Fraig_SupergateAddClausesExor ( Fraig_Man_t *  p, Fraig_Node_t *  pNode  )

static

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

Synopsis [Adds clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1163 of file fraigSat.c.

{
    Fraig_Node_t * pNode1, * pNode2;
    int fComp, RetValue;

    assert( !Fraig_IsComplement( pNode ) );
    assert( Fraig_NodeIsExorType( pNode ) );
    // get nodes
    pNode1 = Fraig_Regular(Fraig_Regular(pNode->p1)->p1);
    pNode2 = Fraig_Regular(Fraig_Regular(pNode->p1)->p2);
    // get the complemented attribute of the EXOR/NEXOR gate
    fComp = Fraig_NodeIsExor( pNode ); // 1 if EXOR, 0 if NEXOR

    // create four clauses
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,   fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num,  fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num,  fComp) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,   fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,  !fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num,  fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,  !fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num,  fComp) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
}

void Fraig_SupergateAddClausesMux ( Fraig_Man_t *  p, Fraig_Node_t *  pNode  )

static

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

Synopsis [Adds clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1214 of file fraigSat.c.

{
    Fraig_Node_t * pNodeI, * pNodeT, * pNodeE;
    int RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;

    assert( !Fraig_IsComplement( pNode ) );
    assert( Fraig_NodeIsMuxType( pNode ) );
    // get nodes (I = if, T = then, E = else)
    pNodeI = Fraig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
    // get the variable numbers
    VarF = pNode->Num;
    VarI = pNodeI->Num;
    VarT = Fraig_Regular(pNodeT)->Num;
    VarE = Fraig_Regular(pNodeE)->Num;
    // get the complementation flags
    fCompT = Fraig_IsComplement(pNodeT);
    fCompE = Fraig_IsComplement(pNodeE);

    // f = ITE(i, t, e)

    // i' + t' + f
    // i' + t  + f'
    // i  + e' + f
    // i  + e  + f'

    // create four clauses
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  1) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  1^fCompT) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  1) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  0^fCompT) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  0) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  1^fCompE) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  0) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  0^fCompE) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );

    // two additional clauses
    // t' & e' -> f'
    // t  & e  -> f 

    // t  + e   + f'
    // t' + e'  + f 

    if ( VarT == VarE )
    {
//        assert( fCompT == !fCompE );
        return;
    }

    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  0^fCompT) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  0^fCompE) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
    Msat_IntVecClear( p->vProj );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  1^fCompT) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  1^fCompE) );
    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );

}

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? '+':'-' );
}

Variable Documentation

int nMuxes

static

Definition at line 48 of file fraigSat.c.