Improvements to CNF generation.

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);

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] <file>\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" );