summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/aig/gia/giaQbf.c35
1 files changed, 25 insertions, 10 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c
index 33216ce3..dd040548 100644
--- a/src/aig/gia/giaQbf.c
+++ b/src/aig/gia/giaQbf.c
@@ -43,7 +43,9 @@ struct Qbf_Man_t_
sat_solver * pSatSyn; // synthesis instance
Vec_Int_t * vValues; // variable values
Vec_Int_t * vParMap; // parameter mapping
+ Vec_Int_t * vLits; // literals for the SAT solver
abctime clkStart; // global timeout
+ abctime clkSat; // SAT solver time
};
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
@@ -67,7 +69,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars )
{
// original problem: \exists p \forall x \exists y. M(p,x,y)
// negated problem: \forall p \exists x \exists y. !M(p,x,y)
- Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 0, 0 );
+ Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
Vec_Int_t * vVarMap, * vForAlls, * vExists;
Gia_Obj_t * pObj;
char * pFileName;
@@ -108,18 +110,23 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars )
***********************************************************************/
Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
{
- Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 0, 0 );
- Qbf_Man_t * p = ABC_CALLOC( Qbf_Man_t, 1 );
+ Qbf_Man_t * p;
+ Cnf_Dat_t * pCnf;
+ Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
+ pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
+ Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
+ p = ABC_CALLOC( Qbf_Man_t, 1 );
p->clkStart = Abc_Clock();
p->pGia = pGia;
p->nPars = nPars;
p->nVars = Gia_ManPiNum(pGia) - nPars;
p->fVerbose = fVerbose;
- p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 2;
+ p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1;
p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
p->pSatSyn = sat_solver_new();
p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) );
p->vParMap = Vec_IntStartFull( nPars );
+ p->vLits = Vec_IntAlloc( nPars );
sat_solver_setnvars( p->pSatSyn, nPars );
Cnf_DataFree( pCnf );
return p;
@@ -128,6 +135,7 @@ void Gia_QbfFree( Qbf_Man_t * p )
{
sat_solver_delete( p->pSatVer );
sat_solver_delete( p->pSatSyn );
+ Vec_IntFree( p->vLits );
Vec_IntFree( p->vValues );
Vec_IntFree( p->vParMap );
ABC_FREE( p );
@@ -166,8 +174,8 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_
}
int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
{
- Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 0, 0 );
- int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 2;
+ Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
+ int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1;
pCnf->pMan = NULL;
Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) );
for ( i = 0; i < pCnf->nClauses; i++ )
@@ -198,7 +206,7 @@ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
void Gia_QbfOnePattern( Qbf_Man_t * p, Vec_Int_t * vValues )
{
int i;
- Vec_IntClear( vValues );
+ Vec_IntClear( p->vValues );
for ( i = 0; i < p->nPars; i++ )
Vec_IntPush( vValues, sat_solver_var_value(p->pSatSyn, i) );
}
@@ -228,9 +236,10 @@ int Gia_QbfVerify( Qbf_Man_t * p, Vec_Int_t * vValues )
{
int i, Entry, RetValue;
assert( Vec_IntSize(vValues) == p->nPars );
+ Vec_IntClear( p->vLits );
Vec_IntForEachEntry( vValues, Entry, i )
- Vec_IntWriteEntry( vValues, i, Abc_Var2Lit(p->iParVarBeg+i, !Entry) );
- RetValue = sat_solver_solve( p->pSatVer, Vec_IntArray(vValues), Vec_IntLimit(vValues), 0, 0, 0, 0 );
+ Vec_IntPush( p->vLits, Abc_Var2Lit(p->iParVarBeg+i, !Entry) );
+ RetValue = sat_solver_solve( p->pSatVer, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 );
if ( RetValue == l_True )
{
Vec_IntClear( vValues );
@@ -256,6 +265,7 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose );
Gia_Man_t * pCof;
int i, status, RetValue = 0;
+ abctime clk;
assert( Gia_ManRegNum(pGia) == 0 );
Vec_IntFill( p->vValues, nPars, 0 );
for ( i = 0; Gia_QbfVerify(p, p->vValues) && (!nIterLimit || i < nIterLimit); i++ )
@@ -267,7 +277,9 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
Gia_ManStop( pCof );
if ( status == 0 ) { RetValue = 1; break; }
// synthesize next assignment
+ clk = Abc_Clock();
status = sat_solver_solve( p->pSatSyn, NULL, NULL, nConfLimit, 0, 0, 0 );
+ p->clkSat += Abc_Clock() - clk;
if ( fVerbose )
Gia_QbfPrint( p, p->vValues, i );
if ( status == l_Undef ) { RetValue = -1; break; }
@@ -284,7 +296,10 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
printf( "The problem is UNSAT. " );
else
printf( "The problem is SAT. " );
- Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
+ printf( "\n" );
+ Abc_PrintTime( 1, "SAT ", p->clkSat );
+ Abc_PrintTime( 1, "Other", Abc_Clock() - p->clkStart - p->clkSat );
+ Abc_PrintTime( 1, "TOTAL", Abc_Clock() - p->clkStart );
if ( RetValue == 0 )
{
assert( Vec_IntSize(p->vValues) == nPars );