Analysis/FlowSensitive/SimplifyConstraints.h

0001 //===-- SimplifyConstraints.h -----------------------------------*- C++ -*-===//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008
0009 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
0010 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
0011
0012 #include "clang/Analysis/FlowSensitive/Arena.h"
0013 #include "clang/Analysis/FlowSensitive/Formula.h"
0014 #include "llvm/ADT/SetVector.h"
0015
0016 namespace clang {
0017 namespace dataflow {
0018
0019 /// Information on the way a set of constraints was simplified.
0020 struct SimplifyConstraintsInfo {
0021   /// List of equivalence classes of atoms. For each equivalence class, the
0022   /// original constraints imply that all atoms in it must be equivalent.
0023   /// Simplification replaces all occurrences of atoms in an equivalence class
0024   /// with a single representative atom from the class.
0025   /// Does not contain equivalence classes with just one member or atoms
0026   /// contained in `TrueAtoms` or `FalseAtoms`.
0027   llvm::SmallVector<llvm::SmallVector<Atom>> EquivalentAtoms;
0028   /// Atoms that the original constraints imply must be true.
0029   /// Simplification replaces all occurrences of these atoms by a true literal
0030   /// (which may enable additional simplifications).
0031   llvm::SmallVector<Atom> TrueAtoms;
0032   /// Atoms that the original constraints imply must be false.
0033   /// Simplification replaces all occurrences of these atoms by a false literal
0034   /// (which may enable additional simplifications).
0035   llvm::SmallVector<Atom> FalseAtoms;
0036 };
0037
0038 /// Simplifies a set of constraints (implicitly connected by "and") in a way
0039 /// that does not change satisfiability of the constraints. This does _not_ mean
0040 /// that the set of solutions is the same before and after simplification.
0041 /// `Info`, if non-null, will be populated with information about the
0042 /// simplifications that were made to the formula (e.g. to display to the user).
0043 void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
0044                          Arena &arena, SimplifyConstraintsInfo *Info = nullptr);
0045
0046 } // namespace dataflow
0047 } // namespace clang
0048
0049 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H