/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/include/clang/Analysis/FlowSensitive/Solver.h
Line | Count | Source |
1 | | //===- Solver.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 an interface for a SAT solver that can be used by |
10 | | // dataflow analyses. |
11 | | // |
12 | | //===----------------------------------------------------------------------===// |
13 | | |
14 | | #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H |
15 | | #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H |
16 | | |
17 | | #include "clang/Analysis/FlowSensitive/Value.h" |
18 | | #include "llvm/ADT/DenseSet.h" |
19 | | |
20 | | namespace clang { |
21 | | namespace dataflow { |
22 | | |
23 | | /// An interface for a SAT solver that can be used by dataflow analyses. |
24 | | class Solver { |
25 | | public: |
26 | | enum class Result { |
27 | | /// Indicates that there exists a satisfying assignment for a boolean |
28 | | /// formula. |
29 | | Satisfiable, |
30 | | |
31 | | /// Indicates that there is no satisfying assignment for a boolean formula. |
32 | | Unsatisfiable, |
33 | | |
34 | | /// Indicates that the solver gave up trying to find a satisfying assignment |
35 | | /// for a boolean formula. |
36 | | TimedOut, |
37 | | }; |
38 | | |
39 | 332 | virtual ~Solver() = default; |
40 | | |
41 | | /// Checks if the conjunction of `Vals` is satisfiable and returns the |
42 | | /// corresponding result. |
43 | | /// |
44 | | /// Requirements: |
45 | | /// |
46 | | /// All elements in `Vals` must not be null. |
47 | | /// |
48 | | /// FIXME: Consider returning a model in case the conjunction of `Vals` is |
49 | | /// satisfiable so that it can be used to generate warning messages. |
50 | | virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0; |
51 | | }; |
52 | | |
53 | | } // namespace dataflow |
54 | | } // namespace clang |
55 | | |
56 | | #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H |