Unverified Commit 37813e09 authored by martinboehme's avatar martinboehme Committed by GitHub
Browse files

[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.
parent 352dc7d4
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment