Function makeSingleDeltaRule

engine/seminaivebottomup.go:332–362

makeSingleDeltaRule turns rule into a delta rule, with i-th subgoal used as "delta subgoal." The i-th subgoal must be a positive atom or temporal literal.

(rule ast.Clause, i int)

// makeSingleDeltaRule turns rule into a delta rule, with i-th subgoal used as "delta subgoal."
// The i-th subgoal must be a positive atom or temporal literal.
func makeSingleDeltaRule(rule ast.Clause, i int) ast.Clause {
	var newpremises []ast.Term

	for j, subgoal := range rule.Premises {
		if i == j {
			switch p := subgoal.(type) {
			case ast.Atom:
				newpremises = append(newpremises, makeDeltaAtom(p))
			case ast.TemporalLiteral:
				if atom, ok := p.Literal.(ast.Atom); ok {
					deltaAtom := makeDeltaAtom(atom)
					tl := ast.TemporalLiteral{
						Literal:  deltaAtom,
						Operator: p.Operator,
						Interval: p.Interval,
					}
					newpremises = append(newpremises, tl)
				} else {
					newpremises = append(newpremises, subgoal) // Should not happen
				}
			default:
				newpremises = append(newpremises, subgoal)
			}
		} else {
			newpremises = append(newpremises, subgoal)
		}
	}
	clause := ast.NewClause(rule.Head, newpremises)
	clause.Transform = rule.Transform
	return clause
}

// makeDeltaRules creates delta rules to check if newly added facts lead to new derivations.
func makeDeltaRules(decls map[ast.PredicateSym]*ast.Decl, predToRules map[ast.PredicateSym][]ast.Clause) map[ast.PredicateSym][]ast.Clause {