Version abc80116

2 files changed, 23 insertions, 0 deletions

diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 77c87f3f..5726469f 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -133,6 +133,7 @@ extern Cnf_Man_t *     Cnf_ManStart();
 extern void            Cnf_ManStop( Cnf_Man_t * p );
 extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 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 );
 /*=== cnfMap.c ========================================================*/
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 4ac06b48..47bc0b67 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -139,6 +139,28 @@ void Cnf_DataFree( Cnf_Dat_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
+{
+    Aig_Obj_t * pObj;
+    int v;
+    Aig_ManForEachObj( p->pMan, pObj, v )
+        if ( p->pVarNums[pObj->Id] )
+            p->pVarNums[pObj->Id] += nVarsPlus;
+    for ( v = 0; v < p->nLiterals; v++ )
+        p->pClauses[0][v] += 2*nVarsPlus;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
 {
     FILE * pFile;