3 files changed, 37 insertions, 3 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index cf763e67..9a49805b 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -138,6 +138,7 @@ extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
+extern void            Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 2ee66916..934aab1c 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -326,6 +326,30 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
     return pSat;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
+{
+    sat_solver * pSat = p;
+    Aig_Obj_t * pObj;
+    int i, * pLits;
+    pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+        pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+    if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
+        assert( 0 );
+    free( pLits );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 23b3e8f0..5556ac2e 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -221,9 +221,18 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     Number = 1;
     if ( nOutputs )
     {
-        assert( nOutputs == Aig_ManRegNum(p->pManAig) );
-        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-            pCnf->pVarNums[pObj->Id] = Number++;
+        if ( Aig_ManRegNum(p->pManAig) == 0 )
+        {
+            assert( nOutputs == Aig_ManPoNum(p->pManAig) );
+            Aig_ManForEachPo( p->pManAig, pObj, i )
+                pCnf->pVarNums[pObj->Id] = Number++;
+        }
+        else
+        {
+            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 )