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

Added several helpful APIs to Satoko.

This commit is contained in:
Alan Mishchenko 2017-08-15 17:07:12 +07:00
parent ca87c1a6a0
commit 7747f21fe6
3 changed files with 33 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/sat/satoko/satoko.h
View File

@ -92,6 +92,7 @@ extern void satoko_assump_push(satoko_t *s, int);
extern void satoko_assump_pop(satoko_t *s);
extern int satoko_simplify(satoko_t *);
extern int satoko_solve(satoko_t *);
extern int satoko_solve_with_assumptions(satoko_t *s, int * plits, int nlits);
extern void satoko_mark_cone(satoko_t *, int *, int);
extern void satoko_unmark_cone(satoko_t *, int *, int);

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

@ -222,6 +222,19 @@ static inline int solver_varnum(solver_t *s)
{
return vec_char_size(s->assigns);
}
static inline int solver_clausenum(solver_t *s)
{
return vec_uint_size(s->originals);
}
static inline int solver_learntnum(solver_t *s)
{
return vec_uint_size(s->learnts);
}
static inline int solver_conflictnum(solver_t *s)
{
return satoko_stats(s).n_conflicts;
}
static inline int solver_has_marks(solver_t *s)
{
return (int)(s->marks != NULL);
@ -234,6 +247,10 @@ static inline void solver_set_stop(solver_t *s, int * pstop)
{
s->pstop = pstop;
}
static inline int solver_read_cex_varvalue(solver_t *s, int ivar)
{
return var_polarity(s, ivar) == LIT_TRUE;
}
//===------------------------------------------------------------------------===
// Inline clause functions

15
src/sat/satoko/solver_api.c
View File

@ -313,6 +313,21 @@ int satoko_solve(solver_t *s)
return status;
}
int satoko_solve_with_assumptions(solver_t *s, int * plits, int nlits)
{
int i, status;
for ( i = 0; i < nlits; i++ )
satoko_assump_push( s, plits[i] );
status = satoko_solve( s );
for ( i = 0; i < nlits; i++ )
satoko_assump_pop( s );
if ( status == SATOKO_UNSAT )
return 1;
if ( status == SATOKO_SAT )
return 0;
return -1;
}
int satoko_final_conflict(solver_t *s, unsigned *out)
{
if (vec_uint_size(s->final_conflict) == 0)