From f79d8e4b0443bda2249735e34545ed2197cbe5ea Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 23 Jun 2014 14:50:46 -0700 Subject: Improvements to CNF generation. --- src/aig/gia/giaMf.c | 9 +++++++++ src/base/io/io.c | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index 043d4fa7..fa48a8c9 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -455,6 +455,15 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) pCnf->pVarNums[Id] = pCnfIds[Gia_ManCiIdToId(p->pGia, i)]; Gia_ManForEachCoId( p->pGia0, Id, i ) pCnf->pVarNums[Id] = pCnfIds[Gia_ManCoIdToId(p->pGia, i)]; +/* + // transform polarity of the internal nodes + Gia_ManSetPhase( p->pGia ); + Gia_ManForEachCo( p->pGia, pObj, i ) + pObj->fPhase = 0; + for ( i = 0; i < pCnf->nLiterals; i++ ) + if ( Gia_ManObj(p->pGia, Abc_Lit2Var(pCnf->pClauses[0][i]))->fPhase ) + pCnf->pClauses[0][i] = Abc_LitNot( pCnf->pClauses[0][i] ); +*/ } else pCnf->pVarNums = Vec_IntReleaseArray(vCnfIds); diff --git a/src/base/io/io.c b/src/base/io/io.c index 2e796cd6..eb8a7f9f 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1914,7 +1914,7 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) usage: fprintf( pAbc->Err, "usage: write_cnf [-nfpcvh] \n" ); - fprintf( pAbc->Err, "\t writes the miter cone into a CNF file\n" ); + fprintf( pAbc->Err, "\t generated CNF for the miter (see also \"&write_cnf\")\n" ); fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" ); fprintf( pAbc->Err, "\t-f : toggle using fast algorithm [default = %s]\n", fFastAlgo? "yes" : "no" ); fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" ); -- cgit v1.2.3