llvm/clang/lib/Analysis/FlowSensitive/CNFFormula.cpp

//===- CNFFormula.cpp -------------------------------------------*- 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.
//
//===----------------------------------------------------------------------===//

#include "clang/Analysis/FlowSensitive/CNFFormula.h"
#include "llvm/ADT/DenseSet.h"

#include <queue>

namespace clang {
namespace dataflow {

namespace {

/// Applies simplifications while building up a BooleanFormula.
/// We keep track of unit clauses, which tell us variables that must be
/// true/false in any model that satisfies the overall formula.
/// Such variables can be dropped from subsequently-added clauses, which
/// may in turn yield more unit clauses or even a contradiction.
/// The total added complexity of this preprocessing is O(N) where we
/// for every clause, we do a lookup for each unit clauses.
/// The lookup is O(1) on average. This method won't catch all
/// contradictory formulas, more passes can in principle catch
/// more cases but we leave all these and the general case to the
/// proper SAT solver.
struct CNFFormulaBuilder { … };

} // namespace

CNFFormula::CNFFormula(Variable LargestVar)
    : … { … }

void CNFFormula::addClause(ArrayRef<Literal> lits) { … }

CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Formulas,
                    llvm::DenseMap<Variable, Atom> &Atomics) { … }

} // namespace dataflow
} // namespace clang