clang 20.0.0git
Classes | Namespaces | Typedefs | Functions | Variables
CNFFormula.h File Reference
#include <cstdint>
#include <vector>
#include "clang/Analysis/FlowSensitive/Formula.h"

Go to the source code of this file.

Classes

class  clang::dataflow::CNFFormula
 A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals per clause). More...
 
class  clang::dataflow::CNFFormula::Iterator
 An iterator over all literals of all clauses in the formula. More...
 

Namespaces

namespace  clang
 The JSON file list parser is used to communicate input to InstallAPI.
 
namespace  clang::dataflow
 Dataflow Directional Tag Classes.
 

Typedefs

using clang::dataflow::Variable = uint32_t
 Boolean variables are represented as positive integers.
 
using clang::dataflow::Literal = uint32_t
 Literals are represented as positive integers.
 
using clang::dataflow::ClauseID = uint32_t
 Clause identifiers are represented as positive integers.
 

Functions

constexpr Literal clang::dataflow::posLit (Variable V)
 Returns the positive literal V.
 
constexpr Literal clang::dataflow::negLit (Variable V)
 Returns the negative literal !V.
 
constexpr bool clang::dataflow::isPosLit (Literal L)
 Returns whether L is a positive literal.
 
constexpr bool clang::dataflow::isNegLit (Literal L)
 Returns whether L is a negative literal.
 
constexpr Literal clang::dataflow::notLit (Literal L)
 Returns the negated literal !L.
 
constexpr Variable clang::dataflow::var (Literal L)
 Returns the variable of L.
 
CNFFormula clang::dataflow::buildCNF (const llvm::ArrayRef< const Formula * > &Formulas, llvm::DenseMap< Variable, Atom > &Atomics)
 Converts the conjunction of Vals into a formula in conjunctive normal form where each clause has at least one and at most three literals.
 

Variables

constexpr Variable clang::dataflow::NullVar = 0
 A null boolean variable is used as a placeholder in various data structures and algorithms.
 
constexpr Literal clang::dataflow::NullLit = 0
 A null literal is used as a placeholder in various data structures and algorithms.
 
constexpr ClauseID clang::dataflow::NullClause = 0
 A null clause identifier is used as a placeholder in various data structures and algorithms.