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

Transforming the solver to use different clause representation.

This commit is contained in:
Alan Mishchenko 2011-12-23 00:43:31 -08:00
parent 9d2893040e
commit 94174d0f04
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -72,7 +72,7 @@ static const int var0 = 1;
static const int var1 = 0;
static const int varX = 3;
struct varinfo_t
struct varinfo2_t
{
// unsigned val : 2; // variable value
unsigned pol : 1; // last polarity
@ -1263,7 +1263,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
while (s->cap < n) s->cap = s->cap*2+1;
s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2);
s->vi = ABC_REALLOC(varinfo, s->vi, s->cap);
s->vi = ABC_REALLOC(varinfo2, s->vi, s->cap);
s->levels = ABC_REALLOC(int, s->levels, s->cap);
s->assigns = ABC_REALLOC(char, s->assigns, s->cap);
s->trail = ABC_REALLOC(lit, s->trail, s->cap);

4
src/sat/bsat/satSolver2.h
View File

@ -80,7 +80,7 @@ extern void Sat_ProofCheck( sat_solver2 * s );
// Solver representation:
struct varinfo_t;
typedef struct varinfo_t varinfo;
typedef struct varinfo2_t varinfo2;
struct sat_solver2_t
{
@ -125,7 +125,7 @@ struct sat_solver2_t
veci claProofs; // clause proofs
// internal state
varinfo * vi; // variable information
varinfo2 * vi; // variable information
int* levels; //
char* assigns; //
lit* trail; // sequence of assignment and implications