summaryrefslogtreecommitdiffstats
path: root/src/aig/cec
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cec')
-rw-r--r--src/aig/cec/cec.h1
-rw-r--r--src/aig/cec/cecChoice.c35
-rw-r--r--src/aig/cec/cecCore.c1
-rw-r--r--src/aig/cec/cecCorr.c14
-rw-r--r--src/aig/cec/cecInt.h4
-rw-r--r--src/aig/cec/cecSolve.c190
6 files changed, 196 insertions, 49 deletions
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 8e14d2ef..fcadb6ab 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -48,6 +48,7 @@ struct Cec_ParSat_t_
int fPolarFlip; // flops polarity of variables
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
+ int fLearnCls; // perform clause learning
int fVerbose; // verbose stats
};
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index 0662d73d..f51d138d 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -380,17 +380,17 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars )
+Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars )
{
- Gia_Man_t * pMiter, * pNew;
+ Gia_Man_t * pNew;
int RetValue;
// compute equivalences of the miter
- pMiter = Gia_ManChoiceMiter( vGias );
- RetValue = Cec_ManChoiceComputation_int( pMiter, pPars );
+// pMiter = Gia_ManChoiceMiter( vGias );
+ RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
// derive AIG with choices
- pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
+ pNew = Gia_ManEquivToChoices( pGia, nGias );
Gia_ManHasChoices( pNew );
- Gia_ManStop( pMiter );
+// Gia_ManStop( pMiter );
// report the results
if ( pPars->fVerbose )
{
@@ -422,11 +422,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
Gia_Man_t * pGia;
if ( 0 )
{
- Vec_Ptr_t * vGias;
- vGias = Vec_PtrAlloc( 1 );
- Vec_PtrPush( vGias, pAig );
- pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
- Vec_PtrFree( vGias );
+ pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );
}
else
{
@@ -439,7 +435,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
pManNew = Dar_ManChoiceNew( pMan, pPars );
pGia = Gia_ManFromAig( pManNew );
Aig_ManStop( pManNew );
- Aig_ManStop( pMan );
+// Aig_ManStop( pMan );
}
return pGia;
}
@@ -455,13 +451,10 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
SeeAlso []
***********************************************************************/
-Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
{
Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
- Vec_Ptr_t * vGias;
- Gia_Man_t * pGia;
Aig_Man_t * pAig;
- int i;
if ( pPars->fVerbose )
ABC_PRT( "Synthesis time", pPars->timeSynth );
Cec_ManChcSetDefaultParams( pParsChc );
@@ -470,14 +463,8 @@ Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
pParsChc->nBTLimit = 100;
pParsChc->fVerbose = pPars->fVerbose;
- vGias = Vec_PtrAlloc( 10 );
- Vec_PtrForEachEntry( vAigs, pAig, i )
- Vec_PtrPush( vGias, Gia_ManFromAig(pAig) );
- pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
- Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) );
- Vec_PtrForEachEntry( vGias, pAig, i )
- Gia_ManStop( (Gia_Man_t *)pAig );
- Vec_PtrFree( vGias );
+ pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );
+ Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
return pAig;
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index dc0fc0d0..9820c05c 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -49,6 +49,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
p->fPolarFlip = 1; // flops polarity of variables
p->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output
+ p->fLearnCls = 0; // perform clause learning
p->fVerbose = 0; // verbose stats
}
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index b4076916..96af801d 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -797,7 +797,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
}
pParsSat->nBTLimit *= 10;
if ( pPars->fUseCSat )
- vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+ vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples
@@ -831,8 +831,9 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
***********************************************************************/
int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
- int nIterMax = 100000;
- int nAddFrames = 1; // additional timeframes to simulate
+ int nIterMax = 100000;
+ int nAddFrames = 1; // additional timeframes to simulate
+ int fRunBmcFirst = 0;
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
@@ -875,8 +876,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
// check the base case
- if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
- Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
+ if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
+ Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
@@ -926,6 +927,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
if ( r == nIterMax )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
+ // check the base case
+ if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
+ Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 1fd48d55..9c012f73 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -199,6 +199,10 @@ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pO
extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
+extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj );
+extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
+extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
+extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p );
/*=== ceFraeep.c ============================================================*/
extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p );
extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 3a8d8588..1aaf54ff 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -404,9 +404,9 @@ void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMi
float dActConeBumpMax = 20.0;
int iVar;
// skip visited variables
- if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
+ if ( Gia_ObjIsTravIdCurrentArray(p->pAig, pObj) )
return;
- Gia_ObjSetTravIdCurrent(p->pAig, pObj);
+ Gia_ObjSetTravIdCurrentArray(p->pAig, pObj);
// add the PI to the list
if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) )
return;
@@ -440,7 +440,7 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
- Gia_ManIncrementTravId( p->pAig );
+ Gia_ManIncrementTravIdArray( p->pAig );
// determine the min and max level to visit
assert( dActConeRatio > 0 && dActConeRatio < 1 );
LevelMax = Gia_ObjLevel(p->pAig,pObj);
@@ -465,9 +465,18 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
***********************************************************************/
int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
{
+ Gia_Obj_t * pObjR = Gia_Regular(pObj);
int nBTLimit = p->pPars->nBTLimit;
int Lit, RetValue, status, clk, clk2, nConflicts;
+ if ( pObj == Gia_ManConst0(p->pAig) )
+ return 1;
+ if ( pObj == Gia_ManConst1(p->pAig) )
+ {
+ assert( 0 );
+ return 0;
+ }
+
p->nCallsSince++; // experiment with this!!!
p->nSatTotal++;
@@ -480,12 +489,12 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
// if the nodes do not have SAT variables, allocate them
clk2 = clock();
- Cec_CnfNodeAddToSolver( p, Gia_ObjFanin0(pObj) );
+ Cec_CnfNodeAddToSolver( p, pObjR );
//ABC_PRT( "cnf", clock() - clk2 );
//printf( "%d \n", p->pSat->size );
clk2 = clock();
-// Cec_SetActivityFactors( p, Gia_ObjFanin0(pObj) );
+// Cec_SetActivityFactors( p, pObjR );
//ABC_PRT( "act", clock() - clk2 );
// propage unit clauses
@@ -498,10 +507,10 @@ clk2 = clock();
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
- Lit = toLitCond( Cec_ObjSatNum(p,Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+ Lit = toLitCond( Cec_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) );
if ( p->pPars->fPolarFlip )
{
- if ( Gia_ObjFanin0(pObj)->fPhase ) Lit = lit_neg( Lit );
+ if ( pObjR->fPhase ) Lit = lit_neg( Lit );
}
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = clock();
@@ -541,6 +550,110 @@ p->timeSatUndec += clock() - clk;
}
}
+/**Function*************************************************************
+
+ Synopsis [Runs equivalence test for the two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
+{
+ Gia_Obj_t * pObjR1 = Gia_Regular(pObj1);
+ Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
+ int nBTLimit = p->pPars->nBTLimit;
+ int Lits[2], RetValue, status, clk, clk2, nConflicts;
+
+ if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
+ return 1;
+ if ( pObj1 == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) )
+ {
+ assert( 0 );
+ return 0;
+ }
+
+ p->nCallsSince++; // experiment with this!!!
+ p->nSatTotal++;
+
+ // check if SAT solver needs recycling
+ if ( p->pSat == NULL ||
+ (p->pPars->nSatVarMax &&
+ p->nSatVars > p->pPars->nSatVarMax &&
+ p->nCallsSince > p->pPars->nCallsRecycle) )
+ Cec_ManSatSolverRecycle( p );
+
+ // if the nodes do not have SAT variables, allocate them
+clk2 = clock();
+ Cec_CnfNodeAddToSolver( p, pObjR1 );
+ Cec_CnfNodeAddToSolver( p, pObjR2 );
+//ABC_PRT( "cnf", clock() - clk2 );
+//printf( "%d \n", p->pSat->size );
+
+clk2 = clock();
+// Cec_SetActivityFactors( p, pObjR1 );
+// Cec_SetActivityFactors( p, pObjR2 );
+//ABC_PRT( "act", clock() - clk2 );
+
+ // propage unit clauses
+ if ( p->pSat->qtail != p->pSat->qhead )
+ {
+ status = sat_solver_simplify(p->pSat);
+ assert( status != 0 );
+ assert( p->pSat->qtail == p->pSat->qhead );
+ }
+
+ // solve under assumptions
+ // A = 1; B = 0 OR A = 1; B = 1
+ Lits[0] = toLitCond( Cec_ObjSatNum(p,pObjR1), Gia_IsComplement(pObj1) );
+ Lits[1] = toLitCond( Cec_ObjSatNum(p,pObjR2), Gia_IsComplement(pObj2) );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pObjR1->fPhase ) Lits[0] = lit_neg( Lits[0] );
+ if ( pObjR2->fPhase ) Lits[1] = lit_neg( Lits[1] );
+ }
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+clk = clock();
+ nConflicts = p->pSat->stats.conflicts;
+
+clk2 = clock();
+ RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2,
+ (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+//ABC_PRT( "sat", clock() - clk2 );
+
+ if ( RetValue == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ Lits[0] = lit_neg( Lits[0] );
+ Lits[1] = lit_neg( Lits[1] );
+ RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
+ assert( RetValue );
+ p->nSatUnsat++;
+ p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
+//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+ return 1;
+ }
+ else if ( RetValue == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ p->nSatSat++;
+ p->nConfSat += p->pSat->stats.conflicts - nConflicts;
+//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+ return 0;
+ }
+ else // if ( RetValue == l_Undef )
+ {
+p->timeSatUndec += clock() - clk;
+ p->nSatUndec++;
+ p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
+//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+ return -1;
+ }
+}
+
/**Function*************************************************************
@@ -570,7 +683,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
}
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
- Gia_ManResetTravId( pAig );
+ Gia_ManResetTravIdArray( pAig );
p = Cec_ManSatCreate( pAig, pPars );
pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
Gia_ManForEachCo( pAig, pObj, i )
@@ -583,7 +696,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
}
Bar_ProgressUpdate( pProgress, i, "SAT..." );
clk2 = clock();
- status = Cec_ManSatCheckNode( p, pObj );
+ status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
pObj->fMark0 = (status == 0);
pObj->fMark1 = (status == 1);
/*
@@ -619,6 +732,22 @@ clk2 = clock();
/**Function*************************************************************
+ Synopsis [Returns the pattern stored.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat )
+{
+ return pSat->vCex;
+}
+
+/**Function*************************************************************
+
Synopsis [Save values in the cone of influence.]
Description []
@@ -630,9 +759,9 @@ clk2 = clock();
***********************************************************************/
void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs )
{
- if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
return;
- Gia_ObjSetTravIdCurrent(p, pObj);
+ Gia_ObjSetTravIdCurrentArray(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
@@ -670,7 +799,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
- Gia_ManResetTravId( pAig );
+ Gia_ManResetTravIdArray( pAig );
p = Cec_ManSatCreate( pAig, pPars );
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
@@ -691,7 +820,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
}
continue;
}
- status = Cec_ManSatCheckNode( p, pObj );
+ status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
//printf( "output %d status = %d\n", i, status );
Vec_StrPush( vStatus, (char)status );
if ( status != 0 )
@@ -707,7 +836,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
if ( iPat % nPatsInit == 0 )
iPat++;
// save the pattern
- Gia_ManIncrementTravId( pAig );
+ Gia_ManIncrementTravIdArray( pAig );
// Vec_IntClear( p->vCex );
Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
// Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
@@ -771,9 +900,9 @@ void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
***********************************************************************/
void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
{
- if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
return;
- Gia_ObjSetTravIdCurrent(p, pObj);
+ Gia_ObjSetTravIdCurrentArray(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
pSat->nCexLits++;
@@ -787,6 +916,26 @@ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * p
/**Function*************************************************************
+ Synopsis [Save patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
+{
+ Vec_IntClear( p->vCex );
+ Gia_ManIncrementTravIdArray( p->pAig );
+ Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) );
+ if ( pObj2 )
+ Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs one round of solving for the POs of the AIG.]
Description [Labels the nodes that have been proved (pObj->fMark1)
@@ -808,7 +957,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
// prepare AIG
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
- Gia_ManResetTravId( pAig );
+ Gia_ManResetTravIdArray( pAig );
// create resulting data-structures
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
vCexStore = Vec_IntAlloc( 10000 );
@@ -834,7 +983,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
}
continue;
}
- status = Cec_ManSatCheckNode( p, pObj );
+ status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
Vec_StrPush( vStatus, (char)status );
if ( status == -1 )
{
@@ -845,8 +994,9 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
continue;
assert( status == 0 );
// save the pattern
- Gia_ManIncrementTravId( pAig );
- Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
+// Gia_ManIncrementTravIdArray( pAig );
+// Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
+ Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL );
// Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
Cec_ManSatAddToStore( vCexStore, p->vCex, i );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-07 16:06:57 +0000