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