src/sat/fraig/fraigSat.c File Reference

#include "fraigInt.h"
#include "math.h"
Include dependency graph for fraigSat.c:

Go to the source code of this file.

Functions

static void Fraig_OrderVariables (Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
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)
void * Msat_ClauseVecReadEntry (void *p, int i)
int Fraig_NodesAreEqual (Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit, int nTimeLimit)
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 1302 of file fraigSat.c.

01303 {
01304     // make the pointer regular
01305     pNode = Fraig_Regular(pNode);
01306     // if the new node is complemented or a PI, another gate begins
01307     if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) )
01308     {
01309         Fraig_NodeVecPushUnique( vSuper, pNode );
01310         return;
01311     }
01312     // go through the branches
01313     Fraig_DetectFanoutFreeCone_rec( pNode->p1, vSuper, vInside, 0 );
01314     Fraig_DetectFanoutFreeCone_rec( pNode->p2, vSuper, vInside, 0 );
01315     // add the node
01316     Fraig_NodeVecPushUnique( vInside, pNode );
01317 }

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 1395 of file fraigSat.c.

01396 {
01397     Fraig_NodeVec_t * vFanins;
01398     Fraig_NodeVec_t * vInside;
01399     int nCubes;
01400     extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside );
01401 
01402     vFanins = Fraig_NodeVecAlloc( 8 );
01403     vInside = Fraig_NodeVecAlloc( 8 );
01404 
01405     Fraig_DetectFanoutFreeConeMux_rec( pNode, vFanins, vInside, 1 );
01406     assert( vInside->pArray[vInside->nSize-1] == pNode );
01407 
01408 //    nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside );
01409     nCubes = 0;
01410 
01411 printf( "%d(%d)", vFanins->nSize, nCubes );
01412     Fraig_NodeVecFree( vFanins );
01413     Fraig_NodeVecFree( vInside );
01414 }

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 1365 of file fraigSat.c.

01366 {
01367     // make the pointer regular
01368     pNode = Fraig_Regular(pNode);
01369     // if the new node is complemented or a PI, another gate begins
01370     if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) || !Fraig_NodeIsMuxType(pNode) )
01371     {
01372         Fraig_NodeVecPushUnique( vSuper, pNode );
01373         return;
01374     }
01375     // go through the branches
01376     Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p1, vSuper, vInside, 0 );
01377     Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p2, vSuper, vInside, 0 );
01378     Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p1, vSuper, vInside, 0 );
01379     Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p2, vSuper, vInside, 0 );
01380     // add the node
01381     Fraig_NodeVecPushUnique( vInside, pNode );
01382 }

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 648 of file fraigSat.c.

00649 {
00650     Fraig_Node_t * pNode1R, * pNode2R;
00651     int RetValue, RetValue1, i, clk;
00652     int fVerbose = 0;
00653 
00654     pNode1R = Fraig_Regular(pNode1);
00655     pNode2R = Fraig_Regular(pNode2);
00656     assert( pNode1R != pNode2R );
00657 
00658     // make sure the solver is allocated and has enough variables
00659     if ( p->pSat == NULL )
00660         Fraig_ManCreateSolver( p );
00661     // make sure the SAT solver has enough variables
00662     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
00663         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
00664 
00665    // get the logic cone
00666 clk = clock();
00667     Fraig_OrderVariables( p, pNode1R, pNode2R );
00668 //    Fraig_PrepareCones( p, pNode1R, pNode2R );
00669 p->timeTrav += clock() - clk;
00670 
00672     // prepare the solver to run incrementally on these variables
00673 //clk = clock();
00674     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00675 //p->time3 += clock() - clk;
00676 
00677     // solve under assumptions
00678     // A = 1; B = 0     OR     A = 1; B = 1 
00679     Msat_IntVecClear( p->vProj );
00680     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
00681     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
00682     // run the solver
00683 clk = clock();
00684     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
00685 p->timeSat += clock() - clk;
00686 
00687     if ( RetValue1 == MSAT_FALSE )
00688     {
00689 //p->time1 += clock() - clk;
00690 
00691 if ( fVerbose )
00692 {
00693     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00694 PRT( "time", clock() - clk );
00695 }
00696 
00697         // add the clause
00698         Msat_IntVecClear( p->vProj );
00699         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
00700         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
00701         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00702         assert( RetValue );
00703 //        p->nSatProofImp++;
00704         return 1;
00705     }
00706     else if ( RetValue1 == MSAT_TRUE )
00707     {
00708 //p->time2 += clock() - clk;
00709 
00710 if ( fVerbose )
00711 {
00712     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00713 PRT( "time", clock() - clk );
00714 }
00715         // record the counter example
00716 //        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
00717         p->nSatCounterImp++;
00718         return 0;
00719     }
00720     else // if ( RetValue1 == MSAT_UNKNOWN )
00721     {
00722 p->time3 += clock() - clk;
00723         p->nSatFailsImp++;
00724         return 0;
00725     }
00726 }

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 127 of file fraigSat.c.

