engine

Documentation

Overview

Package engine contains an implementation of the semi-naive evaluation strategy for datalog programs. It computes the fixpoint of the consequence operator incrementally by applying rules to known facts, taking care of consequences of already seen facts only once, until no new facts have been discovered.

Index

• func EvalProgram(programInfo *analysis.ProgramInfo, store factstore.FactStore, ...) error
• func EvalProgramNaive(program []ast.Clause, store factstore.SimpleInMemoryStore) error
• func EvalTransform(head ast.Atom, transform ast.Transform, input []ast.ConstSubstList, ...) error
• type EvalOption
  • func WithCreatedFactLimit(limit int) EvalOption
• type EvalOptions
• type InclusionChecker
  • func NewInclusionChecker(decls map[ast.PredicateSym]ast.Decl) (*InclusionChecker, error)
  • func NewInclusionCheckerFromDesugared(decls map[ast.PredicateSym]*ast.Decl) *InclusionChecker
  • func (i InclusionChecker) CheckFact(fact ast.Atom, store factstore.FactStore) error
• type QueryContext
  • func (q QueryContext) EvalPremise(premise ast.Term, subst unionfind.UnionFind) ([]unionfind.UnionFind, error)
  • func (q QueryContext) EvalQuery(query ast.Atom, mode []ast.ArgMode, uf unionfind.UnionFind, ...) error
• type Stats
  • func EvalProgramWithStats(programInfo *analysis.ProgramInfo, store factstore.FactStore, ...) (Stats, error)
  • func EvalStratifiedProgramWithStats(programInfo *analysis.ProgramInfo, strata []analysis.Nodeset, ...) (Stats, error)

Functions

func EvalProgram

func EvalProgram(programInfo *analysis.ProgramInfo, store factstore.FactStore, options ...EvalOption) error

EvalProgram evaluates a given program on the given facts, modifying the fact store in the process.

func EvalProgramNaive

func EvalProgramNaive(program []ast.Clause, store factstore.SimpleInMemoryStore) error

EvalProgramNaive evaluates a given program on the given facts, modifying the fact store in the process.

func EvalTransform

func EvalTransform(
	head ast.Atom,
	transform ast.Transform,
	input []ast.ConstSubstList,
	emit func(atom ast.Atom) bool) error

EvalTransform evaluates a transform.

Types

type EvalOption

type EvalOption func(*EvalOptions)

EvalOption affects the way the evaluation is performed.

func WithCreatedFactLimit

func WithCreatedFactLimit(limit int) EvalOption

WithCreatedFactLimit is an evaluation option that limits the maximum number of facts created during evaluation.

type EvalOptions

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

EvalOptions are used to configure the evaluation.

type InclusionChecker

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

InclusionChecker checks inclusion constraints. It does not check type bounds.

func NewInclusionChecker

func NewInclusionChecker(decls map[ast.PredicateSym]ast.Decl) (*InclusionChecker, error)

NewInclusionChecker returns a new InclusionChecker.

func NewInclusionCheckerFromDesugared

func NewInclusionCheckerFromDesugared(decls map[ast.PredicateSym]*ast.Decl) *InclusionChecker

NewInclusionCheckerFromDesugared returns a new InclusionChecker. The declarations must be in desugared form.

func (InclusionChecker) CheckFact

func (i InclusionChecker) CheckFact(fact ast.Atom, store factstore.FactStore) error

CheckFact verifies that a store containing this fact respects inclusion constraints. It also checks types, since after desugaring, the argument types may affect which of the inclusion constraint alternatives need to be checked.

type QueryContext

type QueryContext struct {
	PredToRules map[ast.PredicateSym][]ast.Clause
	PredToDecl  map[ast.PredicateSym]*ast.Decl
	Store       factstore.ReadOnlyFactStore
}

QueryContext groups data needed for evaluating a query top-down (backward chaining).

func (QueryContext) EvalPremise

func (q QueryContext) EvalPremise(premise ast.Term, subst unionfind.UnionFind) ([]unionfind.UnionFind, error)

EvalPremise evaluates a single premise top-down. This is similar to PROLOG style SLD resolution: even though we have negated atoms, they are treated them as lookups (stratified semantics).

func (QueryContext) EvalQuery

func (q QueryContext) EvalQuery(query ast.Atom, mode []ast.ArgMode, uf unionfind.UnionFind, cb func(fact ast.Atom) error) error

EvalQuery evaluates a query top-down, according to mode and union-find-subst. The mode must consist only of ArgModeInput (+) and ArgModeOutput (-). For every input, query.Args[i] is either a constant or a variable that is in the domain of subst.

type Stats

type Stats struct {
	Strata        [][]ast.PredicateSym
	Duration      []time.Duration
	PredToStratum map[ast.PredicateSym]int
}

Stats represents strata and their running times.

func EvalProgramWithStats

func EvalProgramWithStats(programInfo *analysis.ProgramInfo, store factstore.FactStore, options ...EvalOption) (Stats, error)

EvalProgramWithStats evaluates a given program on the given facts, modifying the fact store in the process.

func EvalStratifiedProgramWithStats

func EvalStratifiedProgramWithStats(programInfo *analysis.ProgramInfo,
	strata []analysis.Nodeset, predToStratum map[ast.PredicateSym]int,
	store factstore.FactStore, options ...EvalOption) (Stats, error)

EvalStratifiedProgramWithStats evaluates a given stratified program on the given facts, modifying the fact store in the process.