obs

Documentation

Overview

Package obs provides support for proof obligations.

Index

• Variables
• func RequeueLong(k, d, max int) bool
• func RequeueShort(k, d, max int) bool
• type Id
  • func (i Id) String() string
• type Set
  • func NewSet(d *lits.T) *Set
  • func (s *Set) Block(o Id, ms []z.Lit)
  • func (s *Set) BlockAt(k int, ms []z.Lit)
  • func (s *Set) Choose() Id
  • func (s *Set) DistToBad(o Id) int
  • func (s *Set) Dump(dst io.Writer)
  • func (s *Set) Extend(parent Id, ms []z.Lit, ini z.Lit) Id
  • func (s *Set) Grow()
  • func (s *Set) InitWit(o Id) z.Lit
  • func (s *Set) IsRoot(o Id) bool
  • func (s *Set) K(o Id) int
  • func (s *Set) MaxK() int
  • func (s *Set) Ms(o Id) []z.Lit
  • func (s *Set) Parent(o Id) Id
  • func (s *Set) Root() Id
  • func (s *Set) String(o Id) string

Variables

var Less = func(s *Set, a, b Id) bool {
	da, db := s.DistToBad(a), s.DistToBad(b)
	if da > db {
		return true
	}
	if da < db {
		return false
	}
	la, lb := len(s.Ms(a)), len(s.Ms(b))
	if la < lb {
		return true
	}
	if la > lb {
		return false
	}
	return a < b
}

Less defines how to prioritize proof obligations under the assumption they all are at the same level.

var Requeue = RequeueLong

Requeue is a function which returns true if an proof obligation should be kept in the queue.

A minimal requirement is to return false if k >= max

Functions

func RequeueLong

func RequeueLong(k, d, max int) bool

Requeue function which allows for searching for deep counterexamples

func RequeueShort

func RequeueShort(k, d, max int) bool

Requeue function which only allows for searching for length max+1 counterexamples.

Types

type Id

type Id int

func (Id) String

func (i Id) String() string

type Set

type Set struct {
	FilterBlocked bool
	// contains filtered or unexported fields
}

Set represents a set of proof obligations.

func NewSet

func NewSet(d *lits.T) *Set

NewSet creates a new set of proof obligations backed by d.

func (*Set) Block

func (s *Set) Block(o Id, ms []z.Lit)

func (*Set) BlockAt

func (s *Set) BlockAt(k int, ms []z.Lit)

func (*Set) Choose

func (s *Set) Choose() Id

returns a proof obligation to try to extend or block.

If none available returns 0. Then the user may call s.Grow()

func (*Set) DistToBad

func (s *Set) DistToBad(o Id) int

func (*Set) Dump

func (s *Set) Dump(dst io.Writer)

func (*Set) Extend

func (s *Set) Extend(parent Id, ms []z.Lit, ini z.Lit) Id

Extends extends parent with a new proof obligation that can reach parent in 1 step.

k - the level of the resulting ob d - the distance to the bad state parent - the next step to the bad state ms - a justification of the step over state variables ini - a witness to not being in the initial state.

return the id of a new proof obligation with the properties above.

func (*Set) Grow

func (s *Set) Grow()

func (*Set) InitWit

func (s *Set) InitWit(o Id) z.Lit

func (*Set) IsRoot

func (s *Set) IsRoot(o Id) bool

IsRoot returns whether o is the root proof obligation.

func (*Set) K

func (s *Set) K(o Id) int

func (*Set) MaxK

func (s *Set) MaxK() int

func (*Set) Ms

func (s *Set) Ms(o Id) []z.Lit

func (*Set) Parent

func (s *Set) Parent(o Id) Id

func (*Set) Root

func (s *Set) Root() Id

Root returns the root Obligation

func (*Set) String

func (s *Set) String(o Id) string