diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
commit | 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (patch) | |
tree | 366355938a4af0a92f848841ac65374f338d691b /src/abc8/bsat | |
parent | 6537f941887b06e588d3acfc97b5fdf48875cc4e (diff) | |
download | abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.gz abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.bz2 abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.zip |
Version abc80130
Diffstat (limited to 'src/abc8/bsat')
-rw-r--r-- | src/abc8/bsat/module.make | 6 | ||||
-rw-r--r-- | src/abc8/bsat/satInter.c | 991 | ||||
-rw-r--r-- | src/abc8/bsat/satInterA.c | 970 | ||||
-rw-r--r-- | src/abc8/bsat/satMem.c | 527 | ||||
-rw-r--r-- | src/abc8/bsat/satMem.h | 80 | ||||
-rw-r--r-- | src/abc8/bsat/satSolver.c | 1358 | ||||
-rw-r--r-- | src/abc8/bsat/satSolver.h | 210 | ||||
-rw-r--r-- | src/abc8/bsat/satStore.c | 437 | ||||
-rw-r--r-- | src/abc8/bsat/satStore.h | 146 | ||||
-rw-r--r-- | src/abc8/bsat/satTrace.c | 109 | ||||
-rw-r--r-- | src/abc8/bsat/satUtil.c | 234 | ||||
-rw-r--r-- | src/abc8/bsat/satVec.h | 83 |
12 files changed, 5151 insertions, 0 deletions
diff --git a/src/abc8/bsat/module.make b/src/abc8/bsat/module.make new file mode 100644 index 00000000..563c8dfc --- /dev/null +++ b/src/abc8/bsat/module.make @@ -0,0 +1,6 @@ +SRC += src/sat/bsat/satMem.c \ + src/sat/bsat/satInter.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/abc8/bsat/satInter.c b/src/abc8/bsat/satInter.c new file mode 100644 index 00000000..8e07e9f6 --- /dev/null +++ b/src/abc8/bsat/satInter.c @@ -0,0 +1,991 @@ +/**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/abc8/bsat/satInterA.c b/src/abc8/bsat/satInterA.c new file mode 100644 index 00000000..513a9044 --- /dev/null +++ b/src/abc8/bsat/satInterA.c @@ -0,0 +1,970 @@ +/**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/abc8/bsat/satMem.c b/src/abc8/bsat/satMem.c new file mode 100644 index 00000000..7fa1a824 --- /dev/null +++ b/src/abc8/bsat/satMem.c @@ -0,0 +1,527 @@ +/**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/abc8/bsat/satMem.h b/src/abc8/bsat/satMem.h new file mode 100644 index 00000000..22b7a87c --- /dev/null +++ b/src/abc8/bsat/satMem.h @@ -0,0 +1,80 @@ +/**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/abc8/bsat/satSolver.c b/src/abc8/bsat/satSolver.c new file mode 100644 index 00000000..fbc9874d --- /dev/null +++ b/src/abc8/bsat/satSolver.c @@ -0,0 +1,1358 @@ +/************************************************************************************************** +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/abc8/bsat/satSolver.h b/src/abc8/bsat/satSolver.h new file mode 100644 index 00000000..c1bf32a7 --- /dev/null +++ b/src/abc8/bsat/satSolver.h @@ -0,0 +1,210 @@ +/************************************************************************************************** +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/abc8/bsat/satStore.c b/src/abc8/bsat/satStore.c new file mode 100644 index 00000000..f968162e --- /dev/null +++ b/src/abc8/bsat/satStore.c @@ -0,0 +1,437 @@ +/**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/abc8/bsat/satStore.h b/src/abc8/bsat/satStore.h new file mode 100644 index 00000000..b66abc8f --- /dev/null +++ b/src/abc8/bsat/satStore.h @@ -0,0 +1,146 @@ +/**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/abc8/bsat/satTrace.c b/src/abc8/bsat/satTrace.c new file mode 100644 index 00000000..111e8dfb --- /dev/null +++ b/src/abc8/bsat/satTrace.c @@ -0,0 +1,109 @@ +/**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/abc8/bsat/satUtil.c b/src/abc8/bsat/satUtil.c new file mode 100644 index 00000000..3961cf7e --- /dev/null +++ b/src/abc8/bsat/satUtil.c @@ -0,0 +1,234 @@ +/**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/abc8/bsat/satVec.h b/src/abc8/bsat/satVec.h new file mode 100644 index 00000000..d7fce5c0 --- /dev/null +++ b/src/abc8/bsat/satVec.h @@ -0,0 +1,83 @@ +/************************************************************************************************** +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 |