diff options
Diffstat (limited to 'src/sat/asat')
-rw-r--r-- | src/sat/asat/added.c | 23 | ||||
-rw-r--r-- | src/sat/asat/solver.c | 2 | ||||
-rw-r--r-- | src/sat/asat/solver.h | 4 |
3 files changed, 22 insertions, 7 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index d7358749..662fe1ff 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: added.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: added.c,v 1.4 2005/09/16 22:55:03 casem Exp $] ***********************************************************************/ @@ -57,7 +57,7 @@ static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) SeeAlso [] ***********************************************************************/ -void Asat_SolverWriteDimacs( solver * p, char * pFileName ) +void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ) { FILE * pFile; void ** pClauses; @@ -78,18 +78,31 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName ) nClauses = p->clauses.size; pClauses = p->clauses.ptr; for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); + Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars ); // write the learned clauses nClauses = p->learnts.size; pClauses = p->learnts.ptr; for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); + Asat_ClauseWriteDimacs( 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 0\n", (p->assigns[i] == l_False)? "-": "", i + 1 ); + 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 ); diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index d248b115..3927fac3 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -1099,7 +1099,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds) nof_conflicts *= 1.5; nof_learnts *= 1.1; // if the runtime limit is exceeded, quit the restart loop - if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC ) + if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) ) break; } if (s->verbosity >= 1) diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 9f80bc7e..b82601c4 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -73,7 +73,9 @@ extern int solver_nvars(solver* s); extern int solver_nclauses(solver* s); // additional procedures -extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName ); +extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, + lit* assumptionsBegin, lit* assumptionsEnd, + int incrementVars); struct stats_t { |