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 
24 namespace clang {
25 namespace dataflow {
26 
27 /// An interface for a SAT solver that can be used by dataflow analyses.
28 class Solver {
29 public:
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.
SatisfiableResult50     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.
UnsatisfiableResult56     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.
TimedOutResult60     static Result TimedOut() { return Result(Status::TimedOut, {}); }
61 
62     /// Returns the status of satisfiability checking on the queried boolean
63     /// formula.
getStatusResult64     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.
getSolutionResult68     std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
69       return Solution;
70     }
71 
72   private:
ResultResult73     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 
92 llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
93 llvm::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