LLZK 2.0.0
An open-source IR for Zero Knowledge (ZK) circuits
Loading...
Searching...
No Matches
Namespaces | Classes | Enumerations | Functions
llzk::smt Namespace Reference

Namespaces

namespace  detail

Classes

class  AndOp
class  AndOpAdaptor
class  AndOpGenericAdaptor
class  ApplyFuncOp
class  ApplyFuncOpAdaptor
class  ApplyFuncOpGenericAdaptor
class  ArrayBroadcastOp
class  ArrayBroadcastOpAdaptor
class  ArrayBroadcastOpGenericAdaptor
class  ArraySelectOp
class  ArraySelectOpAdaptor
class  ArraySelectOpGenericAdaptor
class  ArrayStoreOp
class  ArrayStoreOpAdaptor
class  ArrayStoreOpGenericAdaptor
class  ArrayType
class  AssertOp
class  AssertOpAdaptor
class  AssertOpGenericAdaptor
class  BitVectorType
class  BoolConstantOp
class  BoolConstantOpAdaptor
class  BoolConstantOpGenericAdaptor
class  BoolType
class  BV2IntOp
class  BV2IntOpAdaptor
class  BV2IntOpGenericAdaptor
class  BVAddOp
class  BVAddOpAdaptor
class  BVAddOpGenericAdaptor
class  BVAndOp
class  BVAndOpAdaptor
class  BVAndOpGenericAdaptor
class  BVAShrOp
class  BVAShrOpAdaptor
class  BVAShrOpGenericAdaptor
class  BVCmpOp
class  BVCmpOpAdaptor
class  BVCmpOpGenericAdaptor
class  BVCmpPredicateAttr
class  BVConstantOp
class  BVConstantOpAdaptor
class  BVConstantOpGenericAdaptor
class  BVLShrOp
class  BVLShrOpAdaptor
class  BVLShrOpGenericAdaptor
class  BVMulOp
class  BVMulOpAdaptor
class  BVMulOpGenericAdaptor
class  BVNegOp
class  BVNegOpAdaptor
class  BVNegOpGenericAdaptor
class  BVNotOp
class  BVNotOpAdaptor
class  BVNotOpGenericAdaptor
class  BVOrOp
class  BVOrOpAdaptor
class  BVOrOpGenericAdaptor
class  BVSDivOp
class  BVSDivOpAdaptor
class  BVSDivOpGenericAdaptor
class  BVShlOp
class  BVShlOpAdaptor
class  BVShlOpGenericAdaptor
class  BVSModOp
class  BVSModOpAdaptor
class  BVSModOpGenericAdaptor
class  BVSRemOp
class  BVSRemOpAdaptor
class  BVSRemOpGenericAdaptor
class  BVUDivOp
class  BVUDivOpAdaptor
class  BVUDivOpGenericAdaptor
class  BVURemOp
class  BVURemOpAdaptor
class  BVURemOpGenericAdaptor
class  BVXOrOp
class  BVXOrOpAdaptor
class  BVXOrOpGenericAdaptor
class  CheckOp
class  CheckOpAdaptor
class  CheckOpGenericAdaptor
class  ConcatOp
class  ConcatOpAdaptor
class  ConcatOpGenericAdaptor
class  DeclareFunOp
class  DeclareFunOpAdaptor
class  DeclareFunOpGenericAdaptor
class  DistinctOp
class  DistinctOpAdaptor
class  DistinctOpGenericAdaptor
class  EqOp
class  EqOpAdaptor
class  EqOpGenericAdaptor
class  ExistsOp
class  ExistsOpAdaptor
class  ExistsOpGenericAdaptor
class  ExtractOp
class  ExtractOpAdaptor
class  ExtractOpGenericAdaptor
class  ForallOp
class  ForallOpAdaptor
class  ForallOpGenericAdaptor
class  ImpliesOp
class  ImpliesOpAdaptor
class  ImpliesOpGenericAdaptor
class  Int2BVOp
class  Int2BVOpAdaptor
class  Int2BVOpGenericAdaptor
class  IntAbsOp
class  IntAbsOpAdaptor
class  IntAbsOpGenericAdaptor
class  IntAddOp
class  IntAddOpAdaptor
class  IntAddOpGenericAdaptor
class  IntCmpOp
class  IntCmpOpAdaptor
class  IntCmpOpGenericAdaptor
class  IntConstantOp
class  IntConstantOpAdaptor
class  IntConstantOpGenericAdaptor
class  IntDivOp
class  IntDivOpAdaptor
class  IntDivOpGenericAdaptor
class  IntModOp
class  IntModOpAdaptor
class  IntModOpGenericAdaptor
class  IntMulOp
class  IntMulOpAdaptor
class  IntMulOpGenericAdaptor
class  IntNegOp
class  IntNegOpAdaptor
class  IntNegOpGenericAdaptor
class  IntPredicateAttr
class  IntSubOp
class  IntSubOpAdaptor
class  IntSubOpGenericAdaptor
class  IntType
class  IteOp
class  IteOpAdaptor
class  IteOpGenericAdaptor
class  NotOp
class  NotOpAdaptor
class  NotOpGenericAdaptor
class  OrOp
class  OrOpAdaptor
class  OrOpGenericAdaptor
class  PopOp
class  PopOpAdaptor
class  PopOpGenericAdaptor
class  PushOp
class  PushOpAdaptor
class  PushOpGenericAdaptor
class  RepeatOp
class  RepeatOpAdaptor
class  RepeatOpGenericAdaptor
class  ResetOp
class  ResetOpAdaptor
class  ResetOpGenericAdaptor
class  SetLogicOp
class  SetLogicOpAdaptor
class  SetLogicOpGenericAdaptor
class  SMTDialect
class  SMTFuncType
class  SMTOpVisitor
 This helps visit SMT nodes. More...
