llvm/clang/include/clang/Analysis/FlowSensitive/CNFFormula.h

//===- CNFFormula.h ---------------------------------------------*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
//
//  A representation of a boolean formula in 3-CNF.
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_CNFFORMULA_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_CNFFORMULA_H

#include <cstdint>
#include <vector>

#include "clang/Analysis/FlowSensitive/Formula.h"

namespace clang {
namespace dataflow {

/// Boolean variables are represented as positive integers.
Variable;

/// A null boolean variable is used as a placeholder in various data structures
/// and algorithms.
constexpr Variable NullVar = …;

/// Literals are represented as positive integers. Specifically, for a boolean
/// variable `V` that is represented as the positive integer `I`, the positive
/// literal `V` is represented as the integer `2*I` and the negative literal
/// `!V` is represented as the integer `2*I+1`.
Literal;

/// A null literal is used as a placeholder in various data structures and
/// algorithms.
constexpr Literal NullLit = …;

/// Clause identifiers are represented as positive integers.
ClauseID;

/// A null clause identifier is used as a placeholder in various data structures
/// and algorithms.
constexpr ClauseID NullClause = …;

/// Returns the positive literal `V`.
inline constexpr Literal posLit(Variable V) { … }

/// Returns the negative literal `!V`.
inline constexpr Literal negLit(Variable V) { … }

/// Returns whether `L` is a positive literal.
inline constexpr bool isPosLit(Literal L) { … }

/// Returns whether `L` is a negative literal.
inline constexpr bool isNegLit(Literal L) { … }

/// Returns the negated literal `!L`.
inline constexpr Literal notLit(Literal L) { … }

/// Returns the variable of `L`.
inline constexpr Variable var(Literal L) { … }

/// A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals
/// per clause).
class CNFFormula { … };

/// Converts the conjunction of `Vals` into a formula in conjunctive normal
/// form where each clause has at least one and at most three literals.
/// `Atomics` is populated with a mapping from `Variables` to the corresponding
/// `Atom`s for atomic booleans in the input formulas.
CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Formulas,
                    llvm::DenseMap<Variable, Atom> &Atomics);

} // namespace dataflow
} // namespace clang

#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_CNFFORMULA_H