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/Formula.h" |
18 | #include "clang/Basic/LLVM.h" |
19 | #include "llvm/ADT/ArrayRef.h" |
20 | #include "llvm/ADT/DenseMap.h" |
21 | #include <optional> |
22 | #include <vector> |
23 | |
24 | namespace clang { |
25 | namespace dataflow { |
26 | |
27 | /// An interface for a SAT solver that can be used by dataflow analyses. |
28 | class Solver { |
29 | public: |
30 | struct Result { |
31 | enum class Status { |
32 | /// Indicates that there exists a satisfying assignment for a boolean |
33 | /// formula. |
34 | Satisfiable, |
35 | |
36 | /// Indicates that there is no satisfying assignment for a boolean |
37 | /// formula. |
38 | Unsatisfiable, |
39 | |
40 | /// Indicates that the solver gave up trying to find a satisfying |
41 | /// assignment for a boolean formula. |
42 | TimedOut, |
43 | }; |
44 | |
45 | /// A boolean value is set to true or false in a truth assignment. |
46 | enum class Assignment : uint8_t { AssignedFalse = 0, AssignedTrue = 1 }; |
47 | |
48 | /// Constructs a result indicating that the queried boolean formula is |
49 | /// satisfiable. The result will hold a solution found by the solver. |
50 | static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) { |
51 | return Result(Status::Satisfiable, std::move(Solution)); |
52 | } |
53 | |
54 | /// Constructs a result indicating that the queried boolean formula is |
55 | /// unsatisfiable. |
56 | static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); } |
57 | |
58 | /// Constructs a result indicating that satisfiability checking on the |
59 | /// queried boolean formula was not completed. |
60 | static Result TimedOut() { return Result(Status::TimedOut, {}); } |
61 | |
62 | /// Returns the status of satisfiability checking on the queried boolean |
63 | /// formula. |
64 | Status getStatus() const { return SATCheckStatus; } |
65 | |
66 | /// Returns a truth assignment to boolean values that satisfies the queried |
67 | /// boolean formula if available. Otherwise, an empty optional is returned. |
68 | std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const { |
69 | return Solution; |
70 | } |
71 | |
72 | private: |
73 | Result(Status SATCheckStatus, |
74 | std::optional<llvm::DenseMap<Atom, Assignment>> Solution) |
75 | : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {} |
76 | |
77 | Status SATCheckStatus; |
78 | std::optional<llvm::DenseMap<Atom, Assignment>> Solution; |
79 | }; |
80 | |
81 | virtual ~Solver() = default; |
82 | |
83 | /// Checks if the conjunction of `Vals` is satisfiable and returns the |
84 | /// corresponding result. |
85 | /// |
86 | /// Requirements: |
87 | /// |
88 | /// All elements in `Vals` must not be null. |
89 | virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0; |
90 | }; |
91 | |
92 | llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &); |
93 | llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment); |
94 | |
95 | } // namespace dataflow |
96 | } // namespace clang |
97 | |
98 | #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H |
99 | |