Documentation
¶
Overview ¶
Package logic provides representation of Boolean combinational and sequential logic.
Package logic uses a standard https://en.wikipedia.org/wiki/And-inverter_graph (and-inverter graph) to represent circuits. They are simplified using some rules and structural hashing, implemented in the type C. Additionally, Cardinality constraints are supported.
Unlike most AIG libraries, package logic uses the same variables and literals as an associated SAT solver. This means that there is no need to maintain maps for AIG<->SAT flows.
Package logic also supports simple sequential logic (with latches and unrolling) in the type S.
Index ¶
- type C
- func (p *C) And(a, b z.Lit) z.Lit
- func (c *C) Ands(ms ...z.Lit) z.Lit
- func (c *C) At(i int) z.Lit
- func (c *C) CardSort(ms []z.Lit) *CardSort
- func (c *C) Choice(i, t, e z.Lit) z.Lit
- func (c *C) CnfSince(dst inter.Adder, mark []int8, roots ...z.Lit) ([]int8, int)
- func (c *C) Copy() *C
- func (c *C) Eval(vs []bool)
- func (c *C) Eval64(vs []uint64)
- func (c *C) Implies(a, b z.Lit) z.Lit
- func (c *C) InPos(dst []int) []int
- func (c *C) Ins(m z.Lit) (z.Lit, z.Lit)
- func (c *C) Len() int
- func (c *C) Lit() z.Lit
- func (c *C) Or(a, b z.Lit) z.Lit
- func (c *C) Ors(ms ...z.Lit) z.Lit
- func (c *C) ToCnf(dst inter.Adder)
- func (c *C) ToCnfFrom(dst inter.Adder, roots ...z.Lit)
- func (c *C) Xor(a, b z.Lit) z.Lit
- type Card
- type CardSort
- type Roll
- type S
- type SNodeType
Examples ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type C ¶
C represents a formula or combinational circuit.
Example (Equiv) ¶
package main
import (
"fmt"
"github.com/go-air/gini"
"github.com/go-air/gini/logic"
)
func main() {
L := logic.NewC()
a, b, c := L.Lit(), L.Lit(), L.Lit()
c1 := L.Ors(a, b, c)
c2 := L.Ors(a, b, c.Not())
g1 := L.And(c1, c2)
g2 := L.Or(a, b)
// create a "miter", test whether "(a b c) and (a b -c)" is equivalent to "(a b)",
// by testing whether there is an assignment to {a,b,c} which makes the respective
// circuits have a different value.
m := L.Xor(g1, g2)
// encode to sat
s := gini.New()
L.ToCnfFrom(s, m)
// assume the miter
s.Assume(m)
r := s.Solve()
if r == 1 {
// not equivalent, model is a witness to different valuations.
fmt.Printf("sat\n")
} else {
// equivalent.
fmt.Printf("unsat\n")
}
}
Output: unsat
func (*C) Ands ¶
Ands constructs a conjunction of a sequence of literals. If ms is empty, then Ands returns p.T.
func (*C) At ¶
At returns the i'th element. Elements from 0..Len(c) are in topological order: if i < j then c.At(j) is not reachable from c.At(i) via the edge relation defined by c.Ins(). All elements are positive literals.
One variable for internal use, with index 1, is created when c is created. All other variables created by NewIn, And, ... are created in sequence starting with index 2. Internal variables may be created by c. c.Len() - 1 is the maximal index of a variable.
Hence, the implementation of At(i) is simply z.Var(i).Pos().
func (*C) CardSort ¶ added in v1.0.2
CardSort creates a CardSort object whose cardinality predicates over ms are encoded in c.
func (*C) CnfSince ¶ added in v1.0.2
CnfSince adds the circuit rooted at roots to dst assuming mark marks all already added nodes in the circuit`. CnfSince returns marks from previously marked nodes and the total number of nodes added. If mark is nil or does not have sufficient capacity, then new storage is created with a copy of mark.
func (*C) Eval ¶
Eval evaluates the circuit with values vs, where for each literal m in the circuit, vs[i] contains the value for m's variable if m.Var() == i.
vs should contain values for all inputs. In case `c` is embedded in a sequential circuit `s`, then the inputs include the latches of `s`.
func (*C) Eval64 ¶
Eval64 is like Eval but evaluates 64 different inputs in parallel as the bits of a uint64.
func (*C) InPos ¶
InPos returns the positions of all inputs in c in the sequence attainable via Len() and At(). The result is placed in dst if there is space.
If c is part of S, then latches are not included.
func (*C) Ins ¶
Ins returns the children/ operands of m.
If m is an input, then, Ins returns z.LitNull, z.LitNull If m is an and, then Ins returns the two conjuncts
func (*C) Ors ¶
Ors constructs a literal which is the disjuntion of the literals in ms. If ms is empty, then Ors returns p.F
func (*C) ToCnf ¶
ToCnf creates a conjunctive normal form of p in adder.
Adder uses basic Tseitinization.
type Card ¶ added in v0.9.0
Card provides an interface for different implementations of cardinality constraints.
type CardSort ¶ added in v0.9.0
type CardSort struct {
// contains filtered or unexported fields
}
CardSort provides cardinality constraints via sorting networks.
Sorting Networks ¶
CardSort uses sorting networks which implement O log(|ms|)**2 compare/swap to sort |ms| literals. Each compare/swap is coded symbolically and generates 6 clauses with 2 new variables. The resulting network helps the solver achieve arc consistency w.r.t. the variables in ms and the output cardinality constraints. Namely, any partial valuation of ms will cause the solver to deduce the corresponding valid and unsat card constraints by unit propagation.
While not a best fit coding mechanism for all cases, sorting networks are a good choice for a general use single mechanism for coding cardinality constraints and hence solving Boolean optimisation problems.
The idea was originally presented by Nicolas Sorensson and Nicolas Een in "Translating Pseudo-Boolean Constraints into SAT" Journal on Satisfiability, Boolean Modelng, and Computation.
func NewCardSort ¶ added in v0.9.0
NewCardSort creates a new Card object which gives access to unary Cardinality constraints over ms. The resulting predicates reflect how many of the literals in ms are true.
type Roll ¶ added in v1.0.2
type Roll struct {
S *S // the sequential circuit
C *C // the resulting comb circuit
// contains filtered or unexported fields
}
Roll creates an unroller of sequential logic into combinational logic.
Example ¶
package main
import (
"fmt"
"github.com/go-air/gini/logic"
)
func main() {
// create a new sequential circuit, a 16 bit counter
s := logic.NewS()
N := 16
c := s.T
for i := 0; i < N; i++ {
n := s.Latch(s.F)
s.SetNext(n, s.Choice(c, n.Not(), n))
c = s.And(c, n)
}
// create an unroller.
u := logic.NewRoll(s)
// unroll until all 1s
D := (1 << uint(N)) - 1
errs := 0
for i := 0; i < N; i++ {
m := s.Latches[i]
u.At(m, D)
if u.At(m, D) != s.T {
errs++
}
}
fmt.Printf("%d errs\n", errs)
}
Output: 0 errs
func (*Roll) At ¶ added in v1.0.2
At returns the value of literal m from sequential circuit u.S at time/depth d as a literal in u.C
If d < 0, then At panics.
type S ¶
type S struct {
C // the combinational circuit, logic.C
Latches []z.Lit // the memory elements/state variables
}
S adds sequential elements to C, gini's combinational logic representation.
func (*S) Init ¶
Init returns the initial state of the latch latch.
- s.F if false
- s.T if true
- z.LitNull if X
func (*S) Latch ¶
Latch returns a new "latch", which is a value that evolves over time.
The definition of the value of a latch is in discrete time, in which at time 0, the value of the latch is init The value of a latch at time i is the value of the next state literal of the latch at time i-1. By default, this literal is the latch itself. It may be set using SetNext below.
init must be one of the following
s.T s.F z.LitNull
or Latch will panic. z.LitNull means uninitialized, or unknown or 'X' in ternary logic.
func (*S) SetInit ¶ added in v0.9.0
SetInit sets the initial state of 'latch' to 'nxt'. 'nxt' should be either z.LitNull, s.T, or s.F. If it is not, SetInit panics. If 'latch' is not a latch, then subsequent operations on s are undefined.
Source Files
Directories