Documentation
¶
Overview ¶
Package z provides minimal common interface to lits and vars.
Variables and literals are represented as uint32s. The LSB indicates for a literal whether or not it is the negation of a variable.
As is common in SAT solvers, this representation is convenient for data structures indexed by variable or literal.
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type C ¶ added in v1.0.2
type C uint32
C is a clause ref. Clause refs are ephemeral and may change value during solves. Clause refs are used by objects implementing inter.CnfSimp
type Lit ¶
type Lit uint32
const LitNull Lit = 0
LitNull is the constant 0, used in various places to indicate a meaningless literal.
func Dimacs2Lit ¶
Dimacs2Lit takes a dimacs-coded literal and returns a Lit. A Dimacs coded literal for a variable v is
-v for not(v) v for v
type Vars ¶
type Vars struct {
// contains filtered or unexported fields
}
Type Vars provides a mechanism for mapping variables in the presence of a stream of user supplied literals interleaved with a stream of application demands for a new variable (or for the application to free variables).
func (*Vars) Free ¶
Free frees an application literal created by Inner. If m is not an application literal, the subsequent behavior of v is undefined.
func (*Vars) Inner ¶
Inner produces an new application literals. The returned literal is always positive.
func (*Vars) ToInner ¶
ToInner maps a user supplied literal m to an application literal. m may or may not have been previously referenced by the user.
func (*Vars) ToInners ¶
ToInners maps a slice of user supplied literals to a slice of application literals. The user supplied literals may or may not have been previously referenced.
ToInner uses "ms" for scratch space and returns it.
Source Files