00128 {
00129     Fraig_Node_t * pNode;
00130     int i;
00131     FREE( p->pModel );
00132     for ( i = 0; i < p->vOutputs->nSize; i++ )
00133     {
00134         // get the output node (it can be complemented!)
00135         pNode = p->vOutputs->pArray[i];
00136         // if the miter is constant 0, the problem is UNSAT
00137         if ( pNode == Fraig_Not(p->pConst1) )
00138             continue;
00139         // consider the special case when the miter is constant 1
00140         if ( pNode == p->pConst1 )
00141         {
00142             // in this case, any counter example will do to distinquish it from constant 0
00143             // here we pick the counter example composed of all zeros
00144             p->pModel = Fraig_ManAllocCounterExample( p );
00145             return 0;
00146         }
00147         // save the counter example
00148         p->pModel = Fraig_ManSaveCounterExample( p, pNode );
00149         // if the model is not found, return undecided
00150         if ( p->pModel == NULL )
00151             return -1;
00152         else
00153             return 0;
00154     }
00155     return 1;
00156 }

void Fraig_ManProveMiter ( Fraig_Man_t *  p  ) 

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

Synopsis [Tries to prove the final miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 83 of file fraigSat.c.

00084 {
00085     Fraig_Node_t * pNode;
00086     int i, clk;
00087 
00088     if ( !p->fTryProve )
00089         return;
00090  
00091     clk = clock();
00092     // consider all outputs of the multi-output miter
00093     for ( i = 0; i < p->vOutputs->nSize; i++ )
00094     {
00095         pNode = Fraig_Regular(p->vOutputs->pArray[i]);
00096         // skip already constant nodes
00097         if ( pNode == p->pConst1 )
00098             continue;
00099         // skip nodes that are different according to simulation
00100         if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
00101             continue;
00102         if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
00103         {
00104             if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
00105                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
00106             else
00107                 p->vOutputs->pArray[i] = p->pConst1;
00108         }
00109     }
00110     if ( p->fVerboseP ) 
00111     {
00112 //        PRT( "Final miter proof time", clock() - clk );
00113     }
00114 }

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 195 of file fraigSat.c.

00196 {
00197     // skip the visited node
00198     if ( pNode->TravId == pMan->nTravIds )
00199         return 0;
00200     // skip the boundary node
00201     if ( pNode->TravId == pMan->nTravIds-1 )
00202     {
00203         pNode->TravId = pMan->nTravIds;
00204         return 1;
00205     }
00206     pNode->TravId = pMan->nTravIds;
00207     // skip the PI node
00208     if ( pNode->NumPi >= 0 )
00209         return 1;
00210     // check the children
00211     return Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p1) ) +
00212            Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p2) );
00213 }

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 226 of file fraigSat.c.

00227 {
00228     // skip the visited node
00229     if ( pNode->TravId == pMan->nTravIds )
00230         return 1;
00231     // skip the boundary node
00232     if ( pNode->TravId == pMan->nTravIds-1 )
00233     {
00234         pNode->TravId = pMan->nTravIds;
00235         return 1;
00236     }
00237     pNode->TravId = pMan->nTravIds;
00238     // skip the PI node
00239     if ( pNode->NumPi >= 0 )
00240         return 0;
00241     // check the children
00242     return Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p1) ) *
00243            Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p2) );
00244 }

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 170 of file fraigSat.c.

00171 {
00172     // skip the visited node
00173     if ( pNode->TravId == pMan->nTravIds )
00174         return 0;
00175     pNode->TravId = pMan->nTravIds;
00176     // skip the PI node
00177     if ( pNode->NumPi >= 0 )
00178         return 1;
00179     // check the children
00180     return Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p1) ) +
00181            Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p2) );
00182 }

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 299 of file fraigSat.c.

