summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaNf.c106
-rw-r--r--src/aig/gia/giaSatMap.c163
-rw-r--r--src/base/abci/abc.c2
3 files changed, 176 insertions, 95 deletions
diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c
index 29f8679c..510e7ddb 100644
--- a/src/aig/gia/giaNf.c
+++ b/src/aig/gia/giaNf.c
@@ -1895,7 +1895,8 @@ void Nf_ManResetMatches( Nf_Man_t * p, int Round )
else
{
assert( Round > 0 || (!pDc->fBest && !pAc->fBest) );
- if ( (p->pPars->fAreaOnly || (Round & 1)) && !pAc->fCompl )
+// if ( (p->pPars->fAreaOnly || (Round & 1)) && !pAc->fCompl )
+ if ( (Round & 1) && !pAc->fCompl )
ABC_SWAP( Nf_Mat_t, *pDc, *pAc );
pDc->fBest = 1;
pAc->fBest = 0;
@@ -2185,38 +2186,59 @@ void Nf_ManUpdateStats( Nf_Man_t * p )
Vec_Int_t * vCutGates; // gates (cut -> gate)
*/
-int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, int StartVar )
+int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, Vec_Wrd_t * vCutAreas, word * pInvArea, int StartVar, int nVars )
{
Nf_Man_t * p = (Nf_Man_t *)pMan;
int nInputs = Gia_ManCiNum(p->pGia);
+ int LitShift = 2*nInputs+2;
Gia_Obj_t * pObj;
int c, iObj;
- Vec_Int_t * vInvCuts = Vec_IntAlloc( Gia_ManAndNum(p->pGia) );
+ if ( 2*Gia_ManAndNum(p->pGia) + Gia_ManCiNum(p->pGia) > nVars )
+ {
+ printf( "The number of variables is too large: 2*%d + %d = %d > %d.\n", Gia_ManAndNum(p->pGia), Gia_ManCiNum(p->pGia), 2*Gia_ManAndNum(p->pGia) + Gia_ManCiNum(p->pGia), nVars );
+ return 0;
+ }
+ *pInvArea = p->InvAreaW;
// save roots
Vec_IntClear( vRoots );
Gia_ManForEachCo( p->pGia, pObj, c )
- Vec_IntPush( vRoots, Gia_ObjFaninLit0p(p->pGia, pObj)-2*nInputs-2 );
+ {
+ assert( !Gia_ObjIsCi(Gia_ObjFanin0(pObj)) );
+ Vec_IntPush( vRoots, Gia_ObjFaninLit0p(p->pGia, pObj)-LitShift );
+ }
// prepare
Vec_WecClear( vCuts );
Vec_WecClear( vObjCuts );
Vec_IntClear( vSolCuts );
Vec_IntClear( vCutGates );
+ Vec_WrdClear( vCutAreas );
// collect cuts for each node
Gia_ManForEachAndId( p->pGia, iObj )
{
- Vec_Int_t * vObj[2], * vCut;
+ Vec_Int_t * vObj[2], * vCutOne;
int iCut, * pCut, * pCutSet;
int iCutInv[2] = {-1, -1};
// get matches
- Nf_Mat_t * pM[2];
+ Nf_Mat_t * pM[2] = {NULL, NULL};
for ( c = 0; c < 2; c++ )
- pM[c] = Nf_ObjMapRefNum(p, iObj, c) ? Nf_ObjMatchBest(p, iObj, c) : NULL;
+ {
+ if ( Nf_ObjMapRefNum(p, iObj, c) == 0 )
+ continue;
+ if ( Nf_ObjMatchBest(p, iObj, c)->fCompl )
+ {
+ assert( iCutInv[c] == -1 );
+ iCutInv[c] = Vec_IntSize(vSolCuts);
+ Vec_IntPush( vSolCuts, -1 );
+ continue;
+ }
+ pM[c] = Nf_ObjMatchBest(p, iObj, c);
+ }
// start collecting cuts of pos-obj and neg-obj
- assert( Vec_WecSize(vObjCuts) == 2*(iObj-nInputs-1) );
+ assert( Vec_WecSize(vObjCuts) == 2*iObj-LitShift );
for ( c = 0; c < 2; c++ )
{
vObj[c] = Vec_WecPushLevel( vObjCuts );
- Vec_IntPush( vObj[c], Abc_Var2Lit(Abc_Var2Lit(iObj-nInputs-1, c), 1) );
+ Vec_IntPush( vObj[c], Abc_Var2Lit(Abc_Var2Lit(iObj, c)-LitShift, 1) );
}
// enumerate cuts
pCutSet = Nf_ObjCutSet( p, iObj );
@@ -2239,6 +2261,7 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec
Mio_Cell2_t*pC = Nf_ManCell( p, Info );
assert( nFans == (int)pC->nFanins );
Vec_IntPush( vCutGates, Info );
+ Vec_WrdPush( vCutAreas, pC->AreaW );
// to make comparison possible
Cfg.fCompl = 0;
// add solution cut
@@ -2246,31 +2269,26 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec
{
if ( pM[c] == NULL )
continue;
- if ( pM[c]->fCompl )
- {
- assert( iCutInv[c] == -1 );
- iCutInv[c] = Vec_IntSize(vSolCuts);
- Vec_IntPush( vSolCuts, -1 );
- printf( "adding inv for %d\n", Abc_Var2Lit(iObj-nInputs-1, c) );
- }
- else if ( (int)pM[c]->CutH == Nf_CutHandle(pCutSet, pCut) && (int)pM[c]->Gate == Info && Nf_Cfg2Int(pM[c]->Cfg) == Nf_Cfg2Int(Cfg) )
+ if ( (int)pM[c]->CutH == Nf_CutHandle(pCutSet, pCut) && (int)pM[c]->Gate == Info && Nf_Cfg2Int(pM[c]->Cfg) == Nf_Cfg2Int(Cfg) )
{
Vec_IntPush( vSolCuts, Vec_WecSize(vCuts) );
- printf( "adding solution for %d\n", Abc_Var2Lit(iObj-nInputs-1, c) );
+ //printf( "adding solution for %d\n", Abc_Var2Lit(iObj, c)-LitShift );
}
}
// add new cut
iCutLit = Abc_Var2Lit( StartVar + Vec_WecSize(vCuts), 0 );
- vCut = Vec_WecPushLevel( vCuts );
+ vCutOne = Vec_WecPushLevel( vCuts );
// add literals
- Vec_IntPush( vCut, Abc_Var2Lit(iObj, fCompl) );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, fCompl) );
Vec_IntPush( vObj[fCompl], iCutLit );
Nf_CfgForEachVarCompl( Cfg, nFans, iFanin, fComplF, k )
- if ( pFans[iFanin] >= nInputs + 1 ) // and-node
+ if ( pFans[iFanin] >= nInputs + 1 ) // internal node
{
- Vec_IntPush( vCut, Abc_Var2Lit(pFans[iFanin], fComplF) );
- Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(pFans[iFanin]-nInputs-1, fComplF)), iCutLit );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(pFans[iFanin], fComplF) );
+ //Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(pFans[iFanin], fComplF)-LitShift), iCutLit );
}
+ else if ( fComplF ) // complemented primary input
+ Vec_IntPush( vCutOne, Abc_Var2Lit(pFans[iFanin], 1) );
}
}
}
@@ -2280,29 +2298,27 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec
{
if ( iCutInv[c] != -1 )
Vec_IntWriteEntry( vSolCuts, iCutInv[c], Vec_WecSize(vCuts) );
- Vec_IntPush( vInvCuts, Abc_Var2Lit(StartVar + Vec_WecSize(vCuts), 0) );
- vCut = Vec_WecPushLevel( vCuts );
- Vec_IntPush( vCut, Abc_Var2Lit(iObj, c) );
- Vec_IntPush( vCut, Abc_Var2Lit(iObj, !c) );
+ // the obj-lit implies its cut
+ Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj, c)-LitShift), Abc_Var2Lit(StartVar + Vec_WecSize(vCuts), 0) );
+ // the cut includes both literals
+ vCutOne = Vec_WecPushLevel( vCuts );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, c) );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, !c) );
Vec_IntPush( vCutGates, 3 );
+ Vec_WrdPush( vCutAreas, p->InvAreaW );
}
}
- assert( Vec_WecSize(vObjCuts) == Vec_IntSize(vInvCuts) );
- Gia_ManForEachAndId( p->pGia, iObj )
- {
- int iCutInv[2];
- for ( c = 0; c < 2; c++ )
- iCutInv[c] = Vec_IntEntry(vInvCuts, Abc_Var2Lit(iObj-nInputs-1, c));
- for ( c = 0; c < 2; c++ )
- {
- Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj-nInputs-1, c)), iCutInv[0] );
- Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj-nInputs-1, c)), iCutInv[1] );
- }
- }
- Vec_IntFree( vInvCuts );
+// for ( c = 0; c < p->nCells; c++ )
+// printf( "%d=%s ", c, p->pCells[c].pName );
+// printf( "\n" );
+ // add complemented inputs
+ Gia_ManForEachCiId( p->pGia, iObj, c )
+ if ( Nf_ObjMapRefNum(p, iObj, 1) )
+ Vec_IntPush( vSolCuts, -(2*Gia_ManAndNum(p->pGia)+c) );
assert( Vec_WecSize(vCuts) == Vec_IntSize(vCutGates) );
+ assert( Vec_WecSize(vCuts) == Vec_WrdSize(vCutAreas) );
assert( Vec_WecSize(vObjCuts) == 2*Gia_ManAndNum(p->pGia) );
- return 2*nInputs+2;
+ return nInputs;
}
/**Function*************************************************************
@@ -2390,13 +2406,11 @@ Gia_Man_t * Nf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
}
Nf_ManFixPoDrivers( p );
pNew = Nf_ManDeriveMapping( p );
-
- // experimental mapper
+ if ( pPars->fAreaOnly )
{
-// extern int Sbm_ManTestSat( void * p );
-// Sbm_ManTestSat( p );
+ int Sbm_ManTestSat( void * pMan );
+ Sbm_ManTestSat( p );
}
-
Nf_StoDelete( p );
return pNew;
}
diff --git a/src/aig/gia/giaSatMap.c b/src/aig/gia/giaSatMap.c
index 377ce772..db04aa1c 100644
--- a/src/aig/gia/giaSatMap.c
+++ b/src/aig/gia/giaSatMap.c
@@ -21,6 +21,8 @@
#include "gia.h"
#include "sat/bsat/satStore.h"
#include "misc/vec/vecWec.h"
+#include "misc/util/utilNam.h"
+#include "map/scl/sclCon.h"
ABC_NAMESPACE_IMPL_START
@@ -39,12 +41,14 @@ struct Sbm_Man_t_
int LogN; // max vars
int FirstVar; // first variable to be used
int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
+ int nInputs; // the number of inputs
// window
Vec_Int_t * vRoots; // output drivers to be mapped (root -> lit)
Vec_Wec_t * vCuts; // cuts (cut -> node lit + fanin lits)
Vec_Wec_t * vObjCuts; // cuts (obj -> node lit + cut lits)
Vec_Int_t * vSolCuts; // current solution (index -> cut)
Vec_Int_t * vCutGates; // gates (cut -> gate)
+ Vec_Wrd_t * vCutAreas; // area of each cut
// solver
Vec_Int_t * vAssump; // assumptions (root nodes)
Vec_Int_t * vPolar; // polarity of nodes and cuts
@@ -86,12 +90,17 @@ int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol )
Vec_Int_t * vCut;
// clear polarity and assumptions
Vec_IntClear( p->vPolar );
- Vec_IntClear( p->vAssump );
- Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, K), 1) );
// mark used literals
- Vec_IntFill( p->vLit2Used, Vec_WecSize(p->vObjCuts), 0 );
+ Vec_IntFill( p->vLit2Used, Vec_WecSize(p->vObjCuts) + p->nInputs, 0 );
Vec_IntForEachEntry( p->vSolCuts, Cut, i )
{
+ if ( Cut < 0 ) // input inverter variable
+ {
+ Vec_IntWriteEntry( p->vLit2Used, -Cut, 1 );
+ Vec_IntPush( p->vPolar, -Cut );
+ continue;
+ }
+ Vec_IntPush( p->vPolar, p->FirstVar + Cut );
vCut = Vec_WecEntry( p->vCuts, Cut );
Lit = Vec_IntEntry( vCut, 0 ) - p->LitShift; // obj literal
if ( Vec_IntEntry(p->vLit2Used, Lit) )
@@ -104,15 +113,21 @@ int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol )
{
if ( Vec_IntEntry(p->vLit2Used, Lit) == 0 )
printf( "Output literal %d has no cut.\n", Lit ), RetValue = 0;
- // create assumption
- Vec_IntPush( p->vAssump, Abc_Var2Lit(Lit, 0) );
}
// check internal nodes
Vec_IntForEachEntry( p->vSolCuts, Cut, i )
{
+ if ( Cut < 0 )
+ continue;
vCut = Vec_WecEntry( p->vCuts, Cut );
Vec_IntForEachEntryStart( vCut, Lit, j, 1 )
- if ( Vec_IntEntry(p->vLit2Used, Lit - p->LitShift) == 0 )
+ if ( Lit - p->LitShift < 0 )
+ {
+ assert( Abc_LitIsCompl(Lit) );
+ if ( Vec_IntEntry(p->vLit2Used, Vec_WecSize(p->vObjCuts) + Abc_Lit2Var(Lit)-1) == 0 )
+ printf( "Inverter of input %d of cut %d is not mapped.\n", Abc_Lit2Var(Lit)-1, Cut ), RetValue = 0;
+ }
+ else if ( Vec_IntEntry(p->vLit2Used, Lit - p->LitShift) == 0 )
printf( "Internal literal %d of cut %d is not mapped.\n", Lit - p->LitShift, Cut ), RetValue = 0;
// create polarity
Vec_IntPush( p->vPolar, p->FirstVar + Cut ); // cut variable
@@ -134,7 +149,7 @@ int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol )
int Sbm_ManCreateCnf( Sbm_Man_t * p )
{
int i, k, Lit, Lits[2], value;
- Vec_Int_t * vLits;
+ Vec_Int_t * vLits, * vCutOne, * vLitsPrev;
// sat_solver_rollback( p->Sat );
if ( !Sbm_ManCheckSol(p, p->vSolCuts) )
return 0;
@@ -142,11 +157,13 @@ int Sbm_ManCreateCnf( Sbm_Man_t * p )
assert( p->FirstVar == sat_solver_nvars(p->pSat) );
sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WecSize(p->vCuts) );
// iterate over arrays containing obj-lit cuts (neg-obj-lit cut-lits followed by pos-obj-lit cut-lits)
+ vLitsPrev = NULL;
Vec_WecForEachLevel( p->vObjCuts, vLits, i )
{
assert( Vec_IntSize(vLits) >= 2 );
value = sat_solver_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
assert( value );
+/*
// for each cut, add implied nodes
Lits[0] = Abc_LitNot( Vec_IntEntry(vLits, 0) );
assert( Lits[0] < 2*p->FirstVar );
@@ -158,17 +175,38 @@ int Sbm_ManCreateCnf( Sbm_Man_t * p )
assert( value );
//printf( "Adding clause %d + %d.\n", Lits[0], Lits[1]-2*p->FirstVar );
}
+*/
//printf( "\n" );
// create invertor exclusivity clause
if ( i & 1 )
{
- Lits[0] = Abc_LitNot( Vec_IntEntry(vLits, Vec_IntSize(vLits)-1) );
- Lits[1] = Abc_LitNot( Vec_IntEntry(vLits, Vec_IntSize(vLits)-2) );
+ Lits[0] = Abc_LitNot( Vec_IntEntryLast(vLits) );
+ Lits[1] = Abc_LitNot( Vec_IntEntryLast(vLitsPrev) );
value = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
assert( value );
//printf( "Adding exclusivity clause %d + %d.\n", Lits[0]-2*p->FirstVar, Lits[1]-2*p->FirstVar );
}
+ vLitsPrev = vLits;
}
+ // add inverters
+ Vec_WecForEachLevel( p->vCuts, vCutOne, i )
+ Vec_IntForEachEntry( vCutOne, Lit, k )
+ if ( Abc_Lit2Var(Lit)-1 < p->nInputs ) // input
+ {
+ assert( k > 0 );
+ Lits[0] = Abc_Var2Lit( Vec_WecSize(p->vObjCuts) + Abc_Lit2Var(Lit)-1, 0 );
+ Lits[1] = Abc_Var2Lit( p->FirstVar + i, 1 );
+ value = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
+ assert( value );
+ }
+ else // internal node
+ {
+ Lits[0] = Abc_Var2Lit( Lit-p->LitShift, 0 );
+ Lits[1] = Abc_Var2Lit( p->FirstVar + i, 1 );
+ value = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
+ assert( value );
+ }
+
sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolar), Vec_IntSize(p->vPolar) );
return 1;
}
@@ -312,15 +350,6 @@ sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars )
void Sbm_AddCardinConstrTest()
{
-/*
- int Lit, LogN = 3, nVars = 1 << LogN, K = 2, Count = 1;
- int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1), nVarsReal;
- Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
- sat_solver * pSat = sat_solver_new();
- sat_solver_setnvars( pSat, nVarsAlloc );
- nVarsReal = Sbm_AddCardinConstrPairWise( pSat, vVars, 2 );
- assert( nVarsReal == nVarsAlloc );
-*/
int LogN = 3, nVars = 1 << LogN, K = 2, Count = 1;
Vec_Int_t * vVars, * vLits = Vec_IntAlloc( nVars );
sat_solver * pSat = Sbm_AddCardinSolver( LogN, &vVars );
@@ -328,7 +357,6 @@ void Sbm_AddCardinConstrTest()
int Lit = Abc_Var2Lit( Vec_IntEntry(vVars, K), 1 );
printf( "LogN = %d. N = %3d. Vars = %5d. Clauses = %6d. Comb = %d.\n", LogN, nVars, nVarsReal, sat_solver_nclauses(pSat), nVars * (nVars-1)/2 + nVars + 1 );
-
while ( 1 )
{
int i, status = sat_solver_solve( pSat, &Lit, &Lit+1, 0, 0, 0, 0 );
@@ -375,6 +403,7 @@ Sbm_Man_t * Sbm_ManAlloc( int LogN )
p->vObjCuts = Vec_WecAlloc( 1000 );
p->vSolCuts = Vec_IntAlloc( 100 );
p->vCutGates = Vec_IntAlloc( 100 );
+ p->vCutAreas = Vec_WrdAlloc( 100 );
// solver
p->vAssump = Vec_IntAlloc( 100 );
p->vPolar = Vec_IntAlloc( 100 );
@@ -398,6 +427,7 @@ void Sbm_ManStop( Sbm_Man_t * p )
Vec_WecFree( p->vObjCuts );
Vec_IntFree( p->vSolCuts );
Vec_IntFree( p->vCutGates );
+ Vec_WrdFree( p->vCutAreas );
// internal
Vec_IntFree( p->vAssump );
Vec_IntFree( p->vPolar );
@@ -408,24 +438,32 @@ void Sbm_ManStop( Sbm_Man_t * p )
Vec_IntFree( p->vLit2Used );
Vec_IntFree( p->vDelays );
Vec_IntFree( p->vReason );
+ ABC_FREE( p );
}
int Sbm_ManTestSat( void * pMan )
{
abctime clk = Abc_Clock(), clk2;
- int i, LogN = 4, nVars = 1 << LogN, status, Root;
+ int i, k, Lit, LogN = 7, nVars = 1 << LogN, status, Root;
Sbm_Man_t * p = Sbm_ManAlloc( LogN );
+ word InvArea = 0;
+ int fKeepTrying = 1;
+ int StartSol;
// derive window
- extern int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, int StartVar );
- p->LitShift = Nf_ManExtractWindow( pMan, p->vRoots, p->vCuts, p->vObjCuts, p->vSolCuts, p->vCutGates, p->FirstVar );
- assert( Vec_WecSize(p->vObjCuts) <= nVars );
+ extern int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, Vec_Wrd_t * vCutAreas, word * pInvArea, int StartVar, int nVars );
+ p->nInputs = Nf_ManExtractWindow( pMan, p->vRoots, p->vCuts, p->vObjCuts, p->vSolCuts, p->vCutGates, p->vCutAreas, &InvArea, p->FirstVar, nVars );
+ p->LitShift = 2*p->nInputs+2;
+ assert( Vec_WecSize(p->vObjCuts) + p->nInputs <= nVars );
// print-out
// Vec_WecPrint( p->vCuts, 0 );
// printf( "\n" );
- Vec_WecPrint( p->vObjCuts, 0 );
- printf( "\n" );
+// Vec_WecPrint( p->vObjCuts, 0 );
+// printf( "\n" );
Vec_IntPrint( p->vSolCuts );
+ printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n",
+ sat_solver_nclauses(p->pSat), Vec_WecSize(p->vObjCuts), Vec_WecSizeSize(p->vCuts),
+ sat_solver_nclauses(p->pSat) - Vec_WecSize(p->vObjCuts) - Vec_WecSizeSize(p->vCuts) );
// creating CNF
if ( !Sbm_ManCreateCnf(p) )
@@ -434,39 +472,68 @@ int Sbm_ManTestSat( void * pMan )
// create assumptions
// cardinality
Vec_IntClear( p->vAssump );
-// for ( i = 0; i < Vec_IntSize(p->vSolCuts); i++ )
-// Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
- Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, Vec_IntSize(p->vSolCuts)), 1) );
+ Vec_IntPush( p->vAssump, -1 );
// unused variables
- for ( i = Vec_WecSize(p->vObjCuts); i < nVars; i++ )
+ for ( i = Vec_WecSize(p->vObjCuts) + p->nInputs; i < nVars; i++ )
Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
// root variables
Vec_IntForEachEntry( p->vRoots, Root, i )
Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
// Vec_IntPrint( p->vAssump );
- // solve the problem
- clk2 = Abc_Clock();
- status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 );
- if ( status == l_False )
- printf( "UNSAT " );
- else if ( status == l_True )
- printf( "SAT " );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
-
- if ( status == l_True )
+ StartSol = Vec_IntSize(p->vSolCuts);
+// StartSol = 30;
+ while ( fKeepTrying )
{
- for ( i = 0; i < nVars; i++ )
- printf( "%d", sat_solver_var_value(p->pSat, i) );
- printf( "\n" );
- for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
- printf( "%d ", sat_solver_var_value(p->pSat, i) );
- printf( "\n" );
- for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
- printf( "%d=%d ", i-p->FirstVar, sat_solver_var_value(p->pSat, i) );
+ printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
+ // for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )
+ // Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
+ Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
+ // solve the problem
+ clk2 = Abc_Clock();
+ status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 );
+ if ( status == l_True )
+ {
+ word AreaNew = 0;
+ int Count = 0;
+ printf( "AND Lits = %d. Inputs = %d. Vars = %d. All vars = %d.\n", Vec_WecSize(p->vObjCuts), p->nInputs, Vec_WecSize(p->vObjCuts) + p->nInputs, nVars );
+// for ( i = 0; i < nVars; i++ )
+// printf( "%d", sat_solver_var_value(p->pSat, i) );
+// printf( "\n" );
+ for ( i = 0; i < nVars; i++ )
+ if ( sat_solver_var_value(p->pSat, i) )
+ {
+ printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
+ Count++;
+ if ( i >= Vec_WecSize(p->vObjCuts) )
+ AreaNew += InvArea;
+ }
+ printf( "Count = %d\n", Count );
+// for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
+// printf( "%d", sat_solver_var_value(p->pSat, i) );
+// printf( "\n" );
+ Count = 1;
+ for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
+ if ( sat_solver_var_value(p->pSat, i) )
+ {
+ Vec_Int_t * vCutOne = Vec_WecEntry(p->vCuts, i-p->FirstVar);
+ printf( "%2d : Cut %3d (Gate %2d) ", Count, i-p->FirstVar, Vec_IntEntry(p->vCutGates, i-p->FirstVar) );
+ Vec_IntForEachEntry( vCutOne, Lit, k )
+ printf( "%d(%d) ", Lit - 2*(p->nInputs+1), Abc_Lit2Var(Lit) );
+ printf( "\n" );
+ Count++;
+ AreaNew += Vec_WrdEntry(p->vCutAreas, i-p->FirstVar);
+ }
+ printf( "Area = %7.2f\n", Scl_Int2Flt((int)AreaNew) );
+ }
+ if ( status == l_False )
+ printf( "UNSAT " ), fKeepTrying = 0;
+ else if ( status == l_True )
+ printf( "SAT " ), fKeepTrying++;
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
+ Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
printf( "\n" );
}
-
Sbm_ManStop( p );
return 1;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 73175997..92d6557d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -34467,7 +34467,7 @@ usage:
Abc_Print( -2, "\t-E num : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner );
Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer );
Abc_Print( -2, "\t-Q num : internal parameter impacting area of the mapping [default = %d]\n", pPars->nReqTimeFlex );
- Abc_Print( -2, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
+ Abc_Print( -2, "\t-a : toggles SAT-based area-oriented mapping (experimental) [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
Abc_Print( -2, "\t-p : toggles pin permutation (more matches - better quality) [default = %s]\n", pPars->fPinPerm? "yes": "no" );
Abc_Print( -2, "\t-q : toggles quick mapping (fewer matches - worse quality) [default = %s]\n", pPars->fPinQuick? "yes": "no" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-09 09:30:53 +0000