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
- type 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
Constants ¶
This section is empty.
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 ¶
Requeue function which allows for searching for deep counterexamples
func RequeueShort ¶
Requeue function which only allows for searching for length max+1 counterexamples.
Types ¶
type Set ¶
type Set struct {
FilterBlocked bool
// contains filtered or unexported fields
}
Set represents a set of proof obligations.
func (*Set) Choose ¶
returns a proof obligation to try to extend or block.
If none available returns 0. Then the user may call s.Grow()
func (*Set) Extend ¶
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.
Source Files