From 3d01abf481c0115beb5f2aea48ea9007a3e29c39 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 19 Jul 2013 21:01:06 -0700
Subject: Experiment with 'pdr'.

---
 src/sat/cnf/cnf.h     |  2 ++
 src/sat/cnf/cnfMan.c  |  1 +
 src/sat/cnf/cnfUtil.c | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 63 insertions(+)

(limited to 'src/sat/cnf')

diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index e5079a46..ba41ef4e 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -63,6 +63,7 @@ struct Cnf_Dat_t_
     int *           pVarNums;        // the number of CNF variable for each node ID (-1 if unused)
     int *           pObj2Clause;     // the mapping of objects into clauses
     int *           pObj2Count;      // the mapping of objects into clause number
+    unsigned char * pClaPols;        // polarity of input literals in each clause
     Vec_Int_t *     vMapping;        // mapping of internal nodes
 };
 
@@ -176,6 +177,7 @@ extern Vec_Ptr_t *     Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
 extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
 extern Vec_Int_t *     Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 extern Vec_Int_t *     Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
+extern unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p );
 /*=== cnfWrite.c ========================================================*/
 extern Vec_Int_t *     Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
 extern void            Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index 2aa5df6f..8a155f78 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -182,6 +182,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
     if ( p == NULL )
         return;
     Vec_IntFreeP( &p->vMapping );
+    ABC_FREE( p->pClaPols );
     ABC_FREE( p->pObj2Clause );
     ABC_FREE( p->pObj2Count );
     ABC_FREE( p->pClauses[0] );
diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c
index e3828863..98b494b3 100644
--- a/src/sat/cnf/cnfUtil.c
+++ b/src/sat/cnf/cnfUtil.c
@@ -229,6 +229,66 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
     return vCoIds;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
+{
+    int i, c, iClaBeg, iClaEnd, * pLit;
+    unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
+    unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
+    unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses );
+    for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ )
+    {
+        if ( p->pObj2Count[i] == 0 )
+            continue;
+        iClaBeg = p->pObj2Clause[i];
+        iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
+        // go through the negative polarity clauses
+        for ( c = iClaBeg; c < iClaEnd; c++ )
+            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
+                if ( Abc_LitIsCompl(p->pClauses[c][0]) )
+                    pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit));  // taking the opposite (!) -- not the case
+                else
+                    pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit));  // taking the opposite (!) -- not the case
+        // record these clauses
+        for ( c = iClaBeg; c < iClaEnd; c++ )
+            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
+                if ( Abc_LitIsCompl(p->pClauses[c][0]) )
+                    pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
+                else
+                    pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
+        // clean negative polarity
+        for ( c = iClaBeg; c < iClaEnd; c++ )
+            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
+                pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
+    }
+    ABC_FREE( pPols0 );
+    ABC_FREE( pPols1 );
+/*
+//    for ( c = 0; c < p->nClauses; c++ )
+    for ( c = 0; c < 100; c++ )
+    {
+        printf( "Clause %6d : ", c );
+        for ( i = 0; i < 4; i++ )
+            printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
+        printf( "  " );
+        for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
+            printf( "%6d ", *pLit );
+        printf( "\n" );
+    }
+*/
+    return pPres;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-- 
cgit v1.2.3