luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Started experiments with a new solver.

This commit is contained in:
Alan Mishchenko 2011-11-26 11:54:01 -08:00
parent 8ac9515d36
commit 0cfc97b940
1 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/sat/bsat/satSolver2.c
View File

@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
#define SAT_USE_ANALYZE_FINAL
//#define SAT_USE_WATCH_ARRAYS
#define SAT_USE_WATCH_ARRAYS
//=================================================================================================
// Debug:
@ -79,7 +79,9 @@ struct clause_t
{
int size_learnt;
unsigned act;
#ifndef SAT_USE_WATCH_ARRAYS
clause * pNext[2];
#endif
lit lits[0];
};
@ -253,6 +255,8 @@ static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc
//=================================================================================================
// Clause functions:
#ifndef SAT_USE_WATCH_ARRAYS
static inline void clause_watch_( sat_solver2* s, clause* c, lit Lit )
{
if ( c->lits[0] == Lit )
@ -354,6 +358,8 @@ static inline void clause_watch( sat_solver2* s, clause* c, lit Lit )
s->pWatches[lit_neg(Lit)] = c;
}
#endif
static clause* clause_new(sat_solver2* s, lit* begin, lit* end, int learnt)
{
clause* c;
@ -855,6 +861,7 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
#endif
}
#ifndef SAT_USE_WATCH_ARRAYS
static inline clause* clause_propagate__( sat_solver2* s, lit Lit )
{
@ -937,7 +944,6 @@ clause* sat_solver2_propagate_new__( sat_solver2* s )
return NULL;
}
static inline clause* clause_propagate( sat_solver2* s, lit Lit, clause** ppHead, clause** ppTail )
{
clause ** ppPrev = ppHead;
@ -1080,6 +1086,7 @@ clause* sat_solver2_propagate_new( sat_solver2* s )
return NULL;
}
#endif
clause* sat_solver2_propagate(sat_solver2* s)
{
@ -1473,7 +1480,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
int sat_solver2_simplify(sat_solver2* s)
{
clause** reasons;
int type;
// int type;
int Counter = 0;
assert(sat_solver2_dlevel(s) == 0);