diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aig.h | 1 | ||||
-rw-r--r-- | src/aig/aig/aigDfs.c | 62 | ||||
-rw-r--r-- | src/aig/aig/aigPartSat.c | 612 | ||||
-rw-r--r-- | src/aig/aig/module.make | 1 | ||||
-rw-r--r-- | src/aig/cnf/cnf.h | 6 | ||||
-rw-r--r-- | src/aig/cnf/cnfMan.c | 8 | ||||
-rw-r--r-- | src/aig/dar/darScript.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraCec.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 4 | ||||
-rw-r--r-- | src/aig/hop/hopDfs.c | 4 | ||||
-rw-r--r-- | src/aig/mfx/mfxCore.c | 5 | ||||
-rw-r--r-- | src/aig/ntl/ntlExtract.c | 2 | ||||
-rw-r--r-- | src/aig/nwk/nwk.h | 1 | ||||
-rw-r--r-- | src/aig/nwk/nwkCheck.c | 4 | ||||
-rw-r--r-- | src/aig/nwk/nwkFanio.c | 12 | ||||
-rw-r--r-- | src/aig/nwk/nwkUtil.c | 121 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigInter.c | 458 |
19 files changed, 1240 insertions, 69 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 93ca298a..84c1e0b5 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -460,6 +460,7 @@ extern void Aig_ManCutStop( Aig_ManCut_t * p ); /*=== aigDfs.c ==========================================================*/ extern int Aig_ManVerifyTopoOrder( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly ); +extern Vec_Ptr_t * Aig_ManDfsPreorder( Aig_Man_t * p, int fNodesOnly ); extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ); extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 47597f93..c9893ed2 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -166,6 +166,68 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly ) /**Function************************************************************* + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDfsPreorder_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( pObj == NULL ) + return; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + Vec_PtrPush( vNodes, pObj ); + if ( p->pEquivs && Aig_ObjEquiv(p, pObj) ) + Aig_ManDfs_rec( p, Aig_ObjEquiv(p, pObj), vNodes ); + Aig_ManDfsPreorder_rec( p, Aig_ObjFanin0(pObj), vNodes ); + Aig_ManDfsPreorder_rec( p, Aig_ObjFanin1(pObj), vNodes ); +} + +/**Function************************************************************* + + Synopsis [Collects objects of the AIG in the DFS order.] + + Description [Works with choice nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfsPreorder( Aig_Man_t * p, int fNodesOnly ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManIncrementTravId( p ); + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + // start the array of nodes + vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) ); + // mark PIs if they should not be collected + if ( fNodesOnly ) + Aig_ManForEachPi( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + else + Vec_PtrPush( vNodes, Aig_ManConst1(p) ); + // collect nodes reachable in the DFS order + Aig_ManForEachPo( p, pObj, i ) + Aig_ManDfsPreorder_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes ); + if ( fNodesOnly ) + assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) ); + else + assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) ); + return vNodes; +} + +/**Function************************************************************* + Synopsis [Levelizes the nodes.] Description [] diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c new file mode 100644 index 00000000..2a3e975c --- /dev/null +++ b/src/aig/aig/aigPartSat.c @@ -0,0 +1,612 @@ +/**CFile**************************************************************** + + FileName [aigPartSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Partitioning for SAT solving.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigPartSat.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" +#include "satSolver.h" +#include "cnf.h" + +/* + +The node partitioners defined in this file return array of intergers +mapping each AND node's ID into the 0-based number of its partition. +The mapping of PIs/POs will be derived automatically in Aig_ManPartSplit(). + +The partitions can be ordered in any way, but the recommended ordering +is to first include partitions whose nodes are closer to the outputs. + +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [No partitioning.] + + Description [The partitioner ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_ManPartitionMonolithic( Aig_Man_t * p ) +{ + Vec_Int_t * vId2Part; + vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) ); + return vId2Part; +} + +/**Function************************************************************* + + Synopsis [Partitioning using levelized order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_ManPartitionLevelized( Aig_Man_t * p, int nPartSize ) +{ + Vec_Int_t * vId2Part; + Vec_Vec_t * vNodes; + Aig_Obj_t * pObj; + int i, k, Counter = 0; + vNodes = Aig_ManLevelize( p ); + vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) ); + Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k ) + Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize ); + Vec_VecFree( vNodes ); + return vId2Part; +} + +/**Function************************************************************* + + Synopsis [Partitioning using DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_ManPartitionDfs( Aig_Man_t * p, int nPartSize, int fPreorder ) +{ + Vec_Int_t * vId2Part; + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i, Counter = 0; + vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) ); + if ( fPreorder ) + { + vNodes = Aig_ManDfsPreorder( p, 1 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize ); + } + else + { + vNodes = Aig_ManDfs( p, 1 ); + Vec_PtrForEachEntryReverse( vNodes, pObj, i ) + Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize ); + } + Vec_PtrFree( vNodes ); + return vId2Part; +} + +/**Function************************************************************* + + Synopsis [Recursively constructs the partition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPartSplitOne_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPio2Id ) +{ + if ( !Aig_ObjIsTravIdCurrent( p, pObj ) ) + { // new PI + Aig_ObjSetTravIdCurrent( p, pObj ); +/* + if ( pObj->fMarkA ) // const0 + pObj->pData = Aig_ManConst0( pNew ); + else if ( pObj->fMarkB ) // const1 + pObj->pData = Aig_ManConst1( pNew ); + else +*/ + { + pObj->pData = Aig_ObjCreatePi( pNew ); + if ( pObj->fMarkA ) // const0 + ((Aig_Obj_t *)pObj->pData)->fMarkA = 1; + else if ( pObj->fMarkB ) // const1 + ((Aig_Obj_t *)pObj->pData)->fMarkB = 1; + Vec_IntPush( vPio2Id, Aig_ObjId(pObj) ); + } + return; + } + if ( pObj->pData ) + return; + Aig_ManPartSplitOne_rec( pNew, p, Aig_ObjFanin0(pObj), vPio2Id ); + Aig_ManPartSplitOne_rec( pNew, p, Aig_ObjFanin1(pObj), vPio2Id ); + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Carves out one partition of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManPartSplitOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Int_t ** pvPio2Id ) +{ + Vec_Int_t * vPio2Id; + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + // mark these nodes + Aig_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + Aig_ObjSetTravIdCurrent( p, pObj ); + pObj->pData = NULL; + } + // add these nodes in a DFS order + pNew = Aig_ManStart( Vec_PtrSize(vNodes) ); + vPio2Id = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Aig_ManPartSplitOne_rec( pNew, p, pObj, vPio2Id ); + // add the POs + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Aig_ObjRefs(pObj->pData) != Aig_ObjRefs(pObj) ) + { + assert( Aig_ObjRefs(pObj->pData) < Aig_ObjRefs(pObj) ); + Aig_ObjCreatePo( pNew, pObj->pData ); + Vec_IntPush( vPio2Id, Aig_ObjId(pObj) ); + } + assert( Aig_ManNodeNum(pNew) == Vec_PtrSize(vNodes) ); + *pvPio2Id = vPio2Id; + return pNew; +} + +/**Function************************************************************* + + Synopsis [Derives AIGs for each partition.] + + Description [The first argument is a original AIG. The second argument + is the array mapping each AND-node's ID into the 0-based number of its + partition. The last argument is the array of arrays (one for each new AIG) + mapping the index of each terminal in the new AIG (the index of each + terminal is derived by ordering PIs followed by POs in their natural order) + into the ID of the corresponding node in the original AIG. The returned + value is the array of AIGs representing the partitions.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManPartSplit( Aig_Man_t * p, Vec_Int_t * vNode2Part, Vec_Ptr_t ** pvPio2Id, Vec_Ptr_t ** pvPart2Pos ) +{ + Vec_Vec_t * vGroups, * vPart2Pos; + Vec_Ptr_t * vAigs, * vPio2Id, * vNodes; + Vec_Int_t * vPio2IdOne; + Aig_Man_t * pAig; + Aig_Obj_t * pObj, * pDriver; + int i, nodePart, nParts; + vAigs = Vec_PtrAlloc( 100 ); + vPio2Id = Vec_PtrAlloc( 100 ); + // put all nodes into levels according to their partition + nParts = Vec_IntFindMax(vNode2Part) + 1; + assert( nParts > 0 ); + vGroups = Vec_VecAlloc( nParts ); + Vec_IntForEachEntry( vNode2Part, nodePart, i ) + { + pObj = Aig_ManObj( p, i ); + if ( Aig_ObjIsNode(pObj) ) + Vec_VecPush( vGroups, nodePart, pObj ); + } + + // label PIs that should be restricted to some values + Aig_ManForEachPo( p, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + if ( Aig_ObjIsPi(pDriver) ) + { + if ( Aig_ObjFaninC0(pObj) ) + pDriver->fMarkA = 1; // const0 PI + else + pDriver->fMarkB = 1; // const1 PI + } + } + + // create partitions + Vec_VecForEachLevel( vGroups, vNodes, i ) + { + if ( Vec_PtrSize(vNodes) == 0 ) + { + printf( "Aig_ManPartSplit(): Skipping partition # %d without nodes (warning).\n", i ); + continue; + } + pAig = Aig_ManPartSplitOne( p, vNodes, &vPio2IdOne ); + Vec_PtrPush( vPio2Id, vPio2IdOne ); + Vec_PtrPush( vAigs, pAig ); + } + Vec_VecFree( vGroups ); + + // divide POs according to their partitions + vPart2Pos = Vec_VecStart( Vec_PtrSize(vAigs) ); + Aig_ManForEachPo( p, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + if ( Aig_ObjIsPi(pDriver) ) + pDriver->fMarkA = pDriver->fMarkB = 0; + else + Vec_VecPush( vPart2Pos, Vec_IntEntry(vNode2Part, Aig_ObjFaninId0(pObj)), pObj ); + } + + *pvPio2Id = vPio2Id; + *pvPart2Pos = (Vec_Ptr_t *)vPart2Pos; + return vAigs; +} + +/**Function************************************************************* + + Synopsis [Resets node polarity to unbias the polarity of CNF variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPartResetNodePolarity( Aig_Man_t * pPart ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( pPart, pObj, i ) + pObj->fPhase = 0; +} + +/**Function************************************************************* + + Synopsis [Sets polarity according to the original nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManPartSetNodePolarity( Aig_Man_t * p, Aig_Man_t * pPart, Vec_Int_t * vPio2Id ) +{ + Aig_Obj_t * pObj, * pObjInit; + int i; + Aig_ManConst1(pPart)->fPhase = 1; + Aig_ManForEachPi( pPart, pObj, i ) + { + pObjInit = Aig_ManObj( p, Vec_IntEntry(vPio2Id, i) ); + pObj->fPhase = pObjInit->fPhase; + } + Aig_ManForEachNode( pPart, pObj, i ) + pObj->fPhase = (Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pPart, pObj, i ) + { + pObjInit = Aig_ManObj( p, Vec_IntEntry(vPio2Id, Aig_ManPiNum(pPart) + i) ); + pObj->fPhase = (Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj)); + assert( pObj->fPhase == pObjInit->fPhase ); + } +} + +/**Function************************************************************* + + Synopsis [Sets polarity according to the original nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDeriveCounterExample( Aig_Man_t * p, Vec_Int_t * vNode2Var, sat_solver * pSat ) +{ + Vec_Int_t * vPisIds; + Aig_Obj_t * pObj; + int i; + // collect IDs of PI variables + // (fanoutless PIs have SAT var 0, which is an unused in the SAT solver -> has value 0) + vPisIds = Vec_IntAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vPisIds, Vec_IntEntry(vNode2Var, Aig_ObjId(pObj)) ); + // derive the SAT assignment + p->pData = Sat_SolverGetModel( pSat, vPisIds->pArray, vPisIds->nSize ); + Vec_IntFree( vPisIds ); +} + +/**Function************************************************************* + + Synopsis [Derives CNF for the partition (pAig) and adds it to solver.] + + Description [Array vPio2Id contains mapping of the PI/PO terminal of pAig + into the IDs of the corresponding original nodes. Array vNode2Var contains + mapping of the original nodes into their SAT variable numbers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManAddNewCnfToSolver( sat_solver * pSat, Aig_Man_t * pAig, Vec_Int_t * vNode2Var, + Vec_Int_t * vPioIds, Vec_Ptr_t * vPartPos, int fAlignPol ) +{ + Cnf_Dat_t * pCnf; + Aig_Obj_t * pObj; + int * pBeg, * pEnd; + int i, Lits[2], iSatVarOld, iNodeIdOld; + // derive CNF and express it using new SAT variables + pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) ); + Cnf_DataTranformPolarity( pCnf, 1 ); + Cnf_DataLift( pCnf, sat_solver_nvars(pSat) ); + // create new variables in the SAT solver + sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + pCnf->nVars ); + // add clauses for this CNF + Cnf_CnfForClause( pCnf, pBeg, pEnd, i ) + if ( !sat_solver_addclause( pSat, pBeg, pEnd ) ) + { + assert( 0 ); // if it happens, can return 1 (unsatisfiable) + return 1; + } + // derive the connector clauses + Aig_ManForEachPi( pAig, pObj, i ) + { + iNodeIdOld = Vec_IntEntry( vPioIds, i ); + iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld ); + if ( iSatVarOld == 0 ) // iNodeIdOld in the original AIG has no SAT var + { + // map the corresponding original AIG node into this SAT var + Vec_IntWriteEntry( vNode2Var, iNodeIdOld, pCnf->pVarNums[Aig_ObjId(pObj)] ); + continue; + } + // add connector clauses + Lits[0] = toLitCond( iSatVarOld, 0 ); + Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( iSatVarOld, 1 ); + Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // derive the connector clauses + Aig_ManForEachPo( pAig, pObj, i ) + { + iNodeIdOld = Vec_IntEntry( vPioIds, Aig_ManPiNum(pAig) + i ); + iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld ); + if ( iSatVarOld == 0 ) // iNodeIdOld in the original AIG has no SAT var + { + // map the corresponding original AIG node into this SAT var + Vec_IntWriteEntry( vNode2Var, iNodeIdOld, pCnf->pVarNums[Aig_ObjId(pObj)] ); + continue; + } + // add connector clauses + Lits[0] = toLitCond( iSatVarOld, 0 ); + Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( iSatVarOld, 1 ); + Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // transfer the ID of constant 1 node + if ( Vec_IntEntry( vNode2Var, 0 ) == 0 ) + Vec_IntWriteEntry( vNode2Var, 0, pCnf->pVarNums[0] ); + // remove the CNF + Cnf_DataFree( pCnf ); + // constrain the solver with the literals corresponding to the original POs + Vec_PtrForEachEntry( vPartPos, pObj, i ) + { + iNodeIdOld = Aig_ObjFaninId0( pObj ); + iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld ); + assert( iSatVarOld != 0 ); + // assert the original PO to be 1 + Lits[0] = toLitCond( iSatVarOld, Aig_ObjFaninC0(pObj) ); + // correct the polarity if polarity alignment is enabled + if ( fAlignPol && Aig_ObjFanin0(pObj)->fPhase ) + Lits[0] = lit_neg( Lits[0] ); + if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) ) + { + assert( 0 ); // if it happens, can return 1 (unsatisfiable) + return 1; + } + } + // constrain some the primary inputs to constant values + Aig_ManForEachPi( pAig, pObj, i ) + { + if ( !pObj->fMarkA && !pObj->fMarkB ) + continue; + iNodeIdOld = Vec_IntEntry( vPioIds, i ); + iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld ); + Lits[0] = toLitCond( iSatVarOld, pObj->fMarkA ); + if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) ) + { + assert( 0 ); // if it happens, can return 1 (unsatisfiable) + return 1; + } + pObj->fMarkA = pObj->fMarkB = 0; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs partitioned SAT solving.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize, + int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose ) +{ + sat_solver * pSat; + Vec_Ptr_t * vAigs; + Vec_Vec_t * vPio2Id, * vPart2Pos; + Aig_Man_t * pAig, * pTemp; + Vec_Int_t * vNode2Part, * vNode2Var; + int nConfRemaining = nConfTotal, nNodes = 0; + int i, clk, status, RetValue; + + // perform partitioning according to the selected algorithm + clk = clock(); + switch ( nAlgo ) + { + case 0: + vNode2Part = Aig_ManPartitionMonolithic( p ); + break; + case 1: + vNode2Part = Aig_ManPartitionLevelized( p, nPartSize ); + break; + case 2: + vNode2Part = Aig_ManPartitionDfs( p, nPartSize, 0 ); + break; + case 3: + vNode2Part = Aig_ManPartitionDfs( p, nPartSize, 1 ); + break; + default: + printf( "Unknown partitioning algorithm.\n" ); + return -1; + } + + if ( fVerbose ) + { + printf( "Partitioning derived %d partitions. ", Vec_IntFindMax(vNode2Part) + 1 ); + PRT( "Time", clock() - clk ); + } + + // split the original AIG into partition AIGs (vAigs) + // also, derives mapping of PIs/POs of partition AIGs into original nodes + // also, derives mapping of POs of the original AIG into partitions + vAigs = Aig_ManPartSplit( p, vNode2Part, (Vec_Ptr_t **)&vPio2Id, (Vec_Ptr_t **)&vPart2Pos ); + Vec_IntFree( vNode2Part ); + + if ( fVerbose ) + { + printf( "Partions were transformed into AIGs. " ); + PRT( "Time", clock() - clk ); + } + + // synthesize partitions + if ( fSynthesize ) + Vec_PtrForEachEntry( vAigs, pAig, i ) + { + pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 ); + Vec_PtrWriteEntry( vAigs, i, pAig ); + Aig_ManStop( pTemp ); + } + + // start the SAT solver + pSat = sat_solver_new(); +// pSat->verbosity = fVerbose; + // start mapping of the original AIG IDs into their SAT variable numbers + vNode2Var = Vec_IntStart( Aig_ManObjNumMax(p) ); + + // add partitions, one at a time, and run the SAT solver + Vec_PtrForEachEntry( vAigs, pAig, i ) + { +clk = clock(); + // transform polarity of the AIG + if ( fAlignPol ) + Aig_ManPartSetNodePolarity( p, pAig, Vec_VecEntry(vPio2Id,i) ); + else + Aig_ManPartResetNodePolarity( pAig ); + // add CNF of this partition to the SAT solver + if ( Aig_ManAddNewCnfToSolver( pSat, pAig, vNode2Var, + Vec_VecEntry(vPio2Id,i), Vec_VecEntry(vPart2Pos,i), fAlignPol ) ) + { + RetValue = 1; + break; + } + // call the SAT solver + status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfRemaining, (sint64)0, (sint64)0, (sint64)0 ); + if ( fVerbose ) + { + printf( "%4d : Aig = %6d. Vs = %7d. RootCs = %7d. LearnCs = %6d. ", + i, nNodes += Aig_ManNodeNum(pAig), sat_solver_nvars(pSat), + (int)pSat->stats.clauses, (int)pSat->stats.learnts ); +PRT( "Time", clock() - clk ); + } + // analize the result + if ( status == l_False ) + { + RetValue = 1; + break; + } + else if ( status == l_True ) + RetValue = 0; + else + RetValue = -1; + nConfRemaining -= pSat->stats.conflicts; + if ( nConfRemaining <= 0 ) + { + printf( "Exceeded the limit on the total number of conflicts (%d).\n", nConfTotal ); + break; + } + } + if ( RetValue == 0 ) + Aig_ManDeriveCounterExample( p, vNode2Var, pSat ); + // cleanup + sat_solver_delete( pSat ); + Vec_PtrForEachEntry( vAigs, pTemp, i ) + Aig_ManStop( pTemp ); + Vec_PtrFree( vAigs ); + Vec_VecFree( vPio2Id ); + Vec_VecFree( vPart2Pos ); + Vec_IntFree( vNode2Var ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index f1d018af..b1b8c5c2 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -13,6 +13,7 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigOrder.c \ src/aig/aig/aigPart.c \ src/aig/aig/aigPartReg.c \ + src/aig/aig/aigPartSat.c \ src/aig/aig/aigRepr.c \ src/aig/aig/aigRet.c \ src/aig/aig/aigRetF.c \ diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index f4f782df..c9c5bce3 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -108,6 +108,10 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut /// ITERATORS /// //////////////////////////////////////////////////////////////////////// +// iterator over the clauses +#define Cnf_CnfForClause( p, pBeg, pEnd, i ) \ + for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ ) + // iterator over leaves of the cut #define Cnf_CutForEachLeaf( p, pCut, pLeaf, i ) \ for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ ) @@ -142,7 +146,7 @@ extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, i extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); extern int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ); -extern void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ); +extern void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern int Cnf_ManMapForCnf( Cnf_Man_t * p ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 1e650a05..9059b9e5 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -470,7 +470,7 @@ int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) SeeAlso [] ***********************************************************************/ -void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ) +void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos ) { Aig_Obj_t * pObj; int * pVarToPol; @@ -478,8 +478,12 @@ void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ) // create map from the variable number to its polarity pVarToPol = CALLOC( int, pCnf->nVars ); Aig_ManForEachObj( pCnf->pMan, pObj, i ) - if ( !Aig_ObjIsPo(pObj) && pCnf->pVarNums[pObj->Id] >= 0 ) + { + if ( !fTransformPos && Aig_ObjIsPo(pObj) ) + continue; + if ( pCnf->pVarNums[pObj->Id] >= 0 ) pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase; + } // transform literals for ( i = 0; i < pCnf->nLiterals; i++ ) { diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 1354e841..b27addd4 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -54,7 +54,7 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ) /**Function************************************************************* - Synopsis [Reproduces script "compress2".] + Synopsis [Reproduces script "rwsat".] Description [] diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index e5940992..9046d574 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -55,7 +55,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); if ( fFlipBits ) - Cnf_DataTranformPolarity( pCnf ); + Cnf_DataTranformPolarity( pCnf, 0 ); // convert into SAT solver pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 1935bb7f..41f3ac59 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -530,7 +530,7 @@ p->timeTrav += clock() - clk2; pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); else pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); -// Cnf_DataTranformPolarity( pCnf ); +// Cnf_DataTranformPolarity( pCnf, 0 ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 3aafeb18..04adb7e3 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -389,11 +389,11 @@ PRT( "Time", clock() - clkTotal ); clk = clock(); if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 ) { - extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); + extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); int Depth; pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 1, 1, pParSec->fVeryVerbose, &Depth ); + RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 0, 0, 1, 1, pParSec->fVeryVerbose, &Depth ); if ( pParSec->fVerbose ) { if ( RetValue == 1 ) diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c index 29963f6d..bf196aea 100644 --- a/src/aig/hop/hopDfs.c +++ b/src/aig/hop/hopDfs.c @@ -394,7 +394,7 @@ Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, in /**Function************************************************************* - Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + Synopsis [Remaps the AIG (pRoot) to have the given support (uSupp).] Description [] @@ -417,7 +417,7 @@ void Hop_Remap_rec( Hop_Man_t * p, Hop_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + Synopsis [Remaps the AIG (pRoot) to have the given support (uSupp).] Description [] diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c index a7cd3e3c..d9f73c9d 100644 --- a/src/aig/mfx/mfxCore.c +++ b/src/aig/mfx/mfxCore.c @@ -205,7 +205,10 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib ) int nTotalNodesBeg = Nwk_ManNodeNum(pNtk); int nTotalEdgesBeg = Nwk_ManGetTotalFanins(pNtk); -// assert( Nwk_ManCheck( pNtk ) ); + // prepare the network for processing + Nwk_ManRemoveDupFanins( pNtk, 0 ); + assert( Nwk_ManCheck( pNtk ) ); + // check limits on the number of fanins nFaninMax = Nwk_ManGetFaninMax(pNtk); if ( pPars->fResub ) diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index f4d33cf1..79cd640a 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -803,6 +803,8 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan pNtk->pManTime = Tim_ManDup( pManTime, 0 ); else pNtk->pManTime = Tim_ManDup( p->pManTime, 0 ); +// Nwk_ManRemoveDupFanins( pNtk, 0 ); +// assert( Nwk_ManCheck( pNtk ) ); return pNtk; } diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h index 222130f3..603c1fb8 100644 --- a/src/aig/nwk/nwk.h +++ b/src/aig/nwk/nwk.h @@ -301,6 +301,7 @@ extern ABC_DLL void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileNa extern ABC_DLL void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk ); extern ABC_DLL void Nwk_ManCleanMarks( Nwk_Man_t * pNtk ); extern ABC_DLL void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ); +extern ABC_DLL void Nwk_ManRemoveDupFanins( Nwk_Man_t * pNtk, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/nwk/nwkCheck.c b/src/aig/nwk/nwkCheck.c index 6922e439..0890ced8 100644 --- a/src/aig/nwk/nwkCheck.c +++ b/src/aig/nwk/nwkCheck.c @@ -41,7 +41,7 @@ ***********************************************************************/ int Nwk_ManCheck( Nwk_Man_t * p ) { - Nwk_Obj_t * pObj; + Nwk_Obj_t * pObj, * pNext; int i, k, m; // check if the nodes have duplicated fanins Nwk_ManForEachNode( p, pObj, i ) @@ -51,7 +51,6 @@ int Nwk_ManCheck( Nwk_Man_t * p ) if ( pObj->pFanio[k] == pObj->pFanio[m] ) printf( "Node %d has duplicated fanin %d.\n", pObj->Id, pObj->pFanio[k]->Id ); } -/* // check if all nodes are in the correct fanin/fanout relationship Nwk_ManForEachObj( p, pObj, i ) { @@ -62,7 +61,6 @@ int Nwk_ManCheck( Nwk_Man_t * p ) if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 ) printf( "Nwk_ManCheck(): Object %d has fanout %d which does not have a corresponding fanin.\n", pObj->Id, pNext->Id ); } -*/ return 1; } diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c index 4068a1a5..56a13741 100644 --- a/src/aig/nwk/nwkFanio.c +++ b/src/aig/nwk/nwkFanio.c @@ -188,19 +188,25 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ) ***********************************************************************/ void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ) { - int i, k, Limit; + int i, k, Limit, fFound; // remove pFanin from the fanin list of pObj Limit = pObj->nFanins + pObj->nFanouts; + fFound = 0; for ( k = i = 0; i < Limit; i++ ) - if ( pObj->pFanio[i] != pFanin ) + if ( fFound || pObj->pFanio[i] != pFanin ) pObj->pFanio[k++] = pObj->pFanio[i]; + else + fFound = 1; assert( i == k + 1 ); // if it fails, likely because of duplicated fanin pObj->nFanins--; // remove pObj from the fanout list of pFanin Limit = pFanin->nFanins + pFanin->nFanouts; + fFound = 0; for ( k = i = pFanin->nFanins; i < Limit; i++ ) - if ( pFanin->pFanio[i] != pObj ) + if ( fFound || pFanin->pFanio[i] != pObj ) pFanin->pFanio[k++] = pFanin->pFanio[i]; + else + fFound = 1; assert( i == k + 1 ); // if it fails, likely because of duplicated fanout pFanin->nFanouts--; } diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c index d6daca4e..fccac175 100644 --- a/src/aig/nwk/nwkUtil.c +++ b/src/aig/nwk/nwkUtil.c @@ -477,37 +477,116 @@ void Nwk_ManCleanMarks( Nwk_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) +int Nwk_ManMinimumBaseNode( Nwk_Obj_t * pObj, Vec_Int_t * vTruth, int fVerbose ) { unsigned * pTruth; + Nwk_Obj_t * pFanin, * pObjNew; + Nwk_Man_t * pNtk = pObj->pMan; + int uSupp, nSuppSize, k, Counter = 0; + pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); + nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj)); + if ( nSuppSize == Nwk_ObjFaninNum(pObj) ) + return 0; + Counter++; + uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) ); + // create new node with the given support + pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) ); + Nwk_ObjForEachFanin( pObj, pFanin, k ) + if ( uSupp & (1 << k) ) + Nwk_ObjAddFanin( pObjNew, pFanin ); + pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) ); + if ( fVerbose ) + printf( "Reducing node %d fanins from %d to %d.\n", + pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) ); + Nwk_ObjReplace( pObj, pObjNew ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Minimizes the support of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) +{ Vec_Int_t * vTruth; - Nwk_Obj_t * pObj, * pFanin, * pObjNew; - int uSupp, nSuppSize, i, k, Counter = 0; + Nwk_Obj_t * pObj; + int i, Counter = 0; vTruth = Vec_IntAlloc( 1 << 16 ); Nwk_ManForEachNode( pNtk, pObj, i ) - { - pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); - nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj)); - if ( nSuppSize == Nwk_ObjFaninNum(pObj) ) - continue; - Counter++; - uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) ); - // create new node with the given support - pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) ); - Nwk_ObjForEachFanin( pObj, pFanin, k ) - if ( uSupp & (1 << k) ) - Nwk_ObjAddFanin( pObjNew, pFanin ); - pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) ); - if ( fVerbose ) - printf( "Reducing node %d fanins from %d to %d.\n", - pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) ); - Nwk_ObjReplace( pObj, pObjNew ); - } + Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose ); if ( fVerbose && Counter ) printf( "Support minimization reduced support of %d nodes.\n", Counter ); Vec_IntFree( vTruth ); } +/**Function************************************************************* + + Synopsis [Minimizes the support of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManRemoveDupFaninsNode( Nwk_Obj_t * pObj, int iFan0, int iFan1, Vec_Int_t * vTruth ) +{ + Hop_Man_t * pManHop = pObj->pMan->pManHop; +// Nwk_Obj_t * pFanin0 = pObj->pFanio[iFan0]; +// Nwk_Obj_t * pFanin1 = pObj->pFanio[iFan1]; + assert( pObj->pFanio[iFan0] == pObj->pFanio[iFan1] ); + pObj->pFunc = Hop_Compose( pManHop, pObj->pFunc, Hop_IthVar(pManHop,iFan0), iFan1 ); + Nwk_ManMinimumBaseNode( pObj, vTruth, 0 ); +} + +/**Function************************************************************* + + Synopsis [Minimizes the support of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManRemoveDupFanins( Nwk_Man_t * pNtk, int fVerbose ) +{ + Vec_Int_t * vTruth; + Nwk_Obj_t * pObj; + int i, k, m, fFound; + // check if the nodes have duplicated fanins + vTruth = Vec_IntAlloc( 1 << 16 ); + Nwk_ManForEachNode( pNtk, pObj, i ) + { + fFound = 0; + for ( k = 0; k < pObj->nFanins; k++ ) + { + for ( m = k + 1; m < pObj->nFanins; m++ ) + if ( pObj->pFanio[k] == pObj->pFanio[m] ) + { + if ( fVerbose ) + printf( "Removing duplicated fanins of node %d (fanins %d and %d).\n", + pObj->Id, pObj->pFanio[k]->Id, pObj->pFanio[m]->Id ); + Nwk_ManRemoveDupFaninsNode( pObj, k, m, vTruth ); + fFound = 1; + break; + } + if ( fFound ) + break; + } + } + Vec_IntFree( vTruth ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 5a7beeec..e2fbda2d 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -85,7 +85,7 @@ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); /*=== saigInter.c ==========================================================*/ -extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); +extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); /*=== saigMiter.c ==========================================================*/ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); /*=== saigPhase.c ==========================================================*/ diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index 86982d46..65fe6d87 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -67,7 +67,7 @@ struct Saig_IntMan_t_ }; #ifdef ABC_USE_LIBRARIES -static int Saig_M144pPerformOneStep( Saig_IntMan_t * p ); +static int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther ); #endif //////////////////////////////////////////////////////////////////////// @@ -896,7 +896,7 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p, int fSubtractOld ) SeeAlso [] ***********************************************************************/ -int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ) +int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ) { extern int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters ); Saig_IntMan_t * p; @@ -982,8 +982,8 @@ p->timeCnf += clock() - clk; // perform interplation clk = clock(); #ifdef ABC_USE_LIBRARIES - if ( fUseIp ) - RetValue = Saig_M144pPerformOneStep( p ); + if ( fUseMiniSat ) + RetValue = Saig_M144pPerformOneStep( p, fUsePudlak, fUseOther ); else #endif RetValue = Saig_PerformOneStep( p, 0 ); @@ -1177,7 +1177,10 @@ M114p_Solver_t Saig_M144pDeriveSatSolver( { Vec_IntPush( *pvMapRoots, 1 ); if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) - assert( 0 ); + { +// assert( 0 ); + break; + } } // return clauses to the original state Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); @@ -1200,20 +1203,149 @@ M114p_Solver_t Saig_M144pDeriveSatSolver( SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +void Saig_M144pInterpolateReport( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) { - Aig_Man_t * p; - Aig_Obj_t * pInter, * pInter2, * pVar; - Vec_Ptr_t * vInters; Vec_Int_t * vASteps; int * pLits, * pClauses, * pVars; int nLits, nVars, i, k, iVar, haveASteps; int CountA, CountB, CountC, CountCsaved; assert( M114p_SolverProofIsReady(s) ); - vInters = Vec_PtrAlloc( 1000 ); vASteps = Vec_IntAlloc( 1000 ); // process root clauses + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + { + } + else // clause of A + { + } + Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) ); + } +// assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + CountA = CountB = CountC = CountCsaved = 0; + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + haveASteps = Vec_IntEntry( vASteps, pClauses[0] ); + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] ); + if ( iVar == -1 ) // var of A + { + haveASteps = 1; + } + else // var of B or C + { + } + + if ( iVar == -1 ) + CountA++; + else if ( iVar == -2 ) + CountB++; + else + { + if ( haveASteps == 0 ) + CountCsaved++; + CountC++; + } + } + Vec_IntPush( vASteps, haveASteps ); + } + assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) ); + + printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", + CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC ); + Vec_IntFree( vASteps ); +} + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_M144pInterpolateLastStep( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, iVar; + int nSteps, iStepA, iStepB; + assert( M114p_SolverProofIsReady(s) ); + // process root clauses + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + { + } + else // clause of A + { + } + } +// assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) ); + // process learned clauses + nSteps = 0; + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + if ( iVar == -1 ) // var of A + { + iStepA = nSteps; + } + else if ( iVar == -2 ) // var of B + { + iStepB = nSteps; + } + else // var of C + { + } + nSteps++; + } + } +// assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) ); + if ( iStepA < iStepB ) + return iStepB; + return iStepA; +} + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, iVar; + assert( M114p_SolverProofIsReady(s) ); + vInters = Vec_PtrAlloc( 1000 ); + // process root clauses p = Aig_ManStart( 10000 ); M114p_SolverForEachRoot( s, &pLits, nLits, i ) { @@ -1232,50 +1364,306 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_ } } Vec_PtrPush( vInters, pInter ); - Vec_IntPush( vASteps, 0 ); } - assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); +// assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); // process learned clauses - CountA = CountB = CountC = CountCsaved = 0; M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) { pInter = Vec_PtrEntry( vInters, pClauses[0] ); - haveASteps = Vec_IntEntry( vASteps, pClauses[0] ); for ( k = 0; k < nVars; k++ ) { iVar = Vec_IntEntry( vMapVars, pVars[k] ); pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); - haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] ); if ( iVar == -1 ) // var of A - { - haveASteps = 1; pInter = Aig_Or( p, pInter, pInter2 ); - } else // var of B or C pInter = Aig_And( p, pInter, pInter2 ); + } + Vec_PtrPush( vInters, pInter ); + } + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + Vec_PtrFree( vInters ); + Aig_ObjCreatePo( p, pInter ); + Aig_ManCleanup( p ); + return p; +} - if ( iVar == -1 ) - CountA++; - else if ( iVar == -2 ) - CountB++; - else +/**Function************************************************************* + + Synopsis [Performs one resolution step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_M144pResolve( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar ) +{ + int i, k, iLit = -1, fFound = 0; + // find the variable in the clause + for ( i = 0; i < vResolvent->nSize; i++ ) + if ( lit_var(vResolvent->pArray[i]) == iVar ) + { + iLit = vResolvent->pArray[i]; + vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize]; + break; + } + assert( iLit != -1 ); + // add other variables + for ( i = 0; i < nLits; i++ ) + { + if ( lit_var(pLits[i]) == iVar ) + { + assert( iLit == lit_neg(pLits[i]) ); + fFound = 1; + continue; + } + // check if this literal appears + for ( k = 0; k < vResolvent->nSize; k++ ) + if ( vResolvent->pArray[k] == pLits[i] ) + break; + if ( k < vResolvent->nSize ) + continue; + // add this literal + Vec_IntPush( vResolvent, pLits[i] ); + } + assert( fFound ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_M144pInterpolatePudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + Vec_Int_t * vLiterals, * vClauses, * vResolvent; + int * pLitsNext, nLitsNext, nOffset, iLit; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, v, iVar; + assert( M114p_SolverProofIsReady(s) ); + vInters = Vec_PtrAlloc( 1000 ); + + vLiterals = Vec_IntAlloc( 10000 ); + vClauses = Vec_IntAlloc( 1000 ); + vResolvent = Vec_IntAlloc( 100 ); + + // create elementary variables + p = Aig_ManStart( 10000 ); + Vec_IntForEachEntry( vMapVars, iVar, i ) + if ( iVar >= 0 ) + Aig_IthVar(p, iVar); + // process root clauses + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + pInter = Aig_ManConst1(p); + else // clause of A + pInter = Aig_ManConst0(p); + Vec_PtrPush( vInters, pInter ); + + // save the root clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, nLits ); + for ( v = 0; v < nLits; v++ ) + Vec_IntPush( vLiterals, pLits[v] ); + } + assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + pInter = Vec_PtrEntry( vInters, pClauses[0] ); + + // initialize the resolvent + nOffset = Vec_IntEntry( vClauses, pClauses[0] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Vec_IntClear( vResolvent ); + for ( v = 0; v < nLitsNext; v++ ) + Vec_IntPush( vResolvent, pLitsNext[v] ); + + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + + // resolve it with the next clause + nOffset = Vec_IntEntry( vClauses, pClauses[k+1] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] ); + + if ( iVar == -1 ) // var of A + pInter = Aig_Or( p, pInter, pInter2 ); + else if ( iVar == -2 ) // var of B + pInter = Aig_And( p, pInter, pInter2 ); + else // var of C + { + // check polarity of the pivot variable in the clause + for ( v = 0; v < nLitsNext; v++ ) + if ( lit_var(pLitsNext[v]) == pVars[k] ) + break; + assert( v < nLitsNext ); + pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) ); + pInter = Aig_Mux( p, pVar, pInter, pInter2 ); + } + } + Vec_PtrPush( vInters, pInter ); + + // store the resulting clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) ); + Vec_IntForEachEntry( vResolvent, iLit, v ) + Vec_IntPush( vLiterals, iLit ); + } + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause + Vec_PtrFree( vInters ); + Vec_IntFree( vLiterals ); + Vec_IntFree( vClauses ); + Vec_IntFree( vResolvent ); + Aig_ObjCreatePo( p, pInter ); + Aig_ManCleanup( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_M144pInterpolatePudlakASteps( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + Vec_Int_t * vASteps; + Vec_Int_t * vLiterals, * vClauses, * vResolvent; + int * pLitsNext, nLitsNext, nOffset, iLit; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, v, iVar, haveASteps; + assert( M114p_SolverProofIsReady(s) ); + vInters = Vec_PtrAlloc( 1000 ); + vASteps = Vec_IntAlloc( 1000 ); + + vLiterals = Vec_IntAlloc( 10000 ); + vClauses = Vec_IntAlloc( 1000 ); + vResolvent = Vec_IntAlloc( 100 ); + + // create elementary variables + p = Aig_ManStart( 10000 ); + Vec_IntForEachEntry( vMapVars, iVar, i ) + if ( iVar >= 0 ) + Aig_IthVar(p, iVar); + // process root clauses + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + pInter = Aig_ManConst1(p); + else // clause of A + pInter = Aig_ManConst0(p); + Vec_PtrPush( vInters, pInter ); + Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) ); + + // save the root clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, nLits ); + for ( v = 0; v < nLits; v++ ) + Vec_IntPush( vLiterals, pLits[v] ); + } + assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + pInter = Vec_PtrEntry( vInters, pClauses[0] ); + haveASteps = Vec_IntEntry( vASteps, pClauses[0] ); + + // initialize the resolvent + nOffset = Vec_IntEntry( vClauses, pClauses[0] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Vec_IntClear( vResolvent ); + for ( v = 0; v < nLitsNext; v++ ) + Vec_IntPush( vResolvent, pLitsNext[v] ); + + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] ); + + // resolve it with the next clause + nOffset = Vec_IntEntry( vClauses, pClauses[k+1] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] ); + + if ( iVar == -1 ) // var of A + pInter = Aig_Or( p, pInter, pInter2 ), haveASteps = 1; + else if ( iVar == -2 ) // var of B + pInter = Aig_And( p, pInter, pInter2 ); + else // var of C { if ( haveASteps == 0 ) - CountCsaved++; - CountC++; + pInter = Aig_ManConst0(p); + else + { + // check polarity of the pivot variable in the clause + for ( v = 0; v < nLitsNext; v++ ) + if ( lit_var(pLitsNext[v]) == pVars[k] ) + break; + assert( v < nLitsNext ); + pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) ); + pInter = Aig_Mux( p, pVar, pInter, pInter2 ); + } } } Vec_PtrPush( vInters, pInter ); Vec_IntPush( vASteps, haveASteps ); - } -// printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", -// CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC ); + // store the resulting clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) ); + Vec_IntForEachEntry( vResolvent, iLit, v ) + Vec_IntPush( vLiterals, iLit ); + } assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause Vec_PtrFree( vInters ); Vec_IntFree( vASteps ); + Vec_IntFree( vLiterals ); + Vec_IntFree( vClauses ); + Vec_IntFree( vResolvent ); Aig_ObjCreatePo( p, pInter ); Aig_ManCleanup( p ); return p; @@ -1292,7 +1680,7 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_ SeeAlso [] ***********************************************************************/ -int Saig_M144pPerformOneStep( Saig_IntMan_t * p ) +int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther ) { M114p_Solver_t pSat; Vec_Int_t * vMapRoots, * vMapVars; @@ -1310,8 +1698,18 @@ p->timeSat += clock() - clk; if ( status == 0 ) { RetValue = 1; + + ///// report the savings of the modified Pudlak's approach + Saig_M144pInterpolateReport( pSat, vMapRoots, vMapVars ); + ///// + clk = clock(); - p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars ); + if ( fUseOther ) + p->pInterNew = Saig_M144pInterpolatePudlakASteps( pSat, vMapRoots, vMapVars ); + else if ( fUsePudlak ) + p->pInterNew = Saig_M144pInterpolatePudlak( pSat, vMapRoots, vMapVars ); + else + p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars ); p->timeInt += clock() - clk; } else if ( status == 1 ) |