llzk::Field Class Reference

Information about the prime finite field used for the interval analysis. More...

#include <Field.h>

Public Member Functions
	Field ()=delete
	Field (const Field &)=default
	Field (Field &&) noexcept=default
Field &	operator= (const Field &)=default
llvm::DynamicAPInt	prime () const
	For the prime field p, returns p.
llvm::DynamicAPInt	half () const
	Returns p / 2.
llvm::DynamicAPInt	felt (int i) const
	Returns i as a signed field element.
llvm::DynamicAPInt	zero () const
	Returns 0 at the bitwidth of the field.
llvm::DynamicAPInt	one () const
	Returns 1 at the bitwidth of the field.
llvm::DynamicAPInt	maxVal () const
	Returns p - 1, which is the max value possible in a prime field described by p.
llvm::DynamicAPInt	reduce (const llvm::DynamicAPInt &i) const
	Returns i mod p and reduces the result into the appropriate bitwidth.
llvm::DynamicAPInt	reduce (int i) const
llvm::DynamicAPInt	reduce (const llvm::APInt &i) const
unsigned	bitWidth () const
llvm::SMTExprRef	createSymbol (llvm::SMTSolverRef solver, const char *name) const
	Create a SMT solver symbol with the current field's bitwidth.

Static Public Member Functions
static const Field &	getField (const char *fieldName)
	Get a Field from a given field name string.

Friends
bool	operator== (const Field &lhs, const Field &rhs)

Detailed Description

Information about the prime finite field used for the interval analysis.

Note

See implementation of initKnownFields for supported primes.

We use DynamicAPInt to support arithmetic that may require increasing or signed arithmetic (e.g., multiplying field elements before applying the modulus).

Definition at line 25 of file Field.h.

Constructor & Destructor Documentation

Field() [1/3]

llzk::Field::Field ( )

delete

Field() [2/3]

llzk::Field::Field ( const Field & )

default

Field() [3/3]

llzk::Field::Field ( Field && )

defaultnoexcept

Member Function Documentation

bitWidth()

unsigned llzk::Field::bitWidth ( ) const

inline

Definition at line 61 of file Field.h.

createSymbol()

llvm::SMTExprRef llzk::Field::createSymbol ( llvm::SMTSolverRef solver, const char * name ) const

inline

Create a SMT solver symbol with the current field's bitwidth.

Definition at line 64 of file Field.h.

felt()

llvm::DynamicAPInt llzk::Field::felt ( int i ) const

inline

Returns i as a signed field element.

Definition at line 43 of file Field.h.

getField()

const Field & llzk::Field::getField ( const char * fieldName )

static

Get a Field from a given field name string.

Parameters

fieldName

The name of the field.

Definition at line 31 of file Field.cpp.

half()

llvm::DynamicAPInt llzk::Field::half ( ) const

inline

Returns p / 2.

Definition at line 40 of file Field.h.

maxVal()

llvm::DynamicAPInt llzk::Field::maxVal ( ) const

inline

Returns p - 1, which is the max value possible in a prime field described by p.

Definition at line 52 of file Field.h.

one()

llvm::DynamicAPInt llzk::Field::one ( ) const

inline

Returns 1 at the bitwidth of the field.

Definition at line 49 of file Field.h.

operator=()

Field & llzk::Field::operator= ( const Field & )

default

prime()

llvm::DynamicAPInt llzk::Field::prime ( ) const

inline

For the prime field p, returns p.

Definition at line 37 of file Field.h.

reduce() [1/3]

llvm::DynamicAPInt llzk::Field::reduce

(

const llvm::APInt &

i

)

const

reduce() [2/3]

llvm::DynamicAPInt llzk::Field::reduce

(

const llvm::DynamicAPInt &

i

)

const

Returns i mod p and reduces the result into the appropriate bitwidth.

Field elements are returned as signed integers so that negation functions as expected (i.e., reducing -1 will yield p-1).

reduce() [3/3]

llvm::DynamicAPInt llzk::Field::reduce ( int i ) const

inline

Definition at line 58 of file Field.h.

zero()

llvm::DynamicAPInt llzk::Field::zero ( ) const

inline

Returns 0 at the bitwidth of the field.

Definition at line 46 of file Field.h.

Friends And Related Symbol Documentation

operator==

bool operator== ( const Field & lhs, const Field & rhs )

friend

Definition at line 68 of file Field.h.

---

The documentation for this class was generated from the following files:

• include/llzk/Analysis/Field.h
• lib/Analysis/Field.cpp