Documentation
¶
Overview ¶
Package aiger implements aiger format version 1.9 ascii and binary readers and writers.
The aiger objects are backed by sequential circuits as represented in *logic.S
Index ¶
- Variables
- type T
- func (a *T) BadName(index int) (string, bool)
- func (a *T) ConstraintName(index int) (string, bool)
- func (a *T) FairName(index int) (string, bool)
- func (a *T) InputName(index int) (string, bool)
- func (a *T) JusticeName(index int) (string, bool)
- func (a *T) LatchName(index int) (string, bool)
- func (a *T) NameBad(index int, nm string) error
- func (a *T) NameConstraint(index int, nm string) error
- func (a *T) NameFair(index int, nm string) error
- func (a *T) NameInput(index int, nm string) error
- func (a *T) NameJustice(index int, nm string) error
- func (a *T) NameLatch(index int, nm string) error
- func (a *T) NameOutput(index int, nm string) error
- func (a *T) NewIn() z.Lit
- func (a *T) OutputName(index int) (string, bool)
- func (a *T) SetOutput(m z.Lit)
- func (a *T) Sys() *logic.S
- func (a *T) WriteAscii(w io.Writer) error
- func (a *T) WriteBinary(w io.Writer) error
- Bugs
Constants ¶
This section is empty.
Variables ¶
var ( PrematureEOF = errors.New("premature EOF") ReadError = errors.New("Read error") UnexpectedChar = errors.New("Unexpected char") BadHeader = errors.New("Bad header") BadUInt = errors.New("malformed literal") BinaryMismatch = errors.New("binary mismatch") InvalidLatchInit = errors.New("invalid latch init value") LitOOB = errors.New("Literal out of bounds") BadDeltaEncoding = errors.New("Bad Delta Encoding") InvalidIndex = errors.New("invalid index") InvalidSymbolType = errors.New("invalid symbol type") InvalidName = errors.New("invalid symbol name") SignedInput = errors.New("input is negated") SignedLatch = errors.New("latch is negated") SignedAnd = errors.New("and gate def is negated") CombLoop = errors.New("combinational logic has a loop") AndMultiplyDefined = errors.New("and gate multiply defined") UndefinedLit = errors.New("literal not defined") )
Errors related to IO and formatting
Functions ¶
This section is empty.
Types ¶
type T ¶
type T struct {
*logic.S // The Boolean system backing this Aiger object
Inputs []z.Lit
Outputs []z.Lit
Bad []z.Lit // Read/Write List of Bad state literals
Constraints []z.Lit // Read/Write List of Environment Constraints
Justice [][]z.Lit // Read/Write List of Justice Properties
Fair []z.Lit // Read/Write List of Fairness Constraints
// contains filtered or unexported fields
}
Type Aiger contains the information read from or written to disk in Aiger format version 1.9
func Make ¶
Make makes an Aiger object with initial capacity hint c for the underlying logic.S object
func MakeFor ¶
MakeFor makes an Aiger object from a Boolean system. The system is the backing store for the Aiger object, no copy is made
func ReadAscii ¶
ReadAscii reads an ascii coded Aiger file (version 1.9) ReadAscii returns a possibly nil Aiger object system paired with a possibly nil error. If the Aiger object is nil, the error is non-nil and indicates the underlying problem.
func ReadBinary ¶
ReadBinary reads a binary Aiger file (version 1.9) Readbinary returns a possibly nil Aiger object paired with a possibly nil error. The error will be non-nil and describe the underlyng problem if the Aiger object is nil.
func (*T) BadName ¶
BadName gives the name of the index'th Bad state in the aiger system. If no such name exists, BadName returns nil, false. Otherwise, BadName returns name, true.
func (*T) ConstraintName ¶
ConstraintName gives the name of the index'th Constraint in the aiger system. If no such name exists, ConstraintName returns nil, false. Otherwise, ConstraintName returns name, true.
func (*T) FairName ¶
FairName gives the name of the index'th Fair in the aiger system. If no such name exists, FairName returns nil, false. Otherwise, FairName returns name, true.
func (*T) InputName ¶
InputName gives the name of the index'th Input in the aiger system. If no such name exists, InputName returns (nil, false). Otherwise, InputName returns (name, true).
func (*T) JusticeName ¶
JusticeName gives the name of the index'th Justice in the aiger system. If no such name exists, JusticeName returns nil, false. Otherwise, JusticeName returns name, true.
func (*T) LatchName ¶
LatchName gives the name of the index'th Latch in the aiger system. If no such name exists, LatchName returns nil, false. Otherwise, LatchName returns name, true.
func (*T) NameBad ¶
Name index'th Bad State property with name nm return a non-nil error if index is out of bounds or nm contains a new line
func (*T) NameConstraint ¶
Name index'th Constraint with name nm return a non-nil error if index is out of bounds or nm contains a new line
func (*T) NameFair ¶
Name the index'th fairness constraint with name nm return a non-nil error if index is out of bounds or nm contains a new line
func (*T) NameInput ¶
Name index'th input with name nm return a non-nil error if index is out of bounds or nm contains a new line
func (*T) NameJustice ¶
Name index'th justice property with name nm return a non-nil error if index is out of bounds or nm contains a new line
func (*T) NameLatch ¶
Name index'th Latch with name nm return a non-nil error if index is out of bounds or nm contains a new line
func (*T) NameOutput ¶
Name index'th output with name nm return a non-nil error if index is out of bounds or nm contains a new line
func (*T) OutputName ¶
OutputName gives the name of the index'th Output in the aiger system. If no such name exists, OutputName returns nil, false. Otherwise, OutputName returns name, true.
func (*T) WriteAscii ¶
WriteAscii writes an ASCII version of AIGER format for the object a to the writer w. WriteAscii returns a non-nil error if there was an io error while writing.
Notes ¶
Bugs ¶
This package does not support adding or retrieving aiger comments by an API.
Source Files