diff options
-rw-r--r-- | abclib.dsp | 4 | ||||
-rw-r--r-- | src/proof/fra/fraCec.c | 4 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 236 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 53 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 4 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 136 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 28 | ||||
-rw-r--r-- | src/sat/bsat/satSolver_old.c | 1766 | ||||
-rw-r--r-- | src/sat/bsat/satSolver_old.h | 210 | ||||
-rw-r--r-- | src/sat/bsat/satTruth.c | 34 | ||||
-rw-r--r-- | src/sat/bsat/satTruth.h | 2 | ||||
-rw-r--r-- | src/sat/bsat/vecRec.h | 396 | ||||
-rw-r--r-- | src/sat/bsat/vecSet.h | 247 |
13 files changed, 454 insertions, 2666 deletions
@@ -1261,6 +1261,10 @@ SOURCE=.\src\sat\bsat\satVec.h SOURCE=.\src\sat\bsat\vecRec.h # End Source File +# Begin Source File + +SOURCE=.\src\sat\bsat\vecSet.h +# End Source File # End Group # Begin Group "proof" diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c index ac11b0bb..1ef9091a 100644 --- a/src/proof/fra/fraCec.c +++ b/src/proof/fra/fraCec.c @@ -147,7 +147,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize ); } // free the sat_solver2 - if ( fVerbose ) +// if ( fVerbose ) Sat_Solver2PrintStats( stdout, pSat ); //sat_solver2_store_write( pSat, "trace.cnf" ); //sat_solver2_store_free( pSat ); @@ -253,7 +253,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); } // free the sat_solver - if ( fVerbose ) +// if ( fVerbose ) Sat_SolverPrintStats( stdout, pSat ); //sat_solver_store_write( pSat, "trace.cnf" ); //sat_solver_store_free( pSat ); diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 1eaf4407..dcb02bcd 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -22,18 +22,16 @@ #include "src/misc/vec/vec.h" #include "src/aig/aig/aig.h" #include "satTruth.h" -#include "vecRec.h" +#include "vecSet.h" ABC_NAMESPACE_IMPL_START /* - Proof is represented as a vector of integers. - The first entry is -1. - A resolution record is represented by a handle (an offset in this array). + Proof is represented as a vector of records. + A resolution record is represented by a handle (an offset in this vector). A resolution record entry is <size><label><ant1><ant2>...<antN> - Label is initialized to 0. - Root clauses are given by their handles. + Label is initialized to 0. Root clauses are given by their handles. They are marked by bitshifting by 2 bits up and setting the LSB to 1 */ @@ -58,26 +56,25 @@ struct satset_t /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -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 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); } +static inline satset* Proof_ClauseRead ( Vec_Int_t* p, cla h ) { assert( h > 0 ); return satset_read( (veci *)p, h ); } +static inline satset* Proof_NodeRead ( Vec_Set_t* p, cla h ) { assert( h > 0 ); return (satset*)Vec_SetEntry( p, h ); } +static inline int Proof_NodeWordNum ( int nEnts ) { assert( nEnts > 0 ); return 1 + ((nEnts + 1) >> 1); } // iterating through nodes in the proof -#define Proof_ForeachNode( p, pNode, h ) \ - for ( h = 1; (h < Vec_IntSize(p)) && ((pNode) = Proof_NodeRead(p, h)); h += Proof_NodeSize(pNode->nEnts) ) +#define Proof_ForeachClauseVec( pVec, p, pNode, i ) \ + for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ ) #define Proof_ForeachNodeVec( pVec, p, pNode, i ) \ for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ ) +#define Proof_ForeachNodeVec1( pVec, p, pNode, i ) \ + for ( i = 1; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ ) // iterating through fanins of a proof node -#define Proof_NodeForeachFanin( p, pNode, pFanin, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ ) +#define Proof_NodeForeachFanin( pProof, pNode, pFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ ) #define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) -#define Proof_NodeForeachFaninLeaf( p, pClauses, pNode, pFanin, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ ) + for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) +#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ ) //////////////////////////////////////////////////////////////////////// @@ -86,48 +83,6 @@ static inline satset* Proof_ResolveRead (Vec_Rec_t* p, cla h) { return (sats /**Function************************************************************* - Synopsis [Returns the number of proof nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Proof_CountAll( Vec_Int_t * p ) -{ - satset * pNode; - int hNode, Counter = 0; - Proof_ForeachNode( p, pNode, hNode ) - Counter++; - return Counter; -} - -/**Function************************************************************* - - Synopsis [Collects all resolution nodes belonging to the proof.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Proof_CollectAll( Vec_Int_t * p ) -{ - Vec_Int_t * vUsed; - satset * pNode; - int hNode; - vUsed = Vec_IntAlloc( 1000 ); - Proof_ForeachNode( p, pNode, hNode ) - Vec_IntPush( vUsed, hNode ); - return vUsed; -} - -/**Function************************************************************* - Synopsis [Cleans collected resultion nodes belonging to the proof.] Description [] @@ -137,7 +92,7 @@ Vec_Int_t * Proof_CollectAll( Vec_Int_t * p ) SeeAlso [] ***********************************************************************/ -void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed ) +void Proof_CleanCollected( Vec_Set_t * vProof, Vec_Int_t * vUsed ) { satset * pNode; int hNode; @@ -147,7 +102,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed ) /**Function************************************************************* - Synopsis [Recursively visits useful proof nodes.] + Synopsis [Marks useful nodes of the proof.] Description [] @@ -156,7 +111,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed ) SeeAlso [] ***********************************************************************/ -void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) +void Proof_CollectUsed_iter( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) { satset * pNext, * pNode = Proof_NodeRead( vProof, hNode ); int i; @@ -198,46 +153,33 @@ void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, V SeeAlso [] ***********************************************************************/ -Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot ) +Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int fSort ) { + int fVerify = 0; Vec_Int_t * vUsed, * vStack; int clk = clock(); int i, Entry, iPrev = 0; - assert( (hRoot > 0) ^ (vRoots != NULL) ); vUsed = Vec_IntAlloc( 1000 ); vStack = Vec_IntAlloc( 1000 ); - if ( hRoot ) - Proof_CollectUsed_iter( vProof, hRoot, vUsed, vStack ); - else - { - Vec_IntForEachEntry( vRoots, Entry, i ) + Vec_IntForEachEntry( vRoots, Entry, i ) + if ( Entry >= 0 ) Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack ); - } Vec_IntFree( vStack ); // Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk ); - -/* - // verify topological order - iPrev = 0; - Vec_IntForEachEntry( vUsed, Entry, i ) - { - printf( "%d ", Entry - iPrev ); - iPrev = Entry; - } -*/ clk = clock(); -// Vec_IntSort( vUsed, 0 ); Abc_Sort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) ); // Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk ); - // verify topological order - iPrev = 0; - Vec_IntForEachEntry( vUsed, Entry, i ) + if ( fVerify ) { - if ( iPrev >= Entry ) - printf( "Out of topological order!!!\n" ); - assert( iPrev < Entry ); - iPrev = Entry; + iPrev = 0; + Vec_IntForEachEntry( vUsed, Entry, i ) + { + if ( iPrev >= Entry ) + printf( "Out of topological order!!!\n" ); + assert( iPrev < Entry ); + iPrev = Entry; + } } return vUsed; } @@ -253,7 +195,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h SeeAlso [] ***********************************************************************/ -void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed ) +void Proof_CollectUsed_rec( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed ) { satset * pNext, * pNode = Proof_NodeRead( vProof, hNode ); int i; @@ -277,19 +219,14 @@ void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot ) +Vec_Int_t * Proof_CollectUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots ) { Vec_Int_t * vUsed; - assert( (hRoot > 0) ^ (vRoots != NULL) ); + int i, Entry; vUsed = Vec_IntAlloc( 1000 ); - if ( hRoot ) - Proof_CollectUsed_rec( vProof, hRoot, vUsed ); - else - { - int i, Entry; - Vec_IntForEachEntry( vRoots, Entry, i ) + Vec_IntForEachEntry( vRoots, Entry, i ) + if ( Entry >= 0 ) Proof_CollectUsed_rec( vProof, Entry, vUsed ); - } return vUsed; } @@ -307,7 +244,7 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR SeeAlso [] ***********************************************************************/ -void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited ) +void Sat_ProofReduceCheck_rec( Vec_Set_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited ) { satset * pFanin; int k; @@ -323,7 +260,7 @@ void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset } void Sat_ProofReduceCheckOne( sat_solver2 * s, int iLearnt, Vec_Ptr_t * vVisited ) { - Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs; int hProofNode = Vec_IntEntry( vRoots, iLearnt ); @@ -357,26 +294,24 @@ void Sat_ProofReduceCheck( sat_solver2 * s ) ***********************************************************************/ void Sat_ProofReduce( sat_solver2 * s ) { - Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs; Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; int fVerbose = 0; Vec_Int_t * vUsed; satset * pNode, * pFanin; - int i, k, hTemp, hNewHandle = 1, clk = clock(); + int i, k, hTemp, clk = clock(); static int TimeTotal = 0; // collect visited nodes - vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 ); -// printf( "The proof uses %d out of %d proof nodes (%.2f %%)\n", -// Vec_IntSize(vUsed), Proof_CountAll(vProof), -// 100.0 * Vec_IntSize(vUsed) / Proof_CountAll(vProof) ); + vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); // relabel nodes to use smaller space + Vec_SetShrinkS( vProof, 1 ); Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) { - pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts); + pNode->Id = Vec_SetAppendS( vProof, 2+pNode->nEnts ); Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) if ( (pNode->pEnts[k] & 1) == 0 ) // proof node pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); @@ -384,26 +319,27 @@ void Sat_ProofReduce( sat_solver2 * s ) assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); } // update roots - Proof_ForeachNodeVec( vRoots, vProof, pNode, i ) + Proof_ForeachNodeVec1( vRoots, vProof, pNode, i ) Vec_IntWriteEntry( vRoots, i, pNode->Id ); // compact the nodes Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) { hTemp = pNode->Id; pNode->Id = 0; - memmove( Vec_IntArray(vProof) + hTemp, pNode, sizeof(int)*Proof_NodeSize(pNode->nEnts) ); + memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) ); } + Vec_SetWriteEntryNum( vProof, Vec_IntSize(vUsed) ); Vec_IntFree( vUsed ); // report the result if ( fVerbose ) { - printf( "The proof was reduced from %10d to %10d integers (by %6.2f %%) ", - Vec_IntSize(vProof), hNewHandle, 100.0 * (Vec_IntSize(vProof) - hNewHandle) / Vec_IntSize(vProof) ); + printf( "The proof was reduced from %6.2f Mb to %6.2f Mb (by %6.2f %%) ", + 1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20), + 100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) ); TimeTotal += clock() - clk; Abc_PrintTime( 1, "Time", TimeTotal ); } - Vec_IntShrink( vProof, hNewHandle ); - + Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) ); Sat_ProofReduceCheck( s ); } @@ -419,7 +355,7 @@ void Sat_ProofReduce( sat_solver2 * s ) SeeAlso [] ***********************************************************************/ -int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) +int Sat_ProofCheckResolveOne( Vec_Set_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) { satset * c; int h, i, k, Var = -1, Count = 0; @@ -452,9 +388,9 @@ int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t if ( (c2->pEnts[i] >> 1) != Var ) Vec_IntPushUnique( vTemp, c2->pEnts[i] ); // create new resolution entry - h = Vec_RecPush( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) ); + h = Vec_SetAppend( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) ); // return the new entry - c = Proof_ResolveRead( p, h ); + c = Proof_NodeRead( p, h ); c->nEnts = Vec_IntSize(vTemp)-2; return h; } @@ -470,15 +406,15 @@ int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t SeeAlso [] ***********************************************************************/ -satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Rec_t * vResolves, int iAnt ) +satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Set_t * vResolves, int iAnt ) { satset * pAnt; if ( iAnt & 1 ) - return Proof_NodeRead( vClauses, iAnt >> 2 ); + return Proof_ClauseRead( vClauses, iAnt >> 2 ); assert( iAnt > 0 ); pAnt = Proof_NodeRead( vProof, iAnt >> 2 ); assert( pAnt->Id > 0 ); - return Proof_ResolveRead( vResolves, pAnt->Id ); + return Proof_NodeRead( vResolves, pAnt->Id ); } /**Function************************************************************* @@ -495,24 +431,21 @@ satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Re void Sat_ProofCheck( sat_solver2 * s ) { Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; - Vec_Rec_t * vResolves; + Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; + Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; + Vec_Set_t * vResolves; Vec_Int_t * vUsed, * vTemp; satset * pSet, * pSet0, * pSet1; int i, k, hRoot, Handle, Counter = 0, clk = clock(); -// if ( s->hLearntLast < 0 ) -// return; -// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; hRoot = s->hProofLast; if ( hRoot == -1 ) return; - // collect visited clauses - vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); Proof_CleanCollected( vProof, vUsed ); // perform resolution steps vTemp = Vec_IntAlloc( 1000 ); - vResolves = Vec_RecAlloc(); + vResolves = Vec_SetAlloc(); Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) { pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); @@ -520,25 +453,23 @@ void Sat_ProofCheck( sat_solver2 * s ) { pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); Handle = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp ); - pSet0 = Proof_ResolveRead( vResolves, Handle ); + pSet0 = Proof_NodeRead( vResolves, Handle ); } pSet->Id = Handle; -//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) ); -//satset_print( pSet0 ); Counter++; } Vec_IntFree( vTemp ); // clean the proof Proof_CleanCollected( vProof, vUsed ); // compare the final clause - printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_RecSize(vResolves) / (1<<20) ); + printf( "Used %6.2f Mb for resolvents.\n", 1.0 * Vec_SetMemory(vResolves) / (1<<20) ); if ( pSet0->nEnts > 0 ) printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts ); else printf( "Proof verification successful. " ); Abc_PrintTime( 1, "Time", clock() - clk ); // cleanup - Vec_RecFree( vResolves ); + Vec_SetFree( vResolves ); Vec_IntFree( vUsed ); } @@ -554,7 +485,7 @@ void Sat_ProofCheck( sat_solver2 * s ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed, int fUseIds ) +Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Int_t * vUsed, int fUseIds ) { Vec_Int_t * vCore; satset * pNode, * pFanin; @@ -571,12 +502,11 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ } } // clean core clauses and reexpress core in terms of clause IDs - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) { assert( (int*)pNode < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); pNode->mark = 0; if ( fUseIds ) -// Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); Vec_IntWriteEntry( vCore, i, pNode->Id ); } return vCore; @@ -644,8 +574,9 @@ void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars ) void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) { Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; + Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; satset * pNode, * pFanin; Aig_Man_t * pAig; @@ -661,7 +592,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) Sat_ProofInterpolantCheckVars( s, vGlobVars ); // collect visited nodes - vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); // collect core clauses (cleans vUsed and vCore) vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 ); @@ -678,7 +609,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) // copy the numbers out and derive interpol for clause vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) { if ( pNode->partA ) { @@ -719,7 +650,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) Aig_ManCleanup( pAig ); // move the results back - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) pNode->Id = Vec_IntEntry( vCoreNums, i ); Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) pNode->Id = 0; @@ -745,8 +676,9 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) { Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; + Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; satset * pNode, * pFanin; Tru_Man_t * pTru; @@ -755,9 +687,6 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) word * pRes = ABC_ALLOC( word, nWords ); int i, k, iVar, Lit, Entry, hRoot; assert( nVars > 0 && nVars <= 16 ); -// if ( s->hLearntLast < 0 ) -// return NULL; -// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; hRoot = s->hProofLast; if ( hRoot == -1 ) return NULL; @@ -765,7 +694,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) Sat_ProofInterpolantCheckVars( s, vGlobVars ); // collect visited nodes - vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); // collect core clauses (cleans vUsed and vCore) vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 ); @@ -779,7 +708,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) // copy the numbers out and derive interpol for clause vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) { if ( pNode->partA ) { @@ -808,7 +737,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) { // assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) ); - assert( pFanin->Id <= Tru_ManHandleMax(pTru) ); +// assert( pFanin->Id <= Tru_ManHandleMax(pTru) ); if ( k == 0 ) // pObj = Aig_ObjFromLit( pAig, pFanin->Id ); pRes = Tru_ManCopyNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 ); @@ -829,7 +758,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) // Aig_ManCleanup( pAig ); // move the results back - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) pNode->Id = Vec_IntEntry( vCoreNums, i ); Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) pNode->Id = 0; @@ -856,18 +785,15 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) void * Sat_ProofCore( sat_solver2 * s ) { Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; + Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; Vec_Int_t * vCore, * vUsed; int hRoot; -// if ( s->hLearntLast < 0 ) -// return NULL; -// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; hRoot = s->hProofLast; if ( hRoot == -1 ) return NULL; - // collect visited clauses - vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 ); // collect core clauses vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 ); Vec_IntFree( vUsed ); diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 8a3cbc33..181d152a 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -71,11 +71,6 @@ static inline int irand(double* seed, int size) { //================================================================================================= -// Predeclarations: - -static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)); - -//================================================================================================= // Variable datatype + minor functions: static const int var0 = 1; @@ -90,12 +85,12 @@ struct varinfo_t unsigned lev : 28; // variable level }; -static inline int var_level (sat_solver* s, int v) { return s->levels[v]; } -static inline int var_value (sat_solver* s, int v) { return s->assigns[v]; } +static inline int var_level (sat_solver* s, int v) { return s->levels[v]; } +static inline int var_value (sat_solver* s, int v) { return s->assigns[v]; } static inline int var_polar (sat_solver* s, int v) { return s->polarity[v]; } -static inline void var_set_level (sat_solver* s, int v, int lev) { s->levels[v] = lev; } -static inline void var_set_value (sat_solver* s, int v, int val) { s->assigns[v] = val; } +static inline void var_set_level (sat_solver* s, int v, int lev) { s->levels[v] = lev; } +static inline void var_set_value (sat_solver* s, int v, int val) { s->assigns[v] = val; } static inline void var_set_polar (sat_solver* s, int v, int pol) { s->polarity[v] = pol; } // variable tags @@ -130,7 +125,7 @@ int sat_solver_get_var_value(sat_solver* s, int v) assert( 0 ); return 0; } - + //================================================================================================= // Clause datatype + minor functions: @@ -140,6 +135,8 @@ struct clause_t lit lits[0]; }; +static inline clause* clause_read (sat_solver* s, int h) { return (clause *)Vec_SetEntry(&s->Mem, h>>1); } + static inline int clause_nlits (clause* c) { return c->size_learnt >> 1; } static inline lit* clause_begin (clause* c) { return c->lits; } static inline int clause_learnt (clause* c) { return c->size_learnt & 1; } @@ -155,21 +152,18 @@ static inline void clause_print (clause* c) { printf( "}\n" ); } -static inline clause* clause_read( sat_solver* s, int h ) { return (clause *)Vec_RecEntryP(&s->Mem, h); } -static inline int clause_size( int nLits, int fLearnt ) { int a = nLits + fLearnt + 1; return a + (a & 1); } - //================================================================================================= // Encode literals in clause pointers: -static inline int clause_from_lit (lit l) { return l + l + 1; } -static inline int clause_is_lit (int h) { return (h & 1); } -static inline lit clause_read_lit (int h) { return (lit)(h >> 1); } +static inline int clause_from_lit (lit l) { return l + l + 1; } +static inline int clause_is_lit (int h) { return (h & 1); } +static inline lit clause_read_lit (int h) { return (lit)(h >> 1); } //================================================================================================= // Simple helpers: -static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); } -static inline veci* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } +static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); } +static inline veci* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } //================================================================================================= // Variable order functions: @@ -418,15 +412,6 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void } } -void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)) -{ -// int i; - double seed = 91648253; - sortrnd(array,size,comp,&seed); -// for ( i = 1; i < size; i++ ) -// assert(comp(array[i-1], array[i])<0); -} - //================================================================================================= // Clause functions: @@ -451,9 +436,9 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) } // create new clause - h = Vec_RecAppend( &s->Mem, clause_size(size, learnt) ); - c = clause_read( s, h ); + h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 ) << 1; assert( !(h & 1) ); + c = clause_read( s, h ); if ( s->hLearnts == -1 && learnt ) s->hLearnts = h; c->size_learnt = (size << 1) | learnt; @@ -927,9 +912,9 @@ sat_solver* sat_solver_new(void) { sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver)); - Vec_RecAlloc_(&s->Mem); + Vec_SetAlloc_(&s->Mem); s->hLearnts = -1; - s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) ); + s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1; s->binary = clause_read( s, s->hBinary ); s->binary->size_learnt = (2 << 1); @@ -1049,7 +1034,7 @@ void sat_solver_setnvars(sat_solver* s,int n) void sat_solver_delete(sat_solver* s) { - Vec_RecFree_( &s->Mem ); + Vec_SetFree_( &s->Mem ); // delete vectors veci_delete(&s->order); @@ -1087,10 +1072,10 @@ void sat_solver_delete(sat_solver* s) void sat_solver_rollback( sat_solver* s ) { int i; - Vec_RecRestart( &s->Mem ); + Vec_SetRestart( &s->Mem ); s->hLearnts = -1; - s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) ); + s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1; s->binary = clause_read( s, s->hBinary ); s->binary->size_learnt = (2 << 1); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 30b3742b..de102227 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <assert.h> #include "satVec.h" -#include "vecRec.h" +#include "vecSet.h" ABC_NAMESPACE_HEADER_START @@ -92,7 +92,7 @@ struct sat_solver_t int qtail; // Tail index of queue. // clauses - Vec_Rec_t Mem; + Vec_Set_t Mem; int hLearnts; // the first learnt clause int hBinary; // the special binary clause clause * binary; diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 5a54a64e..34908f13 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -172,10 +172,12 @@ static inline void proof_chain_start( sat_solver2* s, satset* c ) { if ( s->fProofLogging ) { - s->iStartChain = veci_size(&s->proofs); - veci_push(&s->proofs, 0); - veci_push(&s->proofs, 0); - veci_push(&s->proofs, clause_proofid(s, c, 0) ); + int ProofId = clause_proofid(s, c, 0); + assert( ProofId > 0 ); + veci_resize( &s->temp_proof, 0 ); + veci_push( &s->temp_proof, 0 ); + veci_push( &s->temp_proof, 0 ); + veci_push( &s->temp_proof, ProofId ); } } @@ -183,12 +185,10 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var ) { if ( s->fProofLogging ) { -// int CapOld = (&s->proofs)->cap; satset* c = cls ? cls : var_unit_clause( s, Var ); - veci_push(&s->proofs, clause_proofid(s, c, var_is_partA(s,Var)) ); -// printf( "%d %d ", clause_proofid(s, c), Var ); -// if ( (&s->proofs)->cap > CapOld ) -// printf( "Resized proof from %d to %d.\n", CapOld, (&s->proofs)->cap ); + int ProofId = clause_proofid(s, c, var_is_partA(s,Var)); + assert( ProofId > 0 ); + veci_push( &s->temp_proof, ProofId ); } } @@ -196,12 +196,10 @@ static inline int proof_chain_stop( sat_solver2* s ) { if ( s->fProofLogging ) { - int RetValue = s->iStartChain; - satset* c = (satset*)(veci_begin(&s->proofs) + s->iStartChain); - assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proofs) ); - c->nEnts = veci_size(&s->proofs) - s->iStartChain - 2; - s->iStartChain = 0; - return RetValue; + int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) ); + satset * c = (satset *)Vec_SetEntry( &s->Proofs, h ); + c->nEnts = veci_size(&s->temp_proof) - 2; + return h; } return 0; } @@ -1119,20 +1117,6 @@ sat_solver2* sat_solver2_new(void) { sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) ); - // initialize vectors - veci_new(&s->order); - veci_new(&s->trail_lim); - veci_new(&s->tagged); - veci_new(&s->stack); - veci_new(&s->temp_clause); - veci_new(&s->conf_final); - veci_new(&s->mark_levels); - veci_new(&s->min_lit_order); - veci_new(&s->min_step_order); - veci_new(&s->learnt_live); - veci_new(&s->claActs); veci_push(&s->claActs, -1); - veci_new(&s->claProofs); veci_push(&s->claProofs, -1); - #ifdef USE_FLOAT_ACTIVITY2 s->var_inc = 1; s->cla_inc = 1; @@ -1156,6 +1140,23 @@ sat_solver2* sat_solver2_new(void) s->nLearntMax = 0; s->fVerbose = 0; + // initialize vectors + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); + veci_new(&s->stack); + veci_new(&s->temp_clause); + veci_new(&s->temp_proof); + veci_new(&s->conf_final); + veci_new(&s->mark_levels); + veci_new(&s->min_lit_order); + veci_new(&s->min_step_order); + veci_new(&s->learnt_live); + veci_new(&s->claActs); veci_push(&s->claActs, -1); + veci_new(&s->claProofs); veci_push(&s->claProofs, -1); + if ( s->fProofLogging ) + Vec_SetAlloc_( &s->Proofs ); + // prealloc clause assert( !s->clauses.ptr ); s->clauses.cap = (1 << 20); @@ -1166,21 +1167,17 @@ sat_solver2* sat_solver2_new(void) s->learnts.cap = (1 << 20); s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap ); veci_push(&s->learnts, -1); - // prealloc proofs - if ( s->fProofLogging ) - { - assert( !s->proofs.ptr ); - s->proofs.cap = (1 << 20); - s->proofs.ptr = ABC_ALLOC( int, s->proofs.cap ); - veci_push(&s->proofs, -1); - } + // initialize clause pointers - s->hLearntLast = -1; // the last learnt clause - s->hProofLast = -1; // the last proof ID - s->hClausePivot = 1; // the pivot among clauses - s->hLearntPivot = 1; // the pivot moang learned clauses - s->iVarPivot = 0; // the pivot among the variables - s->iSimpPivot = 0; // marker of unit-clauses + s->hLearntLast = -1; // the last learnt clause + s->hProofLast = -1; // the last proof ID + // initialize rollback + s->iVarPivot = 0; // the pivot for variables + s->iTrailPivot = 0; // the pivot for trail + s->iProofPivot = 0; // the pivot for proof records + s->hClausePivot = 1; // the pivot for problem clause + s->hLearntPivot = 1; // the pivot for learned clause + s->hProofPivot = 1; // the pivot for proof records return s; } @@ -1241,35 +1238,38 @@ void sat_solver2_setnvars(sat_solver2* s,int n) void sat_solver2_delete(sat_solver2* s) { -// veci * pCore; + int fVerify = 0; + if ( fVerify ) + { + veci * 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 ); + } // 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 ); + printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 1.0 * Vec_SetMemory(&s->Proofs) / (1<<20), s->nUnits ); - if ( s->fProofLogging ) - Sat_ProofCheck( s ); -*/ // delete vectors veci_delete(&s->order); veci_delete(&s->trail_lim); veci_delete(&s->tagged); veci_delete(&s->stack); veci_delete(&s->temp_clause); + veci_delete(&s->temp_proof); veci_delete(&s->conf_final); veci_delete(&s->mark_levels); veci_delete(&s->min_lit_order); veci_delete(&s->min_step_order); veci_delete(&s->learnt_live); - veci_delete(&s->proofs); veci_delete(&s->claActs); veci_delete(&s->claProofs); veci_delete(&s->clauses); veci_delete(&s->learnts); +// veci_delete(&s->proofs); + Vec_SetFree_( &s->Proofs ); // delete arrays if (s->vi != 0){ @@ -1514,11 +1514,13 @@ void sat_solver2_rollback( sat_solver2* s ) { int i, k, j; assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); - assert( s->iSimpPivot >= 0 && s->iSimpPivot <= s->qtail ); + assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail ); + assert( s->iProofPivot >= 0 && s->iProofPivot <= Vec_SetEntryNum(&s->Proofs) ); assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) ); assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) ); + assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) ); // reset implication queue - solver2_canceluntil_rollback( s, s->iSimpPivot ); + solver2_canceluntil_rollback( s, s->iTrailPivot ); // update order if ( s->iVarPivot < s->size ) { @@ -1558,7 +1560,9 @@ void sat_solver2_rollback( sat_solver2* s ) veci_resize(&s->claActs, first->Id); if ( s->fProofLogging ) { veci_resize(&s->claProofs, first->Id); - Sat_ProofReduce( s ); + Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot); + Vec_SetShrink(&s->Proofs, s->hProofPivot); +// Sat_ProofReduce( s ); } s->stats.learnts = first->Id-1; veci_resize(&s->learnts, s->hLearntPivot); @@ -1600,12 +1604,16 @@ void sat_solver2_rollback( sat_solver2* s ) s->stats.learnts_literals = 0; s->stats.tot_literals = 0; // initialize clause pointers - s->hLearntLast = -1; // the last learnt clause - s->hProofLast = -1; // the last proof ID - s->hClausePivot = 1; // the pivot among clauses - s->hLearntPivot = 1; // the pivot among learned clauses - s->iVarPivot = 0; // the pivot among the variables - s->iSimpPivot = 0; // marker of unit-clauses + s->hLearntLast = -1; // the last learnt clause + s->hProofLast = -1; // the last proof ID + + // initialize rollback + s->iVarPivot = 0; // the pivot for variables + s->iTrailPivot = 0; // the pivot for trail + s->iProofPivot = 0; // the pivot for proof records + s->hClausePivot = 1; // the pivot for problem clause + s->hLearntPivot = 1; // the pivot for learned clause + s->hProofPivot = 1; // the pivot for proof records } } @@ -1803,7 +1811,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim printf("==============================================================================\n"); solver2_canceluntil(s,0); - assert( s->qhead == s->qtail ); +// assert( s->qhead == s->qtail ); // if ( status == l_True ) // sat_solver2_verify( s ); return status; diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 4b1eec61..ffbae964 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <assert.h> #include "satVec.h" +#include "vecSet.h" ABC_NAMESPACE_HEADER_START @@ -112,16 +113,19 @@ struct sat_solver2_t veci clauses; // clause memory veci learnts; // learnt memory veci* wlists; // watcher lists (for each literal) + veci claActs; // clause activities + veci claProofs; // clause proofs int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) - int hClausePivot; // the pivot among problem clause - int hLearntPivot; // the pivot among learned clause - int iVarPivot; // the pivot among the variables - int iSimpPivot; // marker of unit-clauses int nof_learnts; // the number of clauses to trigger reduceDB - veci claActs; // clause activities - veci claProofs; // clause proofs + // rollback + int iVarPivot; // the pivot for variables + int iTrailPivot; // the pivot for trail + int iProofPivot; // the pivot for proof records + int hClausePivot; // the pivot for problem clause + int hLearntPivot; // the pivot for learned clause + int hProofPivot; // the pivot for proof records // internal state varinfo2 * vi; // variable information @@ -146,8 +150,8 @@ struct sat_solver2_t veci learnt_live; // remaining clauses after reduce DB // proof logging - veci proofs; // sequence of proof records - int iStartChain; // temporary variable to remember beginning of the current chain in proof logging + Vec_Set_t Proofs; // sequence of proof records + veci temp_proof; // temporary place to store proofs int nUnits; // the total number of unit clauses // statistics @@ -251,10 +255,12 @@ static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax) static inline void sat_solver2_bookmark(sat_solver2* s) { assert( s->qhead == s->qtail ); - s->hLearntPivot = veci_size(&s->learnts); - s->hClausePivot = veci_size(&s->clauses); s->iVarPivot = s->size; - s->iSimpPivot = s->qhead; + s->iTrailPivot = s->qhead; + s->iProofPivot = Vec_SetEntryNum(&s->Proofs); + s->hClausePivot = veci_size(&s->clauses); + s->hLearntPivot = veci_size(&s->learnts); + s->hProofPivot = Vec_SetHandCurrent(&s->Proofs); } static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) diff --git a/src/sat/bsat/satSolver_old.c b/src/sat/bsat/satSolver_old.c deleted file mode 100644 index 4d851d0f..00000000 --- a/src/sat/bsat/satSolver_old.c +++ /dev/null @@ -1,1766 +0,0 @@ -/************************************************************************************************** -MiniSat -- Copyright (c) 2005, Niklas Sorensson -http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ -// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko - -#include <stdio.h> -#include <assert.h> -#include <string.h> -#include <math.h> - -#include "satSolver.h" -#include "satStore.h" - -ABC_NAMESPACE_IMPL_START - -//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT -#define SAT_USE_ANALYZE_FINAL - -//================================================================================================= -// Debug: - -//#define VERBOSEDEBUG - -// For derivation output (verbosity level 2) -#define L_IND "%-*d" -#define L_ind sat_solver_dl(s)*2+2,sat_solver_dl(s) -#define L_LIT "%sx%d" -#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) - -// Just like 'assert()' but expression will be evaluated in the release version as well. -static inline void check(int expr) { assert(expr); } - -static void printlits(lit* begin, lit* end) -{ - int i; - for (i = 0; i < end - begin; i++) - printf(L_LIT" ",L_lit(begin[i])); -} - -//================================================================================================= -// Random numbers: - - -// Returns a random float 0 <= x < 1. Seed must never be 0. -static inline double drand(double* seed) { - int q; - *seed *= 1389796; - q = (int)(*seed / 2147483647); - *seed -= (double)q * 2147483647; - return *seed / 2147483647; } - - -// Returns a random integer 0 <= x < size. Seed must never be 0. -static inline int irand(double* seed, int size) { - return (int)(drand(seed) * size); } - - -//================================================================================================= -// Predeclarations: - -static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)); - -//================================================================================================= -// Clause datatype + minor functions: - -struct clause_t -{ - int size_learnt; - lit lits[0]; -}; - -static inline int clause_size (clause* c) { return c->size_learnt >> 1; } -static inline lit* clause_begin (clause* c) { return c->lits; } -static inline int clause_learnt (clause* c) { return c->size_learnt & 1; } -static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); } -static inline unsigned clause_activity2 (clause* c) { return *((unsigned*)&c->lits[c->size_learnt>>1]); } -static inline void clause_setactivity (clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } -static inline void clause_setactivity2 (clause* c, unsigned a) { *((unsigned*)&c->lits[c->size_learnt>>1]) = a; } -static inline void clause_print (clause* c) { - int i; - printf( "{ " ); - for ( i = 0; i < clause_size(c); i++ ) - printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 ); - printf( "}\n" ); -} - -//================================================================================================= -// Encode literals in clause pointers: - -static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); } -static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); } -static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); } - -//================================================================================================= -// Simple helpers: - -static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); } -static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } - -//================================================================================================= -// Variable order functions: - -static inline void order_update(sat_solver* s, int v) // updateorder -{ - int* orderpos = s->orderpos; - int* heap = veci_begin(&s->order); - int i = orderpos[v]; - int x = heap[i]; - int parent = (i - 1) / 2; - - assert(s->orderpos[v] != -1); - - while (i != 0 && s->activity[x] > s->activity[heap[parent]]){ - heap[i] = heap[parent]; - orderpos[heap[i]] = i; - i = parent; - parent = (i - 1) / 2; - } - heap[i] = x; - orderpos[x] = i; -} - -static inline void order_assigned(sat_solver* s, int v) -{ -} - -static inline void order_unassigned(sat_solver* s, int v) // undoorder -{ - int* orderpos = s->orderpos; - if (orderpos[v] == -1){ - orderpos[v] = veci_size(&s->order); - veci_push(&s->order,v); - order_update(s,v); -//printf( "+%d ", v ); - } -} - -static inline int order_select(sat_solver* s, float random_var_freq) // selectvar -{ - int* heap; - int* orderpos; - - lbool* values = s->assigns; - - // Random decision: - if (drand(&s->random_seed) < random_var_freq){ - int next = irand(&s->random_seed,s->size); - assert(next >= 0 && next < s->size); - if (values[next] == l_Undef) - return next; - } - - // Activity based decision: - - heap = veci_begin(&s->order); - orderpos = s->orderpos; - - - while (veci_size(&s->order) > 0){ - int next = heap[0]; - int size = veci_size(&s->order)-1; - int x = heap[size]; - - veci_resize(&s->order,size); - - orderpos[next] = -1; - - if (size > 0){ - - int i = 0; - int child = 1; - - - while (child < size){ - if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]]) - child++; - - assert(child < size); - - if (s->activity[x] >= s->activity[heap[child]]) - break; - - heap[i] = heap[child]; - orderpos[heap[i]] = i; - i = child; - child = 2 * child + 1; - } - heap[i] = x; - orderpos[heap[i]] = i; - } - -//printf( "-%d ", next ); - if (values[next] == l_Undef) - return next; - } - - return var_Undef; -} - -//================================================================================================= -// Activity functions: - -#ifdef USE_FLOAT_ACTIVITY - -static inline void act_var_rescale(sat_solver* s) { - double* activity = s->activity; - int i; - for (i = 0; i < s->size; i++) - activity[i] *= 1e-100; - s->var_inc *= 1e-100; -} -static inline void act_clause_rescale(sat_solver* s) { - static int Total = 0; - clause** cs = (clause**)vecp_begin(&s->learnts); - int i, clk = clock(); - for (i = 0; i < vecp_size(&s->learnts); i++){ - float a = clause_activity(cs[i]); - clause_setactivity(cs[i], a * (float)1e-20); - } - s->cla_inc *= (float)1e-20; - - Total += clock() - clk; - printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts ); - Abc_PrintTime( 1, "Time", Total ); -} -static inline void act_var_bump(sat_solver* s, int v) { - s->activity[v] += s->var_inc; - if (s->activity[v] > 1e100) - act_var_rescale(s); - if (s->orderpos[v] != -1) - order_update(s,v); -} -static inline void act_var_bump_global(sat_solver* s, int v) { - s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]); - if (s->activity[v] > 1e100) - act_var_rescale(s); - if (s->orderpos[v] != -1) - order_update(s,v); -} -static inline void act_var_bump_factor(sat_solver* s, int v) { - s->activity[v] += (s->var_inc * s->factors[v]); - if (s->activity[v] > 1e100) - act_var_rescale(s); - if (s->orderpos[v] != -1) - order_update(s,v); -} -static inline void act_clause_bump(sat_solver* s, clause *c) { - float a = clause_activity(c) + s->cla_inc; - clause_setactivity(c,a); - if (a > 1e20) act_clause_rescale(s); -} -static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } -static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; } - -#else - -static inline void act_var_rescale(sat_solver* s) { - unsigned* activity = s->activity; - int i; - for (i = 0; i < s->size; i++) - activity[i] >>= 19; - s->var_inc >>= 19; - s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) ); -} -static inline void act_clause_rescale(sat_solver* s) { - static int Total = 0; - clause** cs = (clause**)vecp_begin(&s->learnts); - int i, clk = clock(); - for (i = 0; i < vecp_size(&s->learnts); i++){ - unsigned a = clause_activity2(cs[i]); - clause_setactivity2(cs[i], a >> 14); - } - s->cla_inc >>= 14; - s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); - -// Total += clock() - clk; -// printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts ); -// Abc_PrintTime( 1, "Time", Total ); -} -static inline void act_var_bump(sat_solver* s, int v) { - s->activity[v] += s->var_inc; - if (s->activity[v] & 0x80000000) - act_var_rescale(s); - if (s->orderpos[v] != -1) - order_update(s,v); -} -static inline void act_var_bump_global(sat_solver* s, int v) {} -static inline void act_var_bump_factor(sat_solver* s, int v) {} -static inline void act_clause_bump(sat_solver* s, clause*c) { - unsigned a = clause_activity2(c) + s->cla_inc; - clause_setactivity2(c,a); - if (a & 0x80000000) - act_clause_rescale(s); -} -static inline void act_var_decay(sat_solver* s) { s->var_inc += (s->var_inc >> 4); } -static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); } - -#endif - - -//================================================================================================= -// Clause functions: - -/* pre: size > 1 && no variable occurs twice - */ -static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) -{ - int size; - clause* c; - int i; - - assert(end - begin > 1); - assert(learnt >= 0 && learnt < 2); - size = end - begin; - - // do not allocate memory for the two-literal problem clause - if ( size == 2 && !learnt ) - { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1]))); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0]))); - return NULL; - } - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); -#else - c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); -#endif - - c->size_learnt = (size << 1) | learnt; - assert(((ABC_PTRUINT_T)c & 1) == 0); - - for (i = 0; i < size; i++) - c->lits[i] = begin[i]; - - if (learnt) - *((float*)&c->lits[size]) = 0.0; - - assert(begin[0] >= 0); - assert(begin[0] < s->size*2); - assert(begin[1] >= 0); - assert(begin[1] < s->size*2); - - assert(lit_neg(begin[0]) < s->size*2); - assert(lit_neg(begin[1]) < s->size*2); - - //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); - //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); - - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); - - return c; -} - - -//================================================================================================= -// Minor (solver) functions: - -static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from) -{ - lbool* values = s->assigns; - int v = lit_var(l); - lbool val = values[v]; - lbool sig; -#ifdef VERBOSEDEBUG - printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); -#endif - - sig = !lit_sign(l); sig += sig - 1; - if (val != l_Undef){ - return val == sig; - }else{ - int* levels = s->levels; - clause** reasons = s->reasons; - // New fact -- store it. -#ifdef VERBOSEDEBUG - printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); -#endif - values [v] = sig; - levels [v] = sat_solver_dl(s); - reasons[v] = from; - s->trail[s->qtail++] = l; - - order_assigned(s, v); - return true; - } -} - - -static inline int sat_solver_assume(sat_solver* s, lit l){ - assert(s->qtail == s->qhead); - assert(s->assigns[lit_var(l)] == l_Undef); -#ifdef VERBOSEDEBUG - printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l)); - printf( "act = %.20f\n", s->activity[lit_var(l)] ); -#endif - veci_push(&s->trail_lim,s->qtail); - return sat_solver_enqueue(s,l,(clause*)0); -} - - -static void sat_solver_canceluntil(sat_solver* s, int level) { - lit* trail; - lbool* values; - clause** reasons; - int bound; - int lastLev; - int c; - - if (sat_solver_dl(s) <= level) - return; - - trail = s->trail; - values = s->assigns; - reasons = s->reasons; - bound = (veci_begin(&s->trail_lim))[level]; - lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; - - //////////////////////////////////////// - // added to cancel all assignments -// if ( level == -1 ) -// bound = 0; - //////////////////////////////////////// - - for (c = s->qtail-1; c >= bound; c--) { - int x = lit_var(trail[c]); - values [x] = l_Undef; - reasons[x] = (clause*)0; - if ( c < lastLev ) - s->polarity[x] = !lit_sign(trail[c]); - } - - for (c = s->qhead-1; c >= bound; c--) - order_unassigned(s,lit_var(trail[c])); - - s->qhead = s->qtail = bound; - veci_resize(&s->trail_lim,level); -} - -static void sat_solver_record(sat_solver* s, veci* cls) -{ - lit* begin = veci_begin(cls); - lit* end = begin + veci_size(cls); - clause* c = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0; - sat_solver_enqueue(s,*begin,c); - - /////////////////////////////////// - // add clause to internal storage - if ( s->pStore ) - { - int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); - assert( RetValue ); - } - /////////////////////////////////// - - assert(veci_size(cls) > 0); - - if (c != 0) { - vecp_push(&s->learnts,c); - act_clause_bump(s,c); - s->stats.learnts++; - s->stats.learnts_literals += veci_size(cls); - } -} - - -static double sat_solver_progress(sat_solver* s) -{ - lbool* values = s->assigns; - int* levels = s->levels; - int i; - - double progress = 0; - double F = 1.0 / s->size; - for (i = 0; i < s->size; i++) - if (values[i] != l_Undef) - progress += pow(F, levels[i]); - return progress / s->size; -} - -//================================================================================================= -// Major methods: - -static int sat_solver_lit_removable(sat_solver* s, lit l, int minl) -{ - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; - int top = veci_size(&s->tagged); - - assert(lit_var(l) >= 0 && lit_var(l) < s->size); - assert(reasons[lit_var(l)] != 0); - veci_resize(&s->stack,0); - veci_push(&s->stack,lit_var(l)); - - while (veci_size(&s->stack) > 0){ - clause* c; - int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; - assert(v >= 0 && v < s->size); - veci_resize(&s->stack,veci_size(&s->stack)-1); - assert(reasons[v] != 0); - c = reasons[v]; - - if (clause_is_lit(c)){ - int v = lit_var(clause_read_lit(c)); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - veci_push(&s->stack,v); - tags[v] = l_True; - veci_push(&s->tagged,v); - }else{ - int* tagged = veci_begin(&s->tagged); - int j; - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return false; - } - } - }else{ - lit* lits = clause_begin(c); - int i, j; - - for (i = 1; i < clause_size(c); i++){ - int v = lit_var(lits[i]); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - - veci_push(&s->stack,lit_var(lits[i])); - tags[v] = l_True; - veci_push(&s->tagged,v); - }else{ - int* tagged = veci_begin(&s->tagged); - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return false; - } - } - } - } - } - - return true; -} - - -/*_________________________________________________________________________________________________ -| -| analyzeFinal : (p : Lit) -> [void] -| -| Description: -| Specialized analysis procedure to express the final conflict in terms of assumptions. -| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and -| stores the result in 'out_conflict'. -|________________________________________________________________________________________________@*/ -/* -void Solver::analyzeFinal(Clause* confl, bool skip_first) -{ - // -- NOTE! This code is relatively untested. Please report bugs! - conflict.clear(); - if (root_level == 0) return; - - vec<char>& seen = analyze_seen; - for (int i = skip_first ? 1 : 0; i < confl->size(); i++){ - Var x = var((*confl)[i]); - if (level[x] > 0) - seen[x] = 1; - } - - int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level]; - for (int i = start; i >= trail_lim[0]; i--){ - Var x = var(trail[i]); - if (seen[x]){ - GClause r = reason[x]; - if (r == GClause_NULL){ - assert(level[x] > 0); - conflict.push(~trail[i]); - }else{ - if (r.isLit()){ - Lit p = r.lit(); - if (level[var(p)] > 0) - seen[var(p)] = 1; - }else{ - Clause& c = *r.clause(); - for (int j = 1; j < c.size(); j++) - if (level[var(c[j])] > 0) - seen[var(c[j])] = 1; - } - } - seen[x] = 0; - } - } -} -*/ - -#ifdef SAT_USE_ANALYZE_FINAL - -static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first) -{ - int i, j, start; - veci_resize(&s->conf_final,0); - if ( s->root_level == 0 ) - return; - assert( veci_size(&s->tagged) == 0 ); -// assert( s->tags[lit_var(p)] == l_Undef ); -// s->tags[lit_var(p)] = l_True; - for (i = skip_first ? 1 : 0; i < clause_size(conf); i++) - { - int x = lit_var(clause_begin(conf)[i]); - if (s->levels[x] > 0) - { - s->tags[x] = l_True; - veci_push(&s->tagged,x); - } - } - - start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level]; - for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){ - int x = lit_var(s->trail[i]); - if (s->tags[x] == l_True){ - if (s->reasons[x] == NULL){ - assert(s->levels[x] > 0); - veci_push(&s->conf_final,lit_neg(s->trail[i])); - }else{ - clause* c = s->reasons[x]; - if (clause_is_lit(c)){ - lit q = clause_read_lit(c); - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (s->levels[lit_var(q)] > 0) - { - s->tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - } - } - else{ - int* lits = clause_begin(c); - for (j = 1; j < clause_size(c); j++) - if (s->levels[lit_var(lits[j])] > 0) - { - s->tags[lit_var(lits[j])] = l_True; - veci_push(&s->tagged,lit_var(lits[j])); - } - } - } - } - } - for (i = 0; i < veci_size(&s->tagged); i++) - s->tags[veci_begin(&s->tagged)[i]] = l_Undef; - veci_resize(&s->tagged,0); -} - -#endif - - -static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) -{ - lit* trail = s->trail; - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; - int cnt = 0; - lit p = lit_Undef; - int ind = s->qtail-1; - lit* lits; - int i, j, minl; - int* tagged; - - veci_push(learnt,lit_Undef); - - do{ - assert(c != 0); - - if (clause_is_lit(c)){ - lit q = clause_read_lit(c); - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - act_var_bump(s,lit_var(q)); - if (levels[lit_var(q)] == sat_solver_dl(s)) - cnt++; - else - veci_push(learnt,q); - } - }else{ - - if (clause_learnt(c)) - act_clause_bump(s,c); - - lits = clause_begin(c); - //printlits(lits,lits+clause_size(c)); printf("\n"); - for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ - lit q = lits[j]; - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - act_var_bump(s,lit_var(q)); - if (levels[lit_var(q)] == sat_solver_dl(s)) - cnt++; - else - veci_push(learnt,q); - } - } - } - - while (tags[lit_var(trail[ind--])] == l_Undef); - - p = trail[ind+1]; - c = reasons[lit_var(p)]; - cnt--; - - }while (cnt > 0); - - *veci_begin(learnt) = lit_neg(p); - - lits = veci_begin(learnt); - minl = 0; - for (i = 1; i < veci_size(learnt); i++){ - int lev = levels[lit_var(lits[i])]; - minl |= 1 << (lev & 31); - } - - // simplify (full) - for (i = j = 1; i < veci_size(learnt); i++){ - if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl)) - lits[j++] = lits[i]; - } - - // update size of learnt + statistics - veci_resize(learnt,j); - s->stats.tot_literals += j; - - // clear tags - tagged = veci_begin(&s->tagged); - for (i = 0; i < veci_size(&s->tagged); i++) - tags[tagged[i]] = l_Undef; - veci_resize(&s->tagged,0); - -#ifdef DEBUG - for (i = 0; i < s->size; i++) - assert(tags[i] == l_Undef); -#endif - -#ifdef VERBOSEDEBUG - printf(L_IND"Learnt {", L_ind); - for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); -#endif - if (veci_size(learnt) > 1){ - int max_i = 1; - int max = levels[lit_var(lits[1])]; - lit tmp; - - for (i = 2; i < veci_size(learnt); i++) - if (levels[lit_var(lits[i])] > max){ - max = levels[lit_var(lits[i])]; - max_i = i; - } - - tmp = lits[1]; - lits[1] = lits[max_i]; - lits[max_i] = tmp; - } -#ifdef VERBOSEDEBUG - { - int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; - printf(" } at level %d\n", lev); - } -#endif -} - - -clause* sat_solver_propagate(sat_solver* s) -{ - lbool* values = s->assigns; - clause* confl = (clause*)0; - lit* lits; - lit false_lit; - lbool sig; - - //printf("sat_solver_propagate\n"); - while (confl == 0 && s->qtail - s->qhead > 0){ - lit p = s->trail[s->qhead++]; - vecp* ws = sat_solver_read_wlist(s,p); - clause **begin = (clause**)vecp_begin(ws); - clause **end = begin + vecp_size(ws); - clause **i, **j; - - s->stats.propagations++; - s->simpdb_props--; - - //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); - for (i = j = begin; i < end; ){ - if (clause_is_lit(*i)){ - - int Lit = clause_read_lit(*i); - sig = !lit_sign(Lit); sig += sig - 1; - if (values[lit_var(Lit)] == sig){ - *j++ = *i++; - continue; - } - - *j++ = *i; - if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ - confl = s->binary; - (clause_begin(confl))[1] = lit_neg(p); - (clause_begin(confl))[0] = clause_read_lit(*i++); - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - }else{ - - lits = clause_begin(*i); - - // Make sure the false literal is data[1]: - false_lit = lit_neg(p); - if (lits[0] == false_lit){ - lits[0] = lits[1]; - lits[1] = false_lit; - } - assert(lits[1] == false_lit); - //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); - - // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig){ - *j++ = *i; - }else{ - // Look for new watch: - lit* stop = lits + clause_size(*i); - lit* k; - for (k = lits + 2; k < stop; k++){ - lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig){ - lits[1] = *k; - *k = false_lit; - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); - goto next; } - } - - *j++ = *i; - // Clause is unit under assignment: - if (!sat_solver_enqueue(s,lits[0], *i)){ - confl = *i++; - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - } - } - next: - i++; - } - - s->stats.inspects += j - (clause**)vecp_begin(ws); - vecp_resize(ws,j - (clause**)vecp_begin(ws)); - } - - return confl; -} - -//================================================================================================= -// External solver functions: - -sat_solver* sat_solver_new(void) -{ - sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver)); - memset( s, 0, sizeof(sat_solver) ); - - // initialize vectors - vecp_new(&s->clauses); - vecp_new(&s->learnts); - veci_new(&s->order); - veci_new(&s->trail_lim); - veci_new(&s->tagged); - veci_new(&s->stack); - veci_new(&s->model); - veci_new(&s->act_vars); - veci_new(&s->temp_clause); - veci_new(&s->conf_final); - - // initialize arrays - s->wlists = 0; - s->activity = 0; - s->factors = 0; - s->assigns = 0; - s->orderpos = 0; - s->reasons = 0; - s->levels = 0; - s->tags = 0; - s->trail = 0; - - - // initialize other vars - s->size = 0; - s->cap = 0; - s->qhead = 0; - s->qtail = 0; -#ifdef USE_FLOAT_ACTIVITY - s->var_inc = 1; - s->cla_inc = 1; - s->var_decay = (float)(1 / 0.95 ); - s->cla_decay = (float)(1 / 0.999 ); -#else - s->var_inc = (1 << 5); - s->cla_inc = (1 << 11); -#endif - s->root_level = 0; - s->simpdb_assigns = 0; - s->simpdb_props = 0; - s->random_seed = 91648253; - s->progress_estimate = 0; - s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); - s->binary->size_learnt = (2 << 1); - s->verbosity = 0; - - s->stats.starts = 0; - s->stats.decisions = 0; - s->stats.propagations = 0; - s->stats.inspects = 0; - s->stats.conflicts = 0; - s->stats.clauses = 0; - s->stats.clauses_literals = 0; - s->stats.learnts = 0; - s->stats.learnts_literals = 0; - s->stats.tot_literals = 0; - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - s->pMem = NULL; -#else - s->pMem = Sat_MmStepStart( 10 ); -#endif - return s; -} - -void sat_solver_setnvars(sat_solver* s,int n) -{ - int var; - - if (s->cap < n){ - int old_cap = s->cap; - while (s->cap < n) s->cap = s->cap*2+1; - - s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2); -#ifdef USE_FLOAT_ACTIVITY - s->activity = ABC_REALLOC(double, s->activity, s->cap); -#else - s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); -#endif - s->factors = ABC_REALLOC(double, s->factors, s->cap); - s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap); - s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); - s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap); - s->levels = ABC_REALLOC(int, s->levels, s->cap); - s->tags = ABC_REALLOC(lbool, s->tags, s->cap); - s->trail = ABC_REALLOC(lit, s->trail, s->cap); - s->polarity = ABC_REALLOC(char, s->polarity, s->cap); - memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) ); - } - - for (var = s->size; var < n; var++){ - assert(!s->wlists[2*var].size); - assert(!s->wlists[2*var+1].size); - if ( s->wlists[2*var].ptr == NULL ) - vecp_new(&s->wlists[2*var]); - if ( s->wlists[2*var+1].ptr == NULL ) - vecp_new(&s->wlists[2*var+1]); -#ifdef USE_FLOAT_ACTIVITY - s->activity[var] = 0; -#else - s->activity[var] = (1<<10); -#endif - s->factors [var] = 0; - s->assigns [var] = l_Undef; - s->orderpos [var] = veci_size(&s->order); - s->reasons [var] = (clause*)0; - s->levels [var] = 0; - s->tags [var] = l_Undef; - s->polarity [var] = 0; - - /* does not hold because variables enqueued at top level will not be reinserted in the heap - assert(veci_size(&s->order) == var); - */ - veci_push(&s->order,var); - order_update(s, var); - } - - s->size = n > s->size ? n : s->size; -} - -void sat_solver_delete(sat_solver* s) -{ - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - int i; - for (i = 0; i < vecp_size(&s->clauses); i++) - ABC_FREE(vecp_begin(&s->clauses)[i]); - for (i = 0; i < vecp_size(&s->learnts); i++) - ABC_FREE(vecp_begin(&s->learnts)[i]); -#else - Sat_MmStepStop( s->pMem, 0 ); -#endif - - // delete vectors - vecp_delete(&s->clauses); - vecp_delete(&s->learnts); - veci_delete(&s->order); - veci_delete(&s->trail_lim); - veci_delete(&s->tagged); - veci_delete(&s->stack); - veci_delete(&s->model); - veci_delete(&s->act_vars); - veci_delete(&s->temp_clause); - veci_delete(&s->conf_final); - ABC_FREE(s->binary); - - // delete arrays - if (s->wlists != 0){ - int i; - for (i = 0; i < s->cap*2; i++) - vecp_delete(&s->wlists[i]); - ABC_FREE(s->wlists ); - ABC_FREE(s->activity ); - ABC_FREE(s->factors ); - ABC_FREE(s->assigns ); - ABC_FREE(s->orderpos ); - ABC_FREE(s->reasons ); - ABC_FREE(s->levels ); - ABC_FREE(s->trail ); - ABC_FREE(s->tags ); - ABC_FREE(s->polarity ); - } - - sat_solver_store_free(s); - ABC_FREE(s); -} - -void sat_solver_rollback( sat_solver* s ) -{ - int i; -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - for (i = 0; i < vecp_size(&s->clauses); i++) - ABC_FREE(vecp_begin(&s->clauses)[i]); - for (i = 0; i < vecp_size(&s->learnts); i++) - ABC_FREE(vecp_begin(&s->learnts)[i]); -#else - Sat_MmStepRestart( s->pMem ); -#endif - vecp_resize(&s->clauses, 0); - vecp_resize(&s->learnts, 0); - veci_resize(&s->trail_lim, 0); - veci_resize(&s->order, 0); - for ( i = 0; i < s->size*2; i++ ) - s->wlists[i].size = 0; - - // initialize other vars - s->size = 0; -// s->cap = 0; - s->qhead = 0; - s->qtail = 0; -#ifdef USE_FLOAT_ACTIVITY - s->var_inc = 1; - s->cla_inc = 1; - s->var_decay = (float)(1 / 0.95 ); - s->cla_decay = (float)(1 / 0.999 ); -#else - s->var_inc = (1 << 5); - s->cla_inc = (1 << 11); -#endif - s->root_level = 0; - s->simpdb_assigns = 0; - s->simpdb_props = 0; - s->random_seed = 91648253; - s->progress_estimate = 0; - s->verbosity = 0; - - s->stats.starts = 0; - s->stats.decisions = 0; - s->stats.propagations = 0; - s->stats.inspects = 0; - s->stats.conflicts = 0; - s->stats.clauses = 0; - s->stats.clauses_literals = 0; - s->stats.learnts = 0; - s->stats.learnts_literals = 0; - s->stats.tot_literals = 0; -} - - -static void clause_remove(sat_solver* s, clause* c) -{ - lit* lits = clause_begin(c); - assert(lit_neg(lits[0]) < s->size*2); - assert(lit_neg(lits[1]) < s->size*2); - - //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c); - //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); - - assert(lits[0] < s->size*2); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); - - if (clause_learnt(c)){ - s->stats.learnts--; - s->stats.learnts_literals -= clause_size(c); - }else{ - s->stats.clauses--; - s->stats.clauses_literals -= clause_size(c); - } - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - ABC_FREE(c); -#else - Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); -#endif -} - -static lbool clause_simplify(sat_solver* s, clause* c) -{ - lit* lits = clause_begin(c); - lbool* values = s->assigns; - int i; - - assert(sat_solver_dl(s) == 0); - - for (i = 0; i < clause_size(c); i++){ - lbool sig = !lit_sign(lits[i]); sig += sig - 1; - if (values[lit_var(lits[i])] == sig) - return l_True; - } - return l_False; -} - -int sat_solver_simplify(sat_solver* s) -{ - clause** reasons; - int type; - - assert(sat_solver_dl(s) == 0); - - if (sat_solver_propagate(s) != 0) - return false; - - if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) - return true; - - reasons = s->reasons; - for (type = 0; type < 2; type++){ - vecp* cs = type ? &s->learnts : &s->clauses; - clause** cls = (clause**)vecp_begin(cs); - - int i, j; - for (j = i = 0; i < vecp_size(cs); i++){ - if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && - clause_simplify(s,cls[i]) == l_True) - clause_remove(s,cls[i]); - else - cls[j++] = cls[i]; - } - vecp_resize(cs,j); - } - - s->simpdb_assigns = s->qhead; - // (shouldn't depend on 'stats' really, but it will do for now) - s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); - - return true; -} - - -static int clause_cmp (const void* x, const void* y) { - return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } - -void sat_solver_reducedb(sat_solver* s) -{ - int i, j; - double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity - clause** learnts = (clause**)vecp_begin(&s->learnts); - clause** reasons = s->reasons; - - sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp); - - for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) - clause_remove(s,learnts[i]); - else - learnts[j++] = learnts[i]; - } - for (; i < vecp_size(&s->learnts); i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) - clause_remove(s,learnts[i]); - else - learnts[j++] = learnts[i]; - } - - //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); - - - vecp_resize(&s->learnts,j); -} - -int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) -{ - clause * c; - lit *i,*j; - int maxvar; - lbool* values; - lit last; - - veci_resize( &s->temp_clause, 0 ); - for ( i = begin; i < end; i++ ) - veci_push( &s->temp_clause, *i ); - begin = veci_begin( &s->temp_clause ); - end = begin + veci_size( &s->temp_clause ); - - if (begin == end) - return false; - - //printlits(begin,end); printf("\n"); - // insertion sort - maxvar = lit_var(*begin); - for (i = begin + 1; i < end; i++){ - lit l = *i; - maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; - for (j = i; j > begin && *(j-1) > l; j--) - *j = *(j-1); - *j = l; - } - sat_solver_setnvars(s,maxvar+1); -// sat_solver_setnvars(s, lit_var(*(end-1))+1 ); - - /////////////////////////////////// - // add clause to internal storage - if ( s->pStore ) - { - int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); - assert( RetValue ); - } - /////////////////////////////////// - - //printlits(begin,end); printf("\n"); - values = s->assigns; - - // delete duplicates - last = lit_Undef; - for (i = j = begin; i < end; i++){ - //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); - lbool sig = !lit_sign(*i); sig += sig - 1; - if (*i == lit_neg(last) || sig == values[lit_var(*i)]) - return true; // tautology - else if (*i != last && values[lit_var(*i)] == l_Undef) - last = *j++ = *i; - } -// j = i; - - if (j == begin) // empty clause - return false; - - if (j - begin == 1) // unit clause - return sat_solver_enqueue(s,*begin,(clause*)0); - - // create new clause - c = clause_create_new(s,begin,j,0); - if ( c ) - vecp_push(&s->clauses,c); - - - s->stats.clauses++; - s->stats.clauses_literals += j - begin; - - return true; -} - - -double luby(double y, int x) -{ - int size, seq; - for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1); - while (size-1 != x){ - size = (size-1) >> 1; - seq--; - x = x % size; - } - return pow(y, (double)seq); -} - -void luby_test() -{ - int i; - for ( i = 0; i < 20; i++ ) - printf( "%d ", (int)luby(2,i) ); - printf( "\n" ); -} - -static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts) -{ - int* levels = s->levels; - double var_decay = 0.95; - double clause_decay = 0.999; - double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; - - ABC_INT64_T conflictC = 0; - veci learnt_clause; - int i; - - assert(s->root_level == sat_solver_dl(s)); - - s->nRestarts++; - s->stats.starts++; -// s->var_decay = (float)(1 / var_decay ); // move this to sat_solver_new() -// s->cla_decay = (float)(1 / clause_decay); // move this to sat_solver_new() - veci_resize(&s->model,0); - veci_new(&learnt_clause); - - // use activity factors in every even restart - if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 ) -// if ( veci_size(&s->act_vars) > 0 ) - for ( i = 0; i < s->act_vars.size; i++ ) - act_var_bump_factor(s, s->act_vars.ptr[i]); - - // use activity factors in every restart - if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 ) - for ( i = 0; i < s->act_vars.size; i++ ) - act_var_bump_global(s, s->act_vars.ptr[i]); - - for (;;){ - clause* confl = sat_solver_propagate(s); - if (confl != 0){ - // CONFLICT - int blevel; - -#ifdef VERBOSEDEBUG - printf(L_IND"**CONFLICT**\n", L_ind); -#endif - s->stats.conflicts++; conflictC++; - if (sat_solver_dl(s) == s->root_level){ -#ifdef SAT_USE_ANALYZE_FINAL - sat_solver_analyze_final(s, confl, 0); -#endif - veci_delete(&learnt_clause); - return l_False; - } - - veci_resize(&learnt_clause,0); - sat_solver_analyze(s, confl, &learnt_clause); - blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; - blevel = s->root_level > blevel ? s->root_level : blevel; - sat_solver_canceluntil(s,blevel); - sat_solver_record(s,&learnt_clause); -#ifdef SAT_USE_ANALYZE_FINAL -// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) - if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0; -#endif - act_var_decay(s); - act_clause_decay(s); - - }else{ - // NO CONFLICT - int next; - - if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ - // Reached bound on number of conflicts: - s->progress_estimate = sat_solver_progress(s); - sat_solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; } - - if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) || -// (s->nInsLimit && s->stats.inspects > s->nInsLimit) ) - (s->nInsLimit && s->stats.propagations > s->nInsLimit) ) - { - // Reached bound on number of conflicts: - s->progress_estimate = sat_solver_progress(s); - sat_solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; - } - - if (sat_solver_dl(s) == 0 && !s->fSkipSimplify) - // Simplify the set of problem clauses: - sat_solver_simplify(s); - -// if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) - // Reduce the set of learnt clauses: -// sat_solver_reducedb(s); - - // New variable decision: - s->stats.decisions++; - next = order_select(s,(float)random_var_freq); - - if (next == var_Undef){ - // Model found: - lbool* values = s->assigns; - int i; - veci_resize(&s->model, 0); - for (i = 0; i < s->size; i++) - veci_push(&s->model,(int)values[i]); - sat_solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - - /* - veci apa; veci_new(&apa); - for (i = 0; i < s->size; i++) - veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); - printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); - veci_delete(&apa); - */ - - return l_True; - } - - if ( s->polarity[next] ) // positive polarity - sat_solver_assume(s,toLit(next)); - else - sat_solver_assume(s,lit_neg(toLit(next))); - } - } - - return l_Undef; // cannot happen -} - -int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) -{ - int restart_iter = 0; - ABC_INT64_T nof_conflicts; - ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3; - lbool status = l_Undef; - lbool* values = s->assigns; - lit* i; - - //////////////////////////////////////////////// - if ( s->fSolved ) - { - if ( s->pStore ) - { - int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); - assert( RetValue ); - } - return l_False; - } - //////////////////////////////////////////////// - - // set the external limits - s->nCalls++; - s->nRestarts = 0; - s->nConfLimit = 0; - s->nInsLimit = 0; - if ( nConfLimit ) - s->nConfLimit = s->stats.conflicts + nConfLimit; - if ( nInsLimit ) -// s->nInsLimit = s->stats.inspects + nInsLimit; - s->nInsLimit = s->stats.propagations + nInsLimit; - if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) ) - s->nConfLimit = nConfLimitGlobal; - if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) - s->nInsLimit = nInsLimitGlobal; - -#ifndef SAT_USE_ANALYZE_FINAL - - //printf("solve: "); printlits(begin, end); printf("\n"); - for (i = begin; i < end; i++){ - switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ - case 1: // l_True: - break; - case 0: // l_Undef - sat_solver_assume(s, *i); - if (sat_solver_propagate(s) == NULL) - break; - // fallthrough - case -1: // l_False - sat_solver_canceluntil(s, 0); - return l_False; - } - } - s->root_level = sat_solver_dl(s); - -#endif - -/* - // Perform assumptions: - root_level = assumps.size(); - for (int i = 0; i < assumps.size(); i++){ - Lit p = assumps[i]; - assert(var(p) < nVars()); - if (!sat_solver_assume(p)){ - GClause r = reason[var(p)]; - if (r != GClause_NULL){ - Clause* confl; - if (r.isLit()){ - confl = propagate_tmpbin; - (*confl)[1] = ~p; - (*confl)[0] = r.lit(); - }else - confl = r.clause(); - analyzeFinal(confl, true); - conflict.push(~p); - }else - conflict.clear(), - conflict.push(~p); - cancelUntil(0); - return false; } - Clause* confl = propagate(); - if (confl != NULL){ - analyzeFinal(confl), assert(conflict.size() > 0); - cancelUntil(0); - return false; } - } - assert(root_level == decisionLevel()); -*/ - -#ifdef SAT_USE_ANALYZE_FINAL - // Perform assumptions: - s->root_level = end - begin; - for ( i = begin; i < end; i++ ) - { - lit p = *i; - assert(lit_var(p) < s->size); - veci_push(&s->trail_lim,s->qtail); - if (!sat_solver_enqueue(s,p,(clause*)0)) - { - clause * r = s->reasons[lit_var(p)]; - if (r != NULL) - { - clause* confl; - if (clause_is_lit(r)) - { - confl = s->binary; - (clause_begin(confl))[1] = lit_neg(p); - (clause_begin(confl))[0] = clause_read_lit(r); - } - else - confl = r; - sat_solver_analyze_final(s, confl, 1); - veci_push(&s->conf_final, lit_neg(p)); - } - else - { - veci_resize(&s->conf_final,0); - veci_push(&s->conf_final, lit_neg(p)); - // the two lines below are a bug fix by Siert Wieringa - if (s->levels[lit_var(p)] > 0) - veci_push(&s->conf_final, p); - } - sat_solver_canceluntil(s, 0); - return l_False; - } - else - { - clause* confl = sat_solver_propagate(s); - if (confl != NULL){ - sat_solver_analyze_final(s, confl, 0); - assert(s->conf_final.size > 0); - sat_solver_canceluntil(s, 0); - return l_False; } - } - } - assert(s->root_level == sat_solver_dl(s)); -#endif - - s->nCalls2++; - - if (s->verbosity >= 1){ - printf("==================================[MINISAT]===================================\n"); - printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); - printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); - printf("==============================================================================\n"); - } - - while (status == l_Undef){ -// int nConfs = 0; - double Ratio = (s->stats.learnts == 0)? 0.0 : - s->stats.learnts_literals / (double)s->stats.learnts; - if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) - break; - - if (s->verbosity >= 1) - { - printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", - (double)s->stats.conflicts, - (double)s->stats.clauses, - (double)s->stats.clauses_literals, - (double)nof_learnts, - (double)s->stats.learnts, - (double)s->stats.learnts_literals, - Ratio, - s->progress_estimate*100); - fflush(stdout); - } - nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) ); -//printf( "%d ", (int)nof_conflicts ); -// nConfs = s->stats.conflicts; - status = sat_solver_search(s, nof_conflicts, nof_learnts); -// if ( status == l_True ) -// printf( "%d ", s->stats.conflicts - nConfs ); - -// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5; - nof_learnts = nof_learnts * 11 / 10; //*= 1.1; -//printf( "%d ", s->stats.conflicts ); - // quit the loop if reached an external limit - if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ) - { -// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); - break; - } -// if ( s->nInsLimit && s->stats.inspects > s->nInsLimit ) - if ( s->nInsLimit && s->stats.propagations > s->nInsLimit ) - { -// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); - break; - } - if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) - break; - } -//printf( "\n" ); - if (s->verbosity >= 1) - printf("==============================================================================\n"); - - sat_solver_canceluntil(s,0); - - //////////////////////////////////////////////// - if ( status == l_False && s->pStore ) - { - int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); - assert( RetValue ); - } - //////////////////////////////////////////////// - return status; -} - - -int sat_solver_nvars(sat_solver* s) -{ - return s->size; -} - - -int sat_solver_nclauses(sat_solver* s) -{ - return vecp_size(&s->clauses); -} - - -int sat_solver_nconflicts(sat_solver* s) -{ - return (int)s->stats.conflicts; -} - -//================================================================================================= -// Clause storage functions: - -void sat_solver_store_alloc( sat_solver * s ) -{ - assert( s->pStore == NULL ); - s->pStore = Sto_ManAlloc(); -} - -void sat_solver_store_write( sat_solver * s, char * pFileName ) -{ - if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName ); -} - -void sat_solver_store_free( sat_solver * s ) -{ - if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore ); - s->pStore = NULL; -} - -int sat_solver_store_change_last( sat_solver * s ) -{ - if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore ); - return -1; -} - -void sat_solver_store_mark_roots( sat_solver * s ) -{ - if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore ); -} - -void sat_solver_store_mark_clauses_a( sat_solver * s ) -{ - if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore ); -} - -void * sat_solver_store_release( sat_solver * s ) -{ - void * pTemp; - if ( s->pStore == NULL ) - return NULL; - pTemp = s->pStore; - s->pStore = NULL; - return pTemp; -} - -//================================================================================================= -// Sorting functions (sigh): - -static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) -{ - int i, j, best_i; - void* tmp; - - for (i = 0; i < size-1; i++){ - best_i = i; - for (j = i+1; j < size; j++){ - if (comp(array[j], array[best_i]) < 0) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} - - -static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) -{ - if (size <= 15) - selectionsort(array, size, comp); - - else{ - void* pivot = array[irand(seed, size)]; - void* tmp; - int i = -1; - int j = size; - - for(;;){ - do i++; while(comp(array[i], pivot)<0); - do j--; while(comp(pivot, array[j])<0); - - if (i >= j) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - - sortrnd(array , i , comp, seed); - sortrnd(&array[i], size-i, comp, seed); - } -} - -void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)) -{ -// int i; - double seed = 91648253; - sortrnd(array,size,comp,&seed); -// for ( i = 1; i < size; i++ ) -// assert(comp(array[i-1], array[i])<0); -} -ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bsat/satSolver_old.h b/src/sat/bsat/satSolver_old.h deleted file mode 100644 index d2228f79..00000000 --- a/src/sat/bsat/satSolver_old.h +++ /dev/null @@ -1,210 +0,0 @@ -/************************************************************************************************** -MiniSat -- Copyright (c) 2005, Niklas Sorensson -http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ -// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko - -#ifndef ABC__sat__bsat__satSolver_old_h -#define ABC__sat__bsat__satSolver_old_h - - -#include <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <assert.h> - -#include "satVec.h" -#include "satMem.h" - -ABC_NAMESPACE_HEADER_START - -//#define USE_FLOAT_ACTIVITY - -//================================================================================================= -// Public interface: - -struct sat_solver_t; -typedef struct sat_solver_t sat_solver; - -extern sat_solver* sat_solver_new(void); -extern void sat_solver_delete(sat_solver* s); - -extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end); -extern int sat_solver_simplify(sat_solver* s); -extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); -extern void sat_solver_rollback( sat_solver* s ); - -extern int sat_solver_nvars(sat_solver* s); -extern int sat_solver_nclauses(sat_solver* s); -extern int sat_solver_nconflicts(sat_solver* s); - -extern void sat_solver_setnvars(sat_solver* s,int n); - -extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); -extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); -extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ); -extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar ); - -// trace recording -extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName ); -extern void Sat_SolverTraceStop( sat_solver * pSat ); -extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot ); - -// clause storage -extern void sat_solver_store_alloc( sat_solver * s ); -extern void sat_solver_store_write( sat_solver * s, char * pFileName ); -extern void sat_solver_store_free( sat_solver * s ); -extern void sat_solver_store_mark_roots( sat_solver * s ); -extern void sat_solver_store_mark_clauses_a( sat_solver * s ); -extern void * sat_solver_store_release( sat_solver * s ); - -//================================================================================================= -// Solver representation: - -struct clause_t; -typedef struct clause_t clause; - -struct sat_solver_t -{ - int size; // nof variables - int cap; // size of varmaps - int qhead; // Head index of queue. - int qtail; // Tail index of queue. - - // clauses - vecp clauses; // List of problem constraints. (contains: clause*) - vecp learnts; // List of learnt clauses. (contains: clause*) - - // activities -#ifdef USE_FLOAT_ACTIVITY - double var_inc; // Amount to bump next variable with. - double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. - float cla_inc; // Amount to bump next clause with. - float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. - double* activity; // A heuristic measurement of the activity of a variable. -#else - int var_inc; // Amount to bump next variable with. - int cla_inc; // Amount to bump next clause with. - unsigned*activity; // A heuristic measurement of the activity of a variable. -#endif - - vecp* wlists; // - lbool* assigns; // Current values of variables. - int* orderpos; // Index in variable order. - clause** reasons; // - int* levels; // - lit* trail; - char* polarity; - - clause* binary; // A temporary binary clause - lbool* tags; // - veci tagged; // (contains: var) - veci stack; // (contains: var) - - veci order; // Variable order. (heap) (contains: var) - veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - veci model; // If problem is solved, this vector contains the model (contains: lbool). - veci conf_final; // If problem is unsatisfiable (possibly under assumptions), - // this vector represent the final conflict clause expressed in the assumptions. - - int root_level; // Level of first proper decision. - int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. - int simpdb_props; // Number of propagations before next 'simplifyDB()'. - double random_seed; - double progress_estimate; - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - - stats_t stats; - - ABC_INT64_T nConfLimit; // external limit on the number of conflicts - ABC_INT64_T nInsLimit; // external limit on the number of implications - int nRuntimeLimit; // external limit on runtime - - veci act_vars; // variables whose activity has changed - double* factors; // the activity factors - int nRestarts; // the number of local restarts - int nCalls; // the number of local restarts - int nCalls2; // the number of local restarts - - Sat_MmStep_t * pMem; - - int fSkipSimplify; // set to one to skip simplification of the clause database - int fNotUseRandom; // do not allow random decisions with a fixed probability - - int * pGlobalVars; // for experiments with global vars during interpolation - // clause store - void * pStore; - int fSolved; - - // trace recording - FILE * pFile; - int nClauses; - int nRoots; - - veci temp_clause; // temporary storage for a CNF clause -}; - -static int sat_solver_var_value( sat_solver* s, int v ) -{ - assert( s->model.ptr != NULL && v < s->size ); - return (int)(s->model.ptr[v] == l_True); -} -static int sat_solver_var_literal( sat_solver* s, int v ) -{ - assert( s->model.ptr != NULL && v < s->size ); - return toLitCond( v, s->model.ptr[v] != l_True ); -} -static void sat_solver_act_var_clear(sat_solver* s) -{ - int i; - for (i = 0; i < s->size; i++) - s->activity[i] = 0.0; - s->var_inc = 1.0; -} -static void sat_solver_compress(sat_solver* s) -{ - if ( s->qtail != s->qhead ) - { - int RetValue = sat_solver_simplify(s); - assert( RetValue != 0 ); - } -} - -static int sat_solver_final(sat_solver* s, int ** ppArray) -{ - *ppArray = s->conf_final.ptr; - return s->conf_final.size; -} - -static int sat_solver_set_runtime_limit(sat_solver* s, int Limit) -{ - int nRuntimeLimit = s->nRuntimeLimit; - s->nRuntimeLimit = Limit; - return nRuntimeLimit; -} - -static int sat_solver_set_random(sat_solver* s, int fNotUseRandom) -{ - int fNotUseRandomOld = s->fNotUseRandom; - s->fNotUseRandom = fNotUseRandom; - return fNotUseRandomOld; -} - -ABC_NAMESPACE_HEADER_END - -#endif diff --git a/src/sat/bsat/satTruth.c b/src/sat/bsat/satTruth.c index 7d69f558..dc5644b3 100644 --- a/src/sat/bsat/satTruth.c +++ b/src/sat/bsat/satTruth.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "satTruth.h" -#include "vecRec.h" +#include "vecSet.h" ABC_NAMESPACE_IMPL_START @@ -39,7 +39,7 @@ struct Tru_Man_t_ int nEntrySize; // the size of one entry in 'int' int nTableSize; // hash table size int * pTable; // hash table - Vec_Rec_t * pMem; // memory for truth tables + Vec_Set_t * pMem; // memory for truth tables word * pZero; // temporary truth table int hIthVars[16]; // variable handles int nTableLookups; @@ -53,7 +53,7 @@ struct Tru_One_t_ word pTruth[0]; // truth table }; -static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_RecEntryP(p->pMem, h) : NULL; } +static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_SetEntry(p->pMem, h) : NULL; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -140,7 +140,7 @@ void Tru_ManResize( Tru_Man_t * p ) *pSpot = pThis->Handle; Counter++; } - assert( Counter == Vec_RecEntryNum(p->pMem) ); + assert( Counter == Vec_SetEntryNum(p->pMem) ); ABC_FREE( pTableOld ); } @@ -163,7 +163,7 @@ int Tru_ManInsert( Tru_Man_t * p, word * pTruth ) if ( Tru_ManEqual1(pTruth, p->nWords) ) return 1; p->nTableLookups++; - if ( Vec_RecEntryNum(p->pMem) > 2 * p->nTableSize ) + if ( Vec_SetEntryNum(p->pMem) > 2 * p->nTableSize ) Tru_ManResize( p ); fCompl = pTruth[0] & 1; if ( fCompl ) @@ -172,7 +172,7 @@ int Tru_ManInsert( Tru_Man_t * p, word * pTruth ) if ( *pSpot == 0 ) { Tru_One_t * pEntry; - *pSpot = Vec_RecAppend( p->pMem, p->nEntrySize ); + *pSpot = Vec_SetAppend( p->pMem, NULL, p->nEntrySize ); assert( (*pSpot & 1) == 0 ); pEntry = Tru_ManReadOne( p, *pSpot ); Tru_ManCopy( pEntry->pTruth, pTruth, p->nWords ); @@ -215,7 +215,7 @@ Tru_Man_t * Tru_ManAlloc( int nVars ) p->nEntrySize = (sizeof(Tru_One_t) + p->nWords * sizeof(word))/sizeof(int); p->nTableSize = 8147; p->pTable = ABC_CALLOC( int, p->nTableSize ); - p->pMem = Vec_RecAlloc(); + p->pMem = Vec_SetAlloc(); // initialize truth tables p->pZero = ABC_ALLOC( word, p->nWords ); for ( i = 0; i < nVars; i++ ) @@ -247,8 +247,8 @@ Tru_Man_t * Tru_ManAlloc( int nVars ) ***********************************************************************/ void Tru_ManFree( Tru_Man_t * p ) { - printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_RecEntryNum(p->pMem) ); - Vec_RecFree( p->pMem ); + printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_SetEntryNum(p->pMem) ); + Vec_SetFree( p->pMem ); ABC_FREE( p->pZero ); ABC_FREE( p->pTable ); ABC_FREE( p ); @@ -287,25 +287,9 @@ word * Tru_ManFunc( Tru_Man_t * p, int h ) assert( (h & 1) == 0 ); if ( h == 0 ) return p->pZero; - assert( Vec_RecChunk(h) ); return Tru_ManReadOne( p, h )->pTruth; } -/**Function************************************************************* - - Synopsis [Returns stored truth table] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Tru_ManHandleMax( Tru_Man_t * p ) -{ - return p->pMem->hCurrent; -} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satTruth.h b/src/sat/bsat/satTruth.h index 2f17b6f0..dcbf6526 100644 --- a/src/sat/bsat/satTruth.h +++ b/src/sat/bsat/satTruth.h @@ -77,7 +77,7 @@ extern void Tru_ManFree( Tru_Man_t * p ); extern word * Tru_ManVar( Tru_Man_t * p, int v ); extern word * Tru_ManFunc( Tru_Man_t * p, int h ); extern int Tru_ManInsert( Tru_Man_t * p, word * pTruth ); -extern int Tru_ManHandleMax( Tru_Man_t * p ); +//extern int Tru_ManHandleMax( Tru_Man_t * p ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h deleted file mode 100644 index 82d7183d..00000000 --- a/src/sat/bsat/vecRec.h +++ /dev/null @@ -1,396 +0,0 @@ -/**CFile**************************************************************** - - FileName [vecRec.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Resizable arrays.] - - Synopsis [Array of records.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: vecRec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef ABC__sat__bsat__vecRec_h -#define ABC__sat__bsat__vecRec_h - - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include <stdio.h> - -ABC_NAMESPACE_HEADER_START - - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -// data-structure for logging entries -// 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 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 - int ** pChunks; // the chunks -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -// p is vector of records -// Size is given by the user -// Handle is returned to the user -// c (chunk) and s (shift) are variables used here -#define Vec_RecForEachEntry( p, Size, Handle, c, s ) \ - for ( c = 1; c <= p->nChunks; c++ ) \ - for ( s = 0; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) ) - -#define Vec_RecForEachEntryStart( p, Size, Handle, c, s, hStart ) \ - for ( c = Vec_RecChunk(hStart), s = Vec_RecShift(hStart); c <= p->nChunks; c++, s = 0 ) \ - for ( ; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) ) - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Vec_Rec_t * Vec_RecAlloc() -{ - Vec_Rec_t * p; - p = ABC_CALLOC( Vec_Rec_t, 1 ); - p->Mask = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb - p->hCurrent = (1 << 16); - p->nChunks = 1; - p->nChunksAlloc = 16; - p->pChunks = ABC_CALLOC( int *, p->nChunksAlloc ); - p->pChunks[0] = NULL; - p->pChunks[1] = ABC_ALLOC( int, (1 << 16) ); - p->pChunks[1][0] = 0; - return p; -} -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->Mask = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb - p->hCurrent = (1 << 16); - p->nChunks = 1; - p->nChunksAlloc = 16; - p->pChunks = ABC_CALLOC( int *, p->nChunksAlloc ); - p->pChunks[0] = NULL; - p->pChunks[1] = ABC_ALLOC( int, (1 << 16) ); - p->pChunks[1][0] = 0; -// return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_RecChunk( int i ) -{ - return i>>16; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_RecShift( int i ) -{ - return i&0xFFFF; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_RecSize( Vec_Rec_t * p ) -{ - return Vec_RecChunk(p->hCurrent) * (p->Mask + 1); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_RecEntryNum( Vec_Rec_t * p ) -{ - return p->nEntries; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_RecEntry( Vec_Rec_t * p, int i ) -{ - assert( i <= p->hCurrent ); - return p->pChunks[Vec_RecChunk(i)][Vec_RecShift(i)]; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int * Vec_RecEntryP( Vec_Rec_t * p, int i ) -{ - assert( i <= p->hCurrent ); - return p->pChunks[Vec_RecChunk(i)] + Vec_RecShift(i); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Vec_RecRestart( Vec_Rec_t * p ) -{ - p->hCurrent = (1 << 16); - p->nChunks = 1; - p->nEntries = 0; - p->pChunks[1][0] = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Vec_RecShrink( Vec_Rec_t * p, int h ) -{ - int i; - assert( Vec_RecEntry(p, h) == 0 ); - for ( i = Vec_RecChunk(h)+1; i < p->nChunksAlloc; i++ ) - ABC_FREE( p->pChunks[i] ); - p->nChunks = Vec_RecChunk(h); - p->hCurrent = h; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Vec_RecFree( Vec_Rec_t * p ) -{ - int i; - for ( i = 0; i < p->nChunksAlloc; i++ ) - ABC_FREE( p->pChunks[i] ); - ABC_FREE( p->pChunks ); - ABC_FREE( p ); -} -static inline void Vec_RecFree_( Vec_Rec_t * p ) -{ - int i; - for ( i = 0; i < p->nChunksAlloc; i++ ) - ABC_FREE( p->pChunks[i] ); - ABC_FREE( p->pChunks ); -// ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize ) -{ - assert( nSize <= p->Mask ); - assert( Vec_RecEntry(p, p->hCurrent) == 0 ); - assert( Vec_RecChunk(p->hCurrent) == p->nChunks ); - if ( Vec_RecShift(p->hCurrent) + nSize >= p->Mask ) - { - if ( ++p->nChunks == p->nChunksAlloc ) - { - p->pChunks = ABC_REALLOC( int *, p->pChunks, p->nChunksAlloc * 2 ); - memset( p->pChunks + p->nChunksAlloc, 0, sizeof(int *) * p->nChunksAlloc ); - p->nChunksAlloc *= 2; - } - if ( p->pChunks[p->nChunks] == NULL ) - p->pChunks[p->nChunks] = ABC_ALLOC( int, (p->Mask + 1) ); - p->pChunks[p->nChunks][0] = 0; - p->hCurrent = p->nChunks << 16; - } - p->hCurrent += nSize; - *Vec_RecEntryP(p, p->hCurrent) = 0; - p->nEntries++; - return p->hCurrent - nSize; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Vec_RecPush( Vec_Rec_t * p, int * pArray, int nSize ) -{ - int Handle = Vec_RecAppend( p, nSize ); - memmove( Vec_RecEntryP(p, Handle), pArray, sizeof(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 - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/sat/bsat/vecSet.h b/src/sat/bsat/vecSet.h new file mode 100644 index 00000000..e95c3332 --- /dev/null +++ b/src/sat/bsat/vecSet.h @@ -0,0 +1,247 @@ +/**CFile**************************************************************** + + FileName [vecSet.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT solvers.] + + Synopsis [Multi-page dynamic array.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: vecSet.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__sat__bsat__vecSet_h +#define ABC__sat__bsat__vecSet_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// data-structure for logging entries +// memory is allocated in 2^16 word-sized pages +// the first 'word' of each page is used storing additional data +// the first 'int' of additional data stores the word limit +// the second 'int' of the additional data stores the shadow word limit + +typedef struct Vec_Set_t_ Vec_Set_t; +struct Vec_Set_t_ +{ + int nEntries; // entry count + int iPage; // current page + int iPageS; // shadow page + int nPagesAlloc; // page count allocated + word ** pPages; // page pointers +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Vec_SetHandPage( int h ) { return h >> 16; } +static inline int Vec_SetHandShift( int h ) { return h & 0xFFFF; } + +static inline word * Vec_SetEntry( Vec_Set_t * p, int h ) { return p->pPages[Vec_SetHandPage(h)] + Vec_SetHandShift(h); } +static inline int Vec_SetEntryNum( Vec_Set_t * p ) { return p->nEntries; } +static inline void Vec_SetWriteEntryNum( Vec_Set_t * p, int i){ p->nEntries = i; } + +static inline int Vec_SetLimit( word * p ) { return ((int*)p)[0]; } +static inline int Vec_SetLimitS( word * p ) { return ((int*)p)[1]; } + +static inline int Vec_SetIncLimit( word * p, int nWords ) { return ((int*)p)[0] += nWords; } +static inline int Vec_SetIncLimitS( word * p, int nWords ) { return ((int*)p)[1] += nWords; } + +static inline void Vec_SetWriteLimit( word * p, int nWords ) { ((int*)p)[0] = nWords; } +static inline void Vec_SetWriteLimitS( word * p, int nWords ) { ((int*)p)[1] = nWords; } + +static inline int Vec_SetHandCurrent( Vec_Set_t * p ) { return (p->iPage << 16) + Vec_SetLimit(p->pPages[p->iPage]); } +static inline int Vec_SetHandCurrentS( Vec_Set_t * p ) { return (p->iPageS << 16) + Vec_SetLimitS(p->pPages[p->iPageS]); } + +static inline int Vec_SetHandMemory( Vec_Set_t * p, int h ) { return Vec_SetHandPage(h) * 0x8FFFF + Vec_SetHandShift(h) * 8; } +static inline int Vec_SetMemory( Vec_Set_t * p ) { return Vec_SetHandMemory(p, Vec_SetHandCurrent(p)); } +static inline int Vec_SetMemoryS( Vec_Set_t * p ) { return Vec_SetHandMemory(p, Vec_SetHandCurrentS(p)); } +static inline int Vec_SetMemoryAll( Vec_Set_t * p ) { return (p->iPage+1) * 0x8FFFF; } + +// Type is the Set type +// pVec is vector of set +// nSize should be given by the user +// pSet is the pointer to the set +// p (page) and s (shift) are variables used here +#define Vec_SetForEachEntry( Type, pVec, nSize, pSet, p, s ) \ + for ( p = 0; p <= pVec->iPage; p++ ) \ + for ( s = 1; s < Vec_SetLimit(pVec->pPages[p]) && ((pSet) = (Type)(pVec->pPages[p] + (s))); s += nSize ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocating vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_SetAlloc_( Vec_Set_t * p ) +{ + memset( p, 0, sizeof(Vec_Set_t) ); + p->nPagesAlloc = 256; + p->pPages = ABC_CALLOC( word *, p->nPagesAlloc ); + p->pPages[0] = ABC_ALLOC( word, 0x10000 ); + p->pPages[0][0] = ~0; + Vec_SetWriteLimit( p->pPages[0], 1 ); +} +static inline Vec_Set_t * Vec_SetAlloc() +{ + Vec_Set_t * p; + p = ABC_CALLOC( Vec_Set_t, 1 ); + Vec_SetAlloc_( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Resetting vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_SetRestart( Vec_Set_t * p ) +{ + p->nEntries = 0; + p->iPage = 0; + p->iPageS = 0; + p->pPages[0][0] = ~0; + Vec_SetWriteLimit( p->pPages[0], 1 ); +} + +/**Function************************************************************* + + Synopsis [Freeing vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_SetFree_( Vec_Set_t * p ) +{ + int i; + for ( i = 0; i < p->nPagesAlloc; i++ ) + ABC_FREE( p->pPages[i] ); + ABC_FREE( p->pPages ); +} +static inline void Vec_SetFree( Vec_Set_t * p ) +{ + Vec_SetFree_( p ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Appending entries to vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) +{ + int nWords = (nSize + 1) >> 1; + assert( nWords < 0x10000 ); + p->nEntries++; + if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > 0x10000 ) + { + if ( ++p->iPage == p->nPagesAlloc ) + { + p->pPages = ABC_REALLOC( word *, p->pPages, p->nPagesAlloc * 2 ); + memset( p->pPages + p->nPagesAlloc, 0, sizeof(word *) * p->nPagesAlloc ); + p->nPagesAlloc *= 2; + } + if ( p->pPages[p->iPage] == NULL ) + p->pPages[p->iPage] = ABC_ALLOC( word, 0x10000 ); + p->pPages[p->iPage][0] = ~0; + Vec_SetWriteLimit( p->pPages[p->iPage], 1 ); + } + if ( pArray ) + memmove( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize ); + Vec_SetIncLimit( p->pPages[p->iPage], nWords ); + return Vec_SetHandCurrent(p) - nWords; +} +static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize ) +{ + int nWords = (nSize + 1) >> 1; + assert( nWords < 0x10000 ); + if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > 0x10000 ) + Vec_SetWriteLimitS( p->pPages[++p->iPageS], 1 ); + Vec_SetIncLimitS( p->pPages[p->iPageS], nWords ); + return Vec_SetHandCurrentS(p) - nWords; +} + +/**Function************************************************************* + + Synopsis [Shrinking vector size.] + + Description [] + + SideEffects [This procedure does not update the number of entries.] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_SetShrink( Vec_Set_t * p, int h ) +{ + assert( h <= Vec_SetHandCurrent(p) ); + p->iPage = Vec_SetHandPage(h); + Vec_SetWriteLimit( p->pPages[p->iPage], Vec_SetHandShift(h) ); +} +static inline void Vec_SetShrinkS( Vec_Set_t * p, int h ) +{ + assert( h <= Vec_SetHandCurrent(p) ); + p->iPageS = Vec_SetHandPage(h); + Vec_SetWriteLimitS( p->pPages[p->iPageS], Vec_SetHandShift(h) ); +} + + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |