Experiment with 'pdr'.

6 files changed, 189 insertions, 34 deletions

diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index 9d2af1d6..0553af3d 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -67,6 +67,8 @@ static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
+//#define USE_PG
+#ifdef USE_PG
 static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
 { 
     Vec_Int_t * vId2Vars = p->pvId2Vars + Aig_ObjId(pObj);
@@ -80,7 +82,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
         int iVarNew = Vec_IntSize( vVar2Ids );
         assert( iVarNew > 0 );
         Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
-        Vec_IntWriteEntry( vId2Vars, k, iVarNew );
+        Vec_IntWriteEntry( vId2Vars, k, iVarNew << 2 );
         sat_solver_setnvars( pSat, iVarNew + 1 );
         if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
         {
@@ -93,42 +95,128 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
     }
     return Vec_IntEntry( vId2Vars, k );
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively adds CNF for the given object.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level )
+int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
 {
     Vec_Int_t * vLits;
     sat_solver * pSat;
     Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k);
     int nVarCount = Vec_IntSize(vVar2Ids);
     int iVarThis  = Pdr_ObjSatVar2FindOrAdd( p, k, pObj );
-    int * pLit, i, iVar, nClauses, iFirstClause, RetValue;
-    if ( nVarCount == Vec_IntSize(vVar2Ids) )
-        return iVarThis;
-    assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
+    int * pLit, i, iVar, iClaBeg, iClaEnd, RetValue;
+    int PolPres = (iVarThis & 3);
+    iVarThis >>= 2;
     if ( Aig_ObjIsCi(pObj) )
         return iVarThis;
-    nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
-    iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
-    assert( nClauses > 0 );
+//    Pol = 3;
+//    if ( nVarCount != Vec_IntSize(vVar2Ids) || (Pol & ~PolPres) )
+    if ( (Pol & ~PolPres) )
+    {
+        *Vec_IntEntryP( p->pvId2Vars + Aig_ObjId(pObj), k ) |= Pol;
+        iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
+        iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
+        assert( iClaBeg < iClaEnd );
+/*
+        if ( (Pol & ~PolPres) != 3 )
+        for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
+        {
+            printf( "Clause %5d : ", i );
+            for ( iVar = 0; iVar < 4; iVar++ )
+                printf( "%d ", ((unsigned)p->pCnf2->pClaPols[i] >> (2*iVar)) & 3 );
+            printf( "  " );
+            for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
+                printf( "%6d ", *pLit );
+            printf( "\n" );
+        }
+*/
+        pSat = Pdr_ManSolver(p, k);
+        vLits = Vec_WecEntry( p->vVLits, Level );
+        if ( (Pol & ~PolPres) == 3 )
+        {
+            assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
+            for ( i = iClaBeg; i < iClaEnd; i++ )
+            {
+                Vec_IntClear( vLits );
+                Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
+                for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
+                {
+                    iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, 3 );
+                    Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+                }
+                RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+                assert( RetValue );
+                (void) RetValue;
+            }
+        }
+        else // if ( (Pol & ~PolPres) == 2 || (Pol & ~PolPres) == 1 ) // write pos/neg polarity
+        {
+            assert( (Pol & ~PolPres) );
+            for ( i = iClaBeg; i < iClaEnd; i++ )
+            if ( 2 - !Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) == (Pol & ~PolPres) ) // taking opposite literal
+            {
+                Vec_IntClear( vLits );
+                Vec_IntPush( vLits, toLitCond( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
+                for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
+                {
+                    iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, ((unsigned)p->pCnf2->pClaPols[i] >> (2*(pLit-p->pCnf2->pClauses[i]-1))) & 3 );
+                    Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+                }
+                RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+                assert( RetValue );
+                (void) RetValue;
+            }
+        }
+    }
+    return iVarThis;
+}
+
+#else
+static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int * pfNewVar )
+{ 
+    Vec_Int_t * vId2Vars = p->pvId2Vars + Aig_ObjId(pObj);
+    assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 );
+    if ( Vec_IntSize(vId2Vars) == 0 )
+        Vec_IntGrow(vId2Vars, 2 * k + 1);
+    if ( Vec_IntGetEntry(vId2Vars, k) == 0 )
+    {
+        sat_solver * pSat = Pdr_ManSolver(p, k);
+        Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k);
+        int iVarNew = Vec_IntSize( vVar2Ids );
+        assert( iVarNew > 0 );
+        Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
+        Vec_IntWriteEntry( vId2Vars, k, iVarNew );
+        sat_solver_setnvars( pSat, iVarNew + 1 );
+        if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
+        {
+            int Lit = toLitCond( iVarNew, 1 );
+            int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+            assert( RetValue == 1 );
+            (void) RetValue;
+            sat_solver_compress( pSat );
+        }
+        *pfNewVar = 1;
+    }
+    return Vec_IntEntry( vId2Vars, k );
+}
+int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
+{
+    Vec_Int_t * vLits;
+    sat_solver * pSat;
+    int fNewVar = 0, iVarThis  = Pdr_ObjSatVar2FindOrAdd( p, k, pObj, &fNewVar );
+    int * pLit, i, iVar, iClaBeg, iClaEnd, RetValue;
+    if ( Aig_ObjIsCi(pObj) || !fNewVar )
+        return iVarThis;
+    iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
+    iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
+    assert( iClaBeg < iClaEnd );
     pSat = Pdr_ManSolver(p, k);
     vLits = Vec_WecEntry( p->vVLits, Level );
-    for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
+    for ( i = iClaBeg; i < iClaEnd; i++ )
     {
         Vec_IntClear( vLits );
-        for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
+        Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
+        for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
         {
-            iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1 );
+            iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, Pol );
             Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
         }
         RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
