| //===- Solver.h -------------------------------------------------*- C++ -*-===// |
| // |
| // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
| // See https://llvm.org/LICENSE.txt for license information. |
| // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
| // |
| //===----------------------------------------------------------------------===// |
| // |
| // This file defines an interface for a SAT solver that can be used by |
| // dataflow analyses. |
| // |
| //===----------------------------------------------------------------------===// |
| |
| #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H |
| #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H |
| |
| #include "clang/Analysis/FlowSensitive/Value.h" |
| #include "llvm/ADT/DenseSet.h" |
| |
| namespace clang { |
| namespace dataflow { |
| |
| /// An interface for a SAT solver that can be used by dataflow analyses. |
| class Solver { |
| public: |
| enum class Result { |
| /// Indicates that there exists a satisfying assignment for a boolean |
| /// formula. |
| Satisfiable, |
| |
| /// Indicates that there is no satisfying assignment for a boolean formula. |
| Unsatisfiable, |
| |
| /// Indicates that the solver gave up trying to find a satisfying assignment |
| /// for a boolean formula. |
| TimedOut, |
| }; |
| |
| virtual ~Solver() = default; |
| |
| /// Checks if the conjunction of `Vals` is satisfiable and returns the |
| /// corresponding result. |
| /// |
| /// Requirements: |
| /// |
| /// All elements in `Vals` must not be null. |
| /// |
| /// FIXME: Consider returning a model in case the conjunction of `Vals` is |
| /// satisfiable so that it can be used to generate warning messages. |
| virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0; |
| }; |
| |
| } // namespace dataflow |
| } // namespace clang |
| |
| #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H |