Analysis/FlowSensitive/WatchedLiteralsSolver.h

0001 //===- WatchedLiteralsSolver.h ----------------------------------*- C++ -*-===//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 //
0009 //  This file defines a SAT solver implementation that can be used by dataflow
0010 //  analyses.
0011 //
0012 //===----------------------------------------------------------------------===//
0013
0014 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
0015 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
0016
0017 #include "clang/Analysis/FlowSensitive/Formula.h"
0018 #include "clang/Analysis/FlowSensitive/Solver.h"
0019 #include "llvm/ADT/ArrayRef.h"
0020
0021 namespace clang {
0022 namespace dataflow {
0023
0024 /// A SAT solver that is an implementation of Algorithm D from Knuth's The Art
0025 /// of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is based on
0026 /// the Davis-Putnam-Logemann-Loveland (DPLL) algorithm [1], keeps references to
0027 /// a single "watched" literal per clause, and uses a set of "active" variables
0028 /// for unit propagation.
0029 //
0030 // [1] https://en.wikipedia.org/wiki/DPLL_algorithm
0031 class WatchedLiteralsSolver : public Solver {
0032   // Count of the iterations of the main loop of the solver. This spans *all*
0033   // calls to the underlying solver across the life of this object. It is
0034   // reduced with every (non-trivial) call to the solver.
0035   //
0036   // We give control over the abstract count of iterations instead of concrete
0037   // measurements like CPU cycles or time to ensure deterministic results.
0038   std::int64_t MaxIterations = std::numeric_limits<std::int64_t>::max();
0039
0040 public:
0041   WatchedLiteralsSolver() = default;
0042
0043   // `Work` specifies a computational limit on the solver. Units of "work"
0044   // roughly correspond to attempts to assign a value to a single
0045   // variable. Since the algorithm is exponential in the number of variables,
0046   // this is the most direct (abstract) unit to target.
0047   explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
0048       : MaxIterations(WorkLimit) {}
0049
0050   Result solve(llvm::ArrayRef<const Formula *> Vals) override;
0051
0052   bool reachedLimit() const override { return MaxIterations == 0; }
0053 };
0054
0055 } // namespace dataflow
0056 } // namespace clang
0057
0058 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H