lits

Documentation

Overview

Package lits supports storage of and miscellaneous operations on literals for iic.

Index

• func CalcSig(ms []z.Lit) (sig uint64)
• func ContainedBySorted(ms, ns []z.Lit) bool
• func ContainedBySortedExcept(ms, ns []z.Lit, except z.Lit) bool
• func Flip(ms []z.Lit) []z.Lit
• func MinLit(ms []z.Lit, measure func(m z.Lit) int) z.Lit
• type Resolver
  • func NewResolver(capHint int) *Resolver
  • func (r *Resolver) Resolve(dst []z.Lit, os []z.Lit) (out []z.Lit, ok bool)
  • func (r *Resolver) Set(ms []z.Lit, pivot z.Var) bool
  • func (r *Resolver) SetPivot(pivot z.Var) bool
  • func (r *Resolver) String() string
• type Span
• type T
  • func New() *T
  • func (d *T) Get(n Span) []z.Lit
  • func (d *T) Len(n Span) int
  • func (d *T) N() int
  • func (d *T) Put(ms []z.Lit) Span
  • func (d *T) Remove(n Span)

Functions

func CalcSig

func CalcSig(ms []z.Lit) (sig uint64)

func ContainedBySorted

func ContainedBySorted(ms, ns []z.Lit) bool

func ContainedBySortedExcept

func ContainedBySortedExcept(ms, ns []z.Lit, except z.Lit) bool

func Flip

func Flip(ms []z.Lit) []z.Lit

func MinLit

func MinLit(ms []z.Lit, measure func(m z.Lit) int) z.Lit

Types

type Resolver

type Resolver struct {
	// contains filtered or unexported fields
}

func NewResolver

func NewResolver(capHint int) *Resolver

func (*Resolver) Resolve

func (r *Resolver) Resolve(dst []z.Lit, os []z.Lit) (out []z.Lit, ok bool)

func (*Resolver) Set

func (r *Resolver) Set(ms []z.Lit, pivot z.Var) bool

func (*Resolver) SetPivot

func (r *Resolver) SetPivot(pivot z.Var) bool

func (*Resolver) String

func (r *Resolver) String() string

type Span

type Span int

Span represents a span of literals in T.

type T

type T struct {
	D []z.Lit
	// contains filtered or unexported fields
}

T represents a contiguous store of literals.

func New

func New() *T

New creates a new store of lits.

func (*T) Get

func (d *T) Get(n Span) []z.Lit

Get returns a slice backed by the contiguous storage in `d` containing the lits represented by `n`.

func (*T) Len

func (d *T) Len(n Span) int

Len returns the number of literals in `n`

func (*T) N

func (d *T) N() int

N returns the number of spans in `d`.

func (*T) Put

func (d *T) Put(ms []z.Lit) Span

Put copies `ms` into `d` and returns the associated Span.

func (*T) Remove

func (d *T) Remove(n Span)

Remove removes the span `n` `n` must no longer be referenced by the user of `d`.