Transforming the solver to use different clause representation.

3 files changed, 83 insertions, 38 deletions

diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 523de8fe..27fd698c 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -59,8 +59,8 @@ struct satset_t
 ////////////////////////////////////////////////////////////////////////
 
 static inline satset* Proof_NodeRead    (Vec_Int_t* p, cla h)     { return satset_read( (veci*)p, h );   }
-static inline cla     Proof_NodeHandle  (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); }
-static inline int     Proof_NodeCheck   (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c );  }
+//static inline cla     Proof_NodeHandle  (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); }
+//static inline int     Proof_NodeCheck   (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c );  }
 static inline int     Proof_NodeSize    (int nEnts)               { return sizeof(satset)/4 + nEnts;     }
 
 static inline satset* Proof_ResolveRead (Vec_Rec_t* p, cla h)     { return (satset*)Vec_RecEntryP(p, h); }
@@ -156,15 +156,15 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_CollectUsed_iter( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
+void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
 {
-    satset * pNext;
-    int i, hNode;
+    satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
+    int i;
     if ( pNode->Id )
         return;
     // start with node
     pNode->Id = 1;
-    Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNode) << 1 );
+    Vec_IntPush( vStack, hNode << 1 );
     // perform DFS search
     while ( Vec_IntSize(vStack) )
     {
@@ -182,7 +182,7 @@ void Proof_CollectUsed_iter( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUs
             if ( pNext && !pNext->Id )
             {
                 pNext->Id = 1;
-                Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNext) << 1 ); // add first time
+                Vec_IntPush( vStack, (pNode->pEnts[i] >> 2) << 1 ); // add first time
             }
     }
 }
@@ -207,13 +207,11 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
     vUsed = Vec_IntAlloc( 1000 );
     vStack = Vec_IntAlloc( 1000 );
     if ( hRoot )
-        Proof_CollectUsed_iter( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack );
+        Proof_CollectUsed_iter( vProof, hRoot, vUsed, vStack );
     else
     {
-        satset * pNode;
-        int i;
-        Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
-            Proof_CollectUsed_iter( vProof, pNode, vUsed, vStack );
+        Vec_IntForEachEntry( vRoots, Entry, i )
+            Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
     }
     Vec_IntFree( vStack );
 //    Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
@@ -255,17 +253,17 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_CollectUsed_rec( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed )
+void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed )
 {
-    satset * pNext;
+    satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
     int i;
     if ( pNode->Id )
         return;
     pNode->Id = 1;
     Proof_NodeForeachFanin( vProof, pNode, pNext, i )
         if ( pNext && !pNext->Id )
-            Proof_CollectUsed_rec( vProof, pNext, vUsed );
-    Vec_IntPush( vUsed, Proof_NodeHandle(vProof, pNode) );
+            Proof_CollectUsed_rec( vProof, pNode->pEnts[i] >> 2, vUsed );
+    Vec_IntPush( vUsed, hNode );
 }
 
 /**Function*************************************************************
@@ -285,13 +283,12 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
     assert( (hRoot > 0) ^ (vRoots != NULL) );
     vUsed = Vec_IntAlloc( 1000 );
     if ( hRoot )
-        Proof_CollectUsed_rec( vProof, Proof_NodeRead(vProof, hRoot), vUsed );
+        Proof_CollectUsed_rec( vProof, hRoot, vUsed );
     else
     {
-        satset * pNode;
-        int i;
-        Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
-            Proof_CollectUsed_rec( vProof, pNode, vUsed );
+        int i, Entry;
+        Vec_IntForEachEntry( vRoots, Entry, i )
+            Proof_CollectUsed_rec( vProof, Entry, vUsed );
     }
     return vUsed;
 }
@@ -512,7 +509,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
             if ( pFanin && !pFanin->mark )
             {
                 pFanin->mark = 1;
-                Vec_IntPush( vCore, Proof_NodeHandle(vClauses, pFanin) );
+                Vec_IntPush( vCore, pNode->pEnts[i] >> 2 );
             }
     }
     // clean core clauses and reexpress core in terms of clause IDs
@@ -653,7 +650,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
         pNode->Id = Aig_ObjToLit(pObj);
     }
     // save the result
-    assert( Proof_NodeHandle(vProof, pNode) == hRoot );
+//    assert( Proof_NodeHandle(vProof, pNode) == hRoot );
     Aig_ObjCreatePo( pAig, pObj );
     Aig_ManCleanup( pAig );
 
@@ -759,7 +756,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
         pNode->Id = Tru_ManInsert( pTru, pRes );
     }
     // save the result
-    assert( Proof_NodeHandle(vProof, pNode) == hRoot );
+//    assert( Proof_NodeHandle(vProof, pNode) == hRoot );
 //    Aig_ObjCreatePo( pAig, pObj );
 //    Aig_ManCleanup( pAig );
 
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index cb0d7b60..a4166fef 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1308,15 +1308,16 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 
 void sat_solver2_delete(sat_solver2* s)
 {
-//    veci * pCore;
+    veci * pCore;
+
     // report statistics
     printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits );
-/*
+
     pCore = Sat_ProofCore( s );
     printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
     veci_delete( pCore );
     ABC_FREE( pCore ); 
-*/
+
     if ( s->fProofLogging )
         Sat_ProofCheck( s );
 
diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h
index 87a168b0..e92129be 100644
--- a/src/sat/bsat/vecRec.h
+++ b/src/sat/bsat/vecRec.h
@@ -40,14 +40,14 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 
 // data-structure for logging entries
-// memory is allocated in 2^(p->LogSize+2) byte chunks
+// memory is allocated in 'p->Mask+1' int chunks
 // the first 'int' of each entry cannot be 0
 typedef struct Vec_Rec_t_ Vec_Rec_t;
 struct Vec_Rec_t_ 
 {
-    int                LogSize;      // the log size of one chunk in 'int'
     int                Mask;         // mask for the log size
     int                hCurrent;     // current position
+    int                hShadow;      // current position
     int                nEntries;     // total number of entries
     int                nChunks;      // total number of chunks
     int                nChunksAlloc; // the number of allocated chunks
@@ -89,8 +89,7 @@ static inline Vec_Rec_t * Vec_RecAlloc()
 {
     Vec_Rec_t * p;
     p = ABC_CALLOC( Vec_Rec_t, 1 );
-    p->LogSize       = 15; // chunk size = 2^15 ints = 128 Kb
-    p->Mask          = (1 << p->LogSize) - 1;
+    p->Mask          = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
     p->hCurrent      = (1 << 16);
     p->nChunks       = 1;
     p->nChunksAlloc  = 16;
@@ -105,8 +104,7 @@ static inline void Vec_RecAlloc_( Vec_Rec_t * p )
 //    Vec_Rec_t * p;
 //    p = ABC_CALLOC( Vec_Rec_t, 1 );
     memset( p, 0, sizeof(Vec_Rec_t) );
-    p->LogSize       = 15; // chunk size = 2^15 ints = 128 Kb
-    p->Mask          = (1 << p->LogSize) - 1;
+    p->Mask          = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
     p->hCurrent      = (1 << 16);
     p->nChunks       = 1;
     p->nChunksAlloc  = 16;
@@ -162,7 +160,7 @@ static inline int Vec_RecShift( int i )
 ***********************************************************************/
 static inline int Vec_RecSize( Vec_Rec_t * p )
 {
-    return Vec_RecChunk(p->hCurrent) * (1 << p->LogSize); 
+    return Vec_RecChunk(p->hCurrent) * (p->Mask + 1); 
 }
 
 /**Function*************************************************************
@@ -296,7 +294,6 @@ static inline void Vec_RecFree_( Vec_Rec_t * p )
 ***********************************************************************/
 static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize )
 {
-    int RetValue;
     assert( nSize <= p->Mask );
     assert( Vec_RecEntry(p, p->hCurrent) == 0 );
     assert( Vec_RecChunk(p->hCurrent) == p->nChunks );
@@ -309,15 +306,14 @@ static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize )
             p->nChunksAlloc *= 2;
         }
         if ( p->pChunks[p->nChunks] == NULL )
-            p->pChunks[p->nChunks] = ABC_ALLOC( int, (1 << p->LogSize) );
+            p->pChunks[p->nChunks] = ABC_ALLOC( int, (p->Mask + 1) );
         p->pChunks[p->nChunks][0] = 0;
         p->hCurrent = p->nChunks << 16;
     }
-    RetValue = p->hCurrent;
     p->hCurrent += nSize;
     *Vec_RecEntryP(p, p->hCurrent) = 0;
     p->nEntries++;
-    return RetValue;
+    return p->hCurrent - nSize;
 }
 
 /**Function*************************************************************
@@ -338,6 +334,57 @@ static inline int Vec_RecPush( Vec_Rec_t * p, int * pArray, int nSize )
     return Handle;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_RecSetShadow( Vec_Rec_t * p, int hShadow )
+{
+    p->hShadow = hShadow;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_RecReadShadow( Vec_Rec_t * p )
+{
+    return p->hShadow;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_RecAppendShadow( Vec_Rec_t * p, int nSize )
+{
+    if ( Vec_RecShift(p->hShadow) + nSize >= p->Mask )
+        p->hShadow = ((Vec_RecChunk(p->hShadow) + 1) << 16);
+    p->hShadow += nSize;
+    return p->hShadow - nSize;
+}
+
 
 ABC_NAMESPACE_HEADER_END