class  SMTTypeVisitor
 This helps visit SMT types. More...
class  SolverOp
class  SolverOpAdaptor
class  SolverOpGenericAdaptor
class  SortType
class  XOrOp
class  XOrOpAdaptor
class  XOrOpGenericAdaptor
class  YieldOp
class  YieldOpAdaptor
class  YieldOpGenericAdaptor

Enumerations

enum class  BVCmpPredicate : uint64_t {
  slt = 0 , sle = 1 , sgt = 2 , sge = 3 ,
  ult = 4 , ule = 5 , ugt = 6 , uge = 7
}
enum class  IntPredicate : uint64_t { lt = 0 , le = 1 , gt = 2 , ge = 3 }

Functions

::llvm::StringRef stringifyBVCmpPredicate (BVCmpPredicate val)
::std::optional< BVCmpPredicate > symbolizeBVCmpPredicate (::llvm::StringRef str)
::std::optional< BVCmpPredicate > symbolizeBVCmpPredicate (uint64_t value)
::llvm::StringRef stringifyIntPredicate (IntPredicate val)
::std::optional< IntPredicate > symbolizeIntPredicate (::llvm::StringRef str)
::std::optional< IntPredicate > symbolizeIntPredicate (uint64_t value)
constexpr unsigned getMaxEnumValForBVCmpPredicate ()
inline ::llvm::StringRef stringifyEnum (BVCmpPredicate enumValue)
template<typename EnumType>
::std::optional< EnumType > symbolizeEnum (::llvm::StringRef)
template<>
inline ::std::optional< BVCmpPredicate > symbolizeEnum< BVCmpPredicate > (::llvm::StringRef str)
constexpr unsigned getMaxEnumValForIntPredicate ()
inline ::llvm::StringRef stringifyEnum (IntPredicate enumValue)
template<>
inline ::std::optional< IntPredicate > symbolizeEnum< IntPredicate > (::llvm::StringRef str)
bool isAnySMTValueType (mlir::Type type)
 Returns whether the given type is an SMT value type.
