Skip to content

A
abc
Commit 2c96c8af by Alan Mishchenko
Options

Version abc80721

parent de978ced
Showing with 1567 additions and 93 deletions
abc.dsp
......@@ -2902,6 +2902,10 @@ SOURCE=.\src\aig\aig\aigPartReg.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigPartSat.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigRepr.c
# End Source File
# Begin Source File
......
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 );
......
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 []
......
src/aig/aig/aigPartSat.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
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 \
......
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 );
......
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++ )
{
......
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 []
......
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 );
......
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 );
......
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 )
......
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 []
......
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 )
......
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;
}
......
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
}
......
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;
}
......
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--;
}
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ==========================================================*/
......
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 )
......
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 );
......
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*************************************************************
......
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 )
......
src/misc/vec/vecInt.h
......@@ -658,6 +658,52 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
/**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.]
Description []
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment