clang 17.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 <optional>
21
22namespace clang {
23namespace dataflow {
24
25/// An interface for a SAT solver that can be used by dataflow analyses.
26class Solver {
27public:
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.
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.
67 std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
68 getSolution() const {
69 return Solution;
70 }
71
72 private:
73 Result(
74 enum Status SATCheckStatus,
75 std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
76 : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
77
78 Status SATCheckStatus;
79 std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
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.
91};
92
93} // namespace dataflow
94} // namespace clang
95
96#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
An interface for a SAT solver that can be used by dataflow analyses.
Definition: Solver.h:26
virtual ~Solver()=default
virtual Result solve(llvm::DenseSet< BoolValue * > Vals)=0
Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
Definition: Format.h:4664
static Result Satisfiable(llvm::DenseMap< AtomicBoolValue *, Assignment > Solution)
Constructs a result indicating that the queried boolean formula is satisfiable.
Definition: Solver.h:49
static Result TimedOut()
Constructs a result indicating that satisfiability checking on the queried boolean formula was not co...
Definition: Solver.h:59
std::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
Status getStatus() const
Returns the status of satisfiability checking on the queried boolean formula.
Definition: Solver.h:63
static Result Unsatisfiable()
Constructs a result indicating that the queried boolean formula is unsatisfiable.
Definition: Solver.h:55
Assignment
A boolean value is set to true or false in a truth assignment.
Definition: Solver.h:44
@ TimedOut
Indicates that the solver gave up trying to find a satisfying assignment for a boolean formula.
@ Unsatisfiable
Indicates that there is no satisfying assignment for a boolean formula.
@ Satisfiable
Indicates that there exists a satisfying assignment for a boolean formula.