Coverage Report

Created: 2022-05-21 09:15

/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