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