From 1c26e2d29768c64315447969f137e3bf9ffa7dac Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 24 Jan 2007 08:01:00 -0800 Subject: Version abc70124 --- src/sat/bsat/module.make | 3 +++ src/sat/bsat/satInter.c | 67 ++++++++++++++++++++++++++---------------------- src/sat/bsat/satSolver.c | 2 +- src/sat/bsat/satStore.c | 2 +- src/sat/bsat/satStore.h | 2 ++ src/sat/bsat/satUtil.c | 8 +++--- 6 files changed, 48 insertions(+), 36 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make index c8ec65dd..563c8dfc 100644 --- a/src/sat/bsat/module.make +++ b/src/sat/bsat/module.make @@ -1,3 +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/sat/bsat/satInter.c b/src/sat/bsat/satInter.c index e22b309c..32a011b9 100644 --- a/src/sat/bsat/satInter.c +++ b/src/sat/bsat/satInter.c @@ -71,18 +71,18 @@ struct Int_Man_t_ int timeTotal; // the total runtime of interpolation }; -// procedure to get hold of the clauses' truth table +// 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_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_ManProofRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } -static inline void Int_ManProofWrite( Int_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } +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 /// @@ -110,7 +110,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc ) p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); // parameters p->fProofWrite = 0; - p->fProofVerif = 0; + p->fProofVerif = 1; return p; } @@ -125,7 +125,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc ) SeeAlso [] ***********************************************************************/ -int Int_ManCommonVars( Int_Man_t * p ) +int Int_ManGlobalVars( Int_Man_t * p ) { Sto_Cls_t * pClause; int Var, nVarsAB, v; @@ -161,8 +161,8 @@ int Int_ManCommonVars( Int_Man_t * p ) nVarsAB = 0; for ( v = 0; v < p->pCnf->nVars; v++ ) if ( p->pVarTypes[v] == -1 ) - p->pVarTypes[v] -= p->nVarsAB++; -printf( "There are %d global variables.\n", nVarsAB ); + p->pVarTypes[v] -= nVarsAB++; +//printf( "There are %d global variables.\n", nVarsAB ); return nVarsAB; } @@ -182,7 +182,6 @@ void Int_ManResize( Int_Man_t * p ) // check if resizing is needed if ( p->nVarsAlloc < p->pCnf->nVars ) { - int nVarsAllocOld = p->nVarsAlloc; // find the new size if ( p->nVarsAlloc == 0 ) p->nVarsAlloc = 1; @@ -205,7 +204,7 @@ void Int_ManResize( Int_Man_t * p ) memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); // compute the number of common variables - p->nVarsAB = Int_ManCommonVars( p ); + p->nVarsAB = Int_ManGlobalVars( p ); // compute the number of words in the truth table p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5))); @@ -228,7 +227,7 @@ void Int_ManResize( Int_Man_t * p ) p->nIntersAlloc = p->nWords * p->pCnf->nClauses; p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc ); } - memset( p->pInters, 0, sizeof(unsigned) * p->nIntersAlloc ); +// memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses ); } /**Function************************************************************* @@ -244,11 +243,12 @@ void Int_ManResize( Int_Man_t * p ) ***********************************************************************/ 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 ); @@ -278,7 +278,7 @@ PRT( "TOTAL ", p->timeTotal ); void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause ) { int i; - printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofRead(p, pClause) ); + 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" ); @@ -534,12 +534,12 @@ p->timeBcp += clock() - clk; ***********************************************************************/ void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause ) { - Int_ManProofWrite( p, pClause, ++p->Counter ); + Int_ManProofSet( p, pClause, ++p->Counter ); if ( p->fProofWrite ) { int v; - fprintf( p->pFile, "%d", Int_ManProofRead(p, pClause) ); + 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" ); @@ -584,7 +584,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords ); // follow the trail backwards - PrevId = Int_ManProofRead(p, pConflict); + PrevId = Int_ManProofGet(p, pConflict); for ( i = p->nTrailSize - 1; i >= 0; i-- ) { // skip literals that are not involved @@ -605,10 +605,10 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin // record the reason clause - assert( Int_ManProofRead(p, pReason) > 0 ); + assert( Int_ManProofGet(p, pReason) > 0 ); p->Counter++; if ( p->fProofWrite ) - fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofRead(p, pReason) ); + fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) ); PrevId = p->Counter; if ( p->pCnf->nClausesA ) @@ -700,7 +700,7 @@ p->timeTrace += clock() - clk; { // Int_ManPrintInterOne( p, pFinal ); } - Int_ManProofWrite( p, pFinal, p->Counter ); + Int_ManProofSet( p, pFinal, p->Counter ); return p->Counter; } @@ -839,7 +839,7 @@ int Int_ManProcessRoots( Int_Man_t * p ) { // detected root level conflict printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" ); - assert( 0 ); +// assert( 0 ); return 0; } @@ -873,7 +873,7 @@ void Int_ManPrepareInter( Int_Man_t * p ) { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } }; Sto_Cls_t * pClause; - int Var, v; + int Var, VarAB, v; assert( p->nVarsAB <= 8 ); // set interpolants for root clauses @@ -892,10 +892,12 @@ void Int_ManPrepareInter( Int_Man_t * p ) 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[ -p->pVarTypes[Var]-1 ], p->nWords ); + Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords ); else - Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords ); + Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords ); } } // Int_ManPrintInterOne( p, pClause ); @@ -922,12 +924,17 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned // check that the CNF makes sense assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); + p->pCnf = pCnf; // adjust the manager Int_ManResize( p ); // propagate root level assignments - Int_ManProcessRoots( p ); + if ( !Int_ManProcessRoots( p ) ) + { + *ppResult = NULL; + return p->nVarsAB; + } // prepare the interpolant computation Int_ManPrepareInter( p ); @@ -969,8 +976,8 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); p->timeTotal += clock() - clkTotal; - Int_ManFree( p ); - return 1; + *ppResult = Int_ManTruthRead( p, p->pCnf->pTail ); + return p->nVarsAB; } //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 6aafc187..1756b5df 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1223,7 +1223,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin sat_solver_canceluntil(s,0); //////////////////////////////////////////////// - if ( status == l_Undef && s->pStore ) + if ( status == l_False && s->pStore ) { extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL ); diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c index 33cba6a7..7c1d7132 100644 --- a/src/sat/bsat/satStore.c +++ b/src/sat/bsat/satStore.c @@ -292,7 +292,7 @@ void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName ) fprintf( pFile, " %d", lit_print(pClause->pLits[i]) ); fprintf( pFile, "\n" ); } - fprintf( pFile, "\n" ); + fprintf( pFile, " 0\n" ); fclose( pFile ); } diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h index 3db52ada..346b59df 100644 --- a/src/sat/bsat/satStore.h +++ b/src/sat/bsat/satStore.h @@ -116,6 +116,8 @@ 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; diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 76cb2dc2..3001957f 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -190,7 +190,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ) ***********************************************************************/ void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) { - clause ** pClauses; + clause * pClause; lit Lit, * pLits; int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v; // get the number of variables @@ -210,11 +210,11 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) } // duplicate clauses nClauses = vecp_size(&p->clauses); - pClauses = (clause**)vecp_begin(&p->clauses); for ( c = 0; c < nClauses; c++ ) { - nLits = clause_size(pClauses[c]); - pLits = clause_begin(pClauses[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 ); -- cgit v1.2.3