shithub: riscv

ref: ce72cab0e49c08c71888c57cf616563b90d7497a
dir: /sys/src/libsat/impl.h/

/* note that internally, literals use a representation different from the API.
 * variables are numbered from 0 (not 1) and 2v and 2v+1 correspond to v
 * and ¬v, resp.  */
#define VAR(l) ((l)>>1)
#define NOT(l) ((l)^1)

/* l[0] and l[1] are special: they are the watched literals.
 * all clauses that have literal l on their watchlist form a linked list starting with s->lit[l].watch
 * and watch[i] having the next clause for l[i] */
struct SATClause {
	SATClause *next;
	SATClause *watch[2];
	double activity; /* activity is increased every time a clause is used to resolve a conflict (tiebreaking heuristic during purging) */
	int n; /* >= 2 for learned clauses and > 2 for input clauses (binary input clauses are kept in the bimp tables) */
	ushort range; /* heuristic used during purging, low range => keep clause (range 0..256) */
	int l[1];
};

struct SATLit {
	int *bimp; /* array of literals implied by this literal through binary clauses (Binary IMPlications) */
	SATClause *watch; /* linked list of watched clauses */
	int nbimp;
	char val; /* -1 = not assigned, 0 = false, 1 = true */
};

struct SATVar {
	double activity; /* activity is increased every time a variable shows up in a conflict */
	union {
		SATClause *reason; /* nil for decision and free literals */
		int binreason; /* used when isbinreason == 1: the reason is the clause l ∨ l->binreason */
	};
	int lvl; /* level at which this variable is defined, or -1 for free variables */
	int heaploc; /* location in binary heap or -1 when not in heap */
	uint stamp; /* "stamp" value used for conflict resolution etc. */
	uchar flags; /* see below */
	char isbinreason;
};

enum {
	VARPHASE = 1, /* for a free variables, VARPHASE is used as a first guess the next time it is picked */
	VARUSER = 0x80, /* user assigned variable (unit clause in input) */
};

/* records conflicts during purging */
struct SATConflict {
	union {
		SATClause *c;
		uvlong b;
	};
	int lvl; /* bit 31 denotes binary conflict */
};
#define CFLLVL(c) ((c).lvl & 0x7fffffff)

enum {
	SATBLOCKSZ = 65536,
	SATVARALLOC = 64,
	CLAUSEALIGN = 8,
	CFLCLALLOC = 16,
};

void saterror(SATSolve *, char *, ...);
void sataddtrail(SATSolve *, int);
void satdebuginit(SATSolve *);
void satprintstate(SATSolve *);
void satsanity(SATSolve *);
SATVar *satheaptake(SATSolve *);
void satheapput(SATSolve *, SATVar *);
void satreheap(SATSolve *, SATVar *);
void satheapreset(SATSolve *);
int satnrand(SATSolve *, int);
void *satrealloc(SATSolve *, void *, ulong);
SATClause *satnewclause(SATSolve *, int, int);
SATClause *satreplclause(SATSolve *, int);
void satcleanup(SATSolve *, int);
void satbackjump(SATSolve *, int);

#define signf(l) (((l)<<31>>31|1)*((l)+2>>1))
#pragma varargck type "Γ" SATClause*

#define ε 2.2250738585072014e-308
#define MAXACTIVITY 1e100