bool isAnyNonFuncSMTValueType (mlir::Type type)
 Returns whether the given type is an SMT value type (excluding functions).

Enumeration Type Documentation

◆ BVCmpPredicate

enum class llzk::smt::BVCmpPredicate : uint64_t
strong
Enumerator
slt 
sle 
sgt 
sge 
ult 
ule 
ugt 
uge 

Definition at line 13 of file SMTEnums.h.inc.

◆ IntPredicate

enum class llzk::smt::IntPredicate : uint64_t
strong
Enumerator
lt 
le 
gt 
ge 

Definition at line 130 of file SMTEnums.h.inc.

Function Documentation

◆ getMaxEnumValForBVCmpPredicate()

unsigned llzk::smt::getMaxEnumValForBVCmpPredicate ( )
inlineconstexpr

Definition at line 27 of file SMTEnums.h.inc.

◆ getMaxEnumValForIntPredicate()

unsigned llzk::smt::getMaxEnumValForIntPredicate ( )
inlineconstexpr

Definition at line 140 of file SMTEnums.h.inc.

◆ isAnyNonFuncSMTValueType()

bool llzk::smt::isAnyNonFuncSMTValueType ( mlir::Type type)

Returns whether the given type is an SMT value type (excluding functions).

◆ isAnySMTValueType()

bool llzk::smt::isAnySMTValueType ( mlir::Type type)

Returns whether the given type is an SMT value type.

◆ stringifyBVCmpPredicate()

llvm::StringRef llzk::smt::stringifyBVCmpPredicate ( BVCmpPredicate val)

Definition at line 12 of file SMTEnums.cpp.inc.

◆ stringifyEnum() [1/2]

inline ::llvm::StringRef llzk::smt::stringifyEnum ( BVCmpPredicate enumValue)

Definition at line 32 of file SMTEnums.h.inc.

◆ stringifyEnum() [2/2]

inline ::llvm::StringRef llzk::smt::stringifyEnum ( IntPredicate enumValue)

Definition at line 145 of file SMTEnums.h.inc.

◆ stringifyIntPredicate()

llvm::StringRef llzk::smt::stringifyIntPredicate ( IntPredicate val)

Definition at line 68 of file SMTEnums.cpp.inc.

◆ symbolizeBVCmpPredicate() [1/2]

std::optional< BVCmpPredicate > llzk::smt::symbolizeBVCmpPredicate ( ::llvm::StringRef str)

Definition at line 26 of file SMTEnums.cpp.inc.

◆ symbolizeBVCmpPredicate() [2/2]

std::optional< BVCmpPredicate > llzk::smt::symbolizeBVCmpPredicate ( uint64_t value)

Definition at line 38 of file SMTEnums.cpp.inc.

◆ symbolizeEnum()

template<typename EnumType>
::std::optional< EnumType > llzk::smt::symbolizeEnum ( ::llvm::StringRef )

◆ symbolizeEnum< BVCmpPredicate >()

template<>
inline ::std::optional< BVCmpPredicate > llzk::smt::symbolizeEnum< BVCmpPredicate > ( ::llvm::StringRef str)

Definition at line 37 of file SMTEnums.h.inc.

◆ symbolizeEnum< IntPredicate >()

template<>
inline ::std::optional< IntPredicate > llzk::smt::symbolizeEnum< IntPredicate > ( ::llvm::StringRef str)

Definition at line 150 of file SMTEnums.h.inc.

◆ symbolizeIntPredicate() [1/2]

std::optional< IntPredicate > llzk::smt::symbolizeIntPredicate ( ::llvm::StringRef str)

Definition at line 78 of file SMTEnums.cpp.inc.

◆ symbolizeIntPredicate() [2/2]

std::optional< IntPredicate > llzk::smt::symbolizeIntPredicate ( uint64_t value)

Definition at line 86 of file SMTEnums.cpp.inc.