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 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 evalution 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 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.