qse

package module
v0.0.0-...-07aeed9 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Apr 24, 2023 License: MPL-2.0 Imports: 13 Imported by: 1

Documentation

Index

Constants

View Source 
const QUIVER_SIMPLE_WALKS_MAX_TRAVERSAL_CYCLE_COUNT = 2
View Source 
const SMTLIBV2_STRING_SYSTEM_OUTPUT_FORMAT = `` /* 164-byte string literal not displayed */

Don't change the order of the `%!...%` substitutions! This gets turned into a regex, so also avoid regex special chars Only ".()|[]" are checked right now Other code depends on it because golang doesn't support named capture groups in regexes!

View Source 
const Z3SMTLibv2Query_TEMP_SMT2_FILENAME_FORMAT = "temp_qse-go_Z3SMTLibv2Query-Run_*_GENERATED.smt2"

Variables

This section is empty.

Functions

func ComparableEqualFunc 

func ComparableEqualFunc(k1, k2 any) (eq bool)

Actually requires k1, k2 comparable

func DedupSortedInPlace 

func DedupSortedInPlace(arr *[]int)

func DigestEqual 

func DigestEqual(a digest_t, b digest_t) (equal bool)

func FixDigest 

func FixDigest(pseudo_digest digest_t, fix_seed byte) (digest digest_t)

func FixDigest32 

func FixDigest32(pseudo_fixed_digest uint32, fix_seed byte) (fixed_digest uint32)

func Greet 

func Greet(name string) (greeting string)

func HashableHashFunc 

func HashableHashFunc(k any) (fixed_digest uint32)

Actually requires k hashable

func InsertionSortInPlace 

func InsertionSortInPlace(arr []int)

func IsInvertedEdge 

func IsInvertedEdge[NODE Hashable](maybe_buf PHashMap[Literal[NODE], struct{}], maybe_inv PHashMap[Literal[NODE], struct{}]) (match bool)

func MixDigests 

func MixDigests(pseudo_a []byte, pseudo_b []byte) (digest digest_t)

func SMTLibv2WrapAssertion 

func SMTLibv2WrapAssertion(clause string) (s_expr string)

func SpliceOutReclaim 

func SpliceOutReclaim[T any](arr *[]T, index int)

func StartSiMReQ 

func StartSiMReQ[
	QNODE any,
	ATOM comparable,
	IDENT any,
	SORT any,
	MODEL any,
	SCTX SMTSolvedContext[MODEL],
	SYS SMTSystem[
		IdLiteral[ATOM],
		IDENT,
		SORT,
		MODEL,
		SCTX,
	],
](
	in_updates chan Augmented[
		QuiverUpdate[QNODE, PHashMap[Literal[WithId_H[ATOM]], struct{}], *DMT[WithId_H[ATOM], QuiverIndex]],
		[]SMTFreeFun[IDENT, SORT],
	],
	out_models chan MODEL,
	sys SYS,
	aot_nodes []QNODE,
) (
	dmtq *Quiver[QNODE, PHashMap[Literal[WithId_H[ATOM]], struct{}], *DMT[WithId_H[ATOM], QuiverIndex]],
	top_node QuiverIndex,
	fail_node QuiverIndex,
	aot_indices []QuiverIndex,
)

func WrapInvert 

func WrapInvert(pseudo_digest digest_t) (digest digest_t)

func WrapInvert32 

func WrapInvert32(pseudo_fixed_digest uint32) (fixed_digest uint32)

func ZeroDigest 

func ZeroDigest() (digest digest_t)

Types

type Augmented 

type Augmented[A any, B any] struct {
	Value   A
	Augment B
}

func NewAugmentedSimple 

func NewAugmentedSimple[A any](value A) (aug Augmented[A, struct{}])

type DMT 

type DMT[NODE Hashable, LEAF Hashable] struct {
	// contains filtered or unexported fields
}

func NewDMT 

func NewDMT[NODE Hashable, LEAF Hashable]() (t DMT[NODE, LEAF])

func (DMT[NODE, LEAF]) EntryList 

func (dmt DMT[NODE, LEAF]) EntryList() (out []TrieEntry[Literal[NODE], LEAF])

func (DMT[NODE, LEAF]) ForEachPair 

func (t DMT[NODE, LEAF]) ForEachPair(fn func(PHashMap[Literal[NODE], struct{}], LEAF))

