summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/cec/cecClass.c2
-rw-r--r--src/aig/cec/cecMan.c3
-rw-r--r--src/aig/gia/giaCSat.c10
-rw-r--r--src/aig/gia/giaCSatOld.c5
-rw-r--r--src/aig/gia/giaDfs.c30
-rw-r--r--src/aig/gia/giaEquiv.c2
6 files changed, 46 insertions, 6 deletions
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 5a52e913..cd3ce7b9 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -711,6 +711,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
pRes = Cec_ManSimSimRef( p, i );
pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
+
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
@@ -729,6 +730,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w] & pRes1[w];
}
+
references:
// if this node is candidate constant, collect it
if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index eb582e4c..de71ecc9 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -70,7 +70,8 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
***********************************************************************/
void Cec_ManSatPrintStats( Cec_ManSat_t * p )
{
- printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
printf( "Conf = %5d ", p->pPars->nBTLimit );
printf( "MinVar = %5d ", p->pPars->nSatVarMax );
printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 832eff26..f53a3d33 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -885,6 +885,8 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
pDecVar = Gia_Not(Gia_ObjChild0(pVar));
else
pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+// pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase );
+// pDecVar = Gia_Not(pDecVar);
// decide on first fanin
Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
@@ -955,8 +957,9 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
***********************************************************************/
void Cbs_ManSatPrintStats( Cbs_Man_t * p )
{
- printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
- printf( "Conf = %5d ", p->Pars.nBTLimit );
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
+ printf( "Conf = %6d ", p->Pars.nBTLimit );
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
@@ -984,6 +987,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
***********************************************************************/
Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
{
+ extern void Gia_ManCollectTest( Gia_Man_t * pAig );
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
Cbs_Man_t * p;
Vec_Int_t * vCex, * vVisit, * vCexStore;
@@ -991,11 +995,13 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
Gia_Obj_t * pRoot;
int i, status, clk, clkTotal = clock();
assert( Gia_ManRegNum(pAig) == 0 );
+// Gia_ManCollectTest( pAig );
// prepare AIG
Gia_ManCreateRefs( pAig );
Gia_ManCleanMark0( pAig );
Gia_ManCleanMark1( pAig );
Gia_ManFillValue( pAig ); // maps nodes into trail ids
+ Gia_ManSetPhase( pAig ); // maps nodes into trail ids
// create logic network
p = Cbs_ManAlloc();
p->Pars.nBTLimit = nConfs;
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index 409af56c..a0d97693 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -674,8 +674,9 @@ int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
***********************************************************************/
void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
{
- printf( "CO = %6d ", Gia_ManCoNum(p->pAig) );
- printf( "Conf = %5d ", p->Pars.nBTLimit );
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
+ printf( "Conf = %6d ", p->Pars.nBTLimit );
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index a978dcc3..8a3aef92 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -122,7 +122,7 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
Gia_Obj_t * pObj;
int i;
Vec_IntClear( vNodes );
- Gia_ManIncrementTravId( p );
+// Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
for ( i = 0; i < nNodes; i++ )
{
@@ -145,6 +145,34 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
SeeAlso []
***********************************************************************/
+void Gia_ManCollectTest( Gia_Man_t * p )
+{
+ Vec_Int_t * vNodes;
+ Gia_Obj_t * pObj;
+ int i, iNode, clk = clock();
+ vNodes = Vec_IntAlloc( 100 );
+ Gia_ManResetTravId( p );
+ Gia_ManIncrementTravId( p );
+ Gia_ManForEachCo( p, pObj, i )
+ {
+ iNode = Gia_ObjId(p, pObj);
+ Gia_ManCollectAnds( p, &iNode, 1, vNodes );
+ }
+ Vec_IntFree( vNodes );
+ ABC_PRT( "DFS from each output", clock() - clk );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects support nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Gia_ManSuppSize_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index cdee73d0..041be0f5 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1135,6 +1135,8 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
return;
}
+ if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
+ return;
assert( pRepr->Value < pObj->Value );
pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 03:44:39 +0000