From 6da21b8b884632c901ae10955e23c0c8206e7e58 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 5 Mar 2015 23:00:30 -0800 Subject: Experiments with SAT-based cube enumeration. --- src/aig/gia/giaQbf.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/aig/gia/giaQbf.c') diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index a14ec443..b7d678b3 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -75,7 +75,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose abctime clkStart = Abc_Clock(); pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1; + iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; Cnf_DataFree( pCnf ); // iterate through the SAT assignment vLits = Vec_IntAlloc( Gia_ManPiNum(pGia) ); @@ -180,7 +180,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) p->nPars = nPars; p->nVars = Gia_ManPiNum(pGia) - nPars; p->fVerbose = fVerbose; - p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1; + 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) ); @@ -280,7 +280,7 @@ 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, 1, 0 ); - int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1; + 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++ ) -- cgit v1.2.3