1 | //===- WatchedLiteralsSolver.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 | // This file defines a SAT solver implementation that can be used by dataflow |
10 | // analyses. |
11 | // |
12 | //===----------------------------------------------------------------------===// |
13 | |
14 | #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H |
15 | #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H |
16 | |
17 | #include "clang/Analysis/FlowSensitive/Formula.h" |
18 | #include "clang/Analysis/FlowSensitive/Solver.h" |
19 | #include "llvm/ADT/ArrayRef.h" |
20 | #include <limits> |
21 | |
22 | namespace clang { |
23 | namespace dataflow { |
24 | |
25 | /// A SAT solver that is an implementation of Algorithm D from Knuth's The Art |
26 | /// of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is based on |
27 | /// the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, keeps references to a |
28 | /// single "watched" literal per clause, and uses a set of "active" variables |
29 | /// for unit propagation. |
30 | class WatchedLiteralsSolver : public Solver { |
31 | // Count of the iterations of the main loop of the solver. This spans *all* |
32 | // calls to the underlying solver across the life of this object. It is |
33 | // reduced with every (non-trivial) call to the solver. |
34 | // |
35 | // We give control over the abstract count of iterations instead of concrete |
36 | // measurements like CPU cycles or time to ensure deterministic results. |
37 | std::int64_t MaxIterations = std::numeric_limits<std::int64_t>::max(); |
38 | |
39 | public: |
40 | WatchedLiteralsSolver() = default; |
41 | |
42 | // `Work` specifies a computational limit on the solver. Units of "work" |
43 | // roughly correspond to attempts to assign a value to a single |
44 | // variable. Since the algorithm is exponential in the number of variables, |
45 | // this is the most direct (abstract) unit to target. |
46 | explicit WatchedLiteralsSolver(std::int64_t WorkLimit) |
47 | : MaxIterations(WorkLimit) {} |
48 | |
49 | Result solve(llvm::ArrayRef<const Formula *> Vals) override; |
50 | |
51 | // The solver reached its maximum number of iterations. |
52 | bool reachedLimit() const { return MaxIterations == 0; } |
53 | }; |
54 | |
55 | } // namespace dataflow |
56 | } // namespace clang |
57 | |
58 | #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H |
59 | |