func (DMT[NODE, LEAF]) FwdLookup 

func (t DMT[NODE, LEAF]) FwdLookup(a PHashMap[Literal[NODE], struct{}]) (item *LEAF)

func (*DMT[NODE, LEAF]) Insert 

func (t *DMT[NODE, LEAF]) Insert(
	seq PHashMap[Literal[NODE], struct{}], leaf LEAF,
)

func (*DMT[NODE, LEAF]) InsertReturn 

func (t *DMT[NODE, LEAF]) InsertReturn(
	seq PHashMap[Literal[NODE], struct{}], leaf LEAF,
) (
	leaf_ptr *TrieLeafNode[Literal[NODE], LEAF, digest_t],
)

func (*DMT[NODE, LEAF]) MergeIdenticalLeaves 

func (t *DMT[NODE, LEAF]) MergeIdenticalLeaves(leaves []*TrieLeafNode[Literal[NODE], LEAF, digest_t])

func (DMT[NODE, LEAF]) RevLookup 

func (t DMT[NODE, LEAF]) RevLookup(b LEAF) (items []PHashMap[Literal[NODE], struct{}])

func (*DMT[NODE, LEAF]) ShiftChildren 

func (t *DMT[NODE, LEAF]) ShiftChildren(node *TrieValueNode[Literal[NODE], LEAF, digest_t], child_i int)

func (*DMT[NODE, LEAF]) SimplifyNode 

func (t *DMT[NODE, LEAF]) SimplifyNode(node *TrieValueNode[Literal[NODE], LEAF, digest_t])

func (*DMT[NODE, LEAF]) UpdateHashes 

func (t *DMT[NODE, LEAF]) UpdateHashes(leaf_ptr *TrieLeafNode[Literal[NODE], LEAF, digest_t])

type DMTQWardenConfig 

type DMTQWardenConfig[N any, ATOM Hashable, AUG any] struct {
	// contains filtered or unexported fields
}

func (DMTQWardenConfig[N, ATOM, AUG]) Start 

func (warden_config DMTQWardenConfig[N, ATOM, AUG]) Start()

type Hashable 

type Hashable interface {
	comparable
	// contains filtered or unexported methods
}

This is the version of Hashable to use

type IdLiteral 

type IdLiteral[ATOM comparable] Literal[WithId_H[ATOM]]

func (IdLiteral[ATOM]) Hash 

func (lit IdLiteral[ATOM]) Hash() (digest digest_t)

func (IdLiteral[ATOM]) Hash32 

func (lit IdLiteral[ATOM]) Hash32() (fixed_digest uint32)

type IdSource 

type IdSource struct {
	// contains filtered or unexported fields
}

func (*IdSource) Gen 

func (idsrc *IdSource) Gen() (id NumericId)

type Literal 

type Literal[NODE Hashable] struct {
	Value NODE
	Eq    bool
}

func BufferingLiteral 

func BufferingLiteral[NODE Hashable](value NODE) (lit Literal[NODE])

func InvertingLiteral 

func InvertingLiteral[NODE Hashable](value NODE) (lit Literal[NODE])

func (Literal[NODE]) Hash 

func (lit Literal[NODE]) Hash() (digest digest_t)

func (Literal[NODE]) Hash32 

func (lit Literal[NODE]) Hash32() (fixed_digest uint32)

func (Literal[NODE]) Invert 

func (lit Literal[NODE]) Invert() (inverted Literal[NODE])

type Neighbor 

type Neighbor[E any] struct {
	// contains filtered or unexported fields
}

type NumericId 

type NumericId = uint32

type PHashMap 

type PHashMap[K comparable, V any] struct {
	// contains filtered or unexported fields
}

A persistent hash map Struct embedding would just make things confusing because this is all pre-generics

func NewPHashMap 

func NewPHashMap[K Hashable, V any]() (pm PHashMap[K, V])

func StdlibMapToPHashMap 

func StdlibMapToPHashMap[K Hashable, V any](m map[K]V) (pm PHashMap[K, V])

func (PHashMap[K, V]) Assoc 

func (pm PHashMap[K, V]) Assoc(key K, val V) (updated PHashMap[K, V])

func (PHashMap[K, V]) Clone 

func (pm PHashMap[K, V]) Clone() (cloned PHashMap[K, V])

func (PHashMap[K, V]) Dissoc 

func (pm PHashMap[K, V]) Dissoc(key K) (updated PHashMap[K, V])

func (PHashMap[K, V]) Equal 

func (a PHashMap[K, V]) Equal(b PHashMap[K, V]) (eq bool)

func (PHashMap[K, V]) HasKey 

func (pm PHashMap[K, V]) HasKey(key K) (has bool)

func (PHashMap[K, V]) Index 

func (pm PHashMap[K, V]) Index(key K) (val V, ok bool)

func (PHashMap[K, V]) ToStdlibMap 

func (pm PHashMap[K, V]) ToStdlibMap() (m map[K]V)

type PhantomData 

type PhantomData[T any] struct{}

Effectively does the same thing as in Rust Unused type parameters are *usually* a mistake so it's nice to be explicit

type PhantomQuiverAssociation 

type PhantomQuiverAssociation[N any, E any, C ReversibleAssoc[E, QuiverIndex]] struct {
	// contains filtered or unexported fields
}

A nicely packaged way to represent association with a particular quiver

func NewPhantomQuiverAssociation 

func NewPhantomQuiverAssociation[N any, E any, C ReversibleAssoc[E, QuiverIndex]]() (
	phantom_association PhantomQuiverAssociation[N, E, C],
)

type Quiver 

type Quiver[N any, E any, C ReversibleAssoc[E, QuiverIndex]] struct {
	// contains filtered or unexported fields
}

A doubly-linked arena-based quiver. Abstracted over arbitrary edge container types, which store all of the edges for a particular node.

func (*Quiver[N, E, C]) AllInneighbors 

func (q *Quiver[N, E, C]) AllInneighbors(src QuiverIndex) (inneighbors []Neighbor[E])

func (*Quiver[N, E, C]) AllOutneighbors 

func (q *Quiver[N, E, C]) AllOutneighbors(src QuiverIndex) (outneighbors []Neighbor[E])

func (*Quiver[N, E, C]) ApplyUpdate 

func (q *Quiver[N, E, C]) ApplyUpdate(update QuiverUpdate[N, E, C]) (src, dst QuiverIndex)

func (*Quiver[N, E, C]) ApplyUpdateAndEmitWalks 

func (q *Quiver[N, E, C]) ApplyUpdateAndEmitWalks(
	out_walks chan QuiverWalk[N, E],
	update QuiverUpdate[N, E, C],
	start_unresolved QuiverIndexParameterized[N, E, C],
	dst_final QuiverIndex,
)

func (Quiver[N, E, C]) EmitSimpleWalksFromToRev 

func (q Quiver[N, E, C]) EmitSimpleWalksFromToRev(
	out_simple_walks chan []E,
	src QuiverIndex,
	dst QuiverIndex,
)

func (Quiver[N, E, C]) EmitSimpleWalksFromToRevPrefix 

func (q Quiver[N, E, C]) EmitSimpleWalksFromToRevPrefix(
	out_simple_walks chan []E,
	src QuiverIndex,
	true_dst QuiverIndex,
	prefix *[]E,
	seen PHashMap[QuiverIndex, uint8],
)

func (*Quiver[N, E, C]) ForEachInneighbor 

func (q *Quiver[N, E, C]) ForEachInneighbor(src QuiverIndex, fn func(Neighbor[E]))

func (*Quiver[N, E, C]) ForEachOutneighbor 

func (q *Quiver[N, E, C]) ForEachOutneighbor(src QuiverIndex, fn func(Neighbor[E]))

func (*Quiver[N, E, C]) InsertEdge 

func (q *Quiver[N, E, C]) InsertEdge(src, dst QuiverIndex, edge_value E)

func (*Quiver[N, E, C]) InsertNode 

func (q *Quiver[N, E, C]) InsertNode(node_value N, container C) (idx QuiverIndex)

func (Quiver[N, E, C]) NewIntendedNode 

func (Quiver[N, E, C]) NewIntendedNode(node N, container C) (intended_node QuiverIntendedNode[N, E, C])

func (Quiver[N, E, C]) ParameterizeIndex 

func (Quiver[N, E, C]) ParameterizeIndex(index QuiverIndex) (indexp QuiverIndexParameterized[N, E, C])

type QuiverIndex 

type QuiverIndex uint

A named type representing an index into the internal data structure of a quiver. It refers to a specific node, and is only usable with a specific Quiver[N, E, C] object.

func (QuiverIndex) Hash 

func (i QuiverIndex) Hash() (digest digest_t)

func (QuiverIndex) Hash32 

func (i QuiverIndex) Hash32() (fixed_digest uint32)

type QuiverIndexParameterized 

type QuiverIndexParameterized[N any, E any, C ReversibleAssoc[E, QuiverIndex]] struct {
	QuiverIndex
	// contains filtered or unexported fields
}

An alternative to the QuiverIndex type that carries type parameters

func TrustingParameterizeQuiverIndex 

func TrustingParameterizeQuiverIndex[N any, E any, C ReversibleAssoc[E, QuiverIndex]](
	index QuiverIndex,
) (
	indexp QuiverIndexParameterized[N, E, C],
)

func (QuiverIndexParameterized[N, E, C]) ResolveAsQuiverUpdateDst 

func (indexp QuiverIndexParameterized[N, E, C]) ResolveAsQuiverUpdateDst(q_ptr *Quiver[N, E, C]) (
	index QuiverIndex,
)

func (QuiverIndexParameterized[N, E, C]) Unparameterize 

func (indexp QuiverIndexParameterized[N, E, C]) Unparameterize() (index QuiverIndex)

type QuiverIntendedNode 

type QuiverIntendedNode[N any, E any, C ReversibleAssoc[E, QuiverIndex]] struct {
	// contains filtered or unexported fields
}

A non-trivial QuiverUpdateDst - a node itself that has to be added to the quiver But this must be wrapped with it's intent (mostly for type parameterization)

func NewQuiverIntendedNode 

func NewQuiverIntendedNode[N any, E any, C ReversibleAssoc[E, QuiverIndex], UNUSED_BOUNDARY any](
	node N, container C,
) (
	intended_node QuiverIntendedNode[N, E, C],
)

func (QuiverIntendedNode[N, E, C]) ResolveAsQuiverUpdateDst 

func (intended_node QuiverIntendedNode[N, E, C]) ResolveAsQuiverUpdateDst(q_ptr *Quiver[N, E, C]) (
	index QuiverIndex,
)

type QuiverNode 

type QuiverNode[N any, E any, C ReversibleAssoc[E, QuiverIndex]] struct {
	// contains filtered or unexported fields
}

A node of a quiver. Parent references are done with QuiverIndex objects and not references.

type QuiverUpdate 

type QuiverUpdate[N any, E any, C ReversibleAssoc[E, QuiverIndex]] struct {
	Src  QuiverIndex
	Dst  QuiverUpdateDst[N, E, C]
	Edge *E
}

A new edge (and possibly a new node) being added to a quiver The new_dst key indicates whether dst is already a part of the quiver or not

type QuiverUpdateDst 

type QuiverUpdateDst[N any, E any, C ReversibleAssoc[E, QuiverIndex]] interface {
	ResolveAsQuiverUpdateDst(q_ptr *Quiver[N, E, C]) (index QuiverIndex)
}

type QuiverWalk 

type QuiverWalk[N any, E any] struct {
	// contains filtered or unexported fields
}

Allow edges to be stored in pointers to chunks to limit (to some extent) duplication

type ReversibleAssoc 

type ReversibleAssoc[A any, B any] interface {
	Insert(a A, b B)
	FwdLookup(a A) (item *B)
	RevLookup(b B) (items []A)
	ForEachPair(fn func(A, B))
}

An interface that represents a data structure that maps values in one direction, but allows you to query in both. Each A is mapped to one B, but you're free to look up all A values associated with a specific B.

type SMRConfig 

type SMRConfig[
	ATOM comparable,
	IDENT any,
	SORT any,
	MODEL any,
	SCTX SMTSolvedContext[MODEL],
	SYS SMTSystem[
		IdLiteral[ATOM],
		IDENT,
		SORT,
		MODEL,
		SCTX,
	],
] struct {
	// contains filtered or unexported fields
}

func NewSMRConfig 

func NewSMRConfig[
	ATOM comparable,
	IDENT any,
	SORT any,
	MODEL any,
	SCTX SMTSolvedContext[MODEL],
	SYS SMTSystem[
		IdLiteral[ATOM],
		IDENT,
		SORT,
		MODEL,
		SCTX,
	],
](
	in_canidates chan SMRDNFClause[ATOM, IDENT, SORT],
	out_models chan MODEL,
	sys SYS,
) (
	smr_config SMRConfig[ATOM, IDENT, SORT, MODEL, SCTX, SYS],
)

func (SMRConfig[ATOM, IDENT, SORT, MODEL, SCTX, SYS]) RunSMR 

func (smr_config SMRConfig[ATOM, IDENT, SORT, MODEL, SCTX, SYS]) RunSMR() (done bool)

func (SMRConfig[ATOM, IDENT, SORT, MODEL, SCTX, SYS]) SMRIterationUnfinishedUnlocked 

func (smr_config SMRConfig[ATOM, IDENT, SORT, MODEL, SCTX, SYS]) SMRIterationUnfinishedUnlocked()

func (SMRConfig[ATOM, IDENT, SORT, MODEL, SCTX, SYS]) Start 

func (smr_config SMRConfig[ATOM, IDENT, SORT, MODEL, SCTX, SYS]) Start()

type SMRDNFClause 

type SMRDNFClause[
	ATOM comparable,
	IDENT any,
	SORT any,
] struct {
	// contains filtered or unexported fields
}

type SMRIsSleeping 

type SMRIsSleeping struct {
	*TrustingNoCopySMRIsSleeping
}

func NewSMRIsSleeping 

func NewSMRIsSleeping() (is_sleeping SMRIsSleeping)

func (SMRIsSleeping) Check 

func (is_sleeping SMRIsSleeping) Check() (is bool)

func (SMRIsSleeping) Sleep 

func (is_sleeping SMRIsSleeping) Sleep() (was bool)

func (SMRIsSleeping) Wake 

func (is_sleeping SMRIsSleeping) Wake() (was bool)

type SMRUnfinishedArray 

type SMRUnfinishedArray[
	ATOM comparable,
	IDENT any,
	SORT any,
] struct {
	*TrustingNoCopySMRUnfinishedArray[ATOM, IDENT, SORT]
}

func NewSMRUnfinishedArray 

func NewSMRUnfinishedArray[
	ATOM comparable,
	IDENT any,
	SORT any,
]() (unfinished SMRUnfinishedArray[ATOM, IDENT, SORT])

type SMTFreeFun 

type SMTFreeFun[IDENT any, SORT any] struct {
	Name IDENT
	Args []SORT
	Ret  SORT
}

type SMTLibv2StringSolvedCtx 

type SMTLibv2StringSolvedCtx struct {
	// contains filtered or unexported fields
}

func (SMTLibv2StringSolvedCtx) ExtractMUS 

func (sctx SMTLibv2StringSolvedCtx) ExtractMUS() (mus *[]int)

func (SMTLibv2StringSolvedCtx) GetModel 

func (sctx SMTLibv2StringSolvedCtx) GetModel() (model *string)

func (SMTLibv2StringSolvedCtx) IsSat 

func (sctx SMTLibv2StringSolvedCtx) IsSat() (is *bool)

type SMTLibv2StringSystem 

type SMTLibv2StringSystem struct {
	Idsrc IdSource
}

func (SMTLibv2StringSystem) CheckSat 

func (sys SMTLibv2StringSystem) CheckSat(
	conjunction []IdLiteral[string],
	free_funs []SMTFreeFun[string, string],
) (sctx SMTLibv2StringSolvedCtx)

func (SMTLibv2StringSystem) DeclSExpr 

func (sys SMTLibv2StringSystem) DeclSExpr(free_fun SMTFreeFun[string, string]) (s_expr string)

func (SMTLibv2StringSystem) Epilogue 

func (sys SMTLibv2StringSystem) Epilogue() (part string)

func (SMTLibv2StringSystem) ExpandStringLiteral 

func (sys SMTLibv2StringSystem) ExpandStringLiteral(lit IdLiteral[string]) (s_expr string)

func (SMTLibv2StringSystem) GenDecls 

func (sys SMTLibv2StringSystem) GenDecls(free_funs []SMTFreeFun[string, string]) (part string)

func (SMTLibv2StringSystem) MakeAtom 

func (sys SMTLibv2StringSystem) MakeAtom(expr string) (atom WithId_H[string])

func (SMTLibv2StringSystem) MarkClauseIndex 

func (sys SMTLibv2StringSystem) MarkClauseIndex(clause string, index uint) (clause_marked string)

func (SMTLibv2StringSystem) ParseSolvedCtx 

func (sys SMTLibv2StringSystem) ParseSolvedCtx(str string) (sctx SMTLibv2StringSolvedCtx)

