z

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

• type C
  • func (p C) String() string
• type Lit
  • func Dimacs2Lit(m int) Lit
  • func (m Lit) Dimacs() int
  • func (m Lit) IsPos() bool
  • func (m Lit) Not() Lit
  • func (m Lit) Sign() int8
  • func (m Lit) String() string
  • func (m Lit) Var() Var
• type Var
  • func (v Var) Neg() Lit
  • func (v Var) Pos() Lit
  • func (v Var) String() string
• type Vars
  • func NewVars() *Vars
  • func (v *Vars) Copy() *Vars
  • func (v *Vars) Free(m Lit)
  • func (v *Vars) Inner() Lit
  • func (v *Vars) String() string
  • func (v *Vars) ToInner(m Lit) Lit
  • func (v *Vars) ToInners(ms []Lit) []Lit
  • func (v *Vars) ToOuter(m Lit) Lit
  • func (v *Vars) ToOuters(ms []Lit) []Lit

Types

type C

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

func (C) String

func (p C) String() string

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

func Dimacs2Lit(m int) Lit

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

func (Lit) Dimacs

func (m Lit) Dimacs() int

Dimacs returns the dimacs coding of the Lit m.

func (Lit) IsPos

func (m Lit) IsPos() bool

IsPos returns true if m is a variable.

func (Lit) Not

func (m Lit) Not() Lit

Not returns the negation of m.

func (Lit) Sign

func (m Lit) Sign() int8

Sign returns

1  if m is a variable

-1 if m is a negated variable

func (Lit) String

func (m Lit) String() string

func (Lit) Var

func (m Lit) Var() Var

Var returns the Var associated with m.

type Var

type Var uint32

Type Var is a representation of a Boolean variable.

func (Var) Neg

func (v Var) Neg() Lit

Neg regurns a Lit which is not(v)

func (Var) Pos

func (v Var) Pos() Lit

Pos returns a Lit which is v.

func (Var) String

func (v Var) String() string

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 NewVars

func NewVars() *Vars

NewVars creates a new Vars object.

func (*Vars) Copy

func (v *Vars) Copy() *Vars

func (*Vars) Free

func (v *Vars) Free(m Lit)

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

func (v *Vars) Inner() Lit

Inner produces an new application literals. The returned literal is always positive.

func (*Vars) String

func (v *Vars) String() string

String implements stringer.

func (*Vars) ToInner

func (v *Vars) ToInner(m Lit) Lit

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

func (v *Vars) ToInners(ms []Lit) []Lit

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.

func (*Vars) ToOuter

func (v *Vars) ToOuter(m Lit) Lit

ToOuter maps an application literal to a user supplied literal, defaulting to LitNull if there is no corresponding user supplied literal.

func (*Vars) ToOuters

func (v *Vars) ToOuters(ms []Lit) []Lit

ToOuters maps a slice of application literals to a slice of user supplied literals, omitting any application literals which do where not referenced by the user.

ToOuters uses "ms" as scratch space and returns it.