LLZK 3.0.0
An open-source IR for Zero Knowledge (ZK) circuits
Loading...
Searching...
No Matches
SMTInfoDetail.h
Go to the documentation of this file.
1//===-- SMTInfoDetail.h - SMT metadata implementation helpers --*- C++ -*-===//
2//
3// Part of the LLZK Project, under the Apache License v2.0.
4// See LICENSE.txt for license information.
5// Copyright 2026 Project LLZK
6// SPDX-License-Identifier: Apache-2.0
7//
8//===----------------------------------------------------------------------===//
9
10#pragma once
11
12#include <mlir/IR/Attributes.h>
13#include <mlir/IR/Diagnostics.h>
14
15namespace llzk::smt_info::detail {
16
19mlir::Attribute getKeywordAttr(mlir::MLIRContext *context, llvm::StringRef value);
20
23mlir::Attribute getSymbolAttr(mlir::MLIRContext *context, llvm::StringRef value);
24
27mlir::LogicalResult
28verifyKeyword(llvm::function_ref<mlir::InFlightDiagnostic()> emitError, llvm::StringRef value);
29
30} // namespace llzk::smt_info::detail
llzk::smt_info::detail
Definition SMTInfoDetail.h:15
llzk::smt_info::detail::getSymbolAttr
mlir::Attribute getSymbolAttr(mlir::MLIRContext *context, llvm::StringRef value)
Creates a symbol attribute without exposing generated attribute storage to operation implementation f...
llzk::smt_info::detail::getKeywordAttr
mlir::Attribute getKeywordAttr(mlir::MLIRContext *context, llvm::StringRef value)
Creates a keyword attribute without exposing generated attribute storage to operation implementation ...
llzk::smt_info::detail::verifyKeyword
mlir::LogicalResult verifyKeyword(llvm::function_ref< mlir::InFlightDiagnostic()> emitError, llvm::StringRef value)
Verifies that value is a valid SMT-LIB keyword and reports failures through emitError.