From 2c96c8af36446d3b855e07d78975cfad50c2917c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 21 Jul 2008 08:01:00 -0700 Subject: Version abc80721 --- src/aig/aig/aig.h | 1 + src/aig/aig/aigDfs.c | 62 +++++ src/aig/aig/aigPartSat.c | 612 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/aig/module.make | 1 + src/aig/cnf/cnf.h | 6 +- src/aig/cnf/cnfMan.c | 8 +- src/aig/dar/darScript.c | 2 +- src/aig/fra/fraCec.c | 2 +- src/aig/fra/fraInd.c | 2 +- src/aig/fra/fraSec.c | 4 +- src/aig/hop/hopDfs.c | 4 +- src/aig/mfx/mfxCore.c | 5 +- src/aig/ntl/ntlExtract.c | 2 + src/aig/nwk/nwk.h | 1 + src/aig/nwk/nwkCheck.c | 4 +- src/aig/nwk/nwkFanio.c | 12 +- src/aig/nwk/nwkUtil.c | 121 ++++++++-- src/aig/saig/saig.h | 2 +- src/aig/saig/saigInter.c | 458 ++++++++++++++++++++++++++++++++--- src/base/abc/abcDfs.c | 2 +- src/base/abci/abc.c | 264 ++++++++++++++++++-- src/base/abci/abcDar.c | 35 ++- src/misc/vec/vecInt.h | 46 ++++ 23 files changed, 1563 insertions(+), 93 deletions(-) create mode 100644 src/aig/aig/aigPartSat.c (limited to 'src') 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 @@ -164,6 +164,68 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly ) return vNodes; } +/**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.] 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 (var of C), + where 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 (var of C), + where 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 (var of C), + where 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 (var of C), + where 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 ) diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index e83bd132..fec01ef7 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -549,7 +549,7 @@ Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll ) } // collect dangling nodes if asked to if ( fCollectAll ) - { + { Abc_NtkForEachNode( pNtk, pObj, i ) if ( !Abc_NodeIsTravIdCurrent(pObj) ) Abc_NtkDfs_iter( vStack, pObj, vNodes ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 264b1df4..b8a9cefe 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -200,6 +200,7 @@ static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -218,6 +219,7 @@ static int Abc_CommandAbc8Write ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8ReadLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8PrintLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8Check ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Pfan ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -458,6 +460,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "dprove", Abc_CommandDProve, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 ); @@ -473,6 +476,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC8", "*wlogic", Abc_CommandAbc8WriteLogic, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*rlut", Abc_CommandAbc8ReadLut, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*plut", Abc_CommandAbc8PrintLut, 0 ); + Cmd_CommandAdd( pAbc, "ABC8", "*check", Abc_CommandAbc8Check, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*ps", Abc_CommandAbc8Ps, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*pfan", Abc_CommandAbc8Pfan, 0 ); @@ -6357,7 +6361,7 @@ int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: topand [-h]\n" ); - fprintf( pErr, "\t AND-decomposition of single-output combinational miter\n" ); + fprintf( pErr, "\t performs AND-decomposition of single-output combinational miter\n" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\tname : the node name\n"); return 1; @@ -14196,7 +14200,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fPartition; int fMiter; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose ); extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -14850,14 +14854,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int RetValue; - int fFlipBits; + int fAlignPol; int fAndOuts; int fVerbose; int nConfLimit; int nInsLimit; int clk; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -14865,13 +14869,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fFlipBits = 0; + fAlignPol = 0; fAndOuts = 0; fVerbose = 0; nConfLimit = 100000; nInsLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIfavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF ) { switch ( c ) { @@ -14897,8 +14901,8 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nInsLimit < 0 ) goto usage; break; - case 'f': - fFlipBits ^= 1; + case 'p': + fAlignPol ^= 1; break; case 'a': fAndOuts ^= 1; @@ -14937,7 +14941,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } clk = clock(); - RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fFlipBits, fAndOuts, fVerbose ); + RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fAlignPol, fAndOuts, fVerbose ); // verify that the pattern is correct if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) { @@ -14970,13 +14974,177 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dsat [-C num] [-I num] [-favh]\n" ); + fprintf( pErr, "usage: dsat [-C num] [-I num] [-pavh]\n" ); fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit ); - fprintf( pErr, "\t-f : flip polarity of SAT variables [default = %s]\n", fFlipBits? "yes": "no" ); - fprintf( pErr, "\t-a : constrain each output of multi-output miter [default = %s]\n", fAndOuts? "yes": "no" ); + fprintf( pErr, "\t-p : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" ); + fprintf( pErr, "\t-a : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int RetValue; + int c, clk; + int nAlgo; + int nPartSize; + int nConfPart; + int nConfTotal; + int fAlignPol; + int fSynthesize; + int fVerbose; + + extern int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nAlgo = 0; + nPartSize = 10000; + nConfPart = 0; + nConfTotal = 1000000; + fAlignPol = 1; + fSynthesize = 0; + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "APCpsvh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + nAlgo = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nAlgo < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nPartSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPartSize < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfTotal = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfTotal < 0 ) + goto usage; + break; + case 'p': + fAlignPol ^= 1; + break; + case 's': + fSynthesize ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); + return 0; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + + clk = clock(); + RetValue = Abc_NtkPartitionedSat( pNtk, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose ); + // verify that the pattern is correct + if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) + { + //int i; + //Abc_Obj_t * pObj; + int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel ); + if ( pSimInfo[0] != 1 ) + printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" ); + free( pSimInfo ); + /* + // print model + Abc_NtkForEachPi( pNtk, pObj, i ) + { + printf( "%d", (int)(pNtk->pModel[i] > 0) ); + if ( i == 70 ) + break; + } + printf( "\n" ); + */ + } + + if ( RetValue == -1 ) + printf( "UNDECIDED " ); + else if ( RetValue == 0 ) + printf( "SATISFIABLE " ); + else + printf( "UNSATISFIABLE " ); + //printf( "\n" ); + PRT( "Time", clock() - clk ); + return 0; + +usage: + fprintf( pErr, "usage: psat [-APC num] [-psvh]\n" ); + fprintf( pErr, "\t solves the combinational miter using partitioning\n" ); + fprintf( pErr, "\t (derives CNF from the current network and leave it unchanged)\n" ); + fprintf( pErr, "\t for multi-output miters, tries to prove that the AND of POs is always 0\n" ); + fprintf( pErr, "\t (if POs should be ORed instead of ANDed, use command \"orpos\")\n" ); + fprintf( pErr, "\t-A num : partitioning algorithm [default = %d]\n", nAlgo ); + fprintf( pErr, "\t 0 : no partitioning\n" ); + fprintf( pErr, "\t 1 : partitioning by level\n" ); + fprintf( pErr, "\t 2 : DFS post-order\n" ); + fprintf( pErr, "\t 3 : DFS pre-order\n" ); + fprintf( pErr, "\t 4 : bit-slicing\n" ); + fprintf( pErr, "\t partitions are ordered by level (high level first)\n" ); + fprintf( pErr, "\t-P num : limit on the partition size [default = %d]\n", nPartSize ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfTotal ); + fprintf( pErr, "\t-p : align polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" ); + fprintf( pErr, "\t-s : apply logic synthesis to each partition [default = %s]\n", fSynthesize? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -15347,11 +15515,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) int fRewrite; int fTransLoop; int fUsePudlak; + int fUseOther; + int fUseMiniSat; int fCheckInd; int fCheckKstep; int fVerbose; - extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose ); + extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -15363,11 +15533,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fRewrite = 0; fTransLoop = 1; fUsePudlak = 0; + fUseOther = 0; + fUseMiniSat= 0; fCheckInd = 0; fCheckKstep= 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpikvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF ) { switch ( c ) { @@ -15402,6 +15574,12 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': fUsePudlak ^= 1; break; + case 'o': + fUseOther ^= 1; + break; + case 'm': + fUseMiniSat ^= 1; + break; case 'i': fCheckInd ^= 1; break; @@ -15437,18 +15615,19 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" ); return 0; } - Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose ); + Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose ); return 0; usage: - fprintf( pErr, "usage: int [-CF num] [-rtpikvh]\n" ); + fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" ); fprintf( pErr, "\t uses interpolation to prove the property\n" ); fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" ); -// fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); - fprintf( pErr, "\t-p : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUsePudlak? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); + fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" ); + fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" ); fprintf( pErr, "\t-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" ); fprintf( pErr, "\t-k : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -16364,6 +16543,55 @@ usage: return 1; /* error exit */ } +/**Function************************************************************* + + Synopsis [Command procedure to read LUT libraries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc8Check( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + int c; + extern int Nwk_ManCheck( void * p ); + + // set the defaults + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) + { + switch (c) + { + case 'h': + goto usage; + break; + default: + goto usage; + } + } + + if ( argc != globalUtilOptind ) + { + goto usage; + } + + // set the new network + if ( pAbc->pAbc8Nwk == NULL ) + printf( "Abc_CommandAbc8Check(): There is no mapped network.\n" ); + else + Nwk_ManCheck( pAbc->pAbc8Nwk ); + return 0; + +usage: + fprintf( stdout, "\nusage: *check [-h]\n"); + fprintf( stdout, "\t checks if the current mapped network has duplicated fanins\n" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; /* error exit */ +} + /**Function************************************************************* diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index e32dbce0..03790c4b 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -954,7 +954,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) // derive CNF pCnf = Cnf_Derive( pMan, 0 ); - Cnf_DataTranformPolarity( pCnf ); + Cnf_DataTranformPolarity( pCnf, 0 ); /* // write the network for verification pManCnf = Cnf_ManRead(); @@ -983,7 +983,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) +int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose ) { Aig_Man_t * pMan; int RetValue;//, clk = clock(); @@ -991,7 +991,32 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFli assert( Abc_NtkLatchNum(pNtk) == 0 ); assert( Abc_NtkPoNum(pNtk) == 1 ); pMan = Abc_NtkToDar( pNtk, 0, 0 ); - RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fFlipBits, fAndOuts, fVerbose ); + RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fVerbose ); + pNtk->pModel = pMan->pData, pMan->pData = NULL; + Aig_ManStop( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Solves combinational miter using a SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose ) +{ + extern int Aig_ManPartitionedSat( Aig_Man_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose ); + Aig_Man_t * pMan; + int RetValue;//, clk = clock(); + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + pMan = Abc_NtkToDar( pNtk, 0, 0 ); + RetValue = Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose ); pNtk->pModel = pMan->pData, pMan->pData = NULL; Aig_ManStop( pMan ); return RetValue; @@ -1270,7 +1295,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose ) { Aig_Man_t * pMan; int RetValue, Depth, clk = clock(); @@ -1282,7 +1307,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR return -1; } assert( pMan->nRegs > 0 ); - RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose, &Depth ); + RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 430b7b63..f20c7cc8 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -656,6 +656,52 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry ) return 1; } +/**Function************************************************************* + + Synopsis [Find entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntFindMax( Vec_Int_t * p ) +{ + int i, Best; + if ( p->nSize == 0 ) + return 0; + Best = p->pArray[0]; + for ( i = 1; i < p->nSize; i++ ) + if ( Best < p->pArray[i] ) + Best = p->pArray[i]; + return Best; +} + +/**Function************************************************************* + + Synopsis [Find entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntFindMin( Vec_Int_t * p ) +{ + int i, Best; + if ( p->nSize == 0 ) + return 0; + Best = p->pArray[0]; + for ( i = 1; i < p->nSize; i++ ) + if ( Best > p->pArray[i] ) + Best = p->pArray[i]; + return Best; +} + /**Function************************************************************* Synopsis [Comparison procedure for two integers.] -- cgit v1.2.3