================ @@ -0,0 +1,180 @@ +//===- 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 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 negative literal `!V`. +inline constexpr Literal negLit(Variable V) { return 2 * V + 1; } ---------------- martinboehme wrote:
Good point -- done! https://github.com/llvm/llvm-project/pull/92401 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