00300 {
00301     int RetValue, RetValue1, i, fComp, clk;
00302     int fVerbose = 0;
00303     int fSwitch = 0;
00304 
00305     // make sure the nodes are not complemented
00306     assert( !Fraig_IsComplement(pNew) );
00307     assert( !Fraig_IsComplement(pOld) );
00308     assert( pNew != pOld );
00309 
00310     // if at least one of the nodes is a failed node, perform adjustments:
00311     // if the backtrack limit is small, simply skip this node
00312     // if the backtrack limit is > 10, take the quare root of the limit
00313     if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
00314     {
00315         p->nSatFails++;
00316 //            return 0;
00317 //        if ( nBTLimit > 10 )
00318 //            nBTLimit /= 10;
00319         if ( nBTLimit <= 10 )
00320             return 0;
00321         nBTLimit = (int)sqrt(nBTLimit);
00322 //        fSwitch = 1;
00323     }
00324 
00325     p->nSatCalls++;
00326 
00327     // make sure the solver is allocated and has enough variables
00328     if ( p->pSat == NULL )
00329         Fraig_ManCreateSolver( p );
00330     // make sure the SAT solver has enough variables
00331     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
00332         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
00333 
00334 
00335  
00336 /*
00337     {
00338         Fraig_Node_t * ppNodes[2] = { pOld, pNew };
00339         extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
00340         Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
00341     }
00342 */
00343 
00344     nMuxes = 0;
00345 
00346 
00347     // get the logic cone
00348 clk = clock();
00349 //    Fraig_VarsStudy( p, pOld, pNew );
00350     Fraig_OrderVariables( p, pOld, pNew );
00351 //    Fraig_PrepareCones( p, pOld, pNew );
00352 p->timeTrav += clock() - clk;
00353 
00354 //    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
00355 //    PRT( "Time", clock() - clk );
00356 
00357 if ( fVerbose )
00358     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
00359 
00360 
00361     // prepare variable activity
00362     Fraig_SetActivity( p, pOld, pNew );
00363 
00364     // get the complemented attribute
00365     fComp = Fraig_NodeComparePhase( pOld, pNew );
00366 //Msat_SolverPrintClauses( p->pSat );
00367 
00369     // prepare the solver to run incrementally on these variables
00370 //clk = clock();
00371     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00372 //p->time3 += clock() - clk;
00373 
00374 
00375     // solve under assumptions
00376     // A = 1; B = 0     OR     A = 1; B = 1 
00377     Msat_IntVecClear( p->vProj );
00378     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
00379     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
00380 
00381 //Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
00382 
00383     // run the solver
00384 clk = clock();
00385     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
00386 p->timeSat += clock() - clk;
00387 
00388     if ( RetValue1 == MSAT_FALSE )
00389     {
00390 //p->time1 += clock() - clk;
00391 
00392 if ( fVerbose )
00393 {
00394     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00395 PRT( "time", clock() - clk );
00396 }
00397 
00398         // add the clause
00399         Msat_IntVecClear( p->vProj );
00400         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
00401         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
00402         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00403         assert( RetValue );
00404         // continue solving the other implication
00405     }
00406     else if ( RetValue1 == MSAT_TRUE )
00407     {
00408 //p->time2 += clock() - clk;
00409 
00410 if ( fVerbose )
00411 {
00412     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00413 PRT( "time", clock() - clk );
00414 }
00415 
00416         // record the counter example
00417         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
00418 
00419 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00420 //            printf( "*" );
00421 //        printf( "s(%d)", pNew->Level );
00422         if ( fSwitch )
00423              printf( "s(%d)", pNew->Level );
00424         p->nSatCounter++;
00425         return 0;
00426     }
00427     else // if ( RetValue1 == MSAT_UNKNOWN )
00428     {
00429 p->time3 += clock() - clk;
00430 
00431 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00432 //            printf( "*" );
00433 //        printf( "T(%d)", pNew->Level );
00434 
00435         // mark the node as the failed node
00436         if ( pOld != p->pConst1 ) 
00437             pOld->fFailTfo = 1;
00438         pNew->fFailTfo = 1;
00439 //        p->nSatFails++;
00440         if ( fSwitch )
00441              printf( "T(%d)", pNew->Level );
00442         p->nSatFailsReal++;
00443         return 0;
00444     }
00445 
00446     // if the old node was constant 0, we already know the answer
00447     if ( pOld == p->pConst1 )
00448         return 1;
00449 
00451     // prepare the solver to run incrementally 
00452 //clk = clock();
00453     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00454 //p->time3 += clock() - clk;
00455     // solve under assumptions
00456     // A = 0; B = 1     OR     A = 0; B = 0 
00457     Msat_IntVecClear( p->vProj );
00458     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
00459     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
00460     // run the solver
00461 clk = clock();
00462     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
00463 p->timeSat += clock() - clk;
00464 
00465     if ( RetValue1 == MSAT_FALSE )
00466     {
00467 //p->time1 += clock() - clk;
00468 
00469 if ( fVerbose )
00470 {
00471     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00472 PRT( "time", clock() - clk );
00473 }
00474 
00475         // add the clause
00476         Msat_IntVecClear( p->vProj );
00477         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
00478         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
00479         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00480         assert( RetValue );
00481         // continue solving the other implication
00482     }
00483     else if ( RetValue1 == MSAT_TRUE )
00484     {
00485 //p->time2 += clock() - clk;
00486 
00487 if ( fVerbose )
00488 {
00489     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00490 PRT( "time", clock() - clk );
00491 }
00492 
00493         // record the counter example
00494         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
00495         p->nSatCounter++;
00496 
00497 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00498 //            printf( "*" );
00499 //        printf( "s(%d)", pNew->Level );
00500         if ( fSwitch )
00501              printf( "s(%d)", pNew->Level );
00502         return 0;
00503     }
00504     else // if ( RetValue1 == MSAT_UNKNOWN )
00505     {
00506 p->time3 += clock() - clk;
00507 
00508 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00509 //            printf( "*" );
00510 //        printf( "T(%d)", pNew->Level );
00511         if ( fSwitch )
00512              printf( "T(%d)", pNew->Level );
00513 
00514         // mark the node as the failed node
00515         pOld->fFailTfo = 1;
00516         pNew->fFailTfo = 1;
00517 //        p->nSatFails++;
00518         p->nSatFailsReal++;
00519         return 0;
00520     }
00521 
00522     // return SAT proof
00523     p->nSatProof++;
00524 
00525 //    if ( pOld->fFailTfo || pNew->fFailTfo )
00526 //        printf( "*" );
00527 //    printf( "u(%d)", pNew->Level );
00528 
00529     if ( fSwitch )
00530          printf( "u(%d)", pNew->Level );
00531 
00532     return 1;
00533 }

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 547 of file fraigSat.c.

