[clang] [llvm] [clang][dataflow] Make `CNFFormula` externally accessible. (PR #92401)

via llvm-commits llvm-commits at lists.llvm.org
Thu May 16 07:11:40 PDT 2024


github-actions[bot] wrote:

<!--LLVM CODE FORMAT COMMENT: {clang-format}-->


:warning: C/C++ code formatter, clang-format found issues in your code. :warning:

<details>
<summary>
You can test this locally with the following command:
</summary>

``````````bash
git-clang-format --diff f89b1b8a68065c4b880417abb0563bce21399b52 e902cf2e18208a118f90c341d3e375d2c20cdc59 -- clang/include/clang/Analysis/FlowSensitive/CNFFormula.h clang/lib/Analysis/FlowSensitive/CNFFormula.cpp clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
``````````

</details>

<details>
<summary>
View the diff from clang-format here.
</summary>

``````````diff
diff --git a/clang/include/clang/Analysis/FlowSensitive/CNFFormula.h b/clang/include/clang/Analysis/FlowSensitive/CNFFormula.h
index 90b0c591b5..850ca66918 100644
--- a/clang/include/clang/Analysis/FlowSensitive/CNFFormula.h
+++ b/clang/include/clang/Analysis/FlowSensitive/CNFFormula.h
@@ -170,9 +170,8 @@ public:
 /// form where each clause has at least one and at most three literals.
 /// `Atomics` is populated with a mapping from `Variables` to the corresponding
 /// `Atom`s for atomic booleans in the input formulas.
-CNFFormula
-buildCNF(const llvm::ArrayRef<const Formula *> &Formulas,
-         llvm::DenseMap<Variable, Atom> &Atomics);
+CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Formulas,
+                    llvm::DenseMap<Variable, Atom> &Atomics);
 
 } // namespace dataflow
 } // namespace clang
diff --git a/clang/lib/Analysis/FlowSensitive/CNFFormula.cpp b/clang/lib/Analysis/FlowSensitive/CNFFormula.cpp
index 521b81fe78..2410ce1e7b 100644
--- a/clang/lib/Analysis/FlowSensitive/CNFFormula.cpp
+++ b/clang/lib/Analysis/FlowSensitive/CNFFormula.cpp
@@ -33,8 +33,7 @@ namespace {
 /// proper SAT solver.
 struct CNFFormulaBuilder {
   // Formula should outlive CNFFormulaBuilder.
-  explicit CNFFormulaBuilder(CNFFormula &CNF)
-      : Formula(CNF) {}
+  explicit CNFFormulaBuilder(CNFFormula &CNF) : Formula(CNF) {}
 
   /// Adds the `L1 v ... v Ln` clause to the formula. Applies
   /// simplifications, based on single-literal clauses.
@@ -51,8 +50,7 @@ struct CNFFormulaBuilder {
     llvm::SmallVector<Literal> Simplified;
     for (auto L : Literals) {
       assert(L != NullLit &&
-             llvm::all_of(Simplified,
-                          [L](Literal S) { return  S != L; }));
+             llvm::all_of(Simplified, [L](Literal S) { return S != L; }));
       auto X = var(L);
       if (trueVars.contains(X)) { // X must be true
         if (isPosLit(L))

``````````

</details>


https://github.com/llvm/llvm-project/pull/92401


More information about the llvm-commits mailing list