func (SMTLibv2StringSystem) Prologue 

func (sys SMTLibv2StringSystem) Prologue() (part string)

type SMTSolvedContext 

type SMTSolvedContext[MODEL any] interface {
	IsSat() *bool
	GetModel() *MODEL
	ExtractMUS() *[]int
}

A context in which an SMT solver has been invoked and results are available

type SMTSystem 

type SMTSystem[
	EXPR Hashable,
	IDENT any,
	SORT any,
	MODEL any,
	SCTX SMTSolvedContext[MODEL],
] interface {
	CheckSat([]EXPR, []SMTFreeFun[IDENT, SORT]) SCTX
}

A system which provides basic interfaces to an SMT solver

type SimpleQuiver 

type SimpleQuiver[N any, E comparable] struct {
	Quiver[N, E, *SimpleReversibleAssoc[E, QuiverIndex]]
}

A simple quiver using SimpleReversibleAssoc as the edge container.

func (*SimpleQuiver[N, E]) InsertNodeSimple 

func (q *SimpleQuiver[N, E]) InsertNodeSimple(node_value N) (idx QuiverIndex)

type SimpleReversibleAssoc 

type SimpleReversibleAssoc[A comparable, B comparable] struct {
	// contains filtered or unexported fields
}

A simple implementation of a ReversibleAssoc data structure backed by a map. The RevLookup method runs in O(n).

func NewSimpleRA 

func NewSimpleRA[A comparable, B comparable]() (obj SimpleReversibleAssoc[A, B])

func (SimpleReversibleAssoc[A, B]) ForEachPair 

func (obj SimpleReversibleAssoc[A, B]) ForEachPair(fn func(A, B))

func (SimpleReversibleAssoc[A, B]) FwdLookup 

func (obj SimpleReversibleAssoc[A, B]) FwdLookup(a A) (item *B)

func (*SimpleReversibleAssoc[A, B]) Insert 

func (obj *SimpleReversibleAssoc[A, B]) Insert(a A, b B)

func (SimpleReversibleAssoc[A, B]) RevLookup 

func (obj SimpleReversibleAssoc[A, B]) RevLookup(b B) (items []A)

type Trie 

type Trie[NODE Hashable, LEAF comparable, META any] struct {
	// contains filtered or unexported fields
}

A trie that maps sets of NODE to values of LEAF.

func NewTrie 

func NewTrie[NODE Hashable, LEAF comparable]() (t Trie[NODE, LEAF, struct{}])

func (Trie[NODE, LEAF, META]) EntryList 

func (t Trie[NODE, LEAF, META]) EntryList() (out []TrieEntry[NODE, LEAF])

Enumerate all mappings contained within a trie

func (Trie[NODE, LEAF, META]) ForEachEntry 

func (t Trie[NODE, LEAF, META]) ForEachEntry(fn func(TrieEntry[NODE, LEAF]))

Recursively call a method on all key-value pairs defined in a trie

func (Trie[NODE, LEAF, META]) ForEachPair 

func (t Trie[NODE, LEAF, META]) ForEachPair(fn func(PHashMap[NODE, struct{}], LEAF))

func (Trie[NODE, LEAF, META]) FwdLookup 

func (t Trie[NODE, LEAF, META]) FwdLookup(a PHashMap[NODE, struct{}]) (item *LEAF)

func (*Trie[NODE, LEAF, META]) Insert 

func (t *Trie[NODE, LEAF, META]) Insert(seq PHashMap[NODE, struct{}], leaf LEAF)

func (*Trie[NODE, LEAF, META]) InsertReturn 

func (t *Trie[NODE, LEAF, META]) InsertReturn(seq PHashMap[NODE, struct{}], leaf LEAF) (leaf_ptr *TrieLeafNode[NODE, LEAF, META])

func (Trie[NODE, LEAF, META]) Lookup 

func (t Trie[NODE, LEAF, META]) Lookup(query PHashMap[NODE, struct{}]) (leaf *LEAF)

func (Trie[NODE, LEAF, META]) LookupLeaf 

func (t Trie[NODE, LEAF, META]) LookupLeaf(leaf LEAF) (seqs []PHashMap[NODE, struct{}])

func (Trie[NODE, LEAF, META]) LookupLeafByNode 

