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

New function to retrieve polarity value of a variable.

This commit is contained in:
Bruno Schmitt 2017-02-18 17:08:54 -08:00
parent ac409b3152
commit 3f0cb6318b
2 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/sat/satoko/solver.c
View File

@ -195,7 +195,7 @@ static inline unsigned solver_decide(solver_t *s)
if (solver_has_marks(s) && !var_mark(s, next_var))
next_var = UNDEF;
}
return var2lit(next_var, vec_char_at(s->polarity, next_var));
return var2lit(next_var, var_polarity(s, next_var));
}
static inline void solver_new_decision(solver_t *s, unsigned lit)

5
src/sat/satoko/solver.h
View File

@ -132,6 +132,11 @@ static inline char var_value(solver_t *s, unsigned var)
return vec_char_at(s->assigns, var);
}
static inline char var_polarity(solver_t *s, unsigned var)
{
return vec_char_at(s->polarity, var);
}
static inline unsigned var_dlevel(solver_t *s, unsigned var)
{
return vec_uint_at(s->levels, var);