1 files changed, 123 insertions, 6 deletions

diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index fa5be801..6faa08d2 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -217,11 +217,12 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) );
     memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) );
     // assign variables to the last (nOutputs) POs
-    Number = 0;
-    for ( i = 0; i < nOutputs; i++ )
+    Number = 1;
+    if ( nOutputs )
     {
-        pObj = Aig_ManPo( p->pManAig, Aig_ManPoNum(p->pManAig) - nOutputs + i );
-        pCnf->pVarNums[pObj->Id] = Number++;
+        assert( nOutputs == Aig_ManRegNum(p->pManAig) );
+        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+            pCnf->pVarNums[pObj->Id] = Number++;
     }
     // assign variables to the internal nodes
     Vec_PtrForEachEntry( vMapped, pObj, i )
@@ -291,16 +292,15 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     // write the output literals
     Aig_ManForEachPo( p->pManAig, pObj, i )
     {
+        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
         if ( i < Aig_ManPoNum(p->pManAig) - nOutputs )
         {
-            OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
             *pClas++ = pLits;
             *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
         }
         else
         {
             PoVar = pCnf->pVarNums[ pObj->Id ];
-            OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
             // first clause
             *pClas++ = pLits;
             *pLits++ = 2 * PoVar; 
@@ -319,6 +319,123 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Derives a simple CNF for the AIG.]
+
+  Description [The last argument shows the number of last outputs
+  of the manager, which will not be converted into clauses but the
+  new variables for which will be introduced.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
+{
+    Aig_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
+    int i, nLiterals, nClauses, Number;
+
+    // count the number of literals and clauses
+    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + 3 * nOutputs;
+    nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + nOutputs;
+
+    // allocate CNF
+    pCnf = ALLOC( Cnf_Dat_t, 1 );
+    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+    pCnf->nLiterals = nLiterals;
+    pCnf->nClauses = nClauses;
+    pCnf->pClauses = ALLOC( int *, nClauses + 1 );
+    pCnf->pClauses[0] = ALLOC( int, nLiterals );
+    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
+
+    // create room for variable numbers
+    pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p) );
+    memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p)) );
+    // assign variables to the last (nOutputs) POs
+    Number = 1;
+    if ( nOutputs )
+    {
+        assert( nOutputs == Aig_ManRegNum(p) );
+        Aig_ManForEachLiSeq( p, pObj, i )
+            pCnf->pVarNums[pObj->Id] = Number++;
+    }
+    // assign variables to the internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pCnf->pVarNums[pObj->Id] = Number++;
+    // assign variables to the PIs and constant node
+    Aig_ManForEachPi( p, pObj, i )
+        pCnf->pVarNums[pObj->Id] = Number++;
+    pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
+    pCnf->nVars = Number;
+/*
+    // print CNF numbers
+    printf( "SAT numbers of each node:\n" );
+    Aig_ManForEachObj( p, pObj, i )
+        printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
+    printf( "\n" );
+*/
+    // assign the clauses
+    pLits = pCnf->pClauses[0];
+    pClas = pCnf->pClauses;
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        OutVar   = pCnf->pVarNums[ pObj->Id ];
+        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
+
+        // positive phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar; 
+        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
+        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
+        // negative phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
+    }
+ 
+    // write the constant literal
+    OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
+    assert( OutVar <= Aig_ManObjIdMax(p) );
+    *pClas++ = pLits;
+    *pLits++ = 2 * OutVar; 
+
+    // write the output literals
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+        if ( i < Aig_ManPoNum(p) - nOutputs )
+        {
+            *pClas++ = pLits;
+            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
+        }
+        else
+        {
+            PoVar  = pCnf->pVarNums[ pObj->Id ];
+            // first clause
+            *pClas++ = pLits;
+            *pLits++ = 2 * PoVar; 
+            *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
+            // second clause
+            *pClas++ = pLits;
+            *pLits++ = 2 * PoVar + 1; 
+            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
+        }
+    }
+
+    // verify that the correct number of literals and clauses was written
+    assert( pLits - pCnf->pClauses[0] == nLiterals );
+    assert( pClas - pCnf->pClauses == nClauses );
+    return pCnf;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////