00548 {
00549     int RetValue, RetValue1, i, fComp, clk;
00550     int fVerbose = 0;
00551 
00552     // make sure the nodes are not complemented
00553     assert( !Fraig_IsComplement(pNew) );
00554     assert( !Fraig_IsComplement(pOld) );
00555     assert( pNew != pOld );
00556 
00557     p->nSatCallsImp++;
00558 
00559     // make sure the solver is allocated and has enough variables
00560     if ( p->pSat == NULL )
00561         Fraig_ManCreateSolver( p );
00562     // make sure the SAT solver has enough variables
00563     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
00564         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
00565 
00566    // get the logic cone
00567 clk = clock();
00568     Fraig_OrderVariables( p, pOld, pNew );
00569 //    Fraig_PrepareCones( p, pOld, pNew );
00570 p->timeTrav += clock() - clk;
00571 
00572 if ( fVerbose )
00573     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
00574 
00575 
00576     // get the complemented attribute
00577     fComp = Fraig_NodeComparePhase( pOld, pNew );
00578 //Msat_SolverPrintClauses( p->pSat );
00579 
00581     // prepare the solver to run incrementally on these variables
00582 //clk = clock();
00583     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00584 //p->time3 += clock() - clk;
00585 
00586     // solve under assumptions
00587     // A = 1; B = 0     OR     A = 1; B = 1 
00588     Msat_IntVecClear( p->vProj );
00589     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
00590     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
00591     // run the solver
00592 clk = clock();
00593     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
00594 p->timeSat += clock() - clk;
00595 
00596     if ( RetValue1 == MSAT_FALSE )
00597     {
00598 //p->time1 += clock() - clk;
00599 
00600 if ( fVerbose )
00601 {
00602     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00603 PRT( "time", clock() - clk );
00604 }
00605 
00606         // add the clause
00607         Msat_IntVecClear( p->vProj );
00608         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
00609         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
00610         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00611         assert( RetValue );
00612 //        p->nSatProofImp++;
00613         return 1;
00614     }
00615     else if ( RetValue1 == MSAT_TRUE )
00616     {
00617 //p->time2 += clock() - clk;
00618 
00619 if ( fVerbose )
00620 {
00621     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00622 PRT( "time", clock() - clk );
00623 }
00624         // record the counter example
00625         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
00626         p->nSatCounterImp++;
00627         return 0;
00628     }
00629     else // if ( RetValue1 == MSAT_UNKNOWN )
00630     {
00631 p->time3 += clock() - clk;
00632         p->nSatFailsImp++;
00633         return 0;
00634     }
00635 }

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 63 of file fraigSat.c.

00064 {
00065     if ( pNode1 == pNode2 )
00066         return 1;
00067     if ( pNode1 == Fraig_Not(pNode2) )
00068         return 0;
00069     return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
00070 }

