Field.h

Go to the documentation of this file.

//===-- Field.h -------------------------------------------------*- C++ -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
// Copyright 2025 Veridise Inc.
// SPDX-License-Identifier: Apache-2.0
//
//===----------------------------------------------------------------------===//
 
#pragma once
 
#include <llvm/ADT/DenseMap.h>
#include <llvm/ADT/DynamicAPInt.h>
#include <llvm/Support/SMTAPI.h>
 
#include <string_view>
 
namespace llzk {

class Field {
public:
  static const Field &getField(const char *fieldName);
 
  Field() = delete;
  Field(const Field &) = default;
  Field(Field &&) noexcept = default;
  Field &operator=(const Field &) = default;

  llvm::DynamicAPInt prime() const { return primeMod; }

  llvm::DynamicAPInt half() const { return halfPrime; }

  inline llvm::DynamicAPInt felt(int i) const { return reduce(i); }

  inline llvm::DynamicAPInt zero() const { return felt(0); }

  inline llvm::DynamicAPInt one() const { return felt(1); }

  inline llvm::DynamicAPInt maxVal() const { return prime() - one(); }

  llvm::DynamicAPInt reduce(const llvm::DynamicAPInt &i) const;
  inline llvm::DynamicAPInt reduce(int i) const { return reduce(llvm::DynamicAPInt(i)); }
  llvm::DynamicAPInt reduce(const llvm::APInt &i) const;
 
  inline unsigned bitWidth() const { return bitwidth; }

  llvm::SMTExprRef createSymbol(llvm::SMTSolverRef solver, const char *name) const {
    return solver->mkSymbol(name, solver->getBitvectorSort(bitWidth()));
  }
 
  friend bool operator==(const Field &lhs, const Field &rhs) {
    return lhs.primeMod == rhs.primeMod;
  }
 
private:
  Field(std::string_view primeStr);
 
  llvm::DynamicAPInt primeMod, halfPrime;
  unsigned bitwidth;
 
  static void initKnownFields(llvm::DenseMap<llvm::StringRef, Field> &knownFields);
};
 
} // namespace llzk