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 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 57