Function premiseNegAtom

engine/premise.go:58–87

premiseNegAtom semi-positive evaluation, i.e. looks up a and fails if it is present.

(a ast.Atom, store factstore.ReadOnlyFactStore, subst unionfind.UnionFind)

// premiseNegAtom semi-positive evaluation, i.e. looks up a and fails if it is present.
func premiseNegAtom(a ast.Atom, store factstore.ReadOnlyFactStore, subst unionfind.UnionFind) ([]unionfind.UnionFind, error) {
	n, err := functional.EvalAtom(a, subst)
	if err != nil {
		return nil, err
	}

	if n.Predicate.IsBuiltin() {
		ok, _, err := builtin.Decide(n, &subst)
		if err != nil {
			return nil, err
		}
		if ok {
			return nil, nil // negated: no solution
		}
		return []unionfind.UnionFind{subst}, nil
	}
	solutions := []unionfind.UnionFind{subst}
	// If we find a single fact that unifies, then subst is not a solution.
	err = store.GetFacts(n, func(fact ast.Atom) error {
		if _, err := unionfind.UnifyTermsExtend(n.Args, fact.Args, subst); err == nil {
			solutions = nil
			return errBreak
		}
		return nil
	})
	if err != nil && err != errBreak {
		return nil, err
	}
	return solutions, nil
}

func premiseEq(left, right ast.BaseTerm, subst unionfind.UnionFind) ([]unionfind.UnionFind, error) {
	left, right, err := functional.EvalBaseTermPair(left, right, subst)