EIC code displayed by LXR master/​include/​clang/​Analysis/​FlowSensitive/​CNFFormula.h	Source navigation Diff markup Identifier search General search
	Version: master test Revert   Change

File indexing completed on 2026-05-10 08:36:24

 //===- 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.
 using Variable = uint32_t;
 
 /// A null boolean variable is used as a placeholder in various data structures
 /// and algorithms.
 constexpr Variable NullVar = 0;
 
 /// 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`.
 using Literal = uint32_t;
 
 /// A null literal is used as a placeholder in various data structures and
 /// algorithms.
 constexpr Literal NullLit = 0;
 
 /// Clause identifiers are represented as positive integers.
 using ClauseID = uint32_t;
 
 /// A null clause identifier is used as a placeholder in various data structures
 /// and algorithms.
 constexpr ClauseID NullClause = 0;
 
 /// Returns the positive literal `V`.
 inline constexpr Literal posLit(Variable V) { return 2 * V; }
 
 /// Returns the negative literal `!V`.
 inline constexpr Literal negLit(Variable V) { return 2 * V + 1; }
 
 /// Returns whether `L` is a positive literal.
 inline constexpr bool isPosLit(Literal L) { return 0 == (L & 1); }
 
 /// Returns whether `L` is a negative literal.
 inline constexpr bool isNegLit(Literal L) { return 1 == (L & 1); }
 
 /// Returns the negated literal `!L`.
 inline constexpr Literal notLit(Literal L) { return L ^ 1; }
 
 /// Returns the variable of `L`.
 inline constexpr Variable var(Literal L) { return L >> 1; }
 
 /// A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals
 /// per clause).
 class CNFFormula {
   /// `LargestVar` is equal to the largest positive integer that represents a
   /// variable in the formula.
   const Variable LargestVar;
 
   /// Literals of all clauses in the formula.
   ///
   /// The element at index 0 stands for the literal in the null clause. It is
   /// set to 0 and isn't used. Literals of clauses in the formula start from the
   /// element at index 1.
   ///
   /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
   /// `Clauses` will be `[0, L1, L2, L2, L3, L4]`.
   std::vector<Literal> Clauses;
 
   /// Start indices of clauses of the formula in `Clauses`.
   ///
   /// The element at index 0 stands for the start index of the null clause. It
   /// is set to 0 and isn't used. Start indices of clauses in the formula start
   /// from the element at index 1.
   ///
   /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
   /// `ClauseStarts` will be `[0, 1, 3]`. Note that the literals of the first
   /// clause always start at index 1. The start index for the literals of the
   /// second clause depends on the size of the first clause and so on.
   std::vector<size_t> ClauseStarts;
 
   /// Indicates that we already know the formula is unsatisfiable.
   /// During construction, we catch simple cases of conflicting unit-clauses.
   bool KnownContradictory;
 
 public:
   explicit CNFFormula(Variable LargestVar);
 
   /// Adds the `L1 v ... v Ln` clause to the formula.
   /// Requirements:
   ///
   ///  `Li` must not be `NullLit`.
   ///
   ///  All literals in the input that are not `NullLit` must be distinct.
   void addClause(ArrayRef<Literal> lits);
 
   /// Returns whether the formula is known to be contradictory.
   /// This is the case if any of the clauses is empty.
   bool knownContradictory() const { return KnownContradictory; }
 
   /// Returns the largest variable in the formula.
   Variable largestVar() const { return LargestVar; }
 
   /// Returns the number of clauses in the formula.
   /// Valid clause IDs are in the range [1, `numClauses()`].
   ClauseID numClauses() const { return ClauseStarts.size() - 1; }
 
   /// Returns the number of literals in clause `C`.
   size_t clauseSize(ClauseID C) const {
     return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
                                         : ClauseStarts[C + 1] - ClauseStarts[C];
   }
 
   /// Returns the literals of clause `C`.
   /// If `knownContradictory()` is false, each clause has at least one literal.
   llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const {
     size_t S = clauseSize(C);
     if (S == 0)
       return llvm::ArrayRef<Literal>();
     return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], S);
   }
 
   /// An iterator over all literals of all clauses in the formula.
   /// The iterator allows mutation of the literal through the `*` operator.
   /// This is to support solvers that mutate the formula during solving.
   class Iterator {
     friend class CNFFormula;
     CNFFormula *CNF;
     size_t Idx;
     Iterator(CNFFormula *CNF, size_t Idx) : CNF(CNF), Idx(Idx) {}
 
   public:
     Iterator(const Iterator &) = default;
     Iterator &operator=(const Iterator &) = default;
 
     Iterator &operator++() {
       ++Idx;
       assert(Idx < CNF->Clauses.size() && "Iterator out of bounds");
       return *this;
     }
 
     Iterator next() const {
       Iterator I = *this;
       ++I;
       return I;
     }
 
     Literal &operator*() const { return CNF->Clauses[Idx]; }
   };
   friend class Iterator;
 
   /// Returns an iterator to the first literal of clause `C`.
   Iterator startOfClause(ClauseID C) { return Iterator(this, ClauseStarts[C]); }
 };
 
 /// 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

This page was automatically generated by the 2.3.7 LXR engine. The LXR team