void Fraig_OrderVariables ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
) [static]

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

FileName [fraigSat.c]

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

Synopsis [Proving functional equivalence using SAT.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

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

] DECLARATIONS ///

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 869 of file fraigSat.c.

00870 {
00871     Fraig_Node_t * pNode, * pFanin;
00872     int i, k, Number, fUseMuxes = 1;
00873     int nVarsAlloc;
00874 
00875     assert( pOld != pNew );
00876     assert( !Fraig_IsComplement(pOld) );
00877     assert( !Fraig_IsComplement(pNew) );
00878 
00879     pMan->nTravIds++;
00880 
00881     // clean the variables
00882     nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed);
00883     Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 );
00884     Msat_IntVecClear( pMan->vVarsInt );
00885 
00886     // add the first node
00887     Msat_IntVecPush( pMan->vVarsInt, pOld->Num );
00888     Msat_IntVecWriteEntry( pMan->vVarsUsed, pOld->Num, 1 );
00889     pOld->TravId = pMan->nTravIds;
00890 
00891     // add the second node
00892     Msat_IntVecPush( pMan->vVarsInt, pNew->Num );
00893     Msat_IntVecWriteEntry( pMan->vVarsUsed, pNew->Num, 1 );
00894     pNew->TravId = pMan->nTravIds;
00895 
00896     // create the variable order
00897     for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
00898     {
00899         // get the new node on the frontier
00900         Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
00901         pNode = pMan->vNodes->pArray[Number];
00902         if ( !Fraig_NodeIsAnd(pNode) )
00903             continue;
00904 
00905         // if the node does not have fanins, create them
00906         if ( pNode->vFanins == NULL )
00907         {
00908             // create the fanins of the supergate
00909             assert( pNode->fClauses == 0 );
00910             // detecting a fanout-free cone (experiment only)
00911 //            Fraig_DetectFanoutFreeCone( pMan, pNode );
00912 
00913             if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
00914             {
00915                 pNode->vFanins = Fraig_NodeVecAlloc( 4 );
00916                 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) );
00917                 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) );
00918                 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) );
00919                 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
00920                 Fraig_SupergateAddClausesMux( pMan, pNode );
00921 //                Fraig_DetectFanoutFreeConeMux( pMan, pNode );
00922 
00923                 nMuxes++;
00924             }
00925             else
00926             {
00927                 pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes );
00928                 Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins );
00929             }
00930             assert( pNode->vFanins->nSize > 1 );
00931             pNode->fClauses = 1;
00932             pMan->nVarsClauses++;
00933 
00934             pNode->fMark2 = 1; // goes together with Fraig_SetupAdjacentMark()
00935         }
00936 
00937         // explore the implication fanins of pNode
00938         for ( k = 0; k < pNode->vFanins->nSize; k++ )
00939         {
00940             pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
00941             if ( pFanin->TravId == pMan->nTravIds ) // already collected
00942                 continue;
00943             // collect and mark
00944             Msat_IntVecPush( pMan->vVarsInt, pFanin->Num );
00945             Msat_IntVecWriteEntry( pMan->vVarsUsed, pFanin->Num, 1 );
00946             pFanin->TravId = pMan->nTravIds;
00947         }
00948     }
00949 
00950     // set up the adjacent variable information
00951 //    Fraig_SetupAdjacent( pMan, pMan->vVarsInt );
00952     Fraig_SetupAdjacentMark( pMan, pMan->vVarsInt );
00953 }

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 740 of file fraigSat.c.

00741 {
00742 //    Msat_IntVec_t * vAdjs;
00743 //    int * pVars, nVars, i, k;
00744     int nVarsAlloc;
00745 
00746     assert( pOld != pNew );
00747     assert( !Fraig_IsComplement(pOld) );
00748     assert( !Fraig_IsComplement(pNew) );
00749     // clean the variables
00750     nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed);
00751     Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 );
00752     Msat_IntVecClear( pMan->vVarsInt );
00753 
00754     pMan->nTravIds++;
00755     Fraig_PrepareCones_rec( pMan, pNew );
00756     Fraig_PrepareCones_rec( pMan, pOld );
00757 
00758 
00759 /*
00760     nVars = Msat_IntVecReadSize( pMan->vVarsInt );
00761     pVars = Msat_IntVecReadArray( pMan->vVarsInt );
00762     for ( i = 0; i < nVars; i++ )
00763     {
00764         // process its connections
00765         vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
00766         printf( "%d=%d { ", pVars[i], Msat_IntVecReadSize(vAdjs) );
00767         for ( k = 0; k < Msat_IntVecReadSize(vAdjs); k++ )
00768             printf( "%d ", Msat_IntVecReadEntry(vAdjs,k) );
00769         printf( "}\n" );
00770 
00771     }
00772     i = 0;
00773 */
00774 }

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 787 of file fraigSat.c.

