Commit b09926e8 by Alan Mishchenko

SAT sweeping under constraints.

parent 17a0d944
...@@ -1097,6 +1097,7 @@ extern void Gia_ManInvertConstraints( Gia_Man_t * pAig ); ...@@ -1097,6 +1097,7 @@ extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
extern void Gia_ManInvertPos( Gia_Man_t * pAig ); extern void Gia_ManInvertPos( Gia_Man_t * pAig );
extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 ); extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p ); extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
extern void Gia_ManSwapPos( Gia_Man_t * p, int i );
/*=== giaCTas.c ===========================================================*/ /*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t; typedef struct Tas_Man_t_ Tas_Man_t;
......
...@@ -600,7 +600,7 @@ void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo ) ...@@ -600,7 +600,7 @@ void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo )
Gia_ManForEachObj1( pTwo, pObj, i ) Gia_ManForEachObj1( pTwo, pObj, i )
{ {
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjIsCi(pObj) ) else if ( Gia_ObjIsCi(pObj) )
pObj->Value = Gia_Obj2Lit( pNew, Gia_ManCi( pNew, Gia_ObjCioId(pObj) ) ); pObj->Value = Gia_Obj2Lit( pNew, Gia_ManCi( pNew, Gia_ObjCioId(pObj) ) );
else if ( Gia_ObjIsCo(pObj) ) else if ( Gia_ObjIsCo(pObj) )
......
...@@ -61,6 +61,7 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ) ...@@ -61,6 +61,7 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
Gia_ManForEachCo( p, pObj, i ) Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew->nConstrs = p->nConstrs;
assert( Gia_ManIsNormalized(pNew) ); assert( Gia_ManIsNormalized(pNew) );
Gia_ManDupRemapEquiv( pNew, p ); Gia_ManDupRemapEquiv( pNew, p );
return pNew; return pNew;
......
...@@ -1338,6 +1338,31 @@ void Gia_ManMarkFanoutDrivers( Gia_Man_t * p ) ...@@ -1338,6 +1338,31 @@ void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
else if ( Gia_ObjIsCo(pObj) ) else if ( Gia_ObjIsCo(pObj) )
Gia_ObjFanin0(pObj)->fMark0 = 1; Gia_ObjFanin0(pObj)->fMark0 = 1;
} }
/**Function*************************************************************
Synopsis [Swaps PO number 0 with PO number i.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManSwapPos( Gia_Man_t * p, int i )
{
int Lit0, LitI;
assert( i >= 0 && i < Gia_ManPoNum(p) );
if ( i == 0 )
return;
Lit0 = Gia_ObjFaninLit0p( p, Gia_ManPo(p, 0) );
LitI = Gia_ObjFaninLit0p( p, Gia_ManPo(p, i) );
Gia_ManPatchCoDriver( p, 0, LitI );
Gia_ManPatchCoDriver( p, i, Lit0 );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
...@@ -27148,7 +27148,7 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27148,7 +27148,7 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Ssc_Pars_t Pars, * pPars = &Pars; Ssc_Pars_t Pars, * pPars = &Pars;
Ssc_ManSetDefaultParams( pPars ); Ssc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "WCavh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -27174,6 +27174,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27174,6 +27174,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 ) if ( pPars->nBTLimit < 0 )
goto usage; goto usage;
break; break;
case 'a':
pPars->fAppend ^= 1;
break;
case 'v': case 'v':
pPars->fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
...@@ -27191,12 +27194,13 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -27191,12 +27194,13 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" ); Abc_Print( -2, "usage: &cfraig [-WC <num>] [-avh]\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping under constraints\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping under constraints\n" );
Abc_Print( -2, "\t which are present in the AIG or set manually using \"constr\"\n" ); Abc_Print( -2, "\t which are present in the AIG or set manually using \"constr\"\n" );
Abc_Print( -2, "\t (constraints are listed as last POs and true when they are 0)\n" ); Abc_Print( -2, "\t (constraints are listed as last POs and true when they are 0)\n" );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-a : toggle appending constraints to the result [default = %s]\n", pPars->fAppend? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
...@@ -31513,7 +31517,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -31513,7 +31517,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Unr_ManTest( Gia_Man_t * pGia ); // extern void Unr_ManTest( Gia_Man_t * pGia );
// extern void Mig_ManTest( Gia_Man_t * pGia ); // extern void Mig_ManTest( Gia_Man_t * pGia );
// extern int Gia_ManVerify( Gia_Man_t * pGia ); // extern int Gia_ManVerify( Gia_Man_t * pGia );
extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); // extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
...@@ -31565,7 +31570,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -31565,7 +31570,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Unr_ManTest( pAbc->pGia ); // Unr_ManTest( pAbc->pGia );
// Mig_ManTest( pAbc->pGia ); // Mig_ManTest( pAbc->pGia );
// Gia_ManVerifyWithBoxes( pAbc->pGia ); // Gia_ManVerifyWithBoxes( pAbc->pGia );
pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 ); // pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
pTemp = Gia_ManOptimizeRing( pAbc->pGia );
Abc_FrameUpdateGia( pAbc, pTemp ); Abc_FrameUpdateGia( pAbc, pTemp );
return 0; return 0;
usage: usage:
......
...@@ -888,6 +888,26 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry ) ...@@ -888,6 +888,26 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntDrop( Vec_Int_t * p, int i )
{
int k;
assert( i >= 0 && i < Vec_IntSize(p) );
p->nSize--;
for ( k = i; k < p->nSize; k++ )
p->pArray[k] = p->pArray[k+1];
}
/**Function*************************************************************
Synopsis [Interts entry at the index iHere. Shifts other entries.] Synopsis [Interts entry at the index iHere. Shifts other entries.]
Description [] Description []
......
...@@ -47,6 +47,7 @@ struct Ssc_Pars_t_ ...@@ -47,6 +47,7 @@ struct Ssc_Pars_t_
int nBTLimit; // conflict limit at a node int nBTLimit; // conflict limit at a node
int nSatVarMax; // the max number of SAT variables int nSatVarMax; // the max number of SAT variables
int nCallsRecycle; // calls to perform before recycling SAT solver int nCallsRecycle; // calls to perform before recycling SAT solver
int fAppend; // append constraints to the resulting AIG
int fVerbose; // verbose stats int fVerbose; // verbose stats
}; };
......
...@@ -313,6 +313,11 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) ...@@ -313,6 +313,11 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
pAig = Gia_ManDupLevelized( pResult = pAig ); pAig = Gia_ManDupLevelized( pResult = pAig );
Gia_ManStop( pResult ); Gia_ManStop( pResult );
pResult = Ssc_PerformSweeping( pAig, pCare, pPars ); pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
if ( pPars->fAppend )
{
Gia_ManDupAppendShare( pResult, pCare );
pResult->nConstrs = Gia_ManPoNum(pCare);
}
Gia_ManStop( pAig ); Gia_ManStop( pAig );
Gia_ManStop( pCare ); Gia_ManStop( pCare );
return pResult; return pResult;
......
...@@ -260,7 +260,7 @@ p->timeCnfGen += clock() - clk; ...@@ -260,7 +260,7 @@ p->timeCnfGen += clock() - clk;
***********************************************************************/ ***********************************************************************/
void Ssc_ManStartSolver( Ssc_Man_t * p ) void Ssc_ManStartSolver( Ssc_Man_t * p )
{ {
Aig_Man_t * pMan = Gia_ManToAig( p->pFraig, 0 ); Aig_Man_t * pMan = Gia_ManToAigSimple( p->pFraig );
Cnf_Dat_t * pDat = Cnf_Derive( pMan, 0 ); Cnf_Dat_t * pDat = Cnf_Derive( pMan, 0 );
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
sat_solver * pSat; sat_solver * pSat;
......
...@@ -19,6 +19,8 @@ ...@@ -19,6 +19,8 @@
***********************************************************************/ ***********************************************************************/
#include "sscInt.h" #include "sscInt.h"
#include "sat/cnf/cnf.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -42,6 +44,117 @@ ABC_NAMESPACE_IMPL_START ...@@ -42,6 +44,117 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Aig_Man_t * pMan = Gia_ManToAigSimple( p );
Cnf_Dat_t * pDat = Cnf_Derive( pMan, Gia_ManPoNum(p) );
Gia_Obj_t * pObj;
Vec_Int_t * vLits, * vKeep;
sat_solver * pSat;
int i, status, Count = 0;
Aig_ManStop( pMan );
vLits = Vec_IntAlloc( Gia_ManPoNum(p) );
Gia_ManForEachPo( p, pObj, i )
{
int iObj = Gia_ObjId( p, pObj );
Vec_IntPush( vLits, Abc_Var2Lit(pDat->pVarNums[iObj], 1) );
}
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pDat->nVars );
for ( i = 0; i < pDat->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, pDat->pClauses[i], pDat->pClauses[i+1] ) )
{
Cnf_DataFree( pDat );
sat_solver_delete( pSat );
Vec_IntFree( vLits );
return NULL;
}
}
status = sat_solver_simplify( pSat );
if ( status == 0 )
{
Cnf_DataFree( pDat );
sat_solver_delete( pSat );
Vec_IntFree( vLits );
return NULL;
}
// iterate over POs
vKeep = Vec_IntAlloc( Gia_ManPoNum(p) );
Gia_ManForEachPo( p, pObj, i )
{
Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits,i)) );
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits,i)) );
if ( status == l_False )
Vec_IntWriteEntry( vLits, i, Abc_Var2Lit(pDat->pVarNums[0], 0) ); // const1 SAT var is always true
else
{
assert( status = l_True );
Vec_IntPush( vKeep, i );
}
}
Cnf_DataFree( pDat );
sat_solver_delete( pSat );
Vec_IntFree( vLits );
if ( Vec_IntSize(vKeep) == Gia_ManPoNum(p) )
{
Vec_IntFree( vKeep );
return Gia_ManDup(p);
}
pNew = Gia_ManDupCones( p, Vec_IntArray(vKeep), Vec_IntSize(vKeep), 0 );
Vec_IntFree( vKeep );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p )
{
Ssc_Pars_t Pars, * pPars = &Pars;
Gia_Man_t * pTemp, * pAux;
int i;
assert( p->nConstrs == 0 );
printf( "User AIG: " );
Gia_ManPrintStats( p, 0, 0, 0 );
pTemp = Gia_ManDropContained( p );
printf( "Drop AIG: " );
Gia_ManPrintStats( pTemp, 0, 0, 0 );
// return pTemp;
if ( Gia_ManPoNum(pTemp) == 1 )
return pTemp;
Ssc_ManSetDefaultParams( pPars );
pPars->fAppend = 1;
pPars->fVerbose = 1;
pTemp->nConstrs = Gia_ManPoNum(pTemp) - 1;
for ( i = 0; i < Gia_ManPoNum(pTemp); i++ )
{
Gia_ManSwapPos( pTemp, i );
pTemp = Ssc_PerformSweepingConstr( pAux = pTemp, pPars );
Gia_ManStop( pAux );
pTemp = Gia_ManDupNormalize( pAux = pTemp );
Gia_ManStop( pAux );
Gia_ManSwapPos( pTemp, i );
printf( "AIG%3d : " );
Gia_ManPrintStats( pTemp, 0, 0, 0 );
}
return pTemp;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
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