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

source code of clang/include/clang/Analysis/FlowSensitive/Solver.h