clang 19.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 "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.
35
36 /// Indicates that there is no satisfying assignment for a boolean
37 /// formula.
39
40 /// Indicates that the solver gave up trying to find a satisfying
41 /// assignment for a boolean formula.
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.
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.
90
91 // Did the solver reach its resource limit?
92 virtual bool reachedLimit() const = 0;
93};
94
95llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
96llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
97
98} // namespace dataflow
99} // namespace clang
100
101#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.
An interface for a SAT solver that can be used by dataflow analyses.
Definition: Solver.h:28
virtual ~Solver()=default
virtual Result solve(llvm::ArrayRef< const Formula * > Vals)=0
Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
virtual bool reachedLimit() const =0
llvm::raw_ostream & operator<<(llvm::raw_ostream &OS, Atom A)
Definition: Formula.h:125
The JSON file list parser is used to communicate input to InstallAPI.
Definition: Format.h:5427
static Result TimedOut()
Constructs a result indicating that satisfiability checking on the queried boolean formula was not co...
Definition: Solver.h:60
Status getStatus() const
Returns the status of satisfiability checking on the queried boolean formula.
Definition: Solver.h:64
static Result Unsatisfiable()
Constructs a result indicating that the queried boolean formula is unsatisfiable.
Definition: Solver.h:56
std::optional< llvm::DenseMap< Atom, Assignment > > getSolution() const
Returns a truth assignment to boolean values that satisfies the queried boolean formula if available.
Definition: Solver.h:68
Assignment
A boolean value is set to true or false in a truth assignment.
Definition: Solver.h:46
static Result Satisfiable(llvm::DenseMap< Atom, Assignment > Solution)
Constructs a result indicating that the queried boolean formula is satisfiable.
Definition: Solver.h:50
@ 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.