00788 {
00789     Fraig_Node_t * pFanin;
00790     Msat_IntVec_t * vAdjs;
00791     int fUseMuxes = 1, i;
00792     int fItIsTime;
00793 
00794     // skip if the node is aleady visited
00795     assert( !Fraig_IsComplement(pNode) );
00796     if ( pNode->TravId == pMan->nTravIds )
00797         return;
00798     pNode->TravId = pMan->nTravIds;
00799 
00800     // collect the node's number (closer to reverse topological order)
00801     Msat_IntVecPush( pMan->vVarsInt, pNode->Num );
00802     Msat_IntVecWriteEntry( pMan->vVarsUsed, pNode->Num, 1 );
00803     if ( !Fraig_NodeIsAnd( pNode ) )
00804         return;
00805 
00806     // if the node does not have fanins, create them
00807     fItIsTime = 0;
00808     if ( pNode->vFanins == NULL )
00809     {
00810         fItIsTime = 1;
00811         // create the fanins of the supergate
00812         assert( pNode->fClauses == 0 );
00813         if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
00814         {
00815             pNode->vFanins = Fraig_NodeVecAlloc( 4 );
00816             Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) );
00817             Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) );
00818             Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) );
00819             Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
00820             Fraig_SupergateAddClausesMux( pMan, pNode );
00821         }
00822         else
00823         {
00824             pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes );
00825             Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins );
00826         }
00827         assert( pNode->vFanins->nSize > 1 );
00828         pNode->fClauses = 1;
00829         pMan->nVarsClauses++;
00830 
00831         // add fanins
00832         vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pNode->Num );
00833         assert( Msat_IntVecReadSize( vAdjs ) == 0 );
00834         for ( i = 0; i < pNode->vFanins->nSize; i++ )
00835         {
00836             pFanin = Fraig_Regular(pNode->vFanins->pArray[i]);
00837             Msat_IntVecPush( vAdjs, pFanin->Num );
00838         }
00839     }
00840 
00841     // recursively visit the fanins
00842     for ( i = 0; i < pNode->vFanins->nSize; i++ )
00843         Fraig_PrepareCones_rec( pMan, Fraig_Regular(pNode->vFanins->pArray[i]) );
00844 
00845     if ( fItIsTime )
00846     {
00847         // recursively visit the fanins
00848         for ( i = 0; i < pNode->vFanins->nSize; i++ )
00849         {
00850             pFanin = Fraig_Regular(pNode->vFanins->pArray[i]);
00851             vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
00852             Msat_IntVecPush( vAdjs, pNode->Num );
00853         }
00854     }
00855 }

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 1430 of file fraigSat.c.

01431 {
01432     Fraig_Node_t * pNode;
01433     int i, Number, MaxLevel;
01434     float * pFactors = Msat_SolverReadFactors(pMan->pSat);
01435     if ( pFactors == NULL )
01436         return;
01437     MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level );
01438     // create the variable order
01439     for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
01440     {
01441         // get the new node on the frontier
01442         Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
01443         pNode = pMan->vNodes->pArray[Number];
01444         pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level );
01445 //        if ( pNode->Num % 50 == 0 )
01446 //        printf( "(%d) %.2f  ", MaxLevel - pNode->Level, pFactors[pNode->Num] );
01447     }
01448 //    printf( "\n" );
01449 }

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 968 of file fraigSat.c.

00969 {
00970     Fraig_Node_t * pNode, * pFanin;
00971     Msat_IntVec_t * vAdjs;
00972     int * pVars, nVars, i, k;
00973 
00974     // clean the adjacents for the variables
00975     nVars = Msat_IntVecReadSize( vConeVars );
00976     pVars = Msat_IntVecReadArray( vConeVars );
00977     for ( i = 0; i < nVars; i++ )
00978     {
00979         // process its connections
00980         vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
00981         Msat_IntVecClear( vAdjs );
00982 
00983         pNode = pMan->vNodes->pArray[pVars[i]];
00984         if ( !Fraig_NodeIsAnd(pNode) )
00985             continue;
00986 
00987         // add fanins
00988         vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
00989         for ( k = 0; k < pNode->vFanins->nSize; k++ )
00990 //        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
00991         {
00992             pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
00993             Msat_IntVecPush( vAdjs, pFanin->Num );
00994 //            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
00995         }
00996     }
00997     // add the fanouts
00998     for ( i = 0; i < nVars; i++ )
00999     {
01000         pNode = pMan->vNodes->pArray[pVars[i]];
01001         if ( !Fraig_NodeIsAnd(pNode) )
01002             continue;
01003 
01004         // add the edges
01005         for ( k = 0; k < pNode->vFanins->nSize; k++ )
01006 //        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
01007         {
01008             pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
01009             vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
01010             Msat_IntVecPush( vAdjs, pNode->Num );
01011 //            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
01012         }
01013     }
01014 }

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 1028 of file fraigSat.c.

