AnalyzeAndCheckBounds checks every rule, including bounds.
(program []parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl, boundsChecking BoundsCheckingMode)
| 124 | |
| 125 | // AnalyzeAndCheckBounds checks every rule, including bounds. |
| 126 | func AnalyzeAndCheckBounds(program []parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl, boundsChecking BoundsCheckingMode) (*ProgramInfo, error) { |
| 127 | pkgs, err := ExtractPackages(program) |
| 128 | if err != nil { |
| 129 | return nil, err |
| 130 | } |
| 131 | var clauses []ast.Clause |
| 132 | var decls []ast.Decl |
| 133 | for _, p := range pkgs { |
| 134 | ds, err := p.Decls() |
| 135 | if err != nil { |
| 136 | return nil, err |
| 137 | } |
| 138 | decls = append(decls, ds...) |
| 139 | cs, err := p.Clauses() |
| 140 | if err != nil { |
| 141 | return nil, err |
| 142 | } |
| 143 | clauses = append(clauses, cs...) |
| 144 | } |
| 145 | |
| 146 | analyzer, err := New(extraPredicates, decls, boundsChecking) |
| 147 | if err != nil { |
| 148 | return nil, err |
| 149 | } |
| 150 | if err := analyzer.EnsureDecl(clauses); err != nil { |
| 151 | return nil, err |
| 152 | } |
| 153 | |
| 154 | // Resolve "MaybeTemporal" declarations. |
| 155 | // If a synthetic declaration is marked MaybeTemporal, it means we saw at least |
| 156 | // one temporal usage. We promote it to Temporal. |
| 157 | // We also filter out the internal MaybeTemporal descriptor. |
| 158 | for pred, decl := range analyzer.decl { |
| 159 | if decl.IsMaybeTemporal() { |
| 160 | // Remove MaybeTemporal descriptor |
| 161 | var newDescr []ast.Atom |
| 162 | for _, d := range decl.Descr { |
| 163 | if d.Predicate.Symbol != ast.DescrMaybeTemporal { |
| 164 | newDescr = append(newDescr, d) |
| 165 | } |
| 166 | } |
| 167 | // Add Temporal descriptor |
| 168 | newDescr = append(newDescr, ast.NewAtom(ast.DescrTemporal)) |
| 169 | decl.Descr = newDescr |
| 170 | analyzer.decl[pred] = decl |
| 171 | } |
| 172 | } |
| 173 | |
| 174 | return analyzer.Analyze(clauses) |
| 175 | } |
| 176 | |
| 177 | func byName(decls map[ast.PredicateSym]ast.Decl) map[string]ast.Decl { |
| 178 | byName := make(map[string]ast.Decl, len(decls)) |