@@ -137,6 +225,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level )
     }
     return iVarThis;
 }
+#endif
 
 /**Function*************************************************************
 
@@ -149,12 +238,12 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level )
   SeeAlso     []
 
 ***********************************************************************/
-int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
+int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj )
 {
     if ( p->pPars->fMonoCnf )
         return Pdr_ObjSatVar1( p, k, pObj );
     else
-        return Pdr_ObjSatVar2( p, k, pObj, 0 );
+        return Pdr_ObjSatVar2( p, k, pObj, 0, Pol );
 }
 
 
@@ -277,7 +366,7 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p,
         assert( p->vVar2Reg == NULL );
         p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
         Saig_ManForEachLi( p->pAig, pObj, i )
-            Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
+            Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, 3, pObj), i );
     }
     pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
     sat_solver_set_runtime_limit( pSat, p->timeToStop );
@@ -303,6 +392,9 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p,
     if ( p->pCnf2 == NULL )
     {
         p->pCnf2     = Cnf_DeriveOtherWithMan( p->pCnfMan, p->pAig, 0 );
+#ifdef USE_PG
+        p->pCnf2->pClaPols = Cnf_DataDeriveLitPolarities( p->pCnf2 );
+#endif
         p->pvId2Vars = ABC_CALLOC( Vec_Int_t, Aig_ManObjNumMax(p->pAig) );
         Vec_PtrGrow( &p->vVar2Ids, 256 );
     }
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 9267ef1e..0eb6bd81 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -156,7 +156,7 @@ static inline abctime      Pdr_ManTimeLimit( Pdr_Man_t * p )
 /*=== pdrCex.c ==========================================================*/
 extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
 /*=== pdrCnf.c ==========================================================*/
-extern int             Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj );
+extern int             Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj );
 extern int             Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
 extern int             Pdr_ManFreeVar( Pdr_Man_t * p, int k );
 extern sat_solver *    Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 663a0e2f..31c05ce6 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -57,9 +57,8 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
     Vec_VecExpand( p->vClauses, k );
     Vec_IntPush( p->vActVars, 0 );
     // add property cone
-//    Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
     Saig_ManForEachPo( p->pAig, pObj, i )
-        Pdr_ObjSatVar( p, k, pObj );
+        Pdr_ObjSatVar( p, k, 1, pObj );
     return pSat;
 }
 
@@ -146,6 +145,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
     int i, iVar, iVarMax = 0;
     abctime clk = Abc_Clock();
     Vec_IntClear( p->vLits );
+    assert( !(fNext && fCompl) );
     for ( i = 0; i < pCube->nLits; i++ )
     {
         if ( pCube->Lits[i] == -1 )
@@ -154,7 +154,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
             pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
         else
             pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
-        iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
+        iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
         iVarMax = Abc_MaxInt( iVarMax, iVar );
         Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
     }
@@ -185,7 +185,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
         // skip solved outputs
         if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
             continue;
-        Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal
+        Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
         assert( RetValue == 1 );
     }
@@ -235,7 +235,7 @@ void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t
     pSat = Pdr_ManSolver(p, k);
     Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
     {
-        iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
+        iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
         Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
     }
 }
@@ -293,7 +293,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
     if ( pCube == NULL ) // solve the property
     {
         clk = Abc_Clock();
-        Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
+        Lit = toLit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
         RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
         sat_solver_set_runtime_limit( pSat, Limit );
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                                ///
 ////////////////////////////////////////////////////////////////////////