func (t Trie[NODE, LEAF, META]) LookupLeafByNode(leaf_node *TrieLeafNode[NODE, LEAF, META]) (seq PHashMap[NODE, struct{}])

func (Trie[NODE, LEAF, META]) LookupRepair 

func (t Trie[NODE, LEAF, META]) LookupRepair(query PHashMap[NODE, struct{}])

func (Trie[NODE, LEAF, META]) RevLookup 

func (t Trie[NODE, LEAF, META]) RevLookup(b LEAF) (items []PHashMap[NODE, struct{}])

type TrieEntry 

type TrieEntry[NODE Hashable, LEAF comparable] struct {
	// contains filtered or unexported fields
}

func (TrieEntry[NODE, LEAF]) PrefixWith 

func (e TrieEntry[NODE, LEAF]) PrefixWith(prefix PHashMap[NODE, struct{}]) (mod TrieEntry[NODE, LEAF])

type TrieLeafNode 

type TrieLeafNode[NODE Hashable, LEAF comparable, META any] struct {
	// contains filtered or unexported fields
}

func (TrieLeafNode[NODE, LEAF, META]) ForEachNodeEntry 

func (node TrieLeafNode[NODE, LEAF, META]) ForEachNodeEntry(fn func(TrieEntry[NODE, LEAF]))

func (TrieLeafNode[NODE, LEAF, META]) IsTrieLeaf 

func (TrieLeafNode[NODE, LEAF, META]) IsTrieLeaf() (is bool)

type TrieNode 

type TrieNode[NODE Hashable, LEAF comparable] interface {
	IsTrieLeaf() (is bool)
	ForEachNodeEntry(fn func(TrieEntry[NODE, LEAF]))
}

type TrieValueNode 

type TrieValueNode[NODE Hashable, LEAF comparable, META any] struct {
	// contains filtered or unexported fields
}

func NewTrieRootNode 

func NewTrieRootNode[NODE Hashable, LEAF comparable]() (node TrieValueNode[NODE, LEAF, struct{}])

func (*TrieValueNode[NODE, LEAF, META]) CutPrefix 

func (node *TrieValueNode[NODE, LEAF, META]) CutPrefix(shared PHashMap[NODE, struct{}]) (parent *TrieValueNode[NODE, LEAF, META])

func (TrieValueNode[NODE, LEAF, META]) ForEachNodeEntry 

func (node TrieValueNode[NODE, LEAF, META]) ForEachNodeEntry(fn func(TrieEntry[NODE, LEAF]))

func (TrieValueNode[NODE, LEAF, META]) IsTrieLeaf 

func (TrieValueNode[NODE, LEAF, META]) IsTrieLeaf() (is bool)

func (*TrieValueNode[NODE, LEAF, META]) PrepChild 

func (node *TrieValueNode[NODE, LEAF, META]) PrepChild(seq *PHashMap[NODE, struct{}], leaf LEAF) (r_child TrieNode[NODE, LEAF])

type TrustingNoCopySMRIsSleeping 

type TrustingNoCopySMRIsSleeping struct {
	// contains filtered or unexported fields
}

type TrustingNoCopySMRUnfinishedArray 

type TrustingNoCopySMRUnfinishedArray[
	ATOM comparable,
	IDENT any,
	SORT any,
] struct {
	// contains filtered or unexported fields
}

func (*TrustingNoCopySMRUnfinishedArray[ATOM, IDENT, SORT]) Append 

func (unfinished *TrustingNoCopySMRUnfinishedArray[ATOM, IDENT, SORT]) Append(
	elems ...SMRDNFClause[ATOM, IDENT, SORT],
)

type WithId_H 

type WithId_H[T comparable] struct {
	Value T
	Id    NumericId
}

func (WithId_H[T]) GeneralDeref 

func (wi WithId_H[T]) GeneralDeref() (val T)

func (WithId_H[T]) Hash 

func (wi WithId_H[T]) Hash() (digest digest_t)

func (WithId_H[T]) Hash32 

func (wi WithId_H[T]) Hash32() (fixed_digest uint32)

type Z3SMTLibv2Query 

type Z3SMTLibv2Query struct {
	// contains filtered or unexported fields
}

func NewZ3SMTLibv2Query 

func NewZ3SMTLibv2Query(query_str string) (query Z3SMTLibv2Query)

func (Z3SMTLibv2Query) Run 

func (query Z3SMTLibv2Query) Run() (output string)

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.