From 6f4bb33ce14dd66b71e41bb71639a74a951a08b1 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 13 Feb 2012 14:35:00 -0800
Subject: Variable timeframe abstraction.
---
src/aig/gia/giaAbsVta.c | 1 +
src/aig/saig/saigGlaPba2.c | 2 +-
src/sat/bsat/satSolver2.c | 8 ++++++--
src/sat/bsat/satSolver2.h | 8 +-------
4 files changed, 9 insertions(+), 10 deletions(-)
(limited to 'src')
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index b373fd27..9c50ae52 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1402,6 +1402,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
// start the manager
p = Vga_ManStart( pAig, pPars );
+ p->pSat->fVerbose = p->pPars->fVerbose;
sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// set runtime limit
if ( p->pPars->nTimeOut )
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c
index 55aa0a3d..4fa0012d 100644
--- a/src/aig/saig/saigGlaPba2.c
+++ b/src/aig/saig/saigGlaPba2.c
@@ -516,7 +516,7 @@ Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
Aig_Gla3ManStop( p );
return NULL;
}
- sat_solver2_set_random( p->pSat, fSkipRand );
+ p->pSat->fNotUseRandom = fSkipRand;
p->timePre += clock() - clk;
// set runtime limit
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index e603d866..e4d713d1 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1153,7 +1153,8 @@ sat_solver2* sat_solver2_new(void)
#endif
s->fSkipSimplify = 1;
s->fNotUseRandom = 0;
- s->nLearntMax = 0;
+ s->nLearntMax = 0;
+ s->fVerbose = 0;
// prealloc clause
assert( !s->clauses.ptr );
@@ -1220,7 +1221,6 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
*((int*)s->vi + var) = 0; //s->vi[var].val = varX;
s->levels [var] = 0;
s->assigns [var] = varX;
- s->orderpos[var] = veci_size(&s->order);
s->reasons [var] = 0;
if ( s->fProofLogging )
s->units [var] = 0;
@@ -1232,6 +1232,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
s->model [var] = 0;
// does not hold because variables enqueued at top level will not be reinserted in the heap
// assert(veci_size(&s->order) == var);
+ s->orderpos[var] = veci_size(&s->order);
veci_push(&s->order,var);
order_update(s, var);
}
@@ -1420,6 +1421,7 @@ void sat_solver2_reducedb(sat_solver2* s)
c->mark = 1;
}
// report the results
+ if ( s->fVerbose )
printf( "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts );
@@ -1488,6 +1490,7 @@ void sat_solver2_reducedb(sat_solver2* s)
Sat_ProofReduce( s );
TimeTotal += clock() - clk;
+ if ( s->fVerbose )
Abc_PrintTime( 1, "Time", TimeTotal );
}
@@ -1548,6 +1551,7 @@ void sat_solver2_rollback( sat_solver2* s )
// reset watcher lists
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
+ // clean the room
for ( i = s->iVarPivot; i < s->size; i++ )
{
*((int*)s->vi + i) = 0;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 4d01427a..4b1eec61 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -106,6 +106,7 @@ struct sat_solver2_t
int fNotUseRandom; // do not allow random decisions with a fixed probability
int fSkipSimplify; // set to one to skip simplification of the clause database
int fProofLogging; // enable proof-logging
+ int fVerbose;
// clauses
veci clauses; // clause memory
@@ -240,13 +241,6 @@ static inline int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit)
return temp;
}
-static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
-{
- int temp = s->fNotUseRandom;
- s->fNotUseRandom = fNotUseRandom;
- return temp;
-}
-
static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax)
{
int temp = s->nLearntMax;
--
cgit v1.2.3