sat: add satget
parent
3cb5494b26
commit
2e2ae33a47
|
@ -36,6 +36,7 @@ SATSolve* satrangev(SATSolve *s, int min, int max, ...);
|
||||||
int satsolve(SATSolve *s);
|
int satsolve(SATSolve *s);
|
||||||
int satmore(SATSolve *s);
|
int satmore(SATSolve *s);
|
||||||
int satval(SATSolve *s, int lit);
|
int satval(SATSolve *s, int lit);
|
||||||
|
int satget(SATSolve *s, int i, int *lit, int nlit);
|
||||||
void satreset(SATSolve *s);
|
void satreset(SATSolve *s);
|
||||||
.SH DESCRIPTION
|
.SH DESCRIPTION
|
||||||
.PP
|
.PP
|
||||||
|
@ -123,6 +124,23 @@ For example, the clause from above corresponds to
|
||||||
.IP
|
.IP
|
||||||
.B "satrangev(s, 1, 1, 1, 2, 3, 0);"
|
.B "satrangev(s, 1, 1, 1, 2, 3, 0);"
|
||||||
.PP
|
.PP
|
||||||
|
For debugging purposes, clauses can be retrieved using
|
||||||
|
.IR satget .
|
||||||
|
It stores the literals of the clause with index
|
||||||
|
.I i
|
||||||
|
(starting from 0) at location
|
||||||
|
.IR lit .
|
||||||
|
If there are more than
|
||||||
|
.I nlit
|
||||||
|
literals, only the first
|
||||||
|
.I nlit
|
||||||
|
literals are stored.
|
||||||
|
If it was successful, it returns the total number of literals in the clause (which may exceed
|
||||||
|
.IR nlit ).
|
||||||
|
Otherwise (if
|
||||||
|
.I idx
|
||||||
|
was out of bounds) it returns -1.
|
||||||
|
.PP
|
||||||
.I Satreset
|
.I Satreset
|
||||||
resets all solver state, deleting all learned clauses and variable assignments.
|
resets all solver state, deleting all learned clauses and variable assignments.
|
||||||
It retains all user provided clauses.
|
It retains all user provided clauses.
|
||||||
|
|
|
@ -9,6 +9,7 @@ OFILES=\
|
||||||
satsolve.$O \
|
satsolve.$O \
|
||||||
satmore.$O \
|
satmore.$O \
|
||||||
debug.$O \
|
debug.$O \
|
||||||
|
satget.$O \
|
||||||
|
|
||||||
HFILES=\
|
HFILES=\
|
||||||
/sys/include/sat.h\
|
/sys/include/sat.h\
|
||||||
|
|
|
@ -0,0 +1,33 @@
|
||||||
|
#include <u.h>
|
||||||
|
#include <libc.h>
|
||||||
|
#include <sat.h>
|
||||||
|
#include "impl.h"
|
||||||
|
|
||||||
|
int
|
||||||
|
satget(SATSolve *s, int i, int *t, int n)
|
||||||
|
{
|
||||||
|
SATClause *c;
|
||||||
|
SATLit *l;
|
||||||
|
int j, k;
|
||||||
|
|
||||||
|
for(c = s->cl; c != s->learncl; c = c->next)
|
||||||
|
if(i-- == 0){
|
||||||
|
for(j = 0; j < n && j < c->n; j++)
|
||||||
|
t[j] = signf(c->l[j]);
|
||||||
|
return c->n;
|
||||||
|
}
|
||||||
|
for(l = s->lit; l < s->lit + 2 * s->nvar; l++)
|
||||||
|
for(k = 0; k < l->nbimp; k++)
|
||||||
|
if(i-- == 0){
|
||||||
|
if(n > 0) t[0] = -signf(l - s->lit);
|
||||||
|
if(n > 1) t[1] = signf(l->bimp[k]);
|
||||||
|
return 2;
|
||||||
|
}
|
||||||
|
for(; c != 0; c = c->next)
|
||||||
|
if(i-- == 0){
|
||||||
|
for(j = 0; j < n && j < c->n; j++)
|
||||||
|
t[j] = signf(c->l[j]);
|
||||||
|
return c->n;
|
||||||
|
}
|
||||||
|
return -1;
|
||||||
|
}
|
Loading…
Reference in New Issue