summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c37
-rw-r--r--src/proof/cec/cec.h1
-rw-r--r--src/proof/cec/cecCore.c2
-rw-r--r--src/proof/cec/cecSolve.c20
4 files changed, 56 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 31f3e270..db8bacf2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -655,6 +655,25 @@ Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes )
Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
return vStatuses;
}
+Vec_Int_t * Abc_FrameDeriveStatusArray2( Vec_Ptr_t * vCexes )
+{
+ Vec_Int_t * vStatuses;
+ Abc_Cex_t * pCex;
+ int i;
+ if ( vCexes == NULL )
+ return NULL;
+ vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) );
+ Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC
+ Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i )
+ if ( pCex == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
+ {
+ Vec_IntWriteEntry( vStatuses, i, 1 ); // set this output as UNSAT
+ Vec_PtrWriteEntry( vCexes, i, NULL );
+ }
+ else if ( pCex != NULL )
+ Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
+ return vStatuses;
+}
/**Function*************************************************************
@@ -2765,8 +2784,8 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_CexPrintStats( pTemp );
}
}
- if ( Counter )
- printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
+// if ( Counter )
+// printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
}
}
if ( pAbc->vStatuses )
@@ -33675,7 +33694,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fNewSolver = 0, fCSat = 0;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxvh" ) ) != EOF )
{
switch ( c )
{
@@ -33727,6 +33746,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
fCSat ^= 1;
break;
+ case 'x':
+ pPars->fSaveCexes ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -33759,10 +33781,16 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Cec_ManSatSolving( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
}
+ if ( pAbc->pGia->vSeqModelVec )
+ {
+ Vec_Int_t * vStatuses = Abc_FrameDeriveStatusArray2( pAbc->pGia->vSeqModelVec );
+ Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
+ Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
+ }
return 0;
usage:
- Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctvh]\n" );
+ Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxvh]\n" );
Abc_Print( -2, "\t performs SAT solving for the combinational outputs\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
@@ -33772,6 +33800,7 @@ usage:
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
Abc_Print( -2, "\t-t : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
+ Abc_Print( -2, "\t-x : toggle solving all outputs and saving counter-examples [default = %s]\n", pPars->fSaveCexes? "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");
return 1;
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index cb4ff27f..757d9fd3 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -51,6 +51,7 @@ struct Cec_ParSat_t_
int fCheckMiter; // the circuit is the miter
// int fFirstStop; // stop on the first sat output
int fLearnCls; // perform clause learning
+ int fSaveCexes; // saves counter-examples
int fVerbose; // verbose stats
};
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 85fcfa26..250cb69e 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -241,6 +241,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
// pNew = Gia_ManDupDfsSkip( pAig );
pNew = Gia_ManDup( pAig );
Cec_ManPatStop( pPat );
+ pNew->vSeqModelVec = pAig->vSeqModelVec;
+ pAig->vSeqModelVec = NULL;
return pNew;
}
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index f75914e4..3c21e589 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -673,6 +673,21 @@ p->timeSatUndec += Abc_Clock() - clk;
SeeAlso []
***********************************************************************/
+Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
+{
+ Abc_Cex_t * pCex;
+ int i;
+ pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 );
+ pCex->iPo = iOut;
+ pCex->iFrame = 0;
+ for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+ {
+ int iVar = Cec_ObjSatNum(p, Gia_ManCi(p->pAig, i));
+ if ( iVar > 0 && sat_solver_var_value(p->pSat, iVar) )
+ pCex->pData[i>>5] |= (1<<(i & 31));
+ }
+ return pCex;
+}
void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
{
Bar_Progress_t * pProgress = NULL;
@@ -680,6 +695,9 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
Gia_Obj_t * pObj;
int i, status;
abctime clk = Abc_Clock(), clk2;
+ Vec_PtrFreeP( &pAig->vSeqModelVec );
+ if ( pPars->fSaveCexes )
+ pAig->vSeqModelVec = Vec_PtrStart( Gia_ManCoNum(pAig) );
// reset the manager
if ( pPat )
{
@@ -715,6 +733,8 @@ clk2 = Abc_Clock();
assert( OrigId1 >= 0 && OrigId2 >= 0 );
Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 );
}
+ if ( pPars->fSaveCexes && status != -1 )
+ Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) );
/*
if ( status == -1 )
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-24 23:33:37 +0000