diff options
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/module.make | 7 | ||||
| -rw-r--r-- | src/sat/bsat/satInter.c | 991 | ||||
| -rw-r--r-- | src/sat/bsat/satInterA.c | 970 | ||||
| -rw-r--r-- | src/sat/bsat/satMem.c | 527 | ||||
| -rw-r--r-- | src/sat/bsat/satMem.h | 80 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.c | 1358 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 210 | ||||
| -rw-r--r-- | src/sat/bsat/satStore.c | 437 | ||||
| -rw-r--r-- | src/sat/bsat/satStore.h | 146 | ||||
| -rw-r--r-- | src/sat/bsat/satTrace.c | 109 | ||||
| -rw-r--r-- | src/sat/bsat/satUtil.c | 234 | ||||
| -rw-r--r-- | src/sat/bsat/satVec.h | 83 |
12 files changed, 0 insertions, 5152 deletions
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make deleted file mode 100644 index 1e52cc0a..00000000 --- a/src/sat/bsat/module.make +++ /dev/null @@ -1,7 +0,0 @@ -SRC += src/sat/bsat/satMem.c \ - src/sat/bsat/satInter.c \ - src/sat/bsat/satInterA.c \ - src/sat/bsat/satSolver.c \ - src/sat/bsat/satStore.c \ - src/sat/bsat/satTrace.c \ - src/sat/bsat/satUtil.c diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c deleted file mode 100644 index 8e07e9f6..00000000 --- a/src/sat/bsat/satInter.c +++ /dev/null @@ -1,991 +0,0 @@ -/**CFile**************************************************************** - - FileName [satInter.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [SAT sat_solver.] - - Synopsis [Interpolation package.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <assert.h> -#include <time.h> -#include "satStore.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// variable assignments -static const lit LIT_UNDEF = 0xffffffff; - -// interpolation manager -struct Int_Man_t_ -{ - // clauses of the problems - Sto_Man_t * pCnf; // the set of CNF clauses for A and B - // various parameters - int fVerbose; // verbosiness flag - int fProofVerif; // verifies the proof - int fProofWrite; // writes the proof file - int nVarsAlloc; // the allocated size of var arrays - int nClosAlloc; // the allocated size of clause arrays - // internal BCP - int nRootSize; // the number of root level assignments - int nTrailSize; // the number of assignments made - lit * pTrail; // chronological order of assignments (size nVars) - lit * pAssigns; // assignments by variable (size nVars) - char * pSeens; // temporary mark (size nVars) - Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) - Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) - // interpolation data - int nVarsAB; // the number of global variables - char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] - unsigned * pInters; // storage for interpolants as truth tables (size nClauses) - int nIntersAlloc; // the allocated size of truth table array - int nWords; // the number of words in the truth table - // proof recording - int Counter; // counter of resolved clauses - int * pProofNums; // the proof numbers for each clause (size nClauses) - FILE * pFile; // the file for proof recording - // internal verification - lit * pResLits; // the literals of the resolvent - int nResLits; // the number of literals of the resolvent - int nResLitsAlloc;// the number of literals of the resolvent - // runtime stats - int timeBcp; // the runtime for BCP - int timeTrace; // the runtime of trace construction - int timeTotal; // the total runtime of interpolation -}; - -// procedure to get hold of the clauses' truth table -static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pInters + pCls->Id * p->nWords; } -static inline void Int_ManTruthClear( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = 0; } -static inline void Int_ManTruthFill( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~0; } -static inline void Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; } -static inline void Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; } -static inline void Int_ManTruthOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; } -static inline void Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; } - -// reading/writing the proof for a clause -static inline int Int_ManProofGet( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } -static inline void Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocate proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Int_Man_t * Int_ManAlloc() -{ - Int_Man_t * p; - // allocate the manager - p = (Int_Man_t *)malloc( sizeof(Int_Man_t) ); - memset( p, 0, sizeof(Int_Man_t) ); - // verification - p->nResLitsAlloc = (1<<16); - p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); - // parameters - p->fProofWrite = 0; - p->fProofVerif = 1; - return p; -} - -/**Function************************************************************* - - Synopsis [Count common variables in the clauses of A and B.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Int_ManGlobalVars( Int_Man_t * p ) -{ - Sto_Cls_t * pClause; - int Var, nVarsAB, v; - - // mark the variable encountered in the clauses of A - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - if ( !pClause->fA ) - break; - for ( v = 0; v < (int)pClause->nLits; v++ ) - p->pVarTypes[lit_var(pClause->pLits[v])] = 1; - } - - // check variables that appear in clauses of B - nVarsAB = 0; - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - if ( pClause->fA ) - continue; - for ( v = 0; v < (int)pClause->nLits; v++ ) - { - Var = lit_var(pClause->pLits[v]); - if ( p->pVarTypes[Var] == 1 ) // var of A - { - // change it into a global variable - nVarsAB++; - p->pVarTypes[Var] = -1; - } - } - } - - // order global variables - nVarsAB = 0; - for ( v = 0; v < p->pCnf->nVars; v++ ) - if ( p->pVarTypes[v] == -1 ) - p->pVarTypes[v] -= nVarsAB++; -//printf( "There are %d global variables.\n", nVarsAB ); - return nVarsAB; -} - -/**Function************************************************************* - - Synopsis [Resize proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Int_ManResize( Int_Man_t * p ) -{ - // check if resizing is needed - if ( p->nVarsAlloc < p->pCnf->nVars ) - { - // find the new size - if ( p->nVarsAlloc == 0 ) - p->nVarsAlloc = 1; - while ( p->nVarsAlloc < p->pCnf->nVars ) - p->nVarsAlloc *= 2; - // resize the arrays - p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); - p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); - p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); - p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc ); - p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); - p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); - } - - // clean the free space - memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); - memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); - memset( p->pVarTypes, 0, sizeof(char) * p->pCnf->nVars ); - memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); - memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); - - // compute the number of common variables - p->nVarsAB = Int_ManGlobalVars( p ); - // compute the number of words in the truth table - p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5))); - - // check if resizing of clauses is needed - if ( p->nClosAlloc < p->pCnf->nClauses ) - { - // find the new size - if ( p->nClosAlloc == 0 ) - p->nClosAlloc = 1; - while ( p->nClosAlloc < p->pCnf->nClauses ) - p->nClosAlloc *= 2; - // resize the arrays - p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); - } - memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); - - // check if resizing of truth tables is needed - if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses ) - { - p->nIntersAlloc = p->nWords * p->pCnf->nClauses; - p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc ); - } -// memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses ); -} - -/**Function************************************************************* - - Synopsis [Deallocate proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Int_ManFree( Int_Man_t * p ) -{ -/* - printf( "Runtime stats:\n" ); -PRT( "BCP ", p->timeBcp ); -PRT( "Trace ", p->timeTrace ); -PRT( "TOTAL ", p->timeTotal ); -*/ - free( p->pInters ); - free( p->pProofNums ); - free( p->pTrail ); - free( p->pAssigns ); - free( p->pSeens ); - free( p->pVarTypes ); - free( p->pReasons ); - free( p->pWatches ); - free( p->pResLits ); - free( p ); -} - - - - -/**Function************************************************************* - - Synopsis [Prints the clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause ) -{ - int i; - printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofGet(p, pClause) ); - for ( i = 0; i < (int)pClause->nLits; i++ ) - printf( " %d", pClause->pLits[i] ); - printf( " }\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints the resolvent.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Int_ManPrintResolvent( lit * pResLits, int nResLits ) -{ - int i; - printf( "Resolvent: {" ); - for ( i = 0; i < nResLits; i++ ) - printf( " %d", pResLits[i] ); - printf( " }\n" ); -} - -/**Function************************************************************* - - Synopsis [Records the proof.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Extra_PrintBinary__( FILE * pFile, unsigned Sign[], int nBits ) -{ - int Remainder, nWords; - int w, i; - - Remainder = (nBits%(sizeof(unsigned)*8)); - nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0); - - for ( w = nWords-1; w >= 0; w-- ) - for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- ) - fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) ); -} - -/**Function************************************************************* - - Synopsis [Prints the interpolant for one clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Int_ManPrintInterOne( Int_Man_t * p, Sto_Cls_t * pClause ) -{ - printf( "Clause %2d : ", pClause->Id ); - Extra_PrintBinary__( stdout, Int_ManTruthRead(p, pClause), (1 << p->nVarsAB) ); - printf( "\n" ); -} - - - -/**Function************************************************************* - - Synopsis [Adds one clause to the watcher list.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Int_ManWatchClause( Int_Man_t * p, Sto_Cls_t * pClause, lit Lit ) -{ - assert( lit_check(Lit, p->pCnf->nVars) ); - if ( pClause->pLits[0] == Lit ) - pClause->pNext0 = p->pWatches[lit_neg(Lit)]; - else - { - assert( pClause->pLits[1] == Lit ); - pClause->pNext1 = p->pWatches[lit_neg(Lit)]; - } - p->pWatches[lit_neg(Lit)] = pClause; -} - - -/**Function************************************************************* - - Synopsis [Records implication.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Int_ManEnqueue( Int_Man_t * p, lit Lit, Sto_Cls_t * pReason ) -{ - int Var = lit_var(Lit); - if ( p->pAssigns[Var] != LIT_UNDEF ) - return p->pAssigns[Var] == Lit; - p->pAssigns[Var] = Lit; - p->pReasons[Var] = pReason; - p->pTrail[p->nTrailSize++] = Lit; -//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Records implication.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Int_ManCancelUntil( Int_Man_t * p, int Level ) -{ - lit Lit; - int i, Var; - for ( i = p->nTrailSize - 1; i >= Level; i-- ) - { - Lit = p->pTrail[i]; - Var = lit_var( Lit ); - p->pReasons[Var] = NULL; - p->pAssigns[Var] = LIT_UNDEF; -//printf( "cancelling var %d\n", Var ); - } - p->nTrailSize = Level; -} - -/**Function************************************************************* - - Synopsis [Propagate one assignment.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Sto_Cls_t * Int_ManPropagateOne( Int_Man_t * p, lit Lit ) -{ - Sto_Cls_t ** ppPrev, * pCur, * pTemp; - lit LitF = lit_neg(Lit); - int i; - // iterate through the literals - ppPrev = p->pWatches + Lit; - for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) - { - // make sure the false literal is in the second literal of the clause - if ( pCur->pLits[0] == LitF ) - { - pCur->pLits[0] = pCur->pLits[1]; - pCur->pLits[1] = LitF; - pTemp = pCur->pNext0; - pCur->pNext0 = pCur->pNext1; - pCur->pNext1 = pTemp; - } - assert( pCur->pLits[1] == LitF ); - - // if the first literal is true, the clause is satisfied - if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) - { - ppPrev = &pCur->pNext1; - continue; - } - - // look for a new literal to watch - for ( i = 2; i < (int)pCur->nLits; i++ ) - { - // skip the case when the literal is false - if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) - continue; - // the literal is either true or unassigned - watch it - pCur->pLits[1] = pCur->pLits[i]; - pCur->pLits[i] = LitF; - // remove this clause from the watch list of Lit - *ppPrev = pCur->pNext1; - // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) - Int_ManWatchClause( p, pCur, pCur->pLits[1] ); - break; - } - if ( i < (int)pCur->nLits ) // found new watch - continue; - - // clause is unit - enqueue new implication - if ( Int_ManEnqueue(p, pCur->pLits[0], pCur) ) - { - ppPrev = &pCur->pNext1; - continue; - } - - // conflict detected - return the conflict clause - return pCur; - } - return NULL; -} - -/**Function************************************************************* - - Synopsis [Propagate the current assignments.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start ) -{ - Sto_Cls_t * pClause; - int i; - int clk = clock(); - for ( i = Start; i < p->nTrailSize; i++ ) - { - pClause = Int_ManPropagateOne( p, p->pTrail[i] ); - if ( pClause ) - { -p->timeBcp += clock() - clk; - return pClause; - } - } -p->timeBcp += clock() - clk; - return NULL; -} - - -/**Function************************************************************* - - Synopsis [Writes one root clause into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause ) -{ - Int_ManProofSet( p, pClause, ++p->Counter ); - - if ( p->fProofWrite ) - { - int v; - fprintf( p->pFile, "%d", Int_ManProofGet(p, pClause) ); - for ( v = 0; v < (int)pClause->nLits; v++ ) - fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); - fprintf( p->pFile, " 0 0\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Traces the proof for one clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal ) -{ - Sto_Cls_t * pReason; - int i, v, Var, PrevId; - int fPrint = 0; - int clk = clock(); - - // collect resolvent literals - if ( p->fProofVerif ) - { - assert( (int)pConflict->nLits <= p->nResLitsAlloc ); - memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); - p->nResLits = pConflict->nLits; - } - - // mark all the variables in the conflict as seen - for ( v = 0; v < (int)pConflict->nLits; v++ ) - p->pSeens[lit_var(pConflict->pLits[v])] = 1; - - // start the anticedents -// pFinal->pAntis = Vec_PtrAlloc( 32 ); -// Vec_PtrPush( pFinal->pAntis, pConflict ); - - if ( p->pCnf->nClausesA ) - Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords ); - - // follow the trail backwards - PrevId = Int_ManProofGet(p, pConflict); - for ( i = p->nTrailSize - 1; i >= 0; i-- ) - { - // skip literals that are not involved - Var = lit_var(p->pTrail[i]); - if ( !p->pSeens[Var] ) - continue; - p->pSeens[Var] = 0; - - // skip literals of the resulting clause - pReason = p->pReasons[Var]; - if ( pReason == NULL ) - continue; - assert( p->pTrail[i] == pReason->pLits[0] ); - - // add the variables to seen - for ( v = 1; v < (int)pReason->nLits; v++ ) - p->pSeens[lit_var(pReason->pLits[v])] = 1; - - - // record the reason clause - assert( Int_ManProofGet(p, pReason) > 0 ); - p->Counter++; - if ( p->fProofWrite ) - fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) ); - PrevId = p->Counter; - - if ( p->pCnf->nClausesA ) - { - if ( p->pVarTypes[Var] == 1 ) // var of A - Int_ManTruthOr( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords ); - else - Int_ManTruthAnd( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords ); - } - - // resolve the temporary resolvent with the reason clause - if ( p->fProofVerif ) - { - int v1, v2; - if ( fPrint ) - Int_ManPrintResolvent( p->pResLits, p->nResLits ); - // check that the var is present in the resolvent - for ( v1 = 0; v1 < p->nResLits; v1++ ) - if ( lit_var(p->pResLits[v1]) == Var ) - break; - if ( v1 == p->nResLits ) - printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); - if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) - printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); - // remove this variable from the resolvent - assert( lit_var(p->pResLits[v1]) == Var ); - p->nResLits--; - for ( ; v1 < p->nResLits; v1++ ) - p->pResLits[v1] = p->pResLits[v1+1]; - // add variables of the reason clause - for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) - { - for ( v1 = 0; v1 < p->nResLits; v1++ ) - if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) - break; - // if it is a new variable, add it to the resolvent - if ( v1 == p->nResLits ) - { - if ( p->nResLits == p->nResLitsAlloc ) - printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id ); - p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; - continue; - } - // if the variable is the same, the literal should be the same too - if ( p->pResLits[v1] == pReason->pLits[v2] ) - continue; - // the literal is different - printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); - } - } - -// Vec_PtrPush( pFinal->pAntis, pReason ); - } - - // unmark all seen variables -// for ( i = p->nTrailSize - 1; i >= 0; i-- ) -// p->pSeens[lit_var(p->pTrail[i])] = 0; - // check that the literals are unmarked -// for ( i = p->nTrailSize - 1; i >= 0; i-- ) -// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); - - // use the resulting clause to check the correctness of resolution - if ( p->fProofVerif ) - { - int v1, v2; - if ( fPrint ) - Int_ManPrintResolvent( p->pResLits, p->nResLits ); - for ( v1 = 0; v1 < p->nResLits; v1++ ) - { - for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) - if ( pFinal->pLits[v2] == p->pResLits[v1] ) - break; - if ( v2 < (int)pFinal->nLits ) - continue; - break; - } - if ( v1 < p->nResLits ) - { - printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); - Int_ManPrintClause( p, pConflict ); - Int_ManPrintResolvent( p->pResLits, p->nResLits ); - Int_ManPrintClause( p, pFinal ); - } - } -p->timeTrace += clock() - clk; - - // return the proof pointer - if ( p->pCnf->nClausesA ) - { -// Int_ManPrintInterOne( p, pFinal ); - } - Int_ManProofSet( p, pFinal, p->Counter ); - return p->Counter; -} - -/**Function************************************************************* - - Synopsis [Records the proof for one clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause ) -{ - Sto_Cls_t * pConflict; - int i; - - // empty clause never ends up there - assert( pClause->nLits > 0 ); - if ( pClause->nLits == 0 ) - printf( "Error: Empty clause is attempted.\n" ); - - // add assumptions to the trail - assert( !pClause->fRoot ); - assert( p->nTrailSize == p->nRootSize ); - for ( i = 0; i < (int)pClause->nLits; i++ ) - if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) - { - assert( 0 ); // impossible - return 0; - } - - // propagate the assumptions - pConflict = Int_ManPropagate( p, p->nRootSize ); - if ( pConflict == NULL ) - { - assert( 0 ); // cannot prove - return 0; - } - - // construct the proof - Int_ManProofTraceOne( p, pConflict, pClause ); - - // undo to the root level - Int_ManCancelUntil( p, p->nRootSize ); - - // add large clauses to the watched lists - if ( pClause->nLits > 1 ) - { - Int_ManWatchClause( p, pClause, pClause->pLits[0] ); - Int_ManWatchClause( p, pClause, pClause->pLits[1] ); - return 1; - } - assert( pClause->nLits == 1 ); - - // if the clause proved is unit, add it and propagate - if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) ) - { - assert( 0 ); // impossible - return 0; - } - - // propagate the assumption - pConflict = Int_ManPropagate( p, p->nRootSize ); - if ( pConflict ) - { - // construct the proof - Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); - if ( p->fVerbose ) - printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); - return 0; - } - - // update the root level - p->nRootSize = p->nTrailSize; - return 1; -} - -/**Function************************************************************* - - Synopsis [Propagate the root clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Int_ManProcessRoots( Int_Man_t * p ) -{ - Sto_Cls_t * pClause; - int Counter; - - // make sure the root clauses are preceeding the learnt clauses - Counter = 0; - Sto_ManForEachClause( p->pCnf, pClause ) - { - assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) ); - assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) ); - Counter++; - } - assert( p->pCnf->nClauses == Counter ); - - // make sure the last clause if empty - assert( p->pCnf->pTail->nLits == 0 ); - - // go through the root unit clauses - p->nTrailSize = 0; - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - // create watcher lists for the root clauses - if ( pClause->nLits > 1 ) - { - Int_ManWatchClause( p, pClause, pClause->pLits[0] ); - Int_ManWatchClause( p, pClause, pClause->pLits[1] ); - } - // empty clause and large clauses - if ( pClause->nLits != 1 ) - continue; - // unit clause - assert( lit_check(pClause->pLits[0], p->pCnf->nVars) ); - if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) ) - { - // detected root level conflict - printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" ); - assert( 0 ); - return 0; - } - } - - // propagate the root unit clauses - pClause = Int_ManPropagate( p, 0 ); - if ( pClause ) - { - // detected root level conflict - Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); - if ( p->fVerbose ) - printf( "Found root level conflict!\n" ); - return 0; - } - - // set the root level - p->nRootSize = p->nTrailSize; - return 1; -} - -/**Function************************************************************* - - Synopsis [Records the proof.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Int_ManPrepareInter( Int_Man_t * p ) -{ - // elementary truth tables - unsigned uTruths[8][8] = { - { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, - { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, - { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, - { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, - { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, - { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, - { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, - { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } - }; - Sto_Cls_t * pClause; - int Var, VarAB, v; - assert( p->nVarsAB <= 8 ); - - // set interpolants for root clauses - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - if ( !pClause->fA ) // clause of B - { - Int_ManTruthFill( Int_ManTruthRead(p, pClause), p->nWords ); -// Int_ManPrintInterOne( p, pClause ); - continue; - } - // clause of A - Int_ManTruthClear( Int_ManTruthRead(p, pClause), p->nWords ); - for ( v = 0; v < (int)pClause->nLits; v++ ) - { - Var = lit_var(pClause->pLits[v]); - if ( p->pVarTypes[Var] < 0 ) // global var - { - VarAB = -p->pVarTypes[Var]-1; - assert( VarAB >= 0 && VarAB < p->nVarsAB ); - if ( lit_sign(pClause->pLits[v]) ) // negative var - Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords ); - else - Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords ); - } - } -// Int_ManPrintInterOne( p, pClause ); - } -} - -/**Function************************************************************* - - Synopsis [Computes interpolant for the given CNF.] - - Description [Returns the number of common variable found and interpolant. - Returns 0, if something did not work.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult ) -{ - Sto_Cls_t * pClause; - int RetValue = 1; - int clkTotal = clock(); - - // check that the CNF makes sense - assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); - p->pCnf = pCnf; - p->fVerbose = fVerbose; - *ppResult = NULL; - - // adjust the manager - Int_ManResize( p ); - - // prepare the interpolant computation - Int_ManPrepareInter( p ); - - // construct proof for each clause - // start the proof - if ( p->fProofWrite ) - { - p->pFile = fopen( "proof.cnf_", "w" ); - p->Counter = 0; - } - - // write the root clauses - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - Int_ManProofWriteOne( p, pClause ); - - // propagate root level assignments - if ( Int_ManProcessRoots( p ) ) - { - // if there is no conflict, consider learned clauses - Sto_ManForEachClause( p->pCnf, pClause ) - { - if ( pClause->fRoot ) - continue; - if ( !Int_ManProofRecordOne( p, pClause ) ) - { - RetValue = 0; - break; - } - } - } - - // stop the proof - if ( p->fProofWrite ) - { - fclose( p->pFile ); - p->pFile = NULL; - } - - if ( fVerbose ) - { - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", - p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, - 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), - 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); -p->timeTotal += clock() - clkTotal; - } - - *ppResult = Int_ManTruthRead( p, p->pCnf->pTail ); - return p->nVarsAB; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c deleted file mode 100644 index 513a9044..00000000 --- a/src/sat/bsat/satInterA.c +++ /dev/null @@ -1,970 +0,0 @@ -/**CFile**************************************************************** - - FileName [satInter.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [SAT sat_solver.] - - Synopsis [Interpolation package.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <assert.h> -#include <time.h> -#include "satStore.h" -#include "aig.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// variable assignments -static const lit LIT_UNDEF = 0xffffffff; - -// interpolation manager -struct Inta_Man_t_ -{ - // clauses of the problems - Sto_Man_t * pCnf; // the set of CNF clauses for A and B - Vec_Int_t * vVarsAB; // the array of global variables - // various parameters - int fVerbose; // verbosiness flag - int fProofVerif; // verifies the proof - int fProofWrite; // writes the proof file - int nVarsAlloc; // the allocated size of var arrays - int nClosAlloc; // the allocated size of clause arrays - // internal BCP - int nRootSize; // the number of root level assignments - int nTrailSize; // the number of assignments made - lit * pTrail; // chronological order of assignments (size nVars) - lit * pAssigns; // assignments by variable (size nVars) - char * pSeens; // temporary mark (size nVars) - Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) - Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) - // interpolation data - Aig_Man_t * pAig; // the AIG manager for recording the interpolant - int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] - Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses) - int nIntersAlloc; // the allocated size of truth table array - // proof recording - int Counter; // counter of resolved clauses - int * pProofNums; // the proof numbers for each clause (size nClauses) - FILE * pFile; // the file for proof recording - // internal verification - lit * pResLits; // the literals of the resolvent - int nResLits; // the number of literals of the resolvent - int nResLitsAlloc;// the number of literals of the resolvent - // runtime stats - int timeBcp; // the runtime for BCP - int timeTrace; // the runtime of trace construction - int timeTotal; // the total runtime of interpolation -}; - -// procedure to get hold of the clauses' truth table -static inline Aig_Obj_t ** Inta_ManAigRead( Inta_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; } -static inline void Inta_ManAigClear( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); } -static inline void Inta_ManAigFill( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); } -static inline void Inta_ManAigCopy( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; } -static inline void Inta_ManAigAnd( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); } -static inline void Inta_ManAigOr( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); } -static inline void Inta_ManAigOrNot( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); } -static inline void Inta_ManAigOrVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); } -static inline void Inta_ManAigOrNotVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); } - -// reading/writing the proof for a clause -static inline int Inta_ManProofGet( Inta_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } -static inline void Inta_ManProofSet( Inta_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocate proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Inta_Man_t * Inta_ManAlloc() -{ - Inta_Man_t * p; - // allocate the manager - p = (Inta_Man_t *)malloc( sizeof(Inta_Man_t) ); - memset( p, 0, sizeof(Inta_Man_t) ); - // verification - p->nResLitsAlloc = (1<<16); - p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); - // parameters - p->fProofWrite = 0; - p->fProofVerif = 1; - return p; -} - -/**Function************************************************************* - - Synopsis [Count common variables in the clauses of A and B.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Inta_ManGlobalVars( Inta_Man_t * p ) -{ - Sto_Cls_t * pClause; - int LargeNum = -100000000; - int Var, nVarsAB, v; - - // mark the variable encountered in the clauses of A - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - if ( !pClause->fA ) - break; - for ( v = 0; v < (int)pClause->nLits; v++ ) - p->pVarTypes[lit_var(pClause->pLits[v])] = 1; - } - - // check variables that appear in clauses of B - nVarsAB = 0; - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - if ( pClause->fA ) - continue; - for ( v = 0; v < (int)pClause->nLits; v++ ) - { - Var = lit_var(pClause->pLits[v]); - if ( p->pVarTypes[Var] == 1 ) // var of A - { - // change it into a global variable - nVarsAB++; - p->pVarTypes[Var] = LargeNum; - } - } - } - assert( nVarsAB <= Vec_IntSize(p->vVarsAB) ); - - // order global variables - nVarsAB = 0; - Vec_IntForEachEntry( p->vVarsAB, Var, v ) - p->pVarTypes[Var] = -(1+nVarsAB++); - - // check that there is no extra global variables - for ( v = 0; v < p->pCnf->nVars; v++ ) - assert( p->pVarTypes[v] != LargeNum ); - return nVarsAB; -} - -/**Function************************************************************* - - Synopsis [Resize proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Inta_ManResize( Inta_Man_t * p ) -{ - // check if resizing is needed - if ( p->nVarsAlloc < p->pCnf->nVars ) - { - // find the new size - if ( p->nVarsAlloc == 0 ) - p->nVarsAlloc = 1; - while ( p->nVarsAlloc < p->pCnf->nVars ) - p->nVarsAlloc *= 2; - // resize the arrays - p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); - p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); - p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); - p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc ); - p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); - p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); - } - - // clean the free space - memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); - memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); - memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars ); - memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); - memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); - - // compute the number of common variables - Inta_ManGlobalVars( p ); - - // check if resizing of clauses is needed - if ( p->nClosAlloc < p->pCnf->nClauses ) - { - // find the new size - if ( p->nClosAlloc == 0 ) - p->nClosAlloc = 1; - while ( p->nClosAlloc < p->pCnf->nClauses ) - p->nClosAlloc *= 2; - // resize the arrays - p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); - } - memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); - - // check if resizing of truth tables is needed - if ( p->nIntersAlloc < p->pCnf->nClauses ) - { - p->nIntersAlloc = p->pCnf->nClauses; - p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc ); - } - memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses ); -} - -/**Function************************************************************* - - Synopsis [Deallocate proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Inta_ManFree( Inta_Man_t * p ) -{ -/* - printf( "Runtime stats:\n" ); -PRT( "BCP ", p->timeBcp ); -PRT( "Trace ", p->timeTrace ); -PRT( "TOTAL ", p->timeTotal ); -*/ - free( p->pInters ); - free( p->pProofNums ); - free( p->pTrail ); - free( p->pAssigns ); - free( p->pSeens ); - free( p->pVarTypes ); - free( p->pReasons ); - free( p->pWatches ); - free( p->pResLits ); - free( p ); -} - - - - -/**Function************************************************************* - - Synopsis [Prints the clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Inta_ManPrintClause( Inta_Man_t * p, Sto_Cls_t * pClause ) -{ - int i; - printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Inta_ManProofGet(p, pClause) ); - for ( i = 0; i < (int)pClause->nLits; i++ ) - printf( " %d", pClause->pLits[i] ); - printf( " }\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints the resolvent.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Inta_ManPrintResolvent( lit * pResLits, int nResLits ) -{ - int i; - printf( "Resolvent: {" ); - for ( i = 0; i < nResLits; i++ ) - printf( " %d", pResLits[i] ); - printf( " }\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints the interpolant for one clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Inta_ManPrintInterOne( Inta_Man_t * p, Sto_Cls_t * pClause ) -{ - printf( "Clause %2d : ", pClause->Id ); -// Extra_PrintBinary___( stdout, Inta_ManAigRead(p, pClause), (1 << p->nVarsAB) ); - printf( "\n" ); -} - - - -/**Function************************************************************* - - Synopsis [Adds one clause to the watcher list.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Inta_ManWatchClause( Inta_Man_t * p, Sto_Cls_t * pClause, lit Lit ) -{ - assert( lit_check(Lit, p->pCnf->nVars) ); - if ( pClause->pLits[0] == Lit ) - pClause->pNext0 = p->pWatches[lit_neg(Lit)]; - else - { - assert( pClause->pLits[1] == Lit ); - pClause->pNext1 = p->pWatches[lit_neg(Lit)]; - } - p->pWatches[lit_neg(Lit)] = pClause; -} - - -/**Function************************************************************* - - Synopsis [Records implication.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Inta_ManEnqueue( Inta_Man_t * p, lit Lit, Sto_Cls_t * pReason ) -{ - int Var = lit_var(Lit); - if ( p->pAssigns[Var] != LIT_UNDEF ) - return p->pAssigns[Var] == Lit; - p->pAssigns[Var] = Lit; - p->pReasons[Var] = pReason; - p->pTrail[p->nTrailSize++] = Lit; -//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Records implication.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Inta_ManCancelUntil( Inta_Man_t * p, int Level ) -{ - lit Lit; - int i, Var; - for ( i = p->nTrailSize - 1; i >= Level; i-- ) - { - Lit = p->pTrail[i]; - Var = lit_var( Lit ); - p->pReasons[Var] = NULL; - p->pAssigns[Var] = LIT_UNDEF; -//printf( "cancelling var %d\n", Var ); - } - p->nTrailSize = Level; -} - -/**Function************************************************************* - - Synopsis [Propagate one assignment.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Sto_Cls_t * Inta_ManPropagateOne( Inta_Man_t * p, lit Lit ) -{ - Sto_Cls_t ** ppPrev, * pCur, * pTemp; - lit LitF = lit_neg(Lit); - int i; - // iterate through the literals - ppPrev = p->pWatches + Lit; - for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) - { - // make sure the false literal is in the second literal of the clause - if ( pCur->pLits[0] == LitF ) - { - pCur->pLits[0] = pCur->pLits[1]; - pCur->pLits[1] = LitF; - pTemp = pCur->pNext0; - pCur->pNext0 = pCur->pNext1; - pCur->pNext1 = pTemp; - } - assert( pCur->pLits[1] == LitF ); - - // if the first literal is true, the clause is satisfied - if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) - { - ppPrev = &pCur->pNext1; - continue; - } - - // look for a new literal to watch - for ( i = 2; i < (int)pCur->nLits; i++ ) - { - // skip the case when the literal is false - if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) - continue; - // the literal is either true or unassigned - watch it - pCur->pLits[1] = pCur->pLits[i]; - pCur->pLits[i] = LitF; - // remove this clause from the watch list of Lit - *ppPrev = pCur->pNext1; - // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) - Inta_ManWatchClause( p, pCur, pCur->pLits[1] ); - break; - } - if ( i < (int)pCur->nLits ) // found new watch - continue; - - // clause is unit - enqueue new implication - if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) ) - { - ppPrev = &pCur->pNext1; - continue; - } - - // conflict detected - return the conflict clause - return pCur; - } - return NULL; -} - -/**Function************************************************************* - - Synopsis [Propagate the current assignments.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start ) -{ - Sto_Cls_t * pClause; - int i; - int clk = clock(); - for ( i = Start; i < p->nTrailSize; i++ ) - { - pClause = Inta_ManPropagateOne( p, p->pTrail[i] ); - if ( pClause ) - { -p->timeBcp += clock() - clk; - return pClause; - } - } -p->timeBcp += clock() - clk; - return NULL; -} - - -/**Function************************************************************* - - Synopsis [Writes one root clause into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Inta_ManProofWriteOne( Inta_Man_t * p, Sto_Cls_t * pClause ) -{ - Inta_ManProofSet( p, pClause, ++p->Counter ); - - if ( p->fProofWrite ) - { - int v; - fprintf( p->pFile, "%d", Inta_ManProofGet(p, pClause) ); - for ( v = 0; v < (int)pClause->nLits; v++ ) - fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); - fprintf( p->pFile, " 0 0\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Traces the proof for one clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal ) -{ - Sto_Cls_t * pReason; - int i, v, Var, PrevId; - int fPrint = 0; - int clk = clock(); - - // collect resolvent literals - if ( p->fProofVerif ) - { - assert( (int)pConflict->nLits <= p->nResLitsAlloc ); - memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); - p->nResLits = pConflict->nLits; - } - - // mark all the variables in the conflict as seen - for ( v = 0; v < (int)pConflict->nLits; v++ ) - p->pSeens[lit_var(pConflict->pLits[v])] = 1; - - // start the anticedents -// pFinal->pAntis = Vec_PtrAlloc( 32 ); -// Vec_PtrPush( pFinal->pAntis, pConflict ); - - if ( p->pCnf->nClausesA ) - Inta_ManAigCopy( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pConflict) ); - - // follow the trail backwards - PrevId = Inta_ManProofGet(p, pConflict); - for ( i = p->nTrailSize - 1; i >= 0; i-- ) - { - // skip literals that are not involved - Var = lit_var(p->pTrail[i]); - if ( !p->pSeens[Var] ) - continue; - p->pSeens[Var] = 0; - - // skip literals of the resulting clause - pReason = p->pReasons[Var]; - if ( pReason == NULL ) - continue; - assert( p->pTrail[i] == pReason->pLits[0] ); - - // add the variables to seen - for ( v = 1; v < (int)pReason->nLits; v++ ) - p->pSeens[lit_var(pReason->pLits[v])] = 1; - - - // record the reason clause - assert( Inta_ManProofGet(p, pReason) > 0 ); - p->Counter++; - if ( p->fProofWrite ) - fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) ); - PrevId = p->Counter; - - if ( p->pCnf->nClausesA ) - { - if ( p->pVarTypes[Var] == 1 ) // var of A - Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) ); - else - Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) ); - } - - // resolve the temporary resolvent with the reason clause - if ( p->fProofVerif ) - { - int v1, v2; - if ( fPrint ) - Inta_ManPrintResolvent( p->pResLits, p->nResLits ); - // check that the var is present in the resolvent - for ( v1 = 0; v1 < p->nResLits; v1++ ) - if ( lit_var(p->pResLits[v1]) == Var ) - break; - if ( v1 == p->nResLits ) - printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); - if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) - printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); - // remove this variable from the resolvent - assert( lit_var(p->pResLits[v1]) == Var ); - p->nResLits--; - for ( ; v1 < p->nResLits; v1++ ) - p->pResLits[v1] = p->pResLits[v1+1]; - // add variables of the reason clause - for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) - { - for ( v1 = 0; v1 < p->nResLits; v1++ ) - if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) - break; - // if it is a new variable, add it to the resolvent - if ( v1 == p->nResLits ) - { - if ( p->nResLits == p->nResLitsAlloc ) - printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id ); - p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; - continue; - } - // if the variable is the same, the literal should be the same too - if ( p->pResLits[v1] == pReason->pLits[v2] ) - continue; - // the literal is different - printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); - } - } - -// Vec_PtrPush( pFinal->pAntis, pReason ); - } - - // unmark all seen variables -// for ( i = p->nTrailSize - 1; i >= 0; i-- ) -// p->pSeens[lit_var(p->pTrail[i])] = 0; - // check that the literals are unmarked -// for ( i = p->nTrailSize - 1; i >= 0; i-- ) -// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); - - // use the resulting clause to check the correctness of resolution - if ( p->fProofVerif ) - { - int v1, v2; - if ( fPrint ) - Inta_ManPrintResolvent( p->pResLits, p->nResLits ); - for ( v1 = 0; v1 < p->nResLits; v1++ ) - { - for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) - if ( pFinal->pLits[v2] == p->pResLits[v1] ) - break; - if ( v2 < (int)pFinal->nLits ) - continue; - break; - } - if ( v1 < p->nResLits ) - { - printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); - Inta_ManPrintClause( p, pConflict ); - Inta_ManPrintResolvent( p->pResLits, p->nResLits ); - Inta_ManPrintClause( p, pFinal ); - } - } -p->timeTrace += clock() - clk; - - // return the proof pointer - if ( p->pCnf->nClausesA ) - { -// Inta_ManPrintInterOne( p, pFinal ); - } - Inta_ManProofSet( p, pFinal, p->Counter ); - return p->Counter; -} - -/**Function************************************************************* - - Synopsis [Records the proof for one clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause ) -{ - Sto_Cls_t * pConflict; - int i; - - // empty clause never ends up there - assert( pClause->nLits > 0 ); - if ( pClause->nLits == 0 ) - printf( "Error: Empty clause is attempted.\n" ); - - // add assumptions to the trail - assert( !pClause->fRoot ); - assert( p->nTrailSize == p->nRootSize ); - for ( i = 0; i < (int)pClause->nLits; i++ ) - if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) - { - assert( 0 ); // impossible - return 0; - } - - // propagate the assumptions - pConflict = Inta_ManPropagate( p, p->nRootSize ); - if ( pConflict == NULL ) - { - assert( 0 ); // cannot prove - return 0; - } - - // construct the proof - Inta_ManProofTraceOne( p, pConflict, pClause ); - - // undo to the root level - Inta_ManCancelUntil( p, p->nRootSize ); - - // add large clauses to the watched lists - if ( pClause->nLits > 1 ) - { - Inta_ManWatchClause( p, pClause, pClause->pLits[0] ); - Inta_ManWatchClause( p, pClause, pClause->pLits[1] ); - return 1; - } - assert( pClause->nLits == 1 ); - - // if the clause proved is unit, add it and propagate - if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) ) - { - assert( 0 ); // impossible - return 0; - } - - // propagate the assumption - pConflict = Inta_ManPropagate( p, p->nRootSize ); - if ( pConflict ) - { - // construct the proof - Inta_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); -// if ( p->fVerbose ) -// printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); - return 0; - } - - // update the root level - p->nRootSize = p->nTrailSize; - return 1; -} - -/**Function************************************************************* - - Synopsis [Propagate the root clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Inta_ManProcessRoots( Inta_Man_t * p ) -{ - Sto_Cls_t * pClause; - int Counter; - - // make sure the root clauses are preceeding the learnt clauses - Counter = 0; - Sto_ManForEachClause( p->pCnf, pClause ) - { - assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) ); - assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) ); - Counter++; - } - assert( p->pCnf->nClauses == Counter ); - - // make sure the last clause if empty - assert( p->pCnf->pTail->nLits == 0 ); - - // go through the root unit clauses - p->nTrailSize = 0; - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - // create watcher lists for the root clauses - if ( pClause->nLits > 1 ) - { - Inta_ManWatchClause( p, pClause, pClause->pLits[0] ); - Inta_ManWatchClause( p, pClause, pClause->pLits[1] ); - } - // empty clause and large clauses - if ( pClause->nLits != 1 ) - continue; - // unit clause - assert( lit_check(pClause->pLits[0], p->pCnf->nVars) ); - if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) ) - { - // detected root level conflict - printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); - assert( 0 ); - return 0; - } - } - - // propagate the root unit clauses - pClause = Inta_ManPropagate( p, 0 ); - if ( pClause ) - { - // detected root level conflict - Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); - if ( p->fVerbose ) - printf( "Found root level conflict!\n" ); - return 0; - } - - // set the root level - p->nRootSize = p->nTrailSize; - return 1; -} - -/**Function************************************************************* - - Synopsis [Records the proof.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Inta_ManPrepareInter( Inta_Man_t * p ) -{ - Sto_Cls_t * pClause; - int Var, VarAB, v; - - // set interpolants for root clauses - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - { - if ( !pClause->fA ) // clause of B - { - Inta_ManAigFill( p, Inta_ManAigRead(p, pClause) ); -// Inta_ManPrintInterOne( p, pClause ); - continue; - } - // clause of A - Inta_ManAigClear( p, Inta_ManAigRead(p, pClause) ); - for ( v = 0; v < (int)pClause->nLits; v++ ) - { - Var = lit_var(pClause->pLits[v]); - if ( p->pVarTypes[Var] < 0 ) // global var - { - VarAB = -p->pVarTypes[Var]-1; - assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) ); - if ( lit_sign(pClause->pLits[v]) ) // negative var - Inta_ManAigOrNotVar( p, Inta_ManAigRead(p, pClause), VarAB ); - else - Inta_ManAigOrVar( p, Inta_ManAigRead(p, pClause), VarAB ); - } - } -// Inta_ManPrintInterOne( p, pClause ); - } -} - -/**Function************************************************************* - - Synopsis [Computes interpolant for the given CNF.] - - Description [Takes the interpolation manager, the CNF deriving by the SAT - solver, which includes ClausesA, ClausesB, and learned clauses. Additional - arguments are the vector of variables common to AB and the verbosiness flag. - Returns the AIG manager with a single output, containing the interpolant.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ) -{ - Aig_Man_t * pRes; - Sto_Cls_t * pClause; - int RetValue = 1; - int clkTotal = clock(); - - // check that the CNF makes sense - assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); - p->pCnf = pCnf; - p->fVerbose = fVerbose; - p->vVarsAB = vVarsAB; - p->pAig = pRes = Aig_ManStart( 10000 ); - Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 ); - - // adjust the manager - Inta_ManResize( p ); - - // prepare the interpolant computation - Inta_ManPrepareInter( p ); - - // construct proof for each clause - // start the proof - if ( p->fProofWrite ) - { - p->pFile = fopen( "proof.cnf_", "w" ); - p->Counter = 0; - } - - // write the root clauses - Sto_ManForEachClauseRoot( p->pCnf, pClause ) - Inta_ManProofWriteOne( p, pClause ); - - // propagate root level assignments - if ( Inta_ManProcessRoots( p ) ) - { - // if there is no conflict, consider learned clauses - Sto_ManForEachClause( p->pCnf, pClause ) - { - if ( pClause->fRoot ) - continue; - if ( !Inta_ManProofRecordOne( p, pClause ) ) - { - RetValue = 0; - break; - } - } - } - - // stop the proof - if ( p->fProofWrite ) - { - fclose( p->pFile ); - p->pFile = NULL; - } - - if ( fVerbose ) - { - PRT( "Interpo", clock() - clkTotal ); - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", - p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, - 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), - 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); -p->timeTotal += clock() - clkTotal; - } - - Aig_ObjCreatePo( pRes, *Inta_ManAigRead( p, p->pCnf->pTail ) ); - Aig_ManCleanup( pRes ); - - p->pAig = NULL; - return pRes; - -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c deleted file mode 100644 index 7fa1a824..00000000 --- a/src/sat/bsat/satMem.c +++ /dev/null @@ -1,527 +0,0 @@ -/**CFile**************************************************************** - - FileName [satMem.c] - - PackageName [SAT solver.] - - Synopsis [Memory management.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: satMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "satMem.h" -#include "vec.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -struct Sat_MmFixed_t_ -{ - // information about individual entries - int nEntrySize; // the size of one entry - int nEntriesAlloc; // the total number of entries allocated - int nEntriesUsed; // the number of entries in use - int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of free entries - - // this is where the memory is stored - int nChunkSize; // the size of one chunk - int nChunksAlloc; // the maximum number of memory chunks - int nChunks; // the current number of memory chunks - char ** pChunks; // the allocated memory - - // statistics - int nMemoryUsed; // memory used in the allocated entries - int nMemoryAlloc; // memory allocated -}; - -struct Sat_MmFlex_t_ -{ - // information about individual entries - int nEntriesUsed; // the number of entries allocated - char * pCurrent; // the current pointer to free memory - char * pEnd; // the first entry outside the free memory - - // this is where the memory is stored - int nChunkSize; // the size of one chunk - int nChunksAlloc; // the maximum number of memory chunks - int nChunks; // the current number of memory chunks - char ** pChunks; // the allocated memory - - // statistics - int nMemoryUsed; // memory used in the allocated entries - int nMemoryAlloc; // memory allocated -}; - -struct Sat_MmStep_t_ -{ - int nMems; // the number of fixed memory managers employed - Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc - int nMapSize; // the size of the memory array - Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates memory pieces of fixed size.] - - Description [The size of the chunk is computed as the minimum of - 1024 entries and 64K. Can only work with entry size at least 4 byte long.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize ) -{ - Sat_MmFixed_t * p; - - p = ALLOC( Sat_MmFixed_t, 1 ); - memset( p, 0, sizeof(Sat_MmFixed_t) ); - - p->nEntrySize = nEntrySize; - p->nEntriesAlloc = 0; - p->nEntriesUsed = 0; - p->pEntriesFree = NULL; - - if ( nEntrySize * (1 << 10) < (1<<16) ) - p->nChunkSize = (1 << 10); - else - p->nChunkSize = (1<<16) / nEntrySize; - if ( p->nChunkSize < 8 ) - p->nChunkSize = 8; - - p->nChunksAlloc = 64; - p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); - - p->nMemoryUsed = 0; - p->nMemoryAlloc = 0; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose ) -{ - int i; - if ( p == NULL ) - return; - if ( fVerbose ) - { - printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", - p->nEntrySize, p->nChunkSize, p->nChunks ); - printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", - p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); - } - for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p ) -{ - char * pTemp; - int i; - - // check if there are still free entries - if ( p->nEntriesUsed == p->nEntriesAlloc ) - { // need to allocate more entries - assert( p->pEntriesFree == NULL ); - if ( p->nChunks == p->nChunksAlloc ) - { - p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); - } - p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); - p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; - // transform these entries into a linked list - pTemp = p->pEntriesFree; - for ( i = 1; i < p->nChunkSize; i++ ) - { - *((char **)pTemp) = pTemp + p->nEntrySize; - pTemp += p->nEntrySize; - } - // set the last link - *((char **)pTemp) = NULL; - // add the chunk to the chunk storage - p->pChunks[ p->nChunks++ ] = p->pEntriesFree; - // add to the number of entries allocated - p->nEntriesAlloc += p->nChunkSize; - } - // incrememt the counter of used entries - p->nEntriesUsed++; - if ( p->nEntriesMax < p->nEntriesUsed ) - p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the free entry list - pTemp = p->pEntriesFree; - p->pEntriesFree = *((char **)pTemp); - return pTemp; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry ) -{ - // decrement the counter of used entries - p->nEntriesUsed--; - // add the entry to the linked list of free entries - *((char **)pEntry) = p->pEntriesFree; - p->pEntriesFree = pEntry; -} - -/**Function************************************************************* - - Synopsis [] - - Description [Relocates all the memory except the first chunk.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_MmFixedRestart( Sat_MmFixed_t * p ) -{ - int i; - char * pTemp; - - // deallocate all chunks except the first one - for ( i = 1; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - p->nChunks = 1; - // transform these entries into a linked list - pTemp = p->pChunks[0]; - for ( i = 1; i < p->nChunkSize; i++ ) - { - *((char **)pTemp) = pTemp + p->nEntrySize; - pTemp += p->nEntrySize; - } - // set the last link - *((char **)pTemp) = NULL; - // set the free entry list - p->pEntriesFree = p->pChunks[0]; - // set the correct statistics - p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; - p->nMemoryUsed = 0; - p->nEntriesAlloc = p->nChunkSize; - p->nEntriesUsed = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p ) -{ - return p->nMemoryAlloc; -} - - - -/**Function************************************************************* - - Synopsis [Allocates entries of flexible size.] - - Description [Can only work with entry size at least 4 byte long.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sat_MmFlex_t * Sat_MmFlexStart() -{ - Sat_MmFlex_t * p; - - p = ALLOC( Sat_MmFlex_t, 1 ); - memset( p, 0, sizeof(Sat_MmFlex_t) ); - - p->nEntriesUsed = 0; - p->pCurrent = NULL; - p->pEnd = NULL; - - p->nChunkSize = (1 << 12); - p->nChunksAlloc = 64; - p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); - - p->nMemoryUsed = 0; - p->nMemoryAlloc = 0; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose ) -{ - int i; - if ( p == NULL ) - return; - if ( fVerbose ) - { - printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n", - p->nChunkSize, p->nChunks ); - printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n", - p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); - } - for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes ) -{ - char * pTemp; - // check if there are still free entries - if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) - { // need to allocate more entries - if ( p->nChunks == p->nChunksAlloc ) - { - p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); - } - if ( nBytes > p->nChunkSize ) - { - // resize the chunk size if more memory is requested than it can give - // (ideally, this should never happen) - p->nChunkSize = 2 * nBytes; - } - p->pCurrent = ALLOC( char, p->nChunkSize ); - p->pEnd = p->pCurrent + p->nChunkSize; - p->nMemoryAlloc += p->nChunkSize; - // add the chunk to the chunk storage - p->pChunks[ p->nChunks++ ] = p->pCurrent; - } - assert( p->pCurrent + nBytes <= p->pEnd ); - // increment the counter of used entries - p->nEntriesUsed++; - // keep track of the memory used - p->nMemoryUsed += nBytes; - // return the next entry - pTemp = p->pCurrent; - p->pCurrent += nBytes; - return pTemp; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p ) -{ - return p->nMemoryAlloc; -} - - - - - -/**Function************************************************************* - - Synopsis [Starts the hierarchical memory manager.] - - Description [This manager can allocate entries of any size. - Iternally they are mapped into the entries with the number of bytes - equal to the power of 2. The smallest entry size is 8 bytes. The - next one is 16 bytes etc. So, if the user requests 6 bytes, he gets - 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc. - The input parameters "nSteps" says how many fixed memory managers - are employed internally. Calling this procedure with nSteps equal - to 10 results in 10 hierarchically arranged internal memory managers, - which can allocate up to 4096 (1Kb) entries. Requests for larger - entries are handed over to malloc() and then free()ed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sat_MmStep_t * Sat_MmStepStart( int nSteps ) -{ - Sat_MmStep_t * p; - int i, k; - p = ALLOC( Sat_MmStep_t, 1 ); - p->nMems = nSteps; - // start the fixed memory managers - p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems ); - for ( i = 0; i < p->nMems; i++ ) - p->pMems[i] = Sat_MmFixedStart( (8<<i) ); - // set up the mapping of the required memory size into the corresponding manager - p->nMapSize = (4<<p->nMems); - p->pMap = ALLOC( Sat_MmFixed_t *, p->nMapSize+1 ); - p->pMap[0] = NULL; - for ( k = 1; k <= 4; k++ ) - p->pMap[k] = p->pMems[0]; - for ( i = 0; i < p->nMems; i++ ) - for ( k = (4<<i)+1; k <= (8<<i); k++ ) - p->pMap[k] = p->pMems[i]; -//for ( i = 1; i < 100; i ++ ) -//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize ); - return p; -} - -/**Function************************************************************* - - Synopsis [Stops the memory manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose ) -{ - int i; - for ( i = 0; i < p->nMems; i++ ) - Sat_MmFixedStop( p->pMems[i], fVerbose ); - free( p->pMems ); - free( p->pMap ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Creates the entry.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes ) -{ - if ( nBytes == 0 ) - return NULL; - if ( nBytes > p->nMapSize ) - { -// printf( "Allocating %d bytes.\n", nBytes ); - return ALLOC( char, nBytes ); - } - return Sat_MmFixedEntryFetch( p->pMap[nBytes] ); -} - - -/**Function************************************************************* - - Synopsis [Recycles the entry.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes ) -{ - if ( nBytes == 0 ) - return; - if ( nBytes > p->nMapSize ) - { - free( pEntry ); - return; - } - Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_MmStepReadMemUsage( Sat_MmStep_t * p ) -{ - int i, nMemTotal = 0; - for ( i = 0; i < p->nMems; i++ ) - nMemTotal += p->pMems[i]->nMemoryAlloc; - return nMemTotal; -} diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h deleted file mode 100644 index 22b7a87c..00000000 --- a/src/sat/bsat/satMem.h +++ /dev/null @@ -1,80 +0,0 @@ -/**CFile**************************************************************** - - FileName [satMem.h] - - PackageName [SAT solver.] - - Synopsis [Memory management.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __SAT_MEM_H__ -#define __SAT_MEM_H__ - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//#include "leaks.h" -#include <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <assert.h> - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Sat_MmFixed_t_ Sat_MmFixed_t; -typedef struct Sat_MmFlex_t_ Sat_MmFlex_t; -typedef struct Sat_MmStep_t_ Sat_MmStep_t; - -//////////////////////////////////////////////////////////////////////// -/// GLOBAL VARIABLES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// fixed-size-block memory manager -extern Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize ); -extern void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose ); -extern char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p ); -extern void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry ); -extern void Sat_MmFixedRestart( Sat_MmFixed_t * p ); -extern int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p ); -// flexible-size-block memory manager -extern Sat_MmFlex_t * Sat_MmFlexStart(); -extern void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose ); -extern char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes ); -extern int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p ); -// hierarchical memory manager -extern Sat_MmStep_t * Sat_MmStepStart( int nSteps ); -extern void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose ); -extern char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes ); -extern void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes ); -extern int Sat_MmStepReadMemUsage( Sat_MmStep_t * p ); - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c deleted file mode 100644 index fbc9874d..00000000 --- a/src/sat/bsat/satSolver.c +++ /dev/null @@ -1,1358 +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" - -//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT - -//================================================================================================= -// Debug: - -//#define VERBOSEDEBUG - -// For derivation output (verbosity level 2) -#define L_IND "%-*d" -#define L_ind sat_solver_dlevel(s)*3+3,sat_solver_dlevel(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 void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } - -//================================================================================================= -// Encode literals in clause pointers: - -static inline clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); } -static inline bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } -static inline lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } - -//================================================================================================= -// Simple helpers: - -static inline int sat_solver_dlevel(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]; } -static inline void vecp_remove(vecp* v, void* e) -{ - void** ws = vecp_begin(v); - int j = 0; - for (; ws[j] != e ; j++); - assert(j < vecp_size(v)); - for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1]; - vecp_resize(v,vecp_size(v)-1); -} - -//================================================================================================= -// Variable order functions: - -static inline void order_update(sat_solver* s, int v) // updateorder -{ - int* orderpos = s->orderpos; - double* activity = s->activity; - 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 && activity[x] > 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; - double* activity; - 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); - activity = s->activity; - 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){ - double act = activity[x]; - - int i = 0; - int child = 1; - - - while (child < size){ - if (child+1 < size && activity[heap[child]] < activity[heap[child+1]]) - child++; - - assert(child < size); - - if (act >= 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: - -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_var_bump(sat_solver* s, int v) { - s->activity[v] += s->var_inc; - if (s->activity[v] > 1e100) - act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); - 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); - //printf("bump %d %f\n", v-1, activity[v]); - if (s->orderpos[v] != -1) - order_update(s,v); -} - -static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } - -static inline void act_clause_rescale(sat_solver* s) { - clause** cs = (clause**)vecp_begin(&s->learnts); - int i; - 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; -} - - -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_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; } - -//================================================================================================= -// Clause functions: - -/* pre: size > 1 && no variable occurs twice - */ -static clause* clause_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; -// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - c = (clause*)malloc(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(((unsigned long)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; -} - - -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 - 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_dlevel(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; -} - -//================================================================================================= -// Minor (solver) functions: - -void sat_solver_setnvars(sat_solver* s,int n) -{ - int var; - - if (s->cap < n){ - - while (s->cap < n) s->cap = s->cap*2+1; - - s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2); - s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap); - s->factors = (double*) realloc(s->factors, sizeof(double)*s->cap); - s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap); - s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap); - s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap); - s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap); - s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap); - s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap); - } - - for (var = s->size; var < n; var++){ - vecp_new(&s->wlists[2*var]); - vecp_new(&s->wlists[2*var+1]); - s->activity [var] = 0; - 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; - - /* 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; -} - - -static inline bool enqueue(sat_solver* s, lit l, clause* from) -{ - lbool* values = s->assigns; - int v = lit_var(l); - lbool val = values[v]; -#ifdef VERBOSEDEBUG - printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); -#endif - - lbool sig = !lit_sign(l); sig += sig - 1; - if (val != l_Undef){ - return val == sig; - }else{ - // New fact -- store it. -#ifdef VERBOSEDEBUG - printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); -#endif - int* levels = s->levels; - clause** reasons = s->reasons; - - values [v] = sig; - levels [v] = sat_solver_dlevel(s); - reasons[v] = from; - s->trail[s->qtail++] = l; - - order_assigned(s, v); - return true; - } -} - - -static inline void 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")\n", L_ind, L_lit(l)); -#endif - veci_push(&s->trail_lim,s->qtail); - enqueue(s,l,(clause*)0); -} - - -static void sat_solver_canceluntil(sat_solver* s, int level) { - lit* trail; - lbool* values; - clause** reasons; - int bound; - int c; - - if (sat_solver_dlevel(s) <= level) - return; - - trail = s->trail; - values = s->assigns; - reasons = s->reasons; - bound = (veci_begin(&s->trail_lim))[level]; - - //////////////////////////////////////// - // 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; - } - - 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_new(s,begin,end,1) : (clause*)0; - enqueue(s,*begin,c); - - /////////////////////////////////// - // add clause to internal storage - if ( s->pStore ) - { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( 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 bool 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; -} - -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_dlevel(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_dlevel(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 - s->stats.max_literals += veci_size(learnt); - 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; - - //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)){ -// s->stats.inspects2++; - *j++ = *i; - if (!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: -// s->stats.inspects2 += end - i; - while (i < end) - *j++ = *i++; - } - }else{ - lit false_lit; - lbool sig; - - 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 (!enqueue(s,lits[0], *i)){ - confl = *i++; - // Copy the remaining watches: -// s->stats.inspects2 += end - i; - 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; -} - -static inline 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); -} - -static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_learnts) -{ - int* levels = s->levels; - double var_decay = 0.95; - double clause_decay = 0.999; - double random_var_freq = 0.02; - - sint64 conflictC = 0; - veci learnt_clause; - int i; - - assert(s->root_level == sat_solver_dlevel(s)); - - s->nRestarts++; - s->stats.starts++; - s->var_decay = (float)(1 / var_decay ); - s->cla_decay = (float)(1 / clause_decay); - 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 ) - for ( i = 0; i < s->act_vars.size; i++ ) - act_var_bump_factor(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_dlevel(s) == s->root_level){ - 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); - 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) ) - { - // 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_dlevel(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; - } - - assume(s,lit_neg(toLit(next))); - } - } - - return l_Undef; // cannot happen -} - -//================================================================================================= -// External solver functions: - -sat_solver* sat_solver_new(void) -{ - sat_solver* s = (sat_solver*)malloc(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); - - // 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; - s->cla_inc = 1; - s->cla_decay = 1; - s->var_inc = 1; - s->var_decay = 1; - s->root_level = 0; - s->simpdb_assigns = 0; - s->simpdb_props = 0; - s->random_seed = 91648253; - s->progress_estimate = 0; - s->binary = (clause*)malloc(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.max_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_delete(sat_solver* s) -{ - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - int i; - for (i = 0; i < vecp_size(&s->clauses); i++) - free(vecp_begin(&s->clauses)[i]); - for (i = 0; i < vecp_size(&s->learnts); i++) - 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); - free(s->binary); - - // delete arrays - if (s->wlists != 0){ - int i; - for (i = 0; i < s->size*2; i++) - vecp_delete(&s->wlists[i]); - - // if one is different from null, all are - free(s->wlists ); - free(s->activity ); - free(s->factors ); - free(s->assigns ); - free(s->orderpos ); - free(s->reasons ); - free(s->levels ); - free(s->trail ); - free(s->tags ); - } - - sat_solver_store_free(s); - free(s); -} - - -bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) -{ - lit *i,*j; - int maxvar; - lbool* values; - lit last; - - 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 ); - - //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; - } - - //printf("final: "); printlits(begin,j); printf("\n"); - - if (j == begin) // empty clause - return false; - - /////////////////////////////////// - // add clause to internal storage - if ( s->pStore ) - { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( s->pStore, begin, j ); - assert( RetValue ); - } - /////////////////////////////////// - - if (j - begin == 1) // unit clause - return enqueue(s,*begin,(clause*)0); - - // create new clause - vecp_push(&s->clauses,clause_new(s,begin,j,0)); - - - s->stats.clauses++; - s->stats.clauses_literals += j - begin; - - return true; -} - - -bool sat_solver_simplify(sat_solver* s) -{ - clause** reasons; - int type; - - assert(sat_solver_dlevel(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; -} - - -int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal) -{ - sint64 nof_conflicts = 100; - sint64 nof_learnts = sat_solver_nclauses(s) / 3; - lbool status = l_Undef; - lbool* values = s->assigns; - lit* i; - - // 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; - if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) ) - s->nConfLimit = nConfLimitGlobal; - if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) - s->nInsLimit = nInsLimitGlobal; - - //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 */ - assume(s, *i); - if (sat_solver_propagate(s) == NULL) - break; - // fallthrough - case -1: /* l_False */ - sat_solver_canceluntil(s, 0); - return l_False; - } - } - s->nCalls2++; - - s->root_level = sat_solver_dlevel(s); - - 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){ - double Ratio = (s->stats.learnts == 0)? 0.0 : - s->stats.learnts_literals / (double)s->stats.learnts; - - 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); - } - status = sat_solver_search(s, nof_conflicts, nof_learnts); - nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5; - nof_learnts = nof_learnts * 11 / 10; //*= 1.1; - - // 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 ) - { -// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); - break; - } - } - if (s->verbosity >= 1) - printf("==============================================================================\n"); - - sat_solver_canceluntil(s,0); - - //////////////////////////////////////////////// - if ( status == l_False && s->pStore ) - { - extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); - int RetValue = Sto_ManAddClause( 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 ) -{ - extern void * Sto_ManAlloc(); - assert( s->pStore == NULL ); - s->pStore = Sto_ManAlloc(); -} - -void sat_solver_store_write( sat_solver * s, char * pFileName ) -{ - extern void Sto_ManDumpClauses( void * p, char * pFileName ); - if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName ); -} - -void sat_solver_store_free( sat_solver * s ) -{ - extern void Sto_ManFree( void * p ); - if ( s->pStore ) Sto_ManFree( s->pStore ); - s->pStore = NULL; -} - -void sat_solver_store_mark_roots( sat_solver * s ) -{ - extern void Sto_ManMarkRoots( void * p ); - if ( s->pStore ) Sto_ManMarkRoots( s->pStore ); -} - -void sat_solver_store_mark_clauses_a( sat_solver * s ) -{ - extern void Sto_ManMarkClausesA( void * p ); - if ( s->pStore ) Sto_ManMarkClausesA( 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 *)) -{ - double seed = 91648253; - sortrnd(array,size,comp,&seed); -} diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h deleted file mode 100644 index c1bf32a7..00000000 --- a/src/sat/bsat/satSolver.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 satSolver_h -#define satSolver_h - -#ifdef _WIN32 -#define inline __inline // compatible with MS VS 6.0 -#endif - -#include "satVec.h" -#include "satMem.h" - -//================================================================================================= -// Simple types: - -// does not work for c++ -//typedef int bool; -#ifndef __cplusplus -#ifndef bool -#define bool int -#endif -#endif - -static const bool true = 1; -static const bool false = 0; - -typedef int lit; -typedef char lbool; - -#ifndef SINT64 -#define SINT64 - -#ifdef _WIN32 -typedef signed __int64 sint64; // compatible with MS VS 6.0 -#else -typedef long long sint64; -#endif - -#endif - -static const int var_Undef = -1; -static const lit lit_Undef = -2; - -static const lbool l_Undef = 0; -static const lbool l_True = 1; -static const lbool l_False = -1; - -static inline lit toLit (int v) { return v + v; } -static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } -static inline lit lit_neg (lit l) { return l ^ 1; } -static inline int lit_var (lit l) { return l >> 1; } -static inline int lit_sign (lit l) { return l & 1; } -static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } -static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } -static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } - - -//================================================================================================= -// 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 bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end); -extern bool sat_solver_simplify(sat_solver* s); -extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal); - -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); - -struct stats_t -{ - sint64 starts, decisions, propagations, inspects, conflicts; - sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; -}; -typedef struct stats_t stats; - -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 - 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. - - vecp* wlists; // - double* activity; // A heuristic measurement of the activity of a variable. - lbool* assigns; // Current values of variables. - int* orderpos; // Index in variable order. - clause** reasons; // - int* levels; // - lit* trail; - - 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). - - 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 stats; - - sint64 nConfLimit; // external limit on the number of conflicts - sint64 nInsLimit; // external limit on the number of implications - - 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 - - // clause store - void * pStore; - - // trace recording - FILE * pFile; - int nClauses; - int nRoots; -}; - -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; -} - -#endif diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c deleted file mode 100644 index f968162e..00000000 --- a/src/sat/bsat/satStore.c +++ /dev/null @@ -1,437 +0,0 @@ -/**CFile**************************************************************** - - FileName [satStore.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [SAT solver.] - - Synopsis [Records the trace of SAT solving in the CNF form.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: satStore.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <assert.h> -#include <time.h> -#include "satStore.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Fetches memory.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Sto_ManMemoryFetch( Sto_Man_t * p, int nBytes ) -{ - char * pMem; - if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed ) - { - pMem = (char *)malloc( p->nChunkSize ); - *(char **)pMem = p->pChunkLast; - p->pChunkLast = pMem; - p->nChunkUsed = sizeof(char *); - } - pMem = p->pChunkLast + p->nChunkUsed; - p->nChunkUsed += nBytes; - return pMem; -} - -/**Function************************************************************* - - Synopsis [Frees memory manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sto_ManMemoryStop( Sto_Man_t * p ) -{ - char * pMem, * pNext; - if ( p->pChunkLast == NULL ) - return; - for ( pMem = p->pChunkLast; (pNext = *(char **)pMem); pMem = pNext ) - free( pMem ); - free( pMem ); -} - -/**Function************************************************************* - - Synopsis [Reports memory usage in bytes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sto_ManMemoryReport( Sto_Man_t * p ) -{ - int Total; - char * pMem, * pNext; - if ( p->pChunkLast == NULL ) - return 0; - Total = p->nChunkUsed; - for ( pMem = p->pChunkLast; (pNext = *(char **)pMem); pMem = pNext ) - Total += p->nChunkSize; - return Total; -} - - -/**Function************************************************************* - - Synopsis [Allocate proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sto_Man_t * Sto_ManAlloc() -{ - Sto_Man_t * p; - // allocate the manager - p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) ); - memset( p, 0, sizeof(Sto_Man_t) ); - // memory management - p->nChunkSize = (1<<16); // use 64K chunks - return p; -} - -/**Function************************************************************* - - Synopsis [Deallocate proof manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sto_ManFree( Sto_Man_t * p ) -{ - Sto_ManMemoryStop( p ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Adds one clause to the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ) -{ - Sto_Cls_t * pClause; - lit Lit, * i, * j; - int nSize; - - // process the literals - if ( pBeg < pEnd ) - { - // insertion sort - for ( i = pBeg + 1; i < pEnd; i++ ) - { - Lit = *i; - for ( j = i; j > pBeg && *(j-1) > Lit; j-- ) - *j = *(j-1); - *j = Lit; - } - // make sure there is no duplicated variables - for ( i = pBeg + 1; i < pEnd; i++ ) - if ( lit_var(*(i-1)) == lit_var(*i) ) - { - printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i ); - return 0; - } - // check the largest var size - p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 ); - } - - // get memory for the clause - nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg); - pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize ); - memset( pClause, 0, sizeof(Sto_Cls_t) ); - - // assign the clause - pClause->Id = p->nClauses++; - pClause->nLits = pEnd - pBeg; - memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) ); - - // add the clause to the list - if ( p->pHead == NULL ) - p->pHead = pClause; - if ( p->pTail == NULL ) - p->pTail = pClause; - else - { - p->pTail->pNext = pClause; - p->pTail = pClause; - } - - // add the empty clause - if ( pClause->nLits == 0 ) - { - if ( p->pEmpty ) - { - printf( "More than one empty clause!\n" ); - return 0; - } - p->pEmpty = pClause; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Mark all clauses added so far as root clauses.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sto_ManMarkRoots( Sto_Man_t * p ) -{ - Sto_Cls_t * pClause; - p->nRoots = 0; - Sto_ManForEachClause( p, pClause ) - { - pClause->fRoot = 1; - p->nRoots++; - } -} - -/**Function************************************************************* - - Synopsis [Mark all clauses added so far as clause of A.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sto_ManMarkClausesA( Sto_Man_t * p ) -{ - Sto_Cls_t * pClause; - p->nClausesA = 0; - Sto_ManForEachClause( p, pClause ) - { - pClause->fA = 1; - p->nClausesA++; - } -} - - -/**Function************************************************************* - - Synopsis [Writes the stored clauses into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName ) -{ - FILE * pFile; - Sto_Cls_t * pClause; - int i; - // start the file - pFile = fopen( pFileName, "w" ); - if ( pFile == NULL ) - { - printf( "Error: Cannot open output file (%s).\n", pFileName ); - return; - } - // write the data - fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA ); - Sto_ManForEachClause( p, pClause ) - { - for ( i = 0; i < (int)pClause->nLits; i++ ) - fprintf( pFile, " %d", lit_print(pClause->pLits[i]) ); - fprintf( pFile, "\n" ); - } - fprintf( pFile, " 0\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Reads one literal from file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sto_ManLoadNumber( FILE * pFile, int * pNumber ) -{ - int Char, Number = 0, Sign = 0; - // skip space-like chars - do { - Char = fgetc( pFile ); - if ( Char == EOF ) - return 0; - } while ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' ); - // read the literal - while ( 1 ) - { - // get the next character - Char = fgetc( pFile ); - if ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' ) - break; - // check that the char is a digit - if ( (Char < '0' || Char > '9') && Char != '-' ) - { - printf( "Error: Wrong char (%c) in the input file.\n", Char ); - return 0; - } - // check if this is a minus - if ( Char == '-' ) - Sign = 1; - else - Number = 10 * Number + Char; - } - // return the number - *pNumber = Sign? -Number : Number; - return 1; -} - -/**Function************************************************************* - - Synopsis [Reads CNF from file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sto_Man_t * Sto_ManLoadClauses( char * pFileName ) -{ - FILE * pFile; - Sto_Man_t * p; - Sto_Cls_t * pClause; - char pBuffer[1024]; - int nLits, nLitsAlloc, Counter, Number; - lit * pLits; - - // start the file - pFile = fopen( pFileName, "r" ); - if ( pFile == NULL ) - { - printf( "Error: Cannot open input file (%s).\n", pFileName ); - return NULL; - } - - // create the manager - p = Sto_ManAlloc(); - - // alloc the array of literals - nLitsAlloc = 1024; - pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc ); - - // read file header - p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0; - while ( fgets( pBuffer, 1024, pFile ) ) - { - if ( pBuffer[0] == 'c' ) - continue; - if ( pBuffer[0] == 'p' ) - { - sscanf( pBuffer + 1, "%d %d %d %d", &p->nVars, &p->nClauses, &p->nRoots, &p->nClausesA ); - break; - } - printf( "Warning: Skipping line: \"%s\"\n", pBuffer ); - } - - // read the clauses - nLits = 0; - while ( Sto_ManLoadNumber(pFile, &Number) ) - { - if ( Number == 0 ) - { - int RetValue; - RetValue = Sto_ManAddClause( p, pLits, pLits + nLits ); - assert( RetValue ); - nLits = 0; - continue; - } - if ( nLits == nLitsAlloc ) - { - nLitsAlloc *= 2; - pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc ); - } - pLits[ nLits++ ] = lit_read(Number); - } - if ( nLits > 0 ) - printf( "Error: The last clause was not saved.\n" ); - - // count clauses - Counter = 0; - Sto_ManForEachClause( p, pClause ) - Counter++; - - // check the number of clauses - if ( p->nClauses != Counter ) - { - printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses ); - Sto_ManFree( p ); - return NULL; - } - - free( pLits ); - fclose( pFile ); - return p; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h deleted file mode 100644 index b66abc8f..00000000 --- a/src/sat/bsat/satStore.h +++ /dev/null @@ -1,146 +0,0 @@ -/**CFile**************************************************************** - - FileName [satStore.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Proof recording.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __SAT_STORE_H__ -#define __SAT_STORE_H__ - -#include "satSolver.h" - -/* - The trace of SAT solving contains the original clauses of the problem - along with the learned clauses derived during SAT solving. - The first line of the resulting file contains 3 numbers instead of 2: - c <num_vars> <num_all_clauses> <num_root_clauses> -*/ - -#ifdef __cplusplus -extern "C" { -#endif - -#ifdef _WIN32 -#define inline __inline // compatible with MS VS 6.0 -#endif - -#ifndef PRT -#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) -#endif - -#define STO_MAX(a,b) ((a) > (b) ? (a) : (b)) - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -/* -typedef unsigned lit; -// variable/literal conversions (taken from MiniSat) -static inline lit toLit (int v) { return v + v; } -static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } -static inline lit lit_neg (lit l) { return l ^ 1; } -static inline int lit_var (lit l) { return l >> 1; } -static inline int lit_sign (lit l) { return l & 1; } -static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } -static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } -static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } -*/ - -typedef struct Sto_Cls_t_ Sto_Cls_t; -struct Sto_Cls_t_ -{ - Sto_Cls_t * pNext; // the next clause - Sto_Cls_t * pNext0; // the next 0-watch - Sto_Cls_t * pNext1; // the next 0-watch - int Id; // the clause ID - unsigned fA : 1; // belongs to A - unsigned fRoot : 1; // original clause - unsigned fVisit : 1; // visited clause - unsigned nLits : 24; // the number of literals - lit pLits[0]; // literals of this clause -}; - -typedef struct Sto_Man_t_ Sto_Man_t; -struct Sto_Man_t_ -{ - // general data - int nVars; // the number of variables - int nRoots; // the number of root clauses - int nClauses; // the number of all clauses - int nClausesA; // the number of clauses of A - Sto_Cls_t * pHead; // the head clause - Sto_Cls_t * pTail; // the tail clause - Sto_Cls_t * pEmpty; // the empty clause - // memory management - int nChunkSize; // the number of bytes in a chunk - int nChunkUsed; // the number of bytes used in the last chunk - char * pChunkLast; // the last memory chunk -}; - -// iterators through the clauses -#define Sto_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext ) -#define Sto_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext ) - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== satStore.c ==========================================================*/ -extern Sto_Man_t * Sto_ManAlloc(); -extern void Sto_ManFree( Sto_Man_t * p ); -extern int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ); -extern int Sto_ManMemoryReport( Sto_Man_t * p ); -extern void Sto_ManMarkRoots( Sto_Man_t * p ); -extern void Sto_ManMarkClausesA( Sto_Man_t * p ); -extern void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName ); -extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName ); - -/*=== satInter.c ==========================================================*/ -typedef struct Int_Man_t_ Int_Man_t; -extern Int_Man_t * Int_ManAlloc(); -extern void Int_ManFree( Int_Man_t * p ); -extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult ); - -/*=== satInterA.c ==========================================================*/ -typedef struct Inta_Man_t_ Inta_Man_t; -extern Inta_Man_t * Inta_ManAlloc(); -extern void Inta_ManFree( Inta_Man_t * p ); -extern void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c deleted file mode 100644 index 111e8dfb..00000000 --- a/src/sat/bsat/satTrace.c +++ /dev/null @@ -1,109 +0,0 @@ -/**CFile**************************************************************** - - FileName [satTrace.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [SAT sat_solver.] - - Synopsis [Records the trace of SAT solving in the CNF form.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "satSolver.h" - -/* - The trace of SAT solving contains the original clause of the problem - along with the learned clauses derived during SAT solving. - The first line of the resulting file contains 3 numbers instead of 2: - c <num_vars> <num_all_clauses> <num_root_clauses> -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Start the trace recording.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverTraceStart( sat_solver * pSat, char * pName ) -{ - assert( pSat->pFile == NULL ); - pSat->pFile = fopen( pName, "w" ); - fprintf( pSat->pFile, " \n" ); - pSat->nClauses = 0; - pSat->nRoots = 0; -} - -/**Function************************************************************* - - Synopsis [Stops the trace recording.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverTraceStop( sat_solver * pSat ) -{ - if ( pSat->pFile == NULL ) - return; - rewind( pSat->pFile ); - fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots ); - fclose( pSat->pFile ); - pSat->pFile = NULL; -} - - -/**Function************************************************************* - - Synopsis [Writes one clause into the trace file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot ) -{ - if ( pSat->pFile == NULL ) - return; - pSat->nClauses++; - pSat->nRoots += fRoot; - for ( ; pBeg < pEnd ; pBeg++ ) - fprintf( pSat->pFile, " %d", lit_print(*pBeg) ); - fprintf( pSat->pFile, " 0\n" ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c deleted file mode 100644 index 3961cf7e..00000000 --- a/src/sat/bsat/satUtil.c +++ /dev/null @@ -1,234 +0,0 @@ -/**CFile**************************************************************** - - FileName [satUtil.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [C-language MiniSat solver.] - - Synopsis [Additional SAT solver procedures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "satSolver.h" -#include "vec.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -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 void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Write the clauses in the solver into a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ) -{ - FILE * pFile; - void ** pClauses; - int nClauses, i; - - // count the number of clauses - nClauses = p->clauses.size + p->learnts.size; - for ( i = 0; i < p->size; i++ ) - if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) - nClauses++; - - // start the file - pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" ); - return; - } -// fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); - fprintf( pFile, "p cnf %d %d\n", p->size, nClauses ); - - // write the original clauses - nClauses = p->clauses.size; - pClauses = p->clauses.ptr; - for ( i = 0; i < nClauses; i++ ) - Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars ); - - // write the learned clauses - nClauses = p->learnts.size; - pClauses = p->learnts.ptr; - for ( i = 0; i < nClauses; i++ ) - Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars ); - - // write zero-level assertions - for ( i = 0; i < p->size; i++ ) - if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) - fprintf( pFile, "%s%d%s\n", - (p->assigns[i] == l_False)? "-": "", - i + (int)(incrementVars>0), - (incrementVars) ? " 0" : ""); - - // write the assumptions - if (assumptionsBegin) { - for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) { - fprintf( pFile, "%s%d%s\n", - lit_sign(*assumptionsBegin)? "-": "", - lit_var(*assumptionsBegin) + (int)(incrementVars>0), - (incrementVars) ? " 0" : ""); - } - } - - fprintf( pFile, "\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) -{ - lit * pLits = clause_begin(pC); - int nLits = clause_size(pC); - int i; - - for ( i = 0; i < nLits; i++ ) - fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (int)(fIncrement>0) ); - if ( fIncrement ) - fprintf( pFile, "0" ); - fprintf( pFile, "\n" ); -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) -{ -// printf( "calls : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); - printf( "starts : %8d\n", (int)p->stats.starts ); - printf( "conflicts : %8d\n", (int)p->stats.conflicts ); - printf( "decisions : %8d\n", (int)p->stats.decisions ); - printf( "propagations : %8d\n", (int)p->stats.propagations ); - printf( "inspects : %8d\n", (int)p->stats.inspects ); -// printf( "inspects2 : %8d\n", (int)p->stats.inspects2 ); -} - -/**Function************************************************************* - - Synopsis [Returns a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ) -{ - int * pModel; - int i; - pModel = ALLOC( int, nVars ); - for ( i = 0; i < nVars; i++ ) - { - assert( pVars[i] >= 0 && pVars[i] < p->size ); - pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True); - } - return pModel; -} - -/**Function************************************************************* - - Synopsis [Duplicates all clauses, complements unit clause of the given var.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) -{ - clause * pClause; - lit Lit, * pLits; - int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v; - // get the number of variables - nVarsOld = p->size; - nLitsOld = 2 * p->size; - // extend the solver to depend on two sets of variables - sat_solver_setnvars( p, 2 * p->size ); - // duplicate implications - for ( v = 0; v < nVarsOld; v++ ) - if ( p->assigns[v] != l_Undef ) - { - Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False ); - if ( v == iVar ) - Lit = lit_neg(Lit); - RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 ); - assert( RetValue ); - } - // duplicate clauses - nClauses = vecp_size(&p->clauses); - for ( c = 0; c < nClauses; c++ ) - { - pClause = p->clauses.ptr[c]; - nLits = clause_size(pClause); - pLits = clause_begin(pClause); - for ( v = 0; v < nLits; v++ ) - pLits[v] += nLitsOld; - RetValue = sat_solver_addclause( p, pLits, pLits + nLits ); - assert( RetValue ); - for ( v = 0; v < nLits; v++ ) - pLits[v] -= nLitsOld; - } -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h deleted file mode 100644 index d7fce5c0..00000000 --- a/src/sat/bsat/satVec.h +++ /dev/null @@ -1,83 +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 satVec_h -#define satVec_h - -#include <stdlib.h> - -// vector of 32-bit intergers (added for 64-bit portability) -struct veci_t { - int size; - int cap; - int* ptr; -}; -typedef struct veci_t veci; - -static inline void veci_new (veci* v) { - v->size = 0; - v->cap = 4; - v->ptr = (int*)malloc(sizeof(int)*v->cap); -} - -static inline void veci_delete (veci* v) { free(v->ptr); } -static inline int* veci_begin (veci* v) { return v->ptr; } -static inline int veci_size (veci* v) { return v->size; } -static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !! -static inline void veci_push (veci* v, int e) -{ - if (v->size == v->cap) { - int newsize = v->cap * 2;//+1; - v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize); - v->cap = newsize; } - v->ptr[v->size++] = e; -} - - -// vector of 32- or 64-bit pointers -struct vecp_t { - int size; - int cap; - void** ptr; -}; -typedef struct vecp_t vecp; - -static inline void vecp_new (vecp* v) { - v->size = 0; - v->cap = 4; - v->ptr = (void**)malloc(sizeof(void*)*v->cap); -} - -static inline void vecp_delete (vecp* v) { free(v->ptr); } -static inline void** vecp_begin (vecp* v) { return v->ptr; } -static inline int vecp_size (vecp* v) { return v->size; } -static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !! -static inline void vecp_push (vecp* v, void* e) -{ - if (v->size == v->cap) { - int newsize = v->cap * 2;//+1; - v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize); - v->cap = newsize; } - v->ptr[v->size++] = e; -} - - -#endif |