Function New

analysis/validation.go:186–213

New creates a new analyzer based on declarations and extra predicates.

(extraPredicates map[ast.PredicateSym]ast.Decl, decls []ast.Decl, boundsChecking BoundsCheckingMode)

// New creates a new analyzer based on declarations and extra predicates.
func New(extraPredicates map[ast.PredicateSym]ast.Decl, decls []ast.Decl, boundsChecking BoundsCheckingMode) (*Analyzer, error) {
	extraByName := byName(extraPredicates)
	declMap := make(map[ast.PredicateSym]ast.Decl)
	for _, decl := range decls {
		pred := decl.DeclaredAtom.Predicate
		if pred == symbols.Package || pred == symbols.Use {
			continue
		}
		if existing, ok := declMap[pred]; ok {
			return nil, fmt.Errorf("predicate %v declared more than once, previous was %v", pred, existing)
		}
		declMap[pred] = decl

		if extraDecl, ok := extraByName[pred.Symbol]; ok {
			// We have a user declaration for a symbol that is also known via extraPredicates.
			if !extraDecl.IsSynthetic() {
				return nil, fmt.Errorf("cannot redeclare %v, previous Decl %v", decl, extraDecl)
			}
			// We can override a synthetic decl, but arity should still match.
			if extraDecl.DeclaredAtom.Predicate.Arity != pred.Arity {
				return nil, fmt.Errorf("declared arity %v conflicts with extra decl %v", decl, extraDecl)
			}
			// Override the synthetic decl with the one we were requested to use.
			delete(extraPredicates, pred)
		}
	}
	return &Analyzer{extraPredicates, nil /* extraFunctions */, declMap, boundsChecking}, nil
}

// EnsureDecl ensures that every predicate in the program is declared.
// It also ensures consistency of temporal usage.