[all-commits] [llvm/llvm-project] 37813e: [clang][dataflow] Make `CNFFormula` externally acc...

[martinboehme via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 37813e09fa8b67ec858ad3c82dcf72a8ff306b03
      https://github.com/llvm/llvm-project/commit/37813e09fa8b67ec858ad3c82dcf72a8ff306b03
  Author: martinboehme <mboehme at google.com>
  Date:   2024-05-21 (Tue, 21 May 2024)

  Changed paths:
    M clang/docs/tools/clang-formatted-files.txt
    A clang/include/clang/Analysis/FlowSensitive/CNFFormula.h
    M clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
    M clang/lib/Analysis/FlowSensitive/CMakeLists.txt
    A clang/lib/Analysis/FlowSensitive/CNFFormula.cpp
    M clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
    M llvm/utils/gn/secondary/clang/lib/Analysis/FlowSensitive/BUILD.gn

  Log Message:
  -----------
  [clang][dataflow] Make `CNFFormula` externally accessible. (#92401)

This component can be useful when creating implementations of `Solver`,
as some
SAT solvers require the input to be in 3-CNF.

As part of making `CNFFormula` externally accessible, I have moved some
member
variables out of it that aren't really part of the representation of a
3-CNF
formula and thus live better elsewhere:

*  `WatchedHead` and `NextWatched` have been moved to
`WatchedLiteralsSolverImpl`, as they're part of the specific algorithm
used
   by that SAT solver.

* `Atomics` has become an output parameter of `buildCNF()` because it
has to do
with the relationship between a `CNFFormula` and the set of `Formula`s
it is
derived from rather than being an integral part of the representation of
a
   3-CNF formula.

I have also made all member variables private and added appropriate
accessors.



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications