engine

type EvalOption ¶

type EvalOption func(*EvalOptions)

EvalOption affects the way the evaluation is performed.

func WithCreatedFactLimit(limit int) EvalOption

func WithExternalPredicates(
	callbacks map[ast.PredicateSym]ExternalPredicateCallback) EvalOption

type EvalOptions ¶

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

EvalOptions are used to configure the evaluation.

type ExternalPredicateCallback ¶ added in v0.4.0

type ExternalPredicateCallback interface {
	// If true, the engine will pass any subgoals of the clause that mention output variables
	// to ExecuteQuery. Otherwise, the pushdown argument will be empty.
	ShouldPushdown() bool
	ShouldQuery(inputs []ast.Constant, filters []ast.BaseTerm, pushdown []ast.Term) bool
	ExecuteQuery(inputs []ast.Constant, filters []ast.BaseTerm, pushdown []ast.Term,
		cb func([]ast.BaseTerm)) error
}

ExternalPredicateCallback is used to query external data sources.

An atom `mydb(input1, ..., inputN, OutputVar1, ..., OutputVarN)` is evaluated as follows:

• the engine checks whether the fact store contains any facts of the shape `mydb(input1, ..., inputN, _, ..., _)`. If so, we use those for evaluation.
• if no facts were found, the engine calls `ShouldQuery(input1, ..., inputN)` if false, evaluation continues.
• if true, the engine calls `Query(input1, ..., inputN, filter1, ..., filterM)` and expects outputs callback. Every output tuple gets added as `mydb(input1, ..., inputN, output1, ..., outputN)` fact to the store, and continues evaluation. if ExecuteQuery returns an error, evaluation fails with that error.

If tuples (input1, ..., inputN) are known to yield empty results, the implementation can keep track of that and prevent an unnecessary call to `ExecuteQuery`. filters contains the arguments that are output positions which are either variables or constants that are used to match the position (filters proper). The implementation may use the constant filter arguments for filter-pushdown, but is also free to ignore them. In any case, when constant filter arguments are present, only matching facts will be added to the store.

type InclusionChecker ¶

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

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

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 ¶ added in v0.2.0

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

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

func (q QueryContext) EvalExternalQuery(query ast.Atom, mode []ast.ArgMode,
	ext ExternalPredicateCallback, pushdown []ast.Term, cb func(fact ast.Atom) error) error

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, cb func(fact ast.Atom) error) error

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(programInfo *analysis.ProgramInfo, store factstore.FactStore, options ...EvalOption) (Stats, error)

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