1 | //===-- SimplifyConstraints.h -----------------------------------*- C++ -*-===// |
2 | // |
3 | // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
4 | // See https://llvm.org/LICENSE.txt for license information. |
5 | // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
6 | // |
7 | //===----------------------------------------------------------------------===// |
8 | |
9 | #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H |
10 | #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H |
11 | |
12 | #include "clang/Analysis/FlowSensitive/Arena.h" |
13 | #include "clang/Analysis/FlowSensitive/Formula.h" |
14 | #include "llvm/ADT/SetVector.h" |
15 | |
16 | namespace clang { |
17 | namespace dataflow { |
18 | |
19 | /// Information on the way a set of constraints was simplified. |
20 | struct SimplifyConstraintsInfo { |
21 | /// List of equivalence classes of atoms. For each equivalence class, the |
22 | /// original constraints imply that all atoms in it must be equivalent. |
23 | /// Simplification replaces all occurrences of atoms in an equivalence class |
24 | /// with a single representative atom from the class. |
25 | /// Does not contain equivalence classes with just one member or atoms |
26 | /// contained in `TrueAtoms` or `FalseAtoms`. |
27 | llvm::SmallVector<llvm::SmallVector<Atom>> EquivalentAtoms; |
28 | /// Atoms that the original constraints imply must be true. |
29 | /// Simplification replaces all occurrences of these atoms by a true literal |
30 | /// (which may enable additional simplifications). |
31 | llvm::SmallVector<Atom> TrueAtoms; |
32 | /// Atoms that the original constraints imply must be false. |
33 | /// Simplification replaces all occurrences of these atoms by a false literal |
34 | /// (which may enable additional simplifications). |
35 | llvm::SmallVector<Atom> FalseAtoms; |
36 | }; |
37 | |
38 | /// Simplifies a set of constraints (implicitly connected by "and") in a way |
39 | /// that does not change satisfiability of the constraints. This does _not_ mean |
40 | /// that the set of solutions is the same before and after simplification. |
41 | /// `Info`, if non-null, will be populated with information about the |
42 | /// simplifications that were made to the formula (e.g. to display to the user). |
43 | void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints, |
44 | Arena &arena, SimplifyConstraintsInfo *Info = nullptr); |
45 | |
46 | } // namespace dataflow |
47 | } // namespace clang |
48 | |
49 | #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H |
50 | |