01029 {
01030     Fraig_Node_t * pNode, * pFanin;
01031     Msat_IntVec_t * vAdjs;
01032     int * pVars, nVars, i, k;
01033 
01034     // clean the adjacents for the variables
01035     nVars = Msat_IntVecReadSize( vConeVars );
01036     pVars = Msat_IntVecReadArray( vConeVars );
01037     for ( i = 0; i < nVars; i++ )
01038     {
01039         pNode = pMan->vNodes->pArray[pVars[i]];
01040         if ( pNode->fMark2 == 0 )
01041             continue;
01042 //        pNode->fMark2 = 0;
01043 
01044         // process its connections
01045 //        vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
01046 //        Msat_IntVecClear( vAdjs );
01047 
01048         if ( !Fraig_NodeIsAnd(pNode) )
01049             continue;
01050 
01051         // add fanins
01052         vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
01053         for ( k = 0; k < pNode->vFanins->nSize; k++ )
01054 //        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
01055         {
01056             pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
01057             Msat_IntVecPush( vAdjs, pFanin->Num );
01058 //            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
01059         }
01060     }
01061     // add the fanouts
01062     for ( i = 0; i < nVars; i++ )
01063     {
01064         pNode = pMan->vNodes->pArray[pVars[i]];
01065         if ( pNode->fMark2 == 0 )
01066             continue;
01067         pNode->fMark2 = 0;
01068 
01069         if ( !Fraig_NodeIsAnd(pNode) )
01070             continue;
01071 
01072         // add the edges
01073         for ( k = 0; k < pNode->vFanins->nSize; k++ )
01074 //        for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
01075         {
01076             pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
01077             vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
01078             Msat_IntVecPush( vAdjs, pNode->Num );
01079 //            Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
01080         }
01081     }
01082 }

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 1098 of file fraigSat.c.

01099 {
01100     int fComp1, RetValue, nVars, Var, Var1, i;
01101 
01102     assert( Fraig_NodeIsAnd( pNode ) );
01103     nVars = Msat_SolverReadVarNum(p->pSat);
01104 
01105     Var = pNode->Num;
01106     assert( Var  < nVars ); 
01107     for ( i = 0; i < vSuper->nSize; i++ )
01108     {
01109         // get the predecessor nodes
01110         // get the complemented attributes of the nodes
01111         fComp1 = Fraig_IsComplement(vSuper->pArray[i]);
01112         // determine the variable numbers
01113         Var1 = Fraig_Regular(vSuper->pArray[i])->Num;
01114         // check that the variables are in the SAT manager
01115         assert( Var1 < nVars );
01116 
01117         // suppose the AND-gate is A * B = C
01118         // add !A => !C   or   A + !C
01119     //  fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
01120         Msat_IntVecClear( p->vProj );
01121         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, fComp1) );
01122         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var,  1) );
01123         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01124         assert( RetValue );
01125     }
01126 
01127     // add A & B => C   or   !A + !B + C
01128 //  fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
01129     Msat_IntVecClear( p->vProj );
01130     for ( i = 0; i < vSuper->nSize; i++ )
01131     {
01132         // get the predecessor nodes
01133         // get the complemented attributes of the nodes
01134         fComp1 = Fraig_IsComplement(vSuper->pArray[i]);
01135         // determine the variable numbers
01136         Var1 = Fraig_Regular(vSuper->pArray[i])->Num;
01137 
01138         // add this variable to the array
01139         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, !fComp1) );
01140     }
01141     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 0) );
01142     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01143     assert( RetValue );
01144 }

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 1157 of file fraigSat.c.

