Versions in this module Expand all Collapse all v0 v0.1.3 Aug 25, 2021 v0.1.2 Aug 7, 2021 Changes in this version + type Output struct + func MakeOutput(g, dir string) (*Output, error) + func OpenOutput(d string) (*Output, error) + func (o *Output) Aiger() (*aiger.T, error) + func (o *Output) AigerPath() string + func (o *Output) AppendResult(bads ...*Result) + func (o *Output) Invariant(dst inter.Adder, i int) error + func (o *Output) InvariantPath(i int) string + func (o *Output) IsVerifiable(i int) bool + func (o *Output) Remove() error + func (o *Output) ResultPath(i int) string + func (o *Output) Results() []*Result + func (o *Output) RootDir() string + func (o *Output) Store() error + func (o *Output) Trace(i int) (*Trace, error) + func (o *Output) TracePath(i int) string + func (o *Output) TryVerify(dur time.Duration) []error + func (o *Output) TryVerifyResult(i int, dur time.Duration) []error + func (o *Output) Verify() []error + func (o *Output) VerifyResult(i int) []error + type Primer struct + func NewPrimer(t *logic.S, ps ...z.Lit) *Primer + func (p *Primer) Prime(m z.Lit) z.Lit + type Result struct + Depth int + Dur time.Duration + Invariant []z.Lit + M z.Lit + Status int + Trace *Trace + func (b *Result) Add(m z.Lit) + func (b *Result) FormatStatus() string + func (b *Result) IsReachable() bool + func (b *Result) IsSolved() bool + func (b *Result) IsUnreachable() bool + func (b *Result) SetReachable(t *Trace) + func (b *Result) SetUnreachable() + func (b *Result) String() string + type Trace struct + Inputs []z.Lit + Latches []z.Lit + Watches []z.Lit + func DecodeTrace(r io.Reader) (*Trace, error) + func NewTrace(s *logic.S, ws ...z.Lit) *Trace + func NewTraceBmc(u *logic.Roll, model inter.Model, ws ...z.Lit) (*Trace, []error) + func NewTraceLen(s *logic.S, sLen int, ws ...z.Lit) *Trace + func (t *Trace) Append(vs []bool) + func (t *Trace) Encode(w io.Writer) error + func (t *Trace) EncodeAigerStim(dst io.Writer) (int, error) + func (t *Trace) InputVal(i, depth int) bool + func (t *Trace) LatchVal(i, depth int) bool + func (t *Trace) Len() int + func (t *Trace) Verify(s *logic.S) []error + func (t *Trace) WatchVal(i, depth int) bool
Go to main page