01158 {
01159     Fraig_Node_t * pNode1, * pNode2;
01160     int fComp, RetValue;
01161 
01162     assert( !Fraig_IsComplement( pNode ) );
01163     assert( Fraig_NodeIsExorType( pNode ) );
01164     // get nodes
01165     pNode1 = Fraig_Regular(Fraig_Regular(pNode->p1)->p1);
01166     pNode2 = Fraig_Regular(Fraig_Regular(pNode->p1)->p2);
01167     // get the complemented attribute of the EXOR/NEXOR gate
01168     fComp = Fraig_NodeIsExor( pNode ); // 1 if EXOR, 0 if NEXOR
01169 
01170     // create four clauses
01171     Msat_IntVecClear( p->vProj );
01172     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,   fComp) );
01173     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num,  fComp) );
01174     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num,  fComp) );
01175     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01176     assert( RetValue );
01177     Msat_IntVecClear( p->vProj );
01178     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,   fComp) );
01179     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) );
01180     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) );
01181     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01182     assert( RetValue );
01183     Msat_IntVecClear( p->vProj );
01184     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,  !fComp) );
01185     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num,  fComp) );
01186     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) );
01187     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01188     assert( RetValue );
01189     Msat_IntVecClear( p->vProj );
01190     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num,  !fComp) );
01191     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) );
01192     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num,  fComp) );
01193     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01194     assert( RetValue );
01195 }

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 1208 of file fraigSat.c.

01209 {
01210     Fraig_Node_t * pNodeI, * pNodeT, * pNodeE;
01211     int RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
01212 
01213     assert( !Fraig_IsComplement( pNode ) );
01214     assert( Fraig_NodeIsMuxType( pNode ) );
01215     // get nodes (I = if, T = then, E = else)
01216     pNodeI = Fraig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
01217     // get the variable numbers
01218     VarF = pNode->Num;
01219     VarI = pNodeI->Num;
01220     VarT = Fraig_Regular(pNodeT)->Num;
01221     VarE = Fraig_Regular(pNodeE)->Num;
01222     // get the complementation flags
01223     fCompT = Fraig_IsComplement(pNodeT);
01224     fCompE = Fraig_IsComplement(pNodeE);
01225 
01226     // f = ITE(i, t, e)
01227 
01228     // i' + t' + f
01229     // i' + t  + f'
01230     // i  + e' + f
01231     // i  + e  + f'
01232 
01233     // create four clauses
01234     Msat_IntVecClear( p->vProj );
01235     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  1) );
01236     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  1^fCompT) );
01237     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
01238     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01239     assert( RetValue );
01240     Msat_IntVecClear( p->vProj );
01241     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  1) );
01242     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  0^fCompT) );
01243     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
01244     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01245     assert( RetValue );
01246     Msat_IntVecClear( p->vProj );
01247     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  0) );
01248     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  1^fCompE) );
01249     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
01250     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01251     assert( RetValue );
01252     Msat_IntVecClear( p->vProj );
01253     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI,  0) );
01254     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  0^fCompE) );
01255     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
01256     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01257     assert( RetValue );
01258 
01259     // two additional clauses
01260     // t' & e' -> f'
01261     // t  & e  -> f 
01262 
01263     // t  + e   + f'
01264     // t' + e'  + f 
01265 
01266     if ( VarT == VarE )
01267     {
01268 //        assert( fCompT == !fCompE );
01269         return;
01270     }
01271 
01272     Msat_IntVecClear( p->vProj );
01273     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  0^fCompT) );
01274     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  0^fCompE) );
01275     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
01276     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01277     assert( RetValue );
01278     Msat_IntVecClear( p->vProj );
01279     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  1^fCompT) );
01280     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  1^fCompE) );
01281     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
01282     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
01283     assert( RetValue );
01284 
01285 }

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file fraigSat.c.

00258 {
00259     int NumPis, NumCut, fContain;
00260 
00261     // mark the TFI of pNew
00262     p->nTravIds++;
00263     NumPis = Fraig_MarkTfi_rec( p, pNew );
00264     printf( "(%d)(%d,%d):", NumPis, pOld->Level, pNew->Level );
00265 
00266     // check if the old is in the TFI
00267     if ( pOld->TravId == p->nTravIds )
00268     {
00269         printf( "* " );
00270         return;
00271     }
00272 
00273     // count the boundary of nodes in pOld
00274     p->nTravIds++;
00275     NumCut = Fraig_MarkTfi2_rec( p, pOld );
00276     printf( "%d", NumCut );
00277 
00278     // check if the new is contained in the old's support
00279     p->nTravIds++;
00280     fContain = Fraig_MarkTfi3_rec( p, pNew );
00281     printf( "%c ", fContain? '+':'-' );
00282 }

void* Msat_ClauseVecReadEntry ( void *  p,
int  i 
)

Variable Documentation

int nMuxes [static]

Definition at line 46 of file fraigSat.c.

Generated on Tue Jan 5 12:19:39 2010 for abc70930 